src/mc/explo/UdporChecker.cpp

   1 /* Copyright (c) 2016-2023. The SimGrid Team. All rights reserved.          */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "src/mc/explo/UdporChecker.hpp"
   7 #include "src/mc/api/State.hpp"
   8 #include <xbt/asserts.h>
   9 #include <xbt/log.h>
  10
  11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification using UDPOR");
  12
  13 namespace simgrid::mc::udpor {
  14
  15 UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args)
  16 {
  17   // Initialize the map
  18 }
  19
  20 void UdporChecker::run()
  21 {
  22   XBT_INFO("Starting a UDPOR exploration");
  23   // NOTE: `A`, `D`, and `C` are derived from the
  24   // original UDPOR paper [1], while `prev_exC` arises
  25   // from the incremental computation of ex(C) from [3]
  26   Configuration C_root;
  27
  28   // TODO: Move computing the root configuration into a method on the Unfolding
  29   auto initial_state      = get_current_state();
  30   auto root_event         = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<Transition>());
  31   auto* root_event_handle = root_event.get();
  32   unfolding.insert(std::move(root_event));
  33   C_root.add_event(root_event_handle);
  34
  35   explore(std::move(C_root), EventSet(), EventSet(), std::move(initial_state), EventSet());
  36
  37   XBT_INFO("UDPOR exploration terminated -- model checking completed");
  38 }
  39
  40 void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::unique_ptr<State> stateC, EventSet prev_exC)
  41 {
  42   // Perform the incremental computation of exC
  43   //
  44   // TODO: This method will have side effects on
  45   // the unfolding, but the naming of the method
  46   // suggests it is doesn't have side effects. We should
  47   // reconcile this in the future
  48   auto [exC, enC] = compute_extension(C, *stateC, prev_exC);
  49
  50   // If enC is a subset of D, intuitively
  51   // there aren't any enabled transitions
  52   // which are "worth" exploring since their
  53   // exploration would lead to a so-called
  54   // "sleep-set blocked" trace.
  55   if (enC.is_subset_of(D)) {
  56
  57     if (C.get_events().size() > 0) {
  58
  59       // g_var::nb_traces++;
  60
  61       // TODO: Log here correctly
  62       // XBT_DEBUG("\n Exploring executions: %d : \n", g_var::nb_traces);
  63       // ...
  64       // ...
  65     }
  66
  67     // When `en(C)` is empty, intuitively this means that there
  68     // are no enabled transitions that can be executed from the
  69     // state reached by `C` (denoted `state(C)`), i.e. by some
  70     // execution of the transitions in C obeying the causality
  71     // relation. Here, then, we would be in a deadlock.
  72     if (enC.empty()) {
  73       get_remote_app().check_deadlock();
  74     }
  75
  76     return;
  77   }
  78
  79   // TODO: Add verbose logging about which event is being explored
  80
  81   UnfoldingEvent* e = select_next_unfolding_event(A, enC);
  82   xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
  83                            "UDPOR guarantees that an event will be chosen at each point in\n"
  84                            "the search, yet no events were actually chosen\n"
  85                            "*********************************\n\n");
  86
  87   // Move the application into stateCe and actually make note of that state
  88   move_to_stateCe(*stateC, *e);
  89   auto stateCe = record_current_state();
  90
  91   // Ce := C + {e}
  92   Configuration Ce = C;
  93   Ce.add_event(e);
  94
  95   A.remove(e);
  96   exC.remove(e);
  97
  98   // Explore(C + {e}, D, A \ {e})
  99   explore(Ce, D, std::move(A), std::move(stateCe), std::move(exC));
 100
 101   // D <-- D + {e}
 102   D.insert(e);
 103
 104   // TODO: Determine a value of K to use or don't use it at all
 105   constexpr unsigned K = 10;
 106   auto J               = compute_partial_alternative(D, C, K);
 107   if (!J.empty()) {
 108     J.subtract(C.get_events());
 109
 110     // Before searching the "right half", we need to make
 111     // sure the program actually reflects the fact
 112     // that we are searching again from `stateC` (the recursive
 113     // search moved the program into `stateCe`)
 114     restore_program_state_to(*stateC);
 115
 116     // Explore(C, D + {e}, J \ C)
 117     explore(C, D, std::move(J), std::move(stateC), std::move(prev_exC));
 118   }
 119
 120   // D <-- D - {e}
 121   D.remove(e);
 122
 123   // Remove(e, C, D)
 124   clean_up_explore(e, C, D);
 125 }
 126
 127 std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C, const State& stateC,
 128                                                                const EventSet& prev_exC) const
 129 {
 130   // See eqs. 5.7 of section 5.2 of [3]
 131   // C = C' + {e_cur}, i.e. C' = C - {e_cur}
 132   //
 133   // Then
 134   //
 135   // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} + U{<a, K> : K is maximal, a depends on all of K, a enabled at K }
 136   UnfoldingEvent* e_cur = C.get_latest_event();
 137   EventSet exC          = prev_exC;
 138   exC.remove(e_cur);
 139
 140   for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
 141     for (const auto& transition : actor_state.get_enabled_transitions()) {
 142       // First check for a specialized function that can compute the extension
 143       // set "quickly" based on its type. Otherwise, fall back to computing
 144       // the set "by hand"
 145       const auto specialized_extension_function = incremental_extension_functions.find(transition->type_);
 146       if (specialized_extension_function != incremental_extension_functions.end()) {
 147         exC.form_union((specialized_extension_function->second)(C, *transition));
 148       } else {
 149         exC.form_union(this->compute_extension_by_enumeration(C, *transition));
 150       }
 151     }
 152   }
 153
 154   EventSet enC;
 155
 156   return std::tuple<EventSet, EventSet>(exC, enC);
 157 }
 158
 159 EventSet UdporChecker::compute_extension_by_enumeration(const Configuration& C, const Transition& action) const
 160 {
 161   // TODO: Do something more interesting here
 162   return EventSet();
 163 }
 164
 165 void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
 166 {
 167   const aid_t next_actor = e.get_transition()->aid_;
 168
 169   // TODO: Add the trace if possible for reporting a bug
 170   xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
 171                               "In reaching this execution path, UDPOR ensures that at least one\n"
 172                               "one transition of the state of an visited event is enabled, yet no\n"
 173                               "state was actually enabled. Please report this as a bug.\n"
 174                               "*********************************\n\n");
 175   state.execute_next(next_actor);
 176 }
 177
 178 void UdporChecker::restore_program_state_to(const State& stateC)
 179 {
 180   // TODO: Perform state regeneration in the same manner as is done
 181   // in the DFSChecker.cpp
 182 }
 183
 184 std::unique_ptr<State> UdporChecker::record_current_state()
 185 {
 186   auto next_state = this->get_current_state();
 187
 188   // In UDPOR, we care about all enabled transitions in a given state
 189   next_state->mark_all_enabled_todo();
 190
 191   return next_state;
 192 }
 193
 194 UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
 195 {
 196   if (!enC.empty()) {
 197     return *(enC.begin());
 198   }
 199
 200   for (const auto& event : A) {
 201     if (enC.contains(event)) {
 202       return event;
 203     }
 204   }
 205   return nullptr;
 206 }
 207
 208 EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
 209 {
 210   // TODO: Compute k-partial alternatives using [2]
 211   return EventSet();
 212 }
 213
 214 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
 215 {
 216   // TODO: Perform clean up here
 217 }
 218
 219 RecordTrace UdporChecker::get_record_trace()
 220 {
 221   RecordTrace res;
 222   return res;
 223 }
 224
 225 std::vector<std::string> UdporChecker::get_textual_trace()
 226 {
 227   // TODO: Topologically sort the events of the latest configuration
 228   // and iterate through that topological sorting
 229   std::vector<std::string> trace;
 230   return trace;
 231 }
 232
 233 } // namespace simgrid::mc::udpor
 234
 235 namespace simgrid::mc {
 236
 237 Exploration* create_udpor_checker(const std::vector<char*>& args)
 238 {
 239   return new simgrid::mc::udpor::UdporChecker(args);
 240 }
 241
 242 } // namespace simgrid::mc