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 "src/mc/explo/udpor/Comb.hpp"
   9 #include "src/mc/explo/udpor/ExtensionSetCalculator.hpp"
  10 #include "src/mc/explo/udpor/History.hpp"
  11 #include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
  12
  13 #include <xbt/asserts.h>
  14 #include <xbt/log.h>
  15 #include <xbt/string.hpp>
  16
  17 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification using UDPOR");
  18
  19 namespace simgrid::mc::udpor {
  20
  21 UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args, true) {}
  22
  23 void UdporChecker::run()
  24 {
  25   XBT_INFO("Starting a UDPOR exploration");
  26   state_stack.clear();
  27   state_stack.push_back(get_current_state());
  28   explore(Configuration(), EventSet(), EventSet(), EventSet());
  29   XBT_INFO("UDPOR exploration terminated -- model checking completed");
  30 }
  31
  32 void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, EventSet prev_exC)
  33 {
  34   auto& stateC   = *state_stack.back();
  35   auto exC       = compute_exC(C, stateC, prev_exC);
  36   const auto enC = compute_enC(C, exC);
  37   XBT_DEBUG("explore(C, D, A) with:\n"
  38             "C\t := %s \n"
  39             "D\t := %s \n"
  40             "A\t := %s \n"
  41             "ex(C)\t := %s \n"
  42             "en(C)\t := %s \n",
  43             C.to_string().c_str(), D.to_string().c_str(), A.to_string().c_str(), exC.to_string().c_str(),
  44             enC.to_string().c_str());
  45   XBT_DEBUG("ex(C) has %zu elements, of which %zu are in en(C)", exC.size(), enC.size());
  46
  47   // If enC is a subset of D, intuitively
  48   // there aren't any enabled transitions
  49   // which are "worth" exploring since their
  50   // exploration would lead to a so-called
  51   // "sleep-set blocked" trace.
  52   if (enC.is_subset_of(D)) {
  53     XBT_DEBUG("en(C) is a subset of the sleep set D (size %zu); if we"
  54               "kept exploring, we'd hit a sleep-set blocked trace",
  55               D.size());
  56     XBT_DEBUG("The current configuration has %zu elements", C.get_events().size());
  57
  58     // When `en(C)` is empty, intuitively this means that there
  59     // are no enabled transitions that can be executed from the
  60     // state reached by `C` (denoted `state(C)`), i.e. by some
  61     // execution of the transitions in C obeying the causality
  62     // relation. Here, then, we may be in a deadlock (the other
  63     // possibility is that we've finished running everything, and
  64     // we wouldn't be in deadlock then)
  65     if (enC.empty()) {
  66       XBT_VERB("Maximal configuration detected. Checking for deadlock...");
  67       get_remote_app().check_deadlock();
  68     }
  69
  70     return;
  71   }
  72   UnfoldingEvent* e = select_next_unfolding_event(A, enC);
  73   xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
  74                            "UDPOR guarantees that an event will be chosen at each point in\n"
  75                            "the search, yet no events were actually chosen\n"
  76                            "*********************************\n\n");
  77   XBT_DEBUG("Selected event `%s` (%zu dependencies) to extend the configuration", e->to_string().c_str(),
  78             e->get_immediate_causes().size());
  79
  80   // Ce := C + {e}
  81   Configuration Ce = C;
  82   Ce.add_event(e);
  83
  84   A.remove(e);
  85   exC.remove(e);
  86
  87   // Explore(C + {e}, D, A \ {e})
  88
  89   // Move the application into stateCe (i.e. `state(C + {e})`) and make note of that state
  90   move_to_stateCe(&stateC, e);
  91   state_stack.push_back(record_current_state());
  92
  93   explore(Ce, D, std::move(A), std::move(exC));
  94
  95   // Prepare to move the application back one state.
  96   // We need only remove the state from the stack here: if we perform
  97   // another `Explore()` after computing an alternative, at that
  98   // point we'll actually create a fresh RemoteProcess
  99   state_stack.pop_back();
 100
 101   // D <-- D + {e}
 102   D.insert(e);
 103
 104   XBT_DEBUG("Checking for the existence of an alternative...");
 105   if (auto J = C.compute_alternative_to(D, this->unfolding); J.has_value()) {
 106     // Before searching the "right half", we need to make
 107     // sure the program actually reflects the fact
 108     // that we are searching again from `state(C)`. While the
 109     // stack of states is properly adjusted to represent
 110     // `state(C)` all together, the RemoteApp is currently sitting
 111     // at some *future* state with resepct to `state(C)` since the
 112     // recursive calls have moved it there.
 113     restore_program_state_with_current_stack();
 114
 115     // Explore(C, D + {e}, J \ C)
 116     auto J_minus_C = J.value().get_events().subtracting(C.get_events());
 117
 118     XBT_DEBUG("Alternative detected! The alternative is:\n"
 119               "J\t := %s \n"
 120               "J / C := %s\n"
 121               "UDPOR is going to explore it...",
 122               J.value().to_string().c_str(), J_minus_C.to_string().c_str());
 123     explore(C, D, std::move(J_minus_C), std::move(prev_exC));
 124   } else {
 125     XBT_DEBUG("No alternative detected with:\n"
 126               "C\t := %s \n"
 127               "D\t := %s \n"
 128               "A\t := %s \n",
 129               C.to_string().c_str(), D.to_string().c_str(), A.to_string().c_str());
 130   }
 131
 132   // D <-- D - {e}
 133   D.remove(e);
 134
 135   // Remove(e, C, D)
 136   clean_up_explore(e, C, D);
 137 }
 138
 139 EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC)
 140 {
 141   // See eqs. 5.7 of section 5.2 of [3]
 142   // C = C' + {e_cur}, i.e. C' = C - {e_cur}
 143   //
 144   // Then
 145   //
 146   // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
 147   //    U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
 148   const UnfoldingEvent* e_cur = C.get_latest_event();
 149   EventSet exC                = prev_exC;
 150   exC.remove(e_cur);
 151
 152   for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
 153     for (const auto& transition : actor_state.get_enabled_transitions()) {
 154       EventSet extension = ExtensionSetCalculator::partially_extend(C, &unfolding, transition);
 155       exC.form_union(extension);
 156     }
 157   }
 158   return exC;
 159 }
 160
 161 EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const
 162 {
 163   EventSet enC;
 164   for (const auto e : exC) {
 165     if (not e->conflicts_with(C)) {
 166       enC.insert(e);
 167     }
 168   }
 169   return enC;
 170 }
 171
 172 void UdporChecker::move_to_stateCe(State* state, UnfoldingEvent* e)
 173 {
 174   const aid_t next_actor = e->get_transition()->aid_;
 175
 176   // TODO: Add the trace if possible for reporting a bug
 177   xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
 178                               "In reaching this execution path, UDPOR ensures that at least one\n"
 179                               "one transition of the state of an visited event is enabled, yet no\n"
 180                               "state was actually enabled. Please report this as a bug.\n"
 181                               "*********************************\n\n");
 182   auto latest_transition_by_next_actor = state->execute_next(next_actor, get_remote_app());
 183
 184   // The transition that is associated with the event was just
 185   // executed, so it's possible that the new version of the transition
 186   // (i.e. the one after execution) has *more* information than
 187   // that which existed *prior* to execution.
 188   //
 189   //
 190   // ------- !!!!! UDPOR INVARIANT !!!!! -------
 191   //
 192   // At this point, we are leveraging the fact that
 193   // UDPOR will not contain more than one copy of any
 194   // transition executed by any actor for any
 195   // particular step taken by that actor. That is,
 196   // if transition `i` of the `j`th actor is contained in the
 197   // configuration `C` currently under consideration
 198   // by UDPOR, then only one and only one copy exists in `C`
 199   //
 200   // This means that we can referesh the transitions associated
 201   // with each event lazily, i.e. only after we have chosen the
 202   // event to continue our execution.
 203   e->set_transition(std::move(latest_transition_by_next_actor));
 204 }
 205
 206 void UdporChecker::restore_program_state_with_current_stack()
 207 {
 208   XBT_DEBUG("Restoring state using the current stack");
 209   get_remote_app().restore_initial_state();
 210
 211   /* Traverse the stack from the state at position start and re-execute the transitions */
 212   for (const std::unique_ptr<State>& state : state_stack) {
 213     if (state == state_stack.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
 214       break;
 215     state->get_transition()->replay(get_remote_app());
 216   }
 217 }
 218
 219 std::unique_ptr<State> UdporChecker::record_current_state()
 220 {
 221   auto next_state = this->get_current_state();
 222
 223   // In UDPOR, we care about all enabled transitions in a given state
 224   next_state->consider_all();
 225
 226   return next_state;
 227 }
 228
 229 UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
 230 {
 231   if (enC.empty()) {
 232     throw std::invalid_argument("There are no unfolding events to select. "
 233                                 "Are you sure that you checked that en(C) was not "
 234                                 "empty before attempting to select an event from it?");
 235   }
 236
 237   if (A.empty()) {
 238     return const_cast<UnfoldingEvent*>(*(enC.begin()));
 239   }
 240
 241   for (const auto& event : A) {
 242     if (enC.contains(event)) {
 243       return const_cast<UnfoldingEvent*>(event);
 244     }
 245   }
 246   return nullptr;
 247 }
 248
 249 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
 250 {
 251   const EventSet C_union_D              = C.get_events().make_union(D);
 252   const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
 253   const EventSet Q_CDU                  = C_union_D.make_union(es_immediate_conflicts.get_local_config());
 254
 255   // Move {e} \ Q_CDU from U to G
 256   if (not Q_CDU.contains(e)) {
 257     XBT_DEBUG("Removing %s from U to G...", e->to_string().c_str());
 258     this->unfolding.remove(e);
 259   }
 260
 261   // foreach ê in #ⁱ_U(e)
 262   for (const auto* e_hat : es_immediate_conflicts) {
 263     // Move [ê] \ Q_CDU from U to G
 264     const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
 265     XBT_DEBUG("Removing {%s} from U to G...", to_remove.to_string().c_str());
 266     this->unfolding.remove(to_remove);
 267   }
 268 }
 269
 270 RecordTrace UdporChecker::get_record_trace()
 271 {
 272   RecordTrace res;
 273   for (auto const& state : state_stack)
 274     res.push_back(state->get_transition());
 275   return res;
 276 }
 277
 278 std::vector<std::string> UdporChecker::get_textual_trace()
 279 {
 280   std::vector<std::string> trace;
 281   for (auto const& state : state_stack) {
 282     const auto* t = state->get_transition();
 283     trace.push_back(xbt::string_printf("%ld: %s", t->aid_, t->to_string().c_str()));
 284   }
 285   return trace;
 286 }
 287
 288 } // namespace simgrid::mc::udpor
 289
 290 namespace simgrid::mc {
 291
 292 Exploration* create_udpor_checker(const std::vector<char*>& args)
 293 {
 294   return new simgrid::mc::udpor::UdporChecker(args);
 295 }
 296
 297 } // namespace simgrid::mc