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
  61       // g_var::nb_traces++;
  62     }
  63
  64     // When `en(C)` is empty, intuitively this means that there
  65     // are no enabled transitions that can be executed from the
  66     // state reached by `C` (denoted `state(C)`), i.e. by some
  67     // execution of the transitions in C obeying the causality
  68     // relation. Here, then, we would be in a deadlock.
  69     if (enC.empty()) {
  70       get_remote_app().check_deadlock();
  71     }
  72
  73     return;
  74   }
  75
  76   // TODO: Add verbose logging about which event is being explored
  77
  78   UnfoldingEvent* e = select_next_unfolding_event(A, enC);
  79   xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
  80                            "UDPOR guarantees that an event will be chosen at each point in\n"
  81                            "the search, yet no events were actually chosen\n"
  82                            "*********************************\n\n");
  83
  84   // Move the application into stateCe and actually make note of that state
  85   move_to_stateCe(*stateC, *e);
  86   auto stateCe = record_current_state();
  87
  88   // Ce := C + {e}
  89   Configuration Ce = C;
  90   Ce.add_event(e);
  91
  92   A.remove(e);
  93   exC.remove(e);
  94
  95   // Explore(C + {e}, D, A \ {e})
  96   explore(Ce, D, std::move(A), std::move(stateCe), std::move(exC));
  97
  98   // D <-- D + {e}
  99   D.insert(e);
 100
 101   // TODO: Determine a value of K to use or don't use it at all
 102   constexpr unsigned K = 10;
 103   if (auto J = compute_partial_alternative(D, C, K); !J.empty()) {
 104     J.subtract(C.get_events());
 105
 106     // Before searching the "right half", we need to make
 107     // sure the program actually reflects the fact
 108     // that we are searching again from `stateC` (the recursive
 109     // search moved the program into `stateCe`)
 110     restore_program_state_to(*stateC);
 111
 112     // Explore(C, D + {e}, J \ C)
 113     explore(C, D, std::move(J), std::move(stateC), std::move(prev_exC));
 114   }
 115
 116   // D <-- D - {e}
 117   D.remove(e);
 118
 119   // Remove(e, C, D)
 120   clean_up_explore(e, C, D);
 121 }
 122
 123 std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C, const State& stateC,
 124                                                                const EventSet& prev_exC) const
 125 {
 126   // See eqs. 5.7 of section 5.2 of [3]
 127   // C = C' + {e_cur}, i.e. C' = C - {e_cur}
 128   //
 129   // Then
 130   //
 131   // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
 132   //    U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at K }
 133   UnfoldingEvent* e_cur = C.get_latest_event();
 134   EventSet exC          = prev_exC;
 135   exC.remove(e_cur);
 136
 137   for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
 138     for (const auto& transition : actor_state.get_enabled_transitions()) {
 139       // First check for a specialized function that can compute the extension
 140       // set "quickly" based on its type. Otherwise, fall back to computing
 141       // the set "by hand"
 142       const auto specialized_extension_function = incremental_extension_functions.find(transition->type_);
 143       if (specialized_extension_function != incremental_extension_functions.end()) {
 144         exC.form_union((specialized_extension_function->second)(C, *transition));
 145       } else {
 146         exC.form_union(this->compute_extension_by_enumeration(C, *transition));
 147       }
 148     }
 149   }
 150
 151   EventSet enC;
 152   // TODO: Compute enC based on conflict relations
 153
 154   return std::tuple<EventSet, EventSet>(exC, enC);
 155 }
 156
 157 EventSet UdporChecker::compute_extension_by_enumeration(const Configuration& C, const Transition& action) const
 158 {
 159   // Here we're computing the following:
 160   //
 161   // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at K }
 162   //
 163   // where `a` is the `action` given to us.
 164   EventSet incremental_exC;
 165
 166   // We only consider those combinations of events for which `action` is dependent with
 167   // the action associated with any given event ("`a` depends on all of K")
 168   const std::unique_ptr<CompatibilityGraph> G = C.make_compatibility_graph_filtered_on([=](const UnfoldingEvent* e) {
 169     const auto e_transition = e->get_transition();
 170     return action.depends(e_transition);
 171   });
 172
 173   // TODO: Now that the graph has been constructed, enumerate
 174   // all possible k-cliques of the complement of G
 175
 176   // TODO: For each enumeration, check all possible
 177   // combinations of selecting a single event from
 178   // each set associated with the graph nodes
 179
 180   return incremental_exC;
 181 }
 182
 183 void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
 184 {
 185   const aid_t next_actor = e.get_transition()->aid_;
 186
 187   // TODO: Add the trace if possible for reporting a bug
 188   xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
 189                               "In reaching this execution path, UDPOR ensures that at least one\n"
 190                               "one transition of the state of an visited event is enabled, yet no\n"
 191                               "state was actually enabled. Please report this as a bug.\n"
 192                               "*********************************\n\n");
 193   state.execute_next(next_actor);
 194 }
 195
 196 void UdporChecker::restore_program_state_to(const State& stateC)
 197 {
 198   // TODO: Perform state regeneration in the same manner as is done
 199   // in the DFSChecker.cpp
 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->mark_all_enabled_todo();
 208
 209   return next_state;
 210 }
 211
 212 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 EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
 227 {
 228   // TODO: Compute k-partial alternatives using [2]
 229   return EventSet();
 230 }
 231
 232 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
 233 {
 234   // TODO: Perform clean up here
 235 }
 236
 237 RecordTrace UdporChecker::get_record_trace()
 238 {
 239   RecordTrace res;
 240   return res;
 241 }
 242
 243 std::vector<std::string> UdporChecker::get_textual_trace()
 244 {
 245   // TODO: Topologically sort the events of the latest configuration
 246   // and iterate through that topological sorting
 247   std::vector<std::string> trace;
 248   return trace;
 249 }
 250
 251 } // namespace simgrid::mc::udpor
 252
 253 namespace simgrid::mc {
 254
 255 Exploration* create_udpor_checker(const std::vector<char*>& args)
 256 {
 257   return new simgrid::mc::udpor::UdporChecker(args);
 258 }
 259
 260 } // namespace simgrid::mc