1 /* Copyright (c) 2016-2023. The SimGrid Team. All rights reserved. */
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. */
6 #include "src/mc/explo/UdporChecker.hpp"
7 #include <xbt/asserts.h>
10 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to MC safety verification ");
12 namespace simgrid::mc::udpor {
14 UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args)
16 /* Create initial data structures, if any ...*/
18 // TODO: Initialize state structures for the search
21 void UdporChecker::run()
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]
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));
36 XBT_INFO("UDPOR exploration terminated -- model checking completed");
39 void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::list<EventSet> max_evt_history,
40 UnfoldingEvent* cur_evt, EventSet prev_exC)
42 // Perform the incremental computation of exC
43 auto [exC, enC] = compute_extension(C, max_evt_history, cur_evt, prev_exC);
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)) {
52 if (C.get_events().size() > 0) {
54 // g_var::nb_traces++;
56 // TODO: Log here correctly
57 // XBT_DEBUG("\n Exploring executions: %d : \n", g_var::nb_traces);
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.
68 get_remote_app().check_deadlock();
74 // TODO: Add verbose logging about which event is being explored
76 const auto next_state_id = observe_unfolding_event(*cur_evt);
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);
89 max_evt_history.push_back(Ce.get_maxmimal_events());
93 // Explore(C + {e}, D, A \ {e})
94 explore(Ce, D, std::move(A), max_evt_history, e, std::move(exC));
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);
103 J.subtract(C.get_events());
104 max_evt_history.pop_back();
106 // Explore(C, D + {e}, J \ C)
107 explore(C, D, std::move(J), std::move(max_evt_history), cur_evt, std::move(prev_exC));
114 clean_up_explore(e, C, D);
117 std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C,
118 const std::list<EventSet>& max_evt_history,
119 UnfoldingEvent* cur_event,
120 const EventSet& prev_exC) const
122 EventSet exC = prev_exC;
124 exC.remove(cur_event);
127 return std::tuple<EventSet, EventSet>(exC, enC);
130 State& UdporChecker::get_state_referenced_by(const UnfoldingEvent& event)
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 %lu does not exist. "
137 "Please report this as a bug.\n"
138 "*********************************\n\n",
140 return wrapped_state.value().get();
143 StateHandle UdporChecker::observe_unfolding_event(const UnfoldingEvent& event)
145 auto& state = this->get_state_referenced_by(event);
146 const aid_t next_actor = state.next_transition();
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();
158 StateHandle UdporChecker::record_current_state()
160 auto next_state = this->get_current_state();
161 const auto next_state_id = this->state_manager_.record_state(std::move(next_state));
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;
168 UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
171 return *(enC.begin());
174 for (const auto& event : A) {
175 if (enC.contains(event)) {
182 EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
184 // TODO: Compute k-partial alternatives using [2]
188 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
190 // TODO: Perform clean up here
193 RecordTrace UdporChecker::get_record_trace()
199 std::vector<std::string> UdporChecker::get_textual_trace()
201 std::vector<std::string> trace;
205 } // namespace simgrid::mc::udpor
207 namespace simgrid::mc {
209 Exploration* create_udpor_checker(const std::vector<char*>& args)
211 return new simgrid::mc::udpor::UdporChecker(args);
214 } // namespace simgrid::mc