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 {
  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   /**
  32    * Maintains the mapping between handles referenced by events in
  33    * the current state of the unfolding
  34    */
  35   StateManager state_manager_;
  36
  37   const auto initial_state    = std::make_unique<State>(get_remote_app());
  38   const auto initial_state_id = state_manager_.record_state(std::move(initial_state));
  39   const auto root_event       = std::make_unique<UnfoldingEvent>(-1, "", EventSet(), initial_state_id);
  40   explore(std::move(C), {EventSet()}, std::move(D), std::move(A), root_event.get(), std::move(prev_exC));
  41 }
  42
  43 void UdporChecker::explore(Configuration C, std::list<EventSet> max_evt_history, EventSet D, EventSet A,
  44                            UnfoldingEvent* cur_evt, EventSet prev_exC)
  45 {
  46   // Perform the incremental computation of exC
  47   auto [exC, enC] = this->extend(C, max_evt_history, *cur_evt, prev_exC);
  48
  49   // If enC is a subset of D, intuitively
  50   // there aren't any enabled transitions
  51   // which are "worth" exploring since their
  52   // exploration would lead to a so-called
  53   // "sleep-set blocked" trace.
  54   if (enC.is_subset_of(D)) {
  55
  56     // Log traces
  57     if (C.events_.size() > 0) {
  58
  59       // g_var::nb_traces++;
  60
  61       // TODO: Log here correctly
  62       // XBT_DEBUG("\n Exploring executions: %d : \n", g_var::nb_traces);
  63       // ...
  64       // ...
  65     }
  66
  67     // When `en(C)` is empty, intuitively this means that there
  68     // are no enabled transitions that can be executed from the
  69     // state reached by `C` (denoted `state(C)`) (i.e. by some
  70     // execution of the transitions in C obeying the causality
  71     // relation). Hence, it is at this point we should check for a deadlock
  72     if (enC.empty()) {
  73       get_remote_app().check_deadlock();
  74     }
  75
  76     return;
  77   }
  78
  79   UnfoldingEvent* e = this->select_next_unfolding_event(A, enC);
  80   if (e == nullptr) {
  81     XBT_ERROR("\n\n****** CRITICAL ERROR ****** \n"
  82               "UDPOR guarantees that an event will be chosen here, yet no events were actually chosen...\n"
  83               "******************");
  84     DIE_IMPOSSIBLE;
  85   }
  86
  87   // TODO: Add verbose logging about which event is being explored
  88
  89   // TODO: Execute the transition associated with the event
  90   // and map the new state
  91
  92   // const auto cur_state_id = cur_evt->get_state_id();
  93   // auto curEv_StateId = currentEvt->get_state_id();
  94   // auto nextState_id  = App::app_side_->execute_transition(curEv_StateId, e->get_transition_tag());
  95   // e->set_state_id(nextState_id);
  96
  97   // Configuration is the same + event e
  98   // C1 = C + {e}
  99   Configuration C1 = C;
 100   C1.events_.insert(e);
 101   C1.updateMaxEvent(e);
 102
 103   max_evt_history.push_back(C1.maxEvent);
 104
 105   // A <-- A \ {e}, ex(C) <-- ex(C) \ {e}
 106   A.remove(e);
 107   exC.remove(e);
 108
 109   // Explore(C + {e}, D, A \ {e})
 110   this->explore(C1, max_evt_history, D, A, e, exC);
 111
 112   // D <-- D + {e}
 113   D.insert(e);
 114
 115   // TODO: Determine a value of K to use or don't use it at all
 116   constexpr unsigned K = 10;
 117   auto J               = this->compute_partial_alternative(D, C, K);
 118   if (!J.empty()) {
 119     J.subtract(C.events_);
 120     max_evt_history.pop_back();
 121     explore(C, max_evt_history, D, J, cur_evt, prev_exC);
 122   }
 123
 124   // D <-- D - {e}
 125   D.remove(e);
 126   this->clean_up_explore(e, C, D);
 127 }
 128
 129 std::tuple<EventSet, EventSet> UdporChecker::extend(const Configuration& C, const std::list<EventSet>& max_evt_history,
 130                                                     const UnfoldingEvent& cur_event, const EventSet& prev_exC) const
 131 {
 132   // exC.remove(cur_event);
 133
 134   // TODO: Compute extend() as it exists in tiny_simgrid
 135
 136   // exC.subtract(C);
 137   return std::tuple<EventSet, EventSet>();
 138 }
 139
 140 UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
 141 {
 142   // TODO: Actually select an event here
 143   return nullptr;
 144 }
 145
 146 EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const EventSet& C, const unsigned k) const
 147 {
 148   // TODO: Compute k-partial alternatives using [2]
 149   return EventSet();
 150 }
 151
 152 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const EventSet& C, const EventSet& D)
 153 {
 154   // TODO: Perform clean up here
 155 }
 156
 157 RecordTrace UdporChecker::get_record_trace()
 158 {
 159   RecordTrace res;
 160   return res;
 161 }
 162
 163 std::vector<std::string> UdporChecker::get_textual_trace()
 164 {
 165   std::vector<std::string> trace;
 166   return trace;
 167 }
 168
 169 Exploration* create_udpor_checker(const std::vector<char*>& args)
 170 {
 171   return new UdporChecker(args);
 172 }
 173
 174 } // namespace simgrid::mc