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