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/log.h>
   8
   9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to MC safety verification ");
  10
  11 namespace simgrid::mc::udpor {
  12
  13 UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args)
  14 {
  15   /* Create initial data structures, if any ...*/
  16   XBT_INFO("Starting a UDPOR exploration");
  17
  18   // TODO: Initialize state structures for the search
  19 }
  20
  21 void UdporChecker::run()
  22 {
  23   // NOTE: `A`, `D`, and `C` are derived from the
  24   // original UDPOR paper [1], while
  25   // `prev_exC` arises from the incremental computation
  26   // of ex(C) from the former paper described in [3]
  27   EventSet A, D;
  28   Configuration C;
  29   EventSet prev_exC;
  30
  31   const auto initial_state    = get_current_state();
  32   const auto initial_state_id = state_manager_.record_state(std::move(initial_state));
  33   const auto root_event       = std::make_unique<UnfoldingEvent>(-1, "", EventSet(), initial_state_id);
  34   explore(std::move(C), std::move(A), std::move(D), {EventSet()}, root_event.get(), std::move(prev_exC));
  35 }
  36
  37 void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::list<EventSet> max_evt_history,
  38                            UnfoldingEvent* cur_evt, EventSet prev_exC)
  39 {
  40   // Perform the incremental computation of exC
  41   auto [exC, enC] = compute_extension(C, max_evt_history, *cur_evt, prev_exC);
  42
  43   // If enC is a subset of D, intuitively
  44   // there aren't any enabled transitions
  45   // which are "worth" exploring since their
  46   // exploration would lead to a so-called
  47   // "sleep-set blocked" trace.
  48   if (enC.is_subset_of(D)) {
  49
  50     if (C.get_events().size() > 0) {
  51
  52       // g_var::nb_traces++;
  53
  54       // TODO: Log here correctly
  55       // XBT_DEBUG("\n Exploring executions: %d : \n", g_var::nb_traces);
  56       // ...
  57       // ...
  58     }
  59
  60     // When `en(C)` is empty, intuitively this means that there
  61     // are no enabled transitions that can be executed from the
  62     // state reached by `C` (denoted `state(C)`), i.e. by some
  63     // execution of the transitions in C obeying the causality
  64     // relation. Here, then, we would be in a deadlock.
  65     if (enC.empty()) {
  66       get_remote_app().check_deadlock();
  67     }
  68
  69     return;
  70   }
  71
  72   // TODO: Add verbose logging about which event is being explored
  73
  74   observe_unfolding_event(*cur_evt);
  75   const auto next_state_id = record_newly_visited_state();
  76
  77   UnfoldingEvent* e = select_next_unfolding_event(A, enC);
  78   xbt_assert(e != nullptr, "UDPOR guarantees that an event will be chosen at each point in"
  79                            "the search, yet no events were actually chosen");
  80   e->set_state_id(next_state_id);
  81
  82   // TODO: Clean up configuration code before moving into the actual
  83   // implementations of everything
  84
  85   // Configuration is the same + event e
  86   // Ce = C + {e}
  87   Configuration Ce = C;
  88   Ce.add_event(e);
  89
  90   max_evt_history.push_back(Ce.get_maxmimal_events());
  91   A.remove(e);
  92   exC.remove(e);
  93
  94   // Explore(C + {e}, D, A \ {e})
  95   explore(Ce, D, std::move(A), max_evt_history, e, std::move(exC));
  96
  97   // D <-- D + {e}
  98   D.insert(e);
  99
 100   // TODO: Determine a value of K to use or don't use it at all
 101   constexpr unsigned K = 10;
 102   auto J               = compute_partial_alternative(D, C, K);
 103   if (!J.empty()) {
 104     J.subtract(C.get_events());
 105     max_evt_history.pop_back();
 106
 107     // Explore(C, D + {e}, J \ C)
 108     explore(C, D, std::move(J), std::move(max_evt_history), cur_evt, std::move(prev_exC));
 109   }
 110
 111   // D <-- D - {e}
 112   D.remove(e);
 113
 114   // Remove(e, C, D)
 115   clean_up_explore(e, C, D);
 116 }
 117
 118 std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C,
 119                                                                const std::list<EventSet>& max_evt_history,
 120                                                                const UnfoldingEvent& cur_event,
 121                                                                const EventSet& prev_exC) const
 122 {
 123   // exC.remove(cur_event);
 124
 125   // TODO: Compute extend() as it exists in tiny_simgrid
 126
 127   // exC.subtract(C);
 128   return std::tuple<EventSet, EventSet>();
 129 }
 130
 131 State& UdporChecker::get_state_referenced_by(const UnfoldingEvent& event)
 132 {
 133   const auto state_id      = event.get_state_id();
 134   const auto wrapped_state = this->state_manager_.get_state(state_id);
 135   xbt_assert(wrapped_state != std::nullopt,
 136              "\n\n****** FATAL ERROR ******\n"
 137              "To each UDPOR event corresponds a state,"
 138              "but state %lu does not exist\n"
 139              "******************\n\n",
 140              state_id);
 141   return wrapped_state.value().get();
 142 }
 143
 144 void UdporChecker::observe_unfolding_event(const UnfoldingEvent& event)
 145 {
 146   auto& state            = this->get_state_referenced_by(event);
 147   const aid_t next_actor = state.next_transition();
 148   xbt_assert(next_actor >= 0, "\n\n****** FATAL ERROR ******\n"
 149                               "In reaching this execution path, UDPOR ensures that at least one\n"
 150                               "one transition of the state of an visited event is enabled, yet no\n"
 151                               "state was actually enabled");
 152   state.execute_next(next_actor);
 153 }
 154
 155 StateHandle UdporChecker::record_newly_visited_state()
 156 {
 157   const auto next_state    = this->get_current_state();
 158   const auto next_state_id = this->state_manager_.record_state(std::move(next_state));
 159
 160   // In UDPOR, we care about all enabled transitions in a given state
 161   next_state->mark_all_enabled_todo();
 162   return next_state_id;
 163 }
 164
 165 UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
 166 {
 167   // TODO: Actually select an event here
 168   return nullptr;
 169 }
 170
 171 EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
 172 {
 173   // TODO: Compute k-partial alternatives using [2]
 174   return EventSet();
 175 }
 176
 177 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
 178 {
 179   // TODO: Perform clean up here
 180 }
 181
 182 RecordTrace UdporChecker::get_record_trace()
 183 {
 184   RecordTrace res;
 185   return res;
 186 }
 187
 188 std::vector<std::string> UdporChecker::get_textual_trace()
 189 {
 190   std::vector<std::string> trace;
 191   return trace;
 192 }
 193
 194 } // namespace simgrid::mc::udpor
 195
 196 namespace simgrid::mc {
 197
 198 Exploration* create_udpor_checker(const std::vector<char*>& args)
 199 {
 200   return new simgrid::mc::udpor::UdporChecker(args);
 201 }
 202
 203 } // namespace simgrid::mc