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 "src/mc/api/State.hpp"
8 #include "src/mc/explo/udpor/Comb.hpp"
9 #include "src/mc/explo/udpor/ExtensionSetCalculator.hpp"
10 #include "src/mc/explo/udpor/History.hpp"
11 #include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
13 #include <xbt/asserts.h>
15 #include <xbt/string.hpp>
17 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification using UDPOR");
19 namespace simgrid::mc::udpor {
21 UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args, true) {}
23 void UdporChecker::run()
25 XBT_INFO("Starting a UDPOR exploration");
27 state_stack.push_back(get_current_state());
28 explore(Configuration(), EventSet(), EventSet(), EventSet());
29 XBT_INFO("UDPOR exploration terminated -- model checking completed");
32 void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, EventSet prev_exC)
34 auto& stateC = *state_stack.back();
35 auto exC = compute_exC(C, stateC, prev_exC);
36 const auto enC = compute_enC(C, exC);
38 // If enC is a subset of D, intuitively
39 // there aren't any enabled transitions
40 // which are "worth" exploring since their
41 // exploration would lead to a so-called
42 // "sleep-set blocked" trace.
43 if (enC.is_subset_of(D)) {
44 if (not C.get_events().empty()) {
45 // Report information...
48 // When `en(C)` is empty, intuitively this means that there
49 // are no enabled transitions that can be executed from the
50 // state reached by `C` (denoted `state(C)`), i.e. by some
51 // execution of the transitions in C obeying the causality
52 // relation. Here, then, we may be in a deadlock (the other
53 // possibility is that we've finished running everything, and
54 // we wouldn't be in deadlock then)
56 get_remote_app().check_deadlock();
62 // TODO: Add verbose logging about which event is being explored
64 UnfoldingEvent* e = select_next_unfolding_event(A, enC);
65 xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
66 "UDPOR guarantees that an event will be chosen at each point in\n"
67 "the search, yet no events were actually chosen\n"
68 "*********************************\n\n");
76 // Explore(C + {e}, D, A \ {e})
78 // Move the application into stateCe (i.e. `state(C + {e})`) and make note of that state
79 move_to_stateCe(&stateC, e);
80 state_stack.push_back(record_current_state());
82 explore(Ce, D, std::move(A), std::move(exC));
84 // Prepare to move the application back one state.
85 // We need only remove the state from the stack here: if we perform
86 // another `Explore()` after computing an alternative, at that
87 // point we'll actually create a fresh RemoteProcess
88 state_stack.pop_back();
93 constexpr unsigned K = 10;
94 if (auto J = C.compute_k_partial_alternative_to(D, this->unfolding, K); J.has_value()) {
95 // Before searching the "right half", we need to make
96 // sure the program actually reflects the fact
97 // that we are searching again from `state(C)`. While the
98 // stack of states is properly adjusted to represent
99 // `state(C)` all together, the RemoteApp is currently sitting
100 // at some *future* state with resepct to `state(C)` since the
101 // recursive calls have moved it there.
102 restore_program_state_with_current_stack();
104 // Explore(C, D + {e}, J \ C)
105 auto J_minus_C = J.value().get_events().subtracting(C.get_events());
106 explore(C, D, std::move(J_minus_C), std::move(prev_exC));
113 clean_up_explore(e, C, D);
116 EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC)
118 // See eqs. 5.7 of section 5.2 of [3]
119 // C = C' + {e_cur}, i.e. C' = C - {e_cur}
123 // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
124 // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
125 const UnfoldingEvent* e_cur = C.get_latest_event();
126 EventSet exC = prev_exC;
129 for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
130 for (const auto& transition : actor_state.get_enabled_transitions()) {
131 EventSet extension = ExtensionSetCalculator::partially_extend(C, &unfolding, transition);
132 exC.form_union(extension);
138 EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const
141 for (const auto e : exC) {
142 if (not e->conflicts_with(C)) {
149 void UdporChecker::move_to_stateCe(State* state, UnfoldingEvent* e)
151 const aid_t next_actor = e->get_transition()->aid_;
153 // TODO: Add the trace if possible for reporting a bug
154 xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
155 "In reaching this execution path, UDPOR ensures that at least one\n"
156 "one transition of the state of an visited event is enabled, yet no\n"
157 "state was actually enabled. Please report this as a bug.\n"
158 "*********************************\n\n");
159 auto latest_transition_by_next_actor = state->execute_next(next_actor, get_remote_app());
161 // The transition that is associated with the event was just
162 // executed, so it's possible that the new version of the transition
163 // (i.e. the one after execution) has *more* information than
164 // that which existed *prior* to execution.
167 // ------- !!!!! UDPOR INVARIANT !!!!! -------
169 // At this point, we are leveraging the fact that
170 // UDPOR will not contain more than one copy of any
171 // transition executed by any actor for any
172 // particular step taken by that actor. That is,
173 // if transition `i` of the `j`th actor is contained in the
174 // configuration `C` currently under consideration
175 // by UDPOR, then only one and only one copy exists in `C`
177 // This means that we can referesh the transitions associated
178 // with each event lazily, i.e. only after we have chosen the
179 // event to continue our execution.
180 e->set_transition(std::move(latest_transition_by_next_actor));
183 void UdporChecker::restore_program_state_with_current_stack()
185 get_remote_app().restore_initial_state();
187 /* Traverse the stack from the state at position start and re-execute the transitions */
188 for (const std::unique_ptr<State>& state : state_stack) {
189 if (state == state_stack.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
191 state->get_transition()->replay(get_remote_app());
195 std::unique_ptr<State> UdporChecker::record_current_state()
197 auto next_state = this->get_current_state();
199 // In UDPOR, we care about all enabled transitions in a given state
200 next_state->consider_all();
205 UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
208 throw std::invalid_argument("There are no unfolding events to select. "
209 "Are you sure that you checked that en(C) was not "
210 "empty before attempting to select an event from it?");
214 return const_cast<UnfoldingEvent*>(*(enC.begin()));
217 for (const auto& event : A) {
218 if (enC.contains(event)) {
219 return const_cast<UnfoldingEvent*>(event);
225 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
227 const EventSet C_union_D = C.get_events().make_union(D);
228 const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
229 const EventSet Q_CDU = C_union_D.make_union(es_immediate_conflicts.get_local_config());
231 // Move {e} \ Q_CDU from U to G
232 if (Q_CDU.contains(e)) {
233 this->unfolding.remove(e);
236 // foreach ê in #ⁱ_U(e)
237 for (const auto* e_hat : es_immediate_conflicts) {
238 // Move [ê] \ Q_CDU from U to G
239 const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
240 this->unfolding.remove(to_remove);
244 RecordTrace UdporChecker::get_record_trace()
247 for (auto const& state : state_stack)
248 res.push_back(state->get_transition());
252 std::vector<std::string> UdporChecker::get_textual_trace()
254 std::vector<std::string> trace;
255 for (auto const& state : state_stack) {
256 const auto* t = state->get_transition();
257 trace.push_back(xbt::string_printf("%ld: %s", t->aid_, t->to_string().c_str()));
262 } // namespace simgrid::mc::udpor
264 namespace simgrid::mc {
266 Exploration* create_udpor_checker(const std::vector<char*>& args)
268 return new simgrid::mc::udpor::UdporChecker(args);
271 } // namespace simgrid::mc