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   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), {}, 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* e_cur, EventSet prev_exC)
  41 {
  42   // Perform the incremental computation of exC
  43   auto [exC, enC] = compute_extension(C, max_evt_history, e_cur, 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   const auto next_state_id = observe_unfolding_event(*e_cur);
  77
  78   UnfoldingEvent* e = select_next_unfolding_event(A, enC);
  79   xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
  80                            "UDPOR guarantees that an event will be chosen at each point in\n"
  81                            "the search, yet no events were actually chosen\n"
  82                            "*********************************\n\n");
  83   e->set_state_id(next_state_id);
  84
  85   // Ce := C + {e}
  86   Configuration Ce = C;
  87   Ce.add_event(e);
  88
  89   max_evt_history.push_back(Ce.get_maximal_events());
  90   A.remove(e);
  91   exC.remove(e);
  92
  93   // Explore(C + {e}, D, A \ {e})
  94   explore(Ce, D, std::move(A), max_evt_history, e, 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   auto J               = compute_partial_alternative(D, C, K);
 102   if (!J.empty()) {
 103     J.subtract(C.get_events());
 104     max_evt_history.pop_back();
 105
 106     // Explore(C, D + {e}, J \ C)
 107     explore(C, D, std::move(J), std::move(max_evt_history), e_cur, std::move(prev_exC));
 108   }
 109
 110   // D <-- D - {e}
 111   D.remove(e);
 112
 113   // Remove(e, C, D)
 114   clean_up_explore(e, C, D);
 115 }
 116
 117 std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C,
 118                                                                const std::list<EventSet>& max_evt_history,
 119                                                                UnfoldingEvent* e_cur, const EventSet& prev_exC) const
 120 {
 121   // See eqs. 5.7 of section 5.2 of [3]
 122   // ex(C + {e_cur}) = ex(C) / {e_cur} + U{<a, > : H }
 123   EventSet exC = prev_exC;
 124   exC.remove(e_cur);
 125
 126   EventSet enC;
 127   return std::tuple<EventSet, EventSet>(exC, enC);
 128 }
 129
 130 State& UdporChecker::get_state_referenced_by(const UnfoldingEvent& event)
 131 {
 132   const auto state_id      = event.get_state_id();
 133   const auto wrapped_state = this->state_manager_.get_state(state_id);
 134   xbt_assert(wrapped_state != std::nullopt,
 135              "\n\n****** INVARIANT VIOLATION ******\n"
 136              "To each UDPOR event corresponds a state, but state %llu does not exist. "
 137              "Please report this as a bug.\n"
 138              "*********************************\n\n",
 139              state_id);
 140   return wrapped_state.value().get();
 141 }
 142
 143 StateHandle UdporChecker::observe_unfolding_event(const UnfoldingEvent& event)
 144 {
 145   auto& state            = this->get_state_referenced_by(event);
 146   const aid_t next_actor = state.next_transition();
 147
 148   // TODO: Add the trace if possible for reporting a bug
 149   xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
 150                               "In reaching this execution path, UDPOR ensures that at least one\n"
 151                               "one transition of the state of an visited event is enabled, yet no\n"
 152                               "state was actually enabled. Please report this as a bug.\n"
 153                               "*********************************\n\n");
 154   state.execute_next(next_actor);
 155   return this->record_current_state();
 156 }
 157
 158 StateHandle UdporChecker::record_current_state()
 159 {
 160   auto next_state          = this->get_current_state();
 161   const auto next_state_id = this->state_manager_.record_state(std::move(next_state));
 162
 163   // In UDPOR, we care about all enabled transitions in a given state
 164   next_state->mark_all_enabled_todo();
 165   return next_state_id;
 166 }
 167
 168 UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
 169 {
 170   if (!enC.empty()) {
 171     return *(enC.begin());
 172   }
 173
 174   for (const auto& event : A) {
 175     if (enC.contains(event)) {
 176       return event;
 177     }
 178   }
 179   return nullptr;
 180 }
 181
 182 EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
 183 {
 184   // TODO: Compute k-partial alternatives using [2]
 185   return EventSet();
 186 }
 187
 188 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
 189 {
 190   // TODO: Perform clean up here
 191 }
 192
 193 RecordTrace UdporChecker::get_record_trace()
 194 {
 195   RecordTrace res;
 196   return res;
 197 }
 198
 199 std::vector<std::string> UdporChecker::get_textual_trace()
 200 {
 201   std::vector<std::string> trace;
 202   return trace;
 203 }
 204
 205 } // namespace simgrid::mc::udpor
 206
 207 namespace simgrid::mc {
 208
 209 Exploration* create_udpor_checker(const std::vector<char*>& args)
 210 {
 211   return new simgrid::mc::udpor::UdporChecker(args);
 212 }
 213
 214 } // namespace simgrid::mc