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   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   XBT_INFO("UDPOR exploration terminated -- model checking completed");
  37 }
  38
  39 void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::list<EventSet> max_evt_history,
  40                            UnfoldingEvent* cur_evt, EventSet prev_exC)
  41 {
  42   // Perform the incremental computation of exC
  43   auto [exC, enC] = compute_extension(C, max_evt_history, *cur_evt, prev_exC);
  44
  45   // If enC is a subset of D, intuitively
  46   // there aren't any enabled transitions
  47   // which are "worth" exploring since their
  48   // exploration would lead to a so-called
  49   // "sleep-set blocked" trace.
  50   if (enC.is_subset_of(D)) {
  51
  52     if (C.get_events().size() > 0) {
  53
  54       // g_var::nb_traces++;
  55
  56       // TODO: Log here correctly
  57       // XBT_DEBUG("\n Exploring executions: %d : \n", g_var::nb_traces);
  58       // ...
  59       // ...
  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   observe_unfolding_event(*cur_evt);
  77   const auto next_state_id = record_newly_visited_state();
  78
  79   UnfoldingEvent* e = select_next_unfolding_event(A, enC);
  80   xbt_assert(e != nullptr, "UDPOR guarantees that an event will be chosen at each point in"
  81                            "the search, yet no events were actually chosen");
  82   e->set_state_id(next_state_id);
  83
  84   // TODO: Clean up configuration code before moving into the actual
  85   // implementations of everything
  86
  87   // Configuration is the same + event e
  88   // Ce = C + {e}
  89   Configuration Ce = C;
  90   Ce.add_event(e);
  91
  92   max_evt_history.push_back(Ce.get_maxmimal_events());
  93   A.remove(e);
  94   exC.remove(e);
  95
  96   // Explore(C + {e}, D, A \ {e})
  97   explore(Ce, D, std::move(A), max_evt_history, e, std::move(exC));
  98
  99   // D <-- D + {e}
 100   D.insert(e);
 101
 102   // TODO: Determine a value of K to use or don't use it at all
 103   constexpr unsigned K = 10;
 104   auto J               = compute_partial_alternative(D, C, K);
 105   if (!J.empty()) {
 106     J.subtract(C.get_events());
 107     max_evt_history.pop_back();
 108
 109     // Explore(C, D + {e}, J \ C)
 110     explore(C, D, std::move(J), std::move(max_evt_history), cur_evt, std::move(prev_exC));
 111   }
 112
 113   // D <-- D - {e}
 114   D.remove(e);
 115
 116   // Remove(e, C, D)
 117   clean_up_explore(e, C, D);
 118 }
 119
 120 std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C,
 121                                                                const std::list<EventSet>& max_evt_history,
 122                                                                const UnfoldingEvent& cur_event,
 123                                                                const EventSet& prev_exC) const
 124 {
 125   // exC.remove(cur_event);
 126
 127   // TODO: Compute extend() as it exists in tiny_simgrid
 128
 129   // exC.subtract(C);
 130   return std::tuple<EventSet, EventSet>();
 131 }
 132
 133 State& UdporChecker::get_state_referenced_by(const UnfoldingEvent& event)
 134 {
 135   const auto state_id      = event.get_state_id();
 136   const auto wrapped_state = this->state_manager_.get_state(state_id);
 137   xbt_assert(wrapped_state != std::nullopt,
 138              "\n\n****** FATAL ERROR ******\n"
 139              "To each UDPOR event corresponds a state,"
 140              "but state %lu does not exist\n"
 141              "******************\n\n",
 142              state_id);
 143   return wrapped_state.value().get();
 144 }
 145
 146 void UdporChecker::observe_unfolding_event(const UnfoldingEvent& event)
 147 {
 148   auto& state            = this->get_state_referenced_by(event);
 149   const aid_t next_actor = state.next_transition();
 150   xbt_assert(next_actor >= 0, "\n\n****** FATAL ERROR ******\n"
 151                               "In reaching this execution path, UDPOR ensures that at least one\n"
 152                               "one transition of the state of an visited event is enabled, yet no\n"
 153                               "state was actually enabled");
 154   state.execute_next(next_actor);
 155 }
 156
 157 StateHandle UdporChecker::record_newly_visited_state()
 158 {
 159   auto next_state          = this->get_current_state();
 160   const auto next_state_id = this->state_manager_.record_state(std::move(next_state));
 161
 162   // In UDPOR, we care about all enabled transitions in a given state
 163   next_state->mark_all_enabled_todo();
 164   return next_state_id;
 165 }
 166
 167 UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
 168 {
 169   if (!enC.empty()) {
 170     return *(enC.begin());
 171   }
 172
 173   for (const auto& event : A) {
 174     if (enC.contains(event)) {
 175       return event;
 176     }
 177   }
 178   return nullptr;
 179 }
 180
 181 EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
 182 {
 183   // TODO: Compute k-partial alternatives using [2]
 184   return EventSet();
 185 }
 186
 187 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
 188 {
 189   // TODO: Perform clean up here
 190 }
 191
 192 RecordTrace UdporChecker::get_record_trace()
 193 {
 194   RecordTrace res;
 195   return res;
 196 }
 197
 198 std::vector<std::string> UdporChecker::get_textual_trace()
 199 {
 200   std::vector<std::string> trace;
 201   return trace;
 202 }
 203
 204 } // namespace simgrid::mc::udpor
 205
 206 namespace simgrid::mc {
 207
 208 Exploration* create_udpor_checker(const std::vector<char*>& args)
 209 {
 210   return new simgrid::mc::udpor::UdporChecker(args);
 211 }
 212
 213 } // namespace simgrid::mc