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) {}
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("**************************");
68 XBT_VERB("*** TRACE INVESTIGATED ***");
69 XBT_VERB("**************************");
70 XBT_VERB("Execution sequence:");
71 for (auto const& s : get_textual_trace())
72 XBT_VERB(" %s", s.c_str());
73 get_remote_app().check_deadlock();
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 XBT_DEBUG("Selected event `%s` (%zu dependencies) to extend the configuration", e->to_string().c_str(),
84 e->get_immediate_causes().size());
93 // Explore(C + {e}, D, A \ {e})
95 // Move the application into stateCe (i.e. `state(C + {e})`) and make note of that state
96 move_to_stateCe(&stateC, e);
97 state_stack.push_back(record_current_state());
99 explore(Ce, D, std::move(A), std::move(exC));
101 // Prepare to move the application back one state.
102 // We need only remove the state from the stack here: if we perform
103 // another `Explore()` after computing an alternative, at that
104 // point we'll actually create a fresh RemoteProcess
105 state_stack.pop_back();
110 XBT_DEBUG("Checking for the existence of an alternative...");
111 if (auto J = C.compute_alternative_to(D, this->unfolding); J.has_value()) {
112 // Before searching the "right half", we need to make
113 // sure the program actually reflects the fact
114 // that we are searching again from `state(C)`. While the
115 // stack of states is properly adjusted to represent
116 // `state(C)` all together, the RemoteApp is currently sitting
117 // at some *future* state with respect to `state(C)` since the
118 // recursive calls had moved it there.
119 restore_program_state_with_current_stack();
121 // Explore(C, D + {e}, J \ C)
122 auto J_minus_C = J.value().get_events().subtracting(C.get_events());
124 XBT_DEBUG("Alternative detected! The alternative is:\n"
127 "UDPOR is going to explore it...",
128 J.value().to_string().c_str(), J_minus_C.to_string().c_str());
129 explore(C, D, std::move(J_minus_C), std::move(prev_exC));
131 XBT_DEBUG("No alternative detected with:\n"
135 C.to_string().c_str(), D.to_string().c_str(), A.to_string().c_str());
142 clean_up_explore(e, C, D);
145 EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC)
147 // See eqs. 5.7 of section 5.2 of [3]
148 // C = C' + {e_cur}, i.e. C' = C - {e_cur}
152 // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
153 // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
154 const UnfoldingEvent* e_cur = C.get_latest_event();
155 EventSet exC = prev_exC;
158 // IMPORTANT NOTE: In order to have deterministic results, we need to process
159 // the actors in a deterministic manner so that events are discovered by
160 // UDPOR in a deterministic order. The processing done here always processes
161 // actors in a consistent order since `std::map` is by-default ordered using
162 // `std::less<Key>` (see the return type of `State::get_actors_list()`)
163 for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
164 const auto& enabled_transitions = actor_state.get_enabled_transitions();
165 if (enabled_transitions.empty()) {
166 XBT_DEBUG("\t Actor `%ld` is disabled: no partial extensions need to be considered", aid);
168 XBT_DEBUG("\t Actor `%ld` is enabled", aid);
169 for (const auto& transition : enabled_transitions) {
170 XBT_DEBUG("\t Considering partial extension for %s", transition->to_string().c_str());
171 EventSet extension = ExtensionSetCalculator::partially_extend(C, &unfolding, transition);
172 exC.form_union(extension);
179 EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const
182 for (const auto* e : exC) {
183 if (C.is_compatible_with(e)) {
190 void UdporChecker::move_to_stateCe(State* state, UnfoldingEvent* e)
192 const aid_t next_actor = e->get_transition()->aid_;
194 // TODO: Add the trace if possible for reporting a bug
195 xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
196 "In reaching this execution path, UDPOR ensures that at least one\n"
197 "one transition of the state of an visited event is enabled, yet no\n"
198 "state was actually enabled. Please report this as a bug.\n"
199 "*********************************\n\n");
200 auto latest_transition_by_next_actor = state->execute_next(next_actor, get_remote_app());
202 // The transition that is associated with the event was just
203 // executed, so it's possible that the new version of the transition
204 // (i.e. the one after execution) has *more* information than
205 // that which existed *prior* to execution.
208 // ------- !!!!! UDPOR INVARIANT !!!!! -------
210 // At this point, we are leveraging the fact that
211 // UDPOR will not contain more than one copy of any
212 // transition executed by any actor for any
213 // particular step taken by that actor. That is,
214 // if transition `i` of the `j`th actor is contained in the
215 // configuration `C` currently under consideration
216 // by UDPOR, then only one and only one copy exists in `C`
218 // This means that we can referesh the transitions associated
219 // with each event lazily, i.e. only after we have chosen the
220 // event to continue our execution.
221 e->set_transition(std::move(latest_transition_by_next_actor));
224 void UdporChecker::restore_program_state_with_current_stack()
226 XBT_DEBUG("Restoring state using the current stack");
227 get_remote_app().restore_initial_state();
229 /* Traverse the stack from the state at position start and re-execute the transitions */
230 for (const std::unique_ptr<State>& state : state_stack) {
231 if (state == state_stack.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
233 state->get_transition_out()->replay(get_remote_app());
237 std::unique_ptr<State> UdporChecker::record_current_state()
239 auto next_state = this->get_current_state();
241 // In UDPOR, we care about all enabled transitions in a given state
242 next_state->consider_all();
247 UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
250 throw std::invalid_argument("There are no unfolding events to select. "
251 "Are you sure that you checked that en(C) was not "
252 "empty before attempting to select an event from it?");
255 // UDPOR's exploration is non-deterministic (as is DPOR's)
256 // in the sense that at any given point there may
257 // be multiple paths that can be followed. The correctness and optimality
258 // of the algorithm remains unaffected by the route taken by UDPOR when
259 // given multiple choices; but to ensure that SimGrid itself has deterministic
260 // behavior on all platforms, we always pick events with lower id's
261 // to ensure we explore the unfolding deterministically.
263 const auto min_event = std::min_element(enC.begin(), enC.end(),
264 [](const auto e1, const auto e2) { return e1->get_id() < e2->get_id(); });
265 return const_cast<UnfoldingEvent*>(*min_event);
267 const auto intersection = A.make_intersection(enC);
268 const auto min_event = std::min_element(intersection.begin(), intersection.end(),
269 [](const auto e1, const auto e2) { return e1->get_id() < e2->get_id(); });
270 return const_cast<UnfoldingEvent*>(*min_event);
274 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
276 // The "clean-up set" conceptually represents
277 // those events which will no longer be considered
278 // by UDPOR during its exploration. The concept is
279 // introduced to avoid modification during iteration
280 // over the current unfolding to determine who needs to
281 // be removed. Since sets are unordered, it's quite possible
282 // that e.g. two events `e` and `e'` such that `e < e'`
283 // which are determined eligible for removal are removed
284 // in the order `e` and then `e'`. Determining that `e'`
285 // needs to be removed requires that its history be in
286 // tact to e.g. compute the conflicts with the event.
288 // Thus, we compute the set and remove all of the events
289 // at once in lieu of removing events while iterating over them.
290 // We can hypothesize that processing the events in reverse
291 // topological order would prevent any issues concerning
292 // the order in which are processed
293 EventSet clean_up_set;
295 // Q_(C, D, U) = C u D u U (complicated expression)
296 // See page 9 of "Unfolding-based Partial Order Reduction"
299 const EventSet C_union_D = C.get_events().make_union(D);
301 // "U (complicated expression)" portion
302 const EventSet conflict_union = std::accumulate(
303 C_union_D.begin(), C_union_D.end(), EventSet(), [&](const EventSet& acc, const UnfoldingEvent* e_prime) {
304 return acc.make_union(unfolding.get_immediate_conflicts_of(e_prime));
307 const EventSet Q_CDU = C_union_D.make_union(conflict_union.get_local_config());
309 XBT_DEBUG("Computed Q_CDU as '%s'", Q_CDU.to_string().c_str());
311 // Move {e} \ Q_CDU from U to G
312 if (not Q_CDU.contains(e)) {
313 XBT_DEBUG("Moving %s from U to G...", e->to_string().c_str());
314 clean_up_set.insert(e);
317 // foreach ê in #ⁱ_U(e)
318 for (const auto* e_hat : this->unfolding.get_immediate_conflicts_of(e)) {
319 // Move [ê] \ Q_CDU from U to G
320 const EventSet to_remove = e_hat->get_local_config().subtracting(Q_CDU);
321 XBT_DEBUG("Moving {%s} from U to G...", to_remove.to_string().c_str());
322 clean_up_set.form_union(to_remove);
325 // TODO: We still perhaps need to
326 // figure out how to deal with the fact that the previous
327 // extension sets computed for past configurations
328 // contain events that may be removed from `U`. Perhaps
329 // it would be best to keep them around forever (they
330 // are moved to `G` after all and can be discarded at will,
331 // which means they may never have to be removed at all).
333 // Of course, the benefit of moving them into the set `G`
334 // is that the computation for immediate conflicts becomes
335 // more efficient (we have to search all of `U` for such conflicts,
336 // and there would be no reason to search those events
337 // that UDPOR has marked as no longer being important)
338 // For now, there appear to be no "obvious" issues (although
339 // UDPOR's behavior is often far from obvious...)
340 this->unfolding.mark_finished(clean_up_set);
343 RecordTrace UdporChecker::get_record_trace()
346 for (auto const& state : state_stack)
347 res.push_back(state->get_transition_out().get());
351 } // namespace simgrid::mc::udpor
353 namespace simgrid::mc {
355 Exploration* create_udpor_checker(const std::vector<char*>& args)
357 return new simgrid::mc::udpor::UdporChecker(args);
360 } // namespace simgrid::mc