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