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>
16 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification using UDPOR");
18 namespace simgrid::mc::udpor {
20 UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args, true) {}
22 void UdporChecker::run()
24 XBT_INFO("Starting a UDPOR exploration");
26 auto state_stack = std::list<std::unique_ptr<State>>();
27 state_stack.push_back(get_current_state());
29 explore(Configuration(), EventSet(), EventSet(), state_stack, EventSet());
30 XBT_INFO("UDPOR exploration terminated -- model checking completed");
33 void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A,
34 std::list<std::unique_ptr<State>>& state_stack, EventSet prev_exC)
36 auto& stateC = *state_stack.back();
37 auto exC = compute_exC(C, stateC, prev_exC);
38 const auto enC = compute_enC(C, exC);
40 // If enC is a subset of D, intuitively
41 // there aren't any enabled transitions
42 // which are "worth" exploring since their
43 // exploration would lead to a so-called
44 // "sleep-set blocked" trace.
45 if (enC.is_subset_of(D)) {
46 if (not C.get_events().empty()) {
47 // Report information...
50 // When `en(C)` is empty, intuitively this means that there
51 // are no enabled transitions that can be executed from the
52 // state reached by `C` (denoted `state(C)`), i.e. by some
53 // execution of the transitions in C obeying the causality
54 // relation. Here, then, we may be in a deadlock (the other
55 // possibility is that we've finished running everything, and
56 // we wouldn't be in deadlock then)
58 get_remote_app().check_deadlock();
64 // TODO: Add verbose logging about which event is being explored
66 const UnfoldingEvent* e = select_next_unfolding_event(A, enC);
67 xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
68 "UDPOR guarantees that an event will be chosen at each point in\n"
69 "the search, yet no events were actually chosen\n"
70 "*********************************\n\n");
78 // Explore(C + {e}, D, A \ {e})
80 // Move the application into stateCe (i.e. `state(C + {e})`) and make note of that state
81 move_to_stateCe(stateC, *e);
82 state_stack.push_back(record_current_state());
84 explore(Ce, D, std::move(A), state_stack, std::move(exC));
86 // Prepare to move the application back one state.
87 // We need only remove the state from the stack here: if we perform
88 // another `Explore()` after computing an alternative, at that
89 // point we'll actually create a fresh RemoteProcess
90 state_stack.pop_back();
95 constexpr unsigned K = 10;
96 if (auto J = C.compute_k_partial_alternative_to(D, this->unfolding, K); J.has_value()) {
97 // Before searching the "right half", we need to make
98 // sure the program actually reflects the fact
99 // that we are searching again from `state(C)`. While the
100 // stack of states is properly adjusted to represent
101 // `state(C)` all together, the RemoteApp is currently sitting
102 // at some *future* state with resepct to `state(C)` since the
103 // recursive calls have moved it there.
104 restore_program_state_with_sequence(state_stack);
106 // Explore(C, D + {e}, J \ C)
107 auto J_minus_C = J.value().get_events().subtracting(C.get_events());
108 explore(C, D, std::move(J_minus_C), state_stack, std::move(prev_exC));
115 clean_up_explore(e, C, D);
118 EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC)
120 // See eqs. 5.7 of section 5.2 of [3]
121 // C = C' + {e_cur}, i.e. C' = C - {e_cur}
125 // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
126 // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
127 const UnfoldingEvent* e_cur = C.get_latest_event();
128 EventSet exC = prev_exC;
131 for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
132 for (const auto& transition : actor_state.get_enabled_transitions()) {
133 EventSet extension = ExtensionSetCalculator::partially_extend(C, &unfolding, transition);
134 exC.form_union(extension);
140 EventSet UdporChecker::compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action)
142 // Here we're computing the following:
144 // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
146 // where `a` is the `action` given to us. Note that `a` is presumed to be enabled
147 EventSet incremental_exC;
150 maximal_subsets_iterator(C, {[&](const UnfoldingEvent* e) { return e->is_dependent_with(action.get()); }});
151 begin != maximal_subsets_iterator(); ++begin) {
152 const EventSet& maximal_subset = *begin;
154 // Determining if `a` is enabled here might not be possible while looking at `a` opaquely
155 // We leave the implementation as-is to ensure that any addition would be simple
156 // if it were ever added
157 const bool enabled_at_config_k = false;
159 if (enabled_at_config_k) {
160 auto event = std::make_unique<UnfoldingEvent>(maximal_subset, action);
161 const auto handle = unfolding.insert(std::move(event));
162 incremental_exC.insert(handle);
165 return incremental_exC;
168 EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const
171 for (const auto e : exC) {
172 if (not e->conflicts_with(C)) {
179 void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
181 const aid_t next_actor = e.get_transition()->aid_;
183 // TODO: Add the trace if possible for reporting a bug
184 xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
185 "In reaching this execution path, UDPOR ensures that at least one\n"
186 "one transition of the state of an visited event is enabled, yet no\n"
187 "state was actually enabled. Please report this as a bug.\n"
188 "*********************************\n\n");
189 state.execute_next(next_actor, get_remote_app());
192 void UdporChecker::restore_program_state_with_sequence(const std::list<std::unique_ptr<State>>& state_stack)
194 get_remote_app().restore_initial_state();
196 /* Traverse the stack from the state at position start and re-execute the transitions */
197 for (const std::unique_ptr<State>& state : state_stack) {
198 if (state == stack_.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
200 state->get_transition()->replay(get_remote_app());
204 std::unique_ptr<State> UdporChecker::record_current_state()
206 auto next_state = this->get_current_state();
208 // In UDPOR, we care about all enabled transitions in a given state
209 next_state->consider_all();
214 const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
217 return *(enC.begin());
220 for (const auto& event : A) {
221 if (enC.contains(event)) {
228 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
230 const EventSet C_union_D = C.get_events().make_union(D);
231 const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
232 const EventSet Q_CDU = C_union_D.make_union(es_immediate_conflicts.get_local_config());
234 // Move {e} \ Q_CDU from U to G
235 if (Q_CDU.contains(e)) {
236 this->unfolding.remove(e);
239 // foreach ê in #ⁱ_U(e)
240 for (const auto* e_hat : es_immediate_conflicts) {
241 // Move [ê] \ Q_CDU from U to G
242 const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
243 this->unfolding.remove(to_remove);
247 RecordTrace UdporChecker::get_record_trace()
253 std::vector<std::string> UdporChecker::get_textual_trace()
255 // TODO: Topologically sort the events of the latest configuration
256 // and iterate through that topological sorting
257 std::vector<std::string> trace;
261 } // namespace simgrid::mc::udpor
263 namespace simgrid::mc {
265 Exploration* create_udpor_checker(const std::vector<char*>& args)
267 return new simgrid::mc::udpor::UdporChecker(args);
270 } // namespace simgrid::mc