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 <xbt/asserts.h>
   8 #include <xbt/log.h>
   9
  10 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification using UDPOR");
  11
  12 namespace simgrid::mc::udpor {
  13
  14 UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args)
  15 {
  16   /* Create initial data structures, if any ...*/
  17
  18   // TODO: Initialize state structures for the search
  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>(std::make_shared<Transition>(), EventSet());
  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, 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 EventSet& prev_exC) const
 129 {
 130   // See eqs. 5.7 of section 5.2 of [3]
 131   // C = C' + {e_cur}, i.e. C' = C - {e_cur}
 132   //
 133   // Then
 134   //
 135   // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} + U{<a, > : H }
 136   UnfoldingEvent* e_cur = C.get_latest_event();
 137   EventSet exC          = prev_exC;
 138   exC.remove(e_cur);
 139
 140   // ... fancy computations
 141
 142   EventSet enC;
 143   return std::tuple<EventSet, EventSet>(exC, enC);
 144 }
 145
 146 void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
 147 {
 148   const aid_t next_actor = e.get_transition()->aid_;
 149
 150   // TODO: Add the trace if possible for reporting a bug
 151   xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
 152                               "In reaching this execution path, UDPOR ensures that at least one\n"
 153                               "one transition of the state of an visited event is enabled, yet no\n"
 154                               "state was actually enabled. Please report this as a bug.\n"
 155                               "*********************************\n\n");
 156   state.execute_next(next_actor);
 157 }
 158
 159 void UdporChecker::restore_program_state_to(const State& stateC)
 160 {
 161   // TODO: Perform state regeneration in the same manner as is done
 162   // in the DFSChecker.cpp
 163 }
 164
 165 std::unique_ptr<State> UdporChecker::record_current_state()
 166 {
 167   auto next_state = this->get_current_state();
 168
 169   // In UDPOR, we care about all enabled transitions in a given state
 170   next_state->mark_all_enabled_todo();
 171
 172   return next_state;
 173 }
 174
 175 UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
 176 {
 177   if (!enC.empty()) {
 178     return *(enC.begin());
 179   }
 180
 181   for (const auto& event : A) {
 182     if (enC.contains(event)) {
 183       return event;
 184     }
 185   }
 186   return nullptr;
 187 }
 188
 189 EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
 190 {
 191   // TODO: Compute k-partial alternatives using [2]
 192   return EventSet();
 193 }
 194
 195 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
 196 {
 197   // TODO: Perform clean up here
 198 }
 199
 200 RecordTrace UdporChecker::get_record_trace()
 201 {
 202   RecordTrace res;
 203   return res;
 204 }
 205
 206 std::vector<std::string> UdporChecker::get_textual_trace()
 207 {
 208   // TODO: Topologically sort the events of the latest configuration
 209   // and iterate through that topological sorting
 210   std::vector<std::string> trace;
 211   return trace;
 212 }
 213
 214 } // namespace simgrid::mc::udpor
 215
 216 namespace simgrid::mc {
 217
 218 Exploration* create_udpor_checker(const std::vector<char*>& args)
 219 {
 220   return new simgrid::mc::udpor::UdporChecker(args);
 221 }
 222
 223 } // namespace simgrid::mc