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   /* Create initial data structures, if any ...*/
  18
  19   // TODO: Initialize state structures for the search
  20 }
  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(std::move(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(Configuration C, EventSet D, EventSet A, std::unique_ptr<State> stateC, 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, 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 (C.get_events().size() > 0) {
  60
  61       // g_var::nb_traces++;
  62
  63       // TODO: Log here correctly
  64       // XBT_DEBUG("\n Exploring executions: %d : \n", g_var::nb_traces);
  65       // ...
  66       // ...
  67     }
  68
  69     // When `en(C)` is empty, intuitively this means that there
  70     // are no enabled transitions that can be executed from the
  71     // state reached by `C` (denoted `state(C)`), i.e. by some
  72     // execution of the transitions in C obeying the causality
  73     // relation. Here, then, we would be in a deadlock.
  74     if (enC.empty()) {
  75       get_remote_app().check_deadlock();
  76     }
  77
  78     return;
  79   }
  80
  81   // TODO: Add verbose logging about which event is being explored
  82
  83   UnfoldingEvent* e = select_next_unfolding_event(A, enC);
  84   xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
  85                            "UDPOR guarantees that an event will be chosen at each point in\n"
  86                            "the search, yet no events were actually chosen\n"
  87                            "*********************************\n\n");
  88
  89   // Move the application into stateCe and actually make note of that state
  90   move_to_stateCe(*stateC, *e);
  91   auto stateCe = record_current_state();
  92
  93   // Ce := C + {e}
  94   Configuration Ce = C;
  95   Ce.add_event(e);
  96
  97   A.remove(e);
  98   exC.remove(e);
  99
 100   // Explore(C + {e}, D, A \ {e})
 101   explore(Ce, D, std::move(A), std::move(stateCe), std::move(exC));
 102
 103   // D <-- D + {e}
 104   D.insert(e);
 105
 106   // TODO: Determine a value of K to use or don't use it at all
 107   constexpr unsigned K = 10;
 108   auto J               = compute_partial_alternative(D, C, K);
 109   if (!J.empty()) {
 110     J.subtract(C.get_events());
 111
 112     // Before searching the "right half", we need to make
 113     // sure the program actually reflects the fact
 114     // that we are searching again from `stateC` (the recursive
 115     // search moved the program into `stateCe`)
 116     restore_program_state_to(*stateC);
 117
 118     // Explore(C, D + {e}, J \ C)
 119     explore(C, D, std::move(J), std::move(stateC), std::move(prev_exC));
 120   }
 121
 122   // D <-- D - {e}
 123   D.remove(e);
 124
 125   // Remove(e, C, D)
 126   clean_up_explore(e, C, D);
 127 }
 128
 129 std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C, 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} + U{<a, > : H }
 137   UnfoldingEvent* e_cur = C.get_latest_event();
 138   EventSet exC          = prev_exC;
 139   exC.remove(e_cur);
 140
 141   // ... fancy computations
 142
 143   EventSet enC;
 144   return std::tuple<EventSet, EventSet>(exC, enC);
 145 }
 146
 147 void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
 148 {
 149   const aid_t next_actor = e.get_transition()->aid_;
 150
 151   // TODO: Add the trace if possible for reporting a bug
 152   xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
 153                               "In reaching this execution path, UDPOR ensures that at least one\n"
 154                               "one transition of the state of an visited event is enabled, yet no\n"
 155                               "state was actually enabled. Please report this as a bug.\n"
 156                               "*********************************\n\n");
 157   state.execute_next(next_actor);
 158 }
 159
 160 void UdporChecker::restore_program_state_to(const State& stateC)
 161 {
 162   // TODO: Perform state regeneration in the same manner as is done
 163   // in the DFSChecker.cpp
 164 }
 165
 166 std::unique_ptr<State> UdporChecker::record_current_state()
 167 {
 168   auto next_state = this->get_current_state();
 169
 170   // In UDPOR, we care about all enabled transitions in a given state
 171   next_state->mark_all_enabled_todo();
 172
 173   return next_state;
 174 }
 175
 176 UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
 177 {
 178   if (!enC.empty()) {
 179     return *(enC.begin());
 180   }
 181
 182   for (const auto& event : A) {
 183     if (enC.contains(event)) {
 184       return event;
 185     }
 186   }
 187   return nullptr;
 188 }
 189
 190 EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
 191 {
 192   // TODO: Compute k-partial alternatives using [2]
 193   return EventSet();
 194 }
 195
 196 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
 197 {
 198   // TODO: Perform clean up here
 199 }
 200
 201 RecordTrace UdporChecker::get_record_trace()
 202 {
 203   RecordTrace res;
 204   return res;
 205 }
 206
 207 std::vector<std::string> UdporChecker::get_textual_trace()
 208 {
 209   // TODO: Topologically sort the events of the latest configuration
 210   // and iterate through that topological sorting
 211   std::vector<std::string> trace;
 212   return trace;
 213 }
 214
 215 } // namespace simgrid::mc::udpor
 216
 217 namespace simgrid::mc {
 218
 219 Exploration* create_udpor_checker(const std::vector<char*>& args)
 220 {
 221   return new simgrid::mc::udpor::UdporChecker(args);
 222 }
 223
 224 } // namespace simgrid::mc