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"
14 #include <xbt/asserts.h>
16 #include <xbt/string.hpp>
18 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification using UDPOR");
20 namespace simgrid::mc::udpor {
22 UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args, true) {}
24 void UdporChecker::run()
26 XBT_INFO("Starting a UDPOR exploration");
28 state_stack.push_back(get_current_state());
29 explore(Configuration(), EventSet(), EventSet(), EventSet());
30 XBT_INFO("UDPOR exploration terminated -- model checking completed");
33 void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, EventSet prev_exC)
35 auto& stateC = *state_stack.back();
36 auto exC = compute_exC(C, stateC, prev_exC);
37 const auto enC = compute_enC(C, exC);
38 XBT_DEBUG("explore(C, D, A) with:\n"
44 C.to_string().c_str(), D.to_string().c_str(), A.to_string().c_str(), exC.to_string().c_str(),
45 enC.to_string().c_str());
46 XBT_DEBUG("ex(C) has %zu elements, of which %zu are in en(C)", exC.size(), enC.size());
48 // If enC is a subset of D, intuitively
49 // there aren't any enabled transitions
50 // which are "worth" exploring since their
51 // exploration would lead to a so-called
52 // "sleep-set blocked" trace.
53 if (enC.is_subset_of(D)) {
54 XBT_DEBUG("en(C) is a subset of the sleep set D (size %zu); if we "
55 "kept exploring, we'd hit a sleep-set blocked trace",
57 XBT_DEBUG("The current configuration has %zu elements", C.get_events().size());
59 // When `en(C)` is empty, intuitively this means that there
60 // are no enabled transitions that can be executed from the
61 // state reached by `C` (denoted `state(C)`), i.e. by some
62 // execution of the transitions in C obeying the causality
63 // relation. Here, then, we may be in a deadlock (the other
64 // possibility is that we've finished running everything, and
65 // we wouldn't be in deadlock then)
67 XBT_VERB("Maximal configuration detected. Checking for deadlock...");
68 get_remote_app().check_deadlock();
73 UnfoldingEvent* e = select_next_unfolding_event(A, enC);
74 xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
75 "UDPOR guarantees that an event will be chosen at each point in\n"
76 "the search, yet no events were actually chosen\n"
77 "*********************************\n\n");
78 XBT_DEBUG("Selected event `%s` (%zu dependencies) to extend the configuration", e->to_string().c_str(),
79 e->get_immediate_causes().size());
88 // Explore(C + {e}, D, A \ {e})
90 // Move the application into stateCe (i.e. `state(C + {e})`) and make note of that state
91 move_to_stateCe(&stateC, e);
92 state_stack.push_back(record_current_state());
94 explore(Ce, D, std::move(A), std::move(exC));
96 // Prepare to move the application back one state.
97 // We need only remove the state from the stack here: if we perform
98 // another `Explore()` after computing an alternative, at that
99 // point we'll actually create a fresh RemoteProcess
100 state_stack.pop_back();
105 XBT_DEBUG("Checking for the existence of an alternative...");
106 if (auto J = C.compute_alternative_to(D, this->unfolding); J.has_value()) {
107 // Before searching the "right half", we need to make
108 // sure the program actually reflects the fact
109 // that we are searching again from `state(C)`. While the
110 // stack of states is properly adjusted to represent
111 // `state(C)` all together, the RemoteApp is currently sitting
112 // at some *future* state with resepct to `state(C)` since the
113 // recursive calls have moved it there.
114 restore_program_state_with_current_stack();
116 // Explore(C, D + {e}, J \ C)
117 auto J_minus_C = J.value().get_events().subtracting(C.get_events());
119 XBT_DEBUG("Alternative detected! The alternative is:\n"
122 "UDPOR is going to explore it...",
123 J.value().to_string().c_str(), J_minus_C.to_string().c_str());
124 explore(C, D, std::move(J_minus_C), std::move(prev_exC));
126 XBT_DEBUG("No alternative detected with:\n"
130 C.to_string().c_str(), D.to_string().c_str(), A.to_string().c_str());
137 clean_up_explore(e, C, D);
140 EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC)
142 // See eqs. 5.7 of section 5.2 of [3]
143 // C = C' + {e_cur}, i.e. C' = C - {e_cur}
147 // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
148 // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
149 const UnfoldingEvent* e_cur = C.get_latest_event();
150 EventSet exC = prev_exC;
153 for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
154 for (const auto& transition : actor_state.get_enabled_transitions()) {
155 XBT_DEBUG("\t Considering partial extension for %s", transition->to_string().c_str());
156 EventSet extension = ExtensionSetCalculator::partially_extend(C, &unfolding, transition);
157 exC.form_union(extension);
163 EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const
166 for (const auto e : exC) {
167 if (C.is_compatible_with(e)) {
174 void UdporChecker::move_to_stateCe(State* state, UnfoldingEvent* e)
176 const aid_t next_actor = e->get_transition()->aid_;
178 // TODO: Add the trace if possible for reporting a bug
179 xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
180 "In reaching this execution path, UDPOR ensures that at least one\n"
181 "one transition of the state of an visited event is enabled, yet no\n"
182 "state was actually enabled. Please report this as a bug.\n"
183 "*********************************\n\n");
184 auto latest_transition_by_next_actor = state->execute_next(next_actor, get_remote_app());
186 // The transition that is associated with the event was just
187 // executed, so it's possible that the new version of the transition
188 // (i.e. the one after execution) has *more* information than
189 // that which existed *prior* to execution.
192 // ------- !!!!! UDPOR INVARIANT !!!!! -------
194 // At this point, we are leveraging the fact that
195 // UDPOR will not contain more than one copy of any
196 // transition executed by any actor for any
197 // particular step taken by that actor. That is,
198 // if transition `i` of the `j`th actor is contained in the
199 // configuration `C` currently under consideration
200 // by UDPOR, then only one and only one copy exists in `C`
202 // This means that we can referesh the transitions associated
203 // with each event lazily, i.e. only after we have chosen the
204 // event to continue our execution.
205 e->set_transition(std::move(latest_transition_by_next_actor));
208 void UdporChecker::restore_program_state_with_current_stack()
210 XBT_DEBUG("Restoring state using the current stack");
211 get_remote_app().restore_initial_state();
213 /* Traverse the stack from the state at position start and re-execute the transitions */
214 for (const std::unique_ptr<State>& state : state_stack) {
215 if (state == state_stack.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
217 state->get_transition()->replay(get_remote_app());
221 std::unique_ptr<State> UdporChecker::record_current_state()
223 auto next_state = this->get_current_state();
225 // In UDPOR, we care about all enabled transitions in a given state
226 next_state->consider_all();
231 UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
234 throw std::invalid_argument("There are no unfolding events to select. "
235 "Are you sure that you checked that en(C) was not "
236 "empty before attempting to select an event from it?");
240 return const_cast<UnfoldingEvent*>(*(enC.begin()));
243 for (const auto& event : A) {
244 if (enC.contains(event)) {
245 return const_cast<UnfoldingEvent*>(event);
251 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
253 // // The "clean-up set" conceptually represents
254 // // those events which will no longer be considered
255 // // by UDPOR during its exploration. The concept is
256 // // introduced to avoid modification during iteration
257 // // over the current unfolding to determine who needs to
258 // // be removed. Since sets are unordered, it's quite possible
259 // // that e.g. two events `e` and `e'` such that `e < e'`
260 // // which are determined eligible for removal are removed
261 // // in the order `e` and then `e'`. Determining that `e'`
262 // // needs to be removed requires that its history be in
263 // // tact to e.g. compute the conflicts with the event.
265 // // Thus, we compute the set and remove all of the events
266 // // at once in lieu of removing events while iterating over them.
267 // // We can hypothesize that processing the events in reverse
268 // // topological order would prevent any issues concerning
269 // // the order in which are processed
270 // EventSet clean_up_set;
272 // // Q_(C, D, U) = C u D u U (complicated expression)
273 // // See page 9 of "Unfolding-based Partial Order Reduction"
275 // // "C u D" portion
276 // const EventSet C_union_D = C.get_events().make_union(D);
278 // // "U (complicated expression)" portion
279 // const EventSet conflict_union = std::accumulate(
280 // C_union_D.begin(), C_union_D.end(), EventSet(), [&](const EventSet acc, const UnfoldingEvent* e_prime) {
281 // return acc.make_union(unfolding.get_immediate_conflicts_of(e_prime));
284 // const EventSet Q_CDU = C_union_D.make_union(conflict_union.get_local_config());
286 // XBT_DEBUG("Computed Q_CDU as '%s'", Q_CDU.to_string().c_str());
288 // // Move {e} \ Q_CDU from U to G
289 // if (not Q_CDU.contains(e)) {
290 // XBT_DEBUG("Moving %s from U to G...", e->to_string().c_str());
291 // clean_up_set.insert(e);
294 // // foreach ê in #ⁱ_U(e)
295 // for (const auto* e_hat : this->unfolding.get_immediate_conflicts_of(e)) {
296 // // Move [ê] \ Q_CDU from U to G
297 // const EventSet to_remove = e_hat->get_local_config().subtracting(Q_CDU);
298 // XBT_DEBUG("Moving {%s} from U to G...", to_remove.to_string().c_str());
299 // clean_up_set.form_union(to_remove);
301 // // this->unfolding.remove(clean_up_set);
304 RecordTrace UdporChecker::get_record_trace()
307 for (auto const& state : state_stack)
308 res.push_back(state->get_transition());
312 std::vector<std::string> UdporChecker::get_textual_trace()
314 std::vector<std::string> trace;
315 for (auto const& state : state_stack) {
316 const auto* t = state->get_transition();
317 trace.push_back(xbt::string_printf("%ld: %s", t->aid_, t->to_string().c_str()));
322 } // namespace simgrid::mc::udpor
324 namespace simgrid::mc {
326 Exploration* create_udpor_checker(const std::vector<char*>& args)
328 return new simgrid::mc::udpor::UdporChecker(args);
331 } // namespace simgrid::mc