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