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
  16 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification using UDPOR");
  17
  18 namespace simgrid::mc::udpor {
  19
  20 UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args, true) {}
  21
  22 void UdporChecker::run()
  23 {
  24   XBT_INFO("Starting a UDPOR exploration");
  25   // NOTE: `A`, `D`, and `C` are derived from the
  26   // original UDPOR paper [1], while `prev_exC` arises
  27   // from the incremental computation of ex(C) from [3]
  28   Configuration C_root;
  29
  30   // TODO: Move computing the root configuration into a method on the Unfolding
  31   auto initial_state      = get_current_state();
  32   auto root_event         = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<Transition>());
  33   auto* root_event_handle = root_event.get();
  34   unfolding.insert(std::move(root_event));
  35   C_root.add_event(root_event_handle);
  36
  37   explore(C_root, EventSet(), EventSet(), std::move(initial_state), EventSet());
  38
  39   XBT_INFO("UDPOR exploration terminated -- model checking completed");
  40 }
  41
  42 void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std::unique_ptr<State> stateC,
  43                            EventSet prev_exC)
  44 {
  45   auto exC       = compute_exC(C, *stateC, prev_exC);
  46   const auto enC = compute_enC(C, exC);
  47
  48   // If enC is a subset of D, intuitively
  49   // there aren't any enabled transitions
  50   // which are "worth" exploring since their
  51   // exploration would lead to a so-called
  52   // "sleep-set blocked" trace.
  53   if (enC.is_subset_of(D)) {
  54     if (not C.get_events().empty()) {
  55       // Report information...
  56     }
  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       get_remote_app().check_deadlock();
  67     }
  68
  69     return;
  70   }
  71
  72   // TODO: Add verbose logging about which event is being explored
  73
  74   const UnfoldingEvent* e = select_next_unfolding_event(A, enC);
  75   xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
  76                            "UDPOR guarantees that an event will be chosen at each point in\n"
  77                            "the search, yet no events were actually chosen\n"
  78                            "*********************************\n\n");
  79
  80   // Move the application into stateCe and make note of that state
  81   move_to_stateCe(*stateC, *e);
  82   auto stateCe = record_current_state();
  83
  84   // Ce := C + {e}
  85   Configuration Ce = C;
  86   Ce.add_event(e);
  87
  88   A.remove(e);
  89   exC.remove(e);
  90
  91   // Explore(C + {e}, D, A \ {e})
  92   explore(Ce, D, std::move(A), std::move(stateCe), std::move(exC));
  93
  94   // D <-- D + {e}
  95   D.insert(e);
  96
  97   constexpr unsigned K = 10;
  98   if (auto J = C.compute_k_partial_alternative_to(D, this->unfolding, K); J.has_value()) {
  99     // Before searching the "right half", we need to make
 100     // sure the program actually reflects the fact
 101     // that we are searching again from `stateC` (the recursive
 102     // search moved the program into `stateCe`)
 103     restore_program_state_to(*stateC);
 104
 105     // Explore(C, D + {e}, J \ C)
 106     auto J_minus_C = J.value().get_events().subtracting(C.get_events());
 107     explore(C, D, std::move(J_minus_C), std::move(stateC), std::move(prev_exC));
 108   }
 109
 110   // D <-- D - {e}
 111   D.remove(e);
 112
 113   // Remove(e, C, D)
 114   clean_up_explore(e, C, D);
 115 }
 116
 117 EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC)
 118 {
 119   // See eqs. 5.7 of section 5.2 of [3]
 120   // C = C' + {e_cur}, i.e. C' = C - {e_cur}
 121   //
 122   // Then
 123   //
 124   // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
 125   //    U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
 126   const UnfoldingEvent* e_cur = C.get_latest_event();
 127   EventSet exC                = prev_exC;
 128   exC.remove(e_cur);
 129
 130   for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
 131     for (const auto& transition : actor_state.get_enabled_transitions()) {
 132       EventSet extension = ExtensionSetCalculator::partially_extend(C, unfolding, transition);
 133       exC.form_union(extension);
 134     }
 135   }
 136   return exC;
 137 }
 138
 139 EventSet UdporChecker::compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action)
 140 {
 141   // Here we're computing the following:
 142   //
 143   // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
 144   //
 145   // where `a` is the `action` given to us. Note that `a` is presumed to be enabled
 146   EventSet incremental_exC;
 147
 148   for (auto begin =
 149            maximal_subsets_iterator(C, {[&](const UnfoldingEvent* e) { return e->is_dependent_with(action.get()); }});
 150        begin != maximal_subsets_iterator(); ++begin) {
 151     const EventSet& maximal_subset = *begin;
 152
 153     // Determining if `a` is enabled here might not be possible while looking at `a` opaquely
 154     // We leave the implementation as-is to ensure that any addition would be simple
 155     // if it were ever added
 156     const bool enabled_at_config_k = false;
 157
 158     if (enabled_at_config_k) {
 159       auto event        = std::make_unique<UnfoldingEvent>(maximal_subset, action);
 160       const auto handle = unfolding.insert(std::move(event));
 161       incremental_exC.insert(handle);
 162     }
 163   }
 164   return incremental_exC;
 165 }
 166
 167 EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const
 168 {
 169   EventSet enC;
 170   for (const auto e : exC) {
 171     if (not e->conflicts_with(C)) {
 172       enC.insert(e);
 173     }
 174   }
 175   return enC;
 176 }
 177
 178 void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
 179 {
 180   const aid_t next_actor = e.get_transition()->aid_;
 181
 182   // TODO: Add the trace if possible for reporting a bug
 183   xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
 184                               "In reaching this execution path, UDPOR ensures that at least one\n"
 185                               "one transition of the state of an visited event is enabled, yet no\n"
 186                               "state was actually enabled. Please report this as a bug.\n"
 187                               "*********************************\n\n");
 188   state.execute_next(next_actor, get_remote_app());
 189 }
 190
 191 void UdporChecker::restore_program_state_to(const State& stateC)
 192 {
 193   get_remote_app().restore_initial_state();
 194   // TODO: We need to have the stack of past states available at this
 195   // point. Since the method is recursive, we'll need to keep track of
 196   // this as we progress
 197 }
 198
 199 std::unique_ptr<State> UdporChecker::record_current_state()
 200 {
 201   auto next_state = this->get_current_state();
 202
 203   // In UDPOR, we care about all enabled transitions in a given state
 204   next_state->consider_all();
 205
 206   return next_state;
 207 }
 208
 209 const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
 210 {
 211   if (!enC.empty()) {
 212     return *(enC.begin());
 213   }
 214
 215   for (const auto& event : A) {
 216     if (enC.contains(event)) {
 217       return event;
 218     }
 219   }
 220   return nullptr;
 221 }
 222
 223 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
 224 {
 225   const EventSet C_union_D              = C.get_events().make_union(D);
 226   const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
 227   const EventSet Q_CDU                  = C_union_D.make_union(es_immediate_conflicts.get_local_config());
 228
 229   // Move {e} \ Q_CDU from U to G
 230   if (Q_CDU.contains(e)) {
 231     this->unfolding.remove(e);
 232   }
 233
 234   // foreach ê in #ⁱ_U(e)
 235   for (const auto* e_hat : es_immediate_conflicts) {
 236     // Move [ê] \ Q_CDU from U to G
 237     const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
 238     this->unfolding.remove(to_remove);
 239   }
 240 }
 241
 242 RecordTrace UdporChecker::get_record_trace()
 243 {
 244   RecordTrace res;
 245   return res;
 246 }
 247
 248 std::vector<std::string> UdporChecker::get_textual_trace()
 249 {
 250   // TODO: Topologically sort the events of the latest configuration
 251   // and iterate through that topological sorting
 252   std::vector<std::string> trace;
 253   return trace;
 254 }
 255
 256 } // namespace simgrid::mc::udpor
 257
 258 namespace simgrid::mc {
 259
 260 Exploration* create_udpor_checker(const std::vector<char*>& args)
 261 {
 262   return new simgrid::mc::udpor::UdporChecker(args);
 263 }
 264
 265 } // namespace simgrid::mc