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
  38   // If enC is a subset of D, intuitively
  39   // there aren't any enabled transitions
  40   // which are "worth" exploring since their
  41   // exploration would lead to a so-called
  42   // "sleep-set blocked" trace.
  43   if (enC.is_subset_of(D)) {
  44     if (not C.get_events().empty()) {
  45       // Report information...
  46     }
  47
  48     // When `en(C)` is empty, intuitively this means that there
  49     // are no enabled transitions that can be executed from the
  50     // state reached by `C` (denoted `state(C)`), i.e. by some
  51     // execution of the transitions in C obeying the causality
  52     // relation. Here, then, we may be in a deadlock (the other
  53     // possibility is that we've finished running everything, and
  54     // we wouldn't be in deadlock then)
  55     if (enC.empty()) {
  56       get_remote_app().check_deadlock();
  57     }
  58
  59     return;
  60   }
  61
  62   // TODO: Add verbose logging about which event is being explored
  63
  64   const UnfoldingEvent* e = select_next_unfolding_event(A, enC);
  65   xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
  66                            "UDPOR guarantees that an event will be chosen at each point in\n"
  67                            "the search, yet no events were actually chosen\n"
  68                            "*********************************\n\n");
  69   // Ce := C + {e}
  70   Configuration Ce = C;
  71   Ce.add_event(e);
  72
  73   A.remove(e);
  74   exC.remove(e);
  75
  76   // Explore(C + {e}, D, A \ {e})
  77
  78   // Move the application into stateCe (i.e. `state(C + {e})`) and make note of that state
  79   move_to_stateCe(stateC, *e);
  80   state_stack.push_back(record_current_state());
  81
  82   explore(Ce, D, std::move(A), std::move(exC));
  83
  84   //  Prepare to move the application back one state.
  85   // We need only remove the state from the stack here: if we perform
  86   // another `Explore()` after computing an alternative, at that
  87   // point we'll actually create a fresh RemoteProcess
  88   state_stack.pop_back();
  89
  90   // D <-- D + {e}
  91   D.insert(e);
  92
  93   constexpr unsigned K = 10;
  94   if (auto J = C.compute_k_partial_alternative_to(D, this->unfolding, K); J.has_value()) {
  95     // Before searching the "right half", we need to make
  96     // sure the program actually reflects the fact
  97     // that we are searching again from `state(C)`. While the
  98     // stack of states is properly adjusted to represent
  99     // `state(C)` all together, the RemoteApp is currently sitting
 100     // at some *future* state with resepct to `state(C)` since the
 101     // recursive calls have moved it there.
 102     restore_program_state_with_current_stack();
 103
 104     // Explore(C, D + {e}, J \ C)
 105     auto J_minus_C = J.value().get_events().subtracting(C.get_events());
 106     explore(C, D, std::move(J_minus_C), std::move(prev_exC));
 107   }
 108
 109   // D <-- D - {e}
 110   D.remove(e);
 111
 112   // Remove(e, C, D)
 113   clean_up_explore(e, C, D);
 114 }
 115
 116 EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC)
 117 {
 118   // See eqs. 5.7 of section 5.2 of [3]
 119   // C = C' + {e_cur}, i.e. C' = C - {e_cur}
 120   //
 121   // Then
 122   //
 123   // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
 124   //    U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
 125   const UnfoldingEvent* e_cur = C.get_latest_event();
 126   EventSet exC                = prev_exC;
 127   exC.remove(e_cur);
 128
 129   for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
 130     for (const auto& transition : actor_state.get_enabled_transitions()) {
 131       EventSet extension = ExtensionSetCalculator::partially_extend(C, &unfolding, transition);
 132       exC.form_union(extension);
 133     }
 134   }
 135   return exC;
 136 }
 137
 138 EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const
 139 {
 140   EventSet enC;
 141   for (const auto e : exC) {
 142     if (not e->conflicts_with(C)) {
 143       enC.insert(e);
 144     }
 145   }
 146   return enC;
 147 }
 148
 149 void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
 150 {
 151   const aid_t next_actor = e.get_transition()->aid_;
 152
 153   // TODO: Add the trace if possible for reporting a bug
 154   xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
 155                               "In reaching this execution path, UDPOR ensures that at least one\n"
 156                               "one transition of the state of an visited event is enabled, yet no\n"
 157                               "state was actually enabled. Please report this as a bug.\n"
 158                               "*********************************\n\n");
 159   state.execute_next(next_actor, get_remote_app());
 160 }
 161
 162 void UdporChecker::restore_program_state_with_current_stack()
 163 {
 164   get_remote_app().restore_initial_state();
 165
 166   /* Traverse the stack from the state at position start and re-execute the transitions */
 167   for (const std::unique_ptr<State>& state : state_stack) {
 168     if (state == state_stack.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
 169       break;
 170     state->get_transition()->replay(get_remote_app());
 171   }
 172 }
 173
 174 std::unique_ptr<State> UdporChecker::record_current_state()
 175 {
 176   auto next_state = this->get_current_state();
 177
 178   // In UDPOR, we care about all enabled transitions in a given state
 179   next_state->consider_all();
 180
 181   return next_state;
 182 }
 183
 184 const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
 185 {
 186   if (enC.empty()) {
 187     throw std::invalid_argument("There are no unfolding events to select. "
 188                                 "Are you sure that you checked that en(C) was not "
 189                                 "empty before attempting to select an event from it?");
 190   }
 191
 192   if (A.empty()) {
 193     return *(enC.begin());
 194   }
 195
 196   for (const auto& event : A) {
 197     if (enC.contains(event)) {
 198       return event;
 199     }
 200   }
 201   return nullptr;
 202 }
 203
 204 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
 205 {
 206   const EventSet C_union_D              = C.get_events().make_union(D);
 207   const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
 208   const EventSet Q_CDU                  = C_union_D.make_union(es_immediate_conflicts.get_local_config());
 209
 210   // Move {e} \ Q_CDU from U to G
 211   if (Q_CDU.contains(e)) {
 212     this->unfolding.remove(e);
 213   }
 214
 215   // foreach ê in #ⁱ_U(e)
 216   for (const auto* e_hat : es_immediate_conflicts) {
 217     // Move [ê] \ Q_CDU from U to G
 218     const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
 219     this->unfolding.remove(to_remove);
 220   }
 221 }
 222
 223 RecordTrace UdporChecker::get_record_trace()
 224 {
 225   RecordTrace res;
 226   for (auto const& state : state_stack)
 227     res.push_back(state->get_transition());
 228   return res;
 229 }
 230
 231 std::vector<std::string> UdporChecker::get_textual_trace()
 232 {
 233   std::vector<std::string> trace;
 234   for (auto const& state : state_stack) {
 235     const auto* t = state->get_transition();
 236     trace.push_back(xbt::string_printf("%ld: %s", t->aid_, t->to_string().c_str()));
 237   }
 238   return trace;
 239 }
 240
 241 } // namespace simgrid::mc::udpor
 242
 243 namespace simgrid::mc {
 244
 245 Exploration* create_udpor_checker(const std::vector<char*>& args)
 246 {
 247   return new simgrid::mc::udpor::UdporChecker(args);
 248 }
 249
 250 } // namespace simgrid::mc