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_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action)
 139 {
 140   // Here we're computing the following:
 141   //
 142   // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
 143   //
 144   // where `a` is the `action` given to us. Note that `a` is presumed to be enabled
 145   EventSet incremental_exC;
 146
 147   for (auto begin =
 148            maximal_subsets_iterator(C, {[&](const UnfoldingEvent* e) { return e->is_dependent_with(action.get()); }});
 149        begin != maximal_subsets_iterator(); ++begin) {
 150     const EventSet& maximal_subset = *begin;
 151
 152     // Determining if `a` is enabled here might not be possible while looking at `a` opaquely
 153     // We leave the implementation as-is to ensure that any addition would be simple
 154     // if it were ever added
 155     const bool enabled_at_config_k = false;
 156
 157     if (enabled_at_config_k) {
 158       auto event        = std::make_unique<UnfoldingEvent>(maximal_subset, action);
 159       const auto handle = unfolding.insert(std::move(event));
 160       incremental_exC.insert(handle);
 161     }
 162   }
 163   return incremental_exC;
 164 }
 165
 166 EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const
 167 {
 168   EventSet enC;
 169   for (const auto e : exC) {
 170     if (not e->conflicts_with(C)) {
 171       enC.insert(e);
 172     }
 173   }
 174   return enC;
 175 }
 176
 177 void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
 178 {
 179   const aid_t next_actor = e.get_transition()->aid_;
 180
 181   // TODO: Add the trace if possible for reporting a bug
 182   xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
 183                               "In reaching this execution path, UDPOR ensures that at least one\n"
 184                               "one transition of the state of an visited event is enabled, yet no\n"
 185                               "state was actually enabled. Please report this as a bug.\n"
 186                               "*********************************\n\n");
 187   state.execute_next(next_actor, get_remote_app());
 188 }
 189
 190 void UdporChecker::restore_program_state_with_current_stack()
 191 {
 192   get_remote_app().restore_initial_state();
 193
 194   /* Traverse the stack from the state at position start and re-execute the transitions */
 195   for (const std::unique_ptr<State>& state : state_stack) {
 196     if (state == state_stack.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
 197       break;
 198     state->get_transition()->replay(get_remote_app());
 199   }
 200 }
 201
 202 std::unique_ptr<State> UdporChecker::record_current_state()
 203 {
 204   auto next_state = this->get_current_state();
 205
 206   // In UDPOR, we care about all enabled transitions in a given state
 207   next_state->consider_all();
 208
 209   return next_state;
 210 }
 211
 212 const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
 213 {
 214   if (!enC.empty()) {
 215     return *(enC.begin());
 216   }
 217
 218   for (const auto& event : A) {
 219     if (enC.contains(event)) {
 220       return event;
 221     }
 222   }
 223   return nullptr;
 224 }
 225
 226 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
 227 {
 228   const EventSet C_union_D              = C.get_events().make_union(D);
 229   const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
 230   const EventSet Q_CDU                  = C_union_D.make_union(es_immediate_conflicts.get_local_config());
 231
 232   // Move {e} \ Q_CDU from U to G
 233   if (Q_CDU.contains(e)) {
 234     this->unfolding.remove(e);
 235   }
 236
 237   // foreach ê in #ⁱ_U(e)
 238   for (const auto* e_hat : es_immediate_conflicts) {
 239     // Move [ê] \ Q_CDU from U to G
 240     const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
 241     this->unfolding.remove(to_remove);
 242   }
 243 }
 244
 245 RecordTrace UdporChecker::get_record_trace()
 246 {
 247   RecordTrace res;
 248   for (auto const& state : state_stack)
 249     res.push_back(state->get_transition());
 250   return res;
 251 }
 252
 253 std::vector<std::string> UdporChecker::get_textual_trace()
 254 {
 255   std::vector<std::string> trace;
 256   for (auto const& state : state_stack) {
 257     const auto* t = state->get_transition();
 258     trace.push_back(xbt::string_printf("%ld: %s", t->aid_, t->to_string().c_str()));
 259   }
 260   return trace;
 261 }
 262
 263 } // namespace simgrid::mc::udpor
 264
 265 namespace simgrid::mc {
 266
 267 Exploration* create_udpor_checker(const std::vector<char*>& args)
 268 {
 269   return new simgrid::mc::udpor::UdporChecker(args);
 270 }
 271
 272 } // namespace simgrid::mc