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/History.hpp"
10 #include "src/mc/explo/udpor/maximal_subsets_iterator.hpp"
12 #include <xbt/asserts.h>
15 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification using UDPOR");
17 namespace simgrid::mc::udpor {
19 UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args, true) {}
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]
29 // TODO: Move computing the root configuration into a method on the Unfolding
30 auto initial_state = get_current_state();
31 auto root_event = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<Transition>());
32 auto* root_event_handle = root_event.get();
33 unfolding.insert(std::move(root_event));
34 C_root.add_event(root_event_handle);
36 explore(C_root, EventSet(), EventSet(), std::move(initial_state), EventSet());
38 XBT_INFO("UDPOR exploration terminated -- model checking completed");
41 void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std::unique_ptr<State> stateC,
44 auto exC = compute_exC(C, *stateC, prev_exC);
45 const auto enC = compute_enC(C, exC);
47 // If enC is a subset of D, intuitively
48 // there aren't any enabled transitions
49 // which are "worth" exploring since their
50 // exploration would lead to a so-called
51 // "sleep-set blocked" trace.
52 if (enC.is_subset_of(D)) {
53 if (not C.get_events().empty()) {
54 // Report information...
57 // When `en(C)` is empty, intuitively this means that there
58 // are no enabled transitions that can be executed from the
59 // state reached by `C` (denoted `state(C)`), i.e. by some
60 // execution of the transitions in C obeying the causality
61 // relation. Here, then, we may be in a deadlock (the other
62 // possibility is that we've finished running everything, and
63 // we wouldn't be in deadlock then)
65 get_remote_app().check_deadlock();
71 // TODO: Add verbose logging about which event is being explored
73 const 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");
79 // Move the application into stateCe and make note of that state
80 move_to_stateCe(*stateC, *e);
81 auto stateCe = record_current_state();
90 // Explore(C + {e}, D, A \ {e})
91 explore(Ce, D, std::move(A), std::move(stateCe), std::move(exC));
96 constexpr unsigned K = 10;
97 if (auto J = C.compute_k_partial_alternative_to(D, this->unfolding, K); J.has_value()) {
98 // Before searching the "right half", we need to make
99 // sure the program actually reflects the fact
100 // that we are searching again from `stateC` (the recursive
101 // search moved the program into `stateCe`)
102 restore_program_state_to(*stateC);
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(stateC), 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 // First check for a specialized function that can compute the extension
132 // set "quickly" based on its type. Otherwise, fall back to computing
134 const auto specialized_extension_function = incremental_extension_functions.find(transition->type_);
135 if (specialized_extension_function != incremental_extension_functions.end()) {
136 exC.form_union((specialized_extension_function->second)(C, transition));
138 exC.form_union(this->compute_exC_by_enumeration(C, transition));
145 EventSet UdporChecker::compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action)
147 // Here we're computing the following:
149 // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
151 // where `a` is the `action` given to us. Note that `a` is presumed to be enabled
152 EventSet incremental_exC;
155 maximal_subsets_iterator(C, {[&](const UnfoldingEvent* e) { return e->is_dependent_with(action.get()); }});
156 begin != maximal_subsets_iterator(); ++begin) {
157 const EventSet& maximal_subset = *begin;
159 // Determining if `a` is enabled here might not be possible while looking at `a` opaquely
160 // We leave the implementation as-is to ensure that any addition would be simple
161 // if it were ever added
162 const bool enabled_at_config_k = false;
164 if (enabled_at_config_k) {
165 auto event = std::make_unique<UnfoldingEvent>(maximal_subset, action);
166 const auto handle = unfolding.insert(std::move(event));
167 incremental_exC.insert(handle);
170 return incremental_exC;
173 EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const
176 for (const auto e : exC) {
177 if (not e->conflicts_with(C)) {
184 void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
186 const aid_t next_actor = e.get_transition()->aid_;
188 // TODO: Add the trace if possible for reporting a bug
189 xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
190 "In reaching this execution path, UDPOR ensures that at least one\n"
191 "one transition of the state of an visited event is enabled, yet no\n"
192 "state was actually enabled. Please report this as a bug.\n"
193 "*********************************\n\n");
194 state.execute_next(next_actor, get_remote_app());
197 void UdporChecker::restore_program_state_to(const State& stateC)
199 get_remote_app().restore_initial_state();
200 // TODO: We need to have the stack of past states available at this
201 // point. Since the method is recursive, we'll need to keep track of
202 // this as we progress
205 std::unique_ptr<State> UdporChecker::record_current_state()
207 auto next_state = this->get_current_state();
209 // In UDPOR, we care about all enabled transitions in a given state
210 next_state->consider_all();
215 const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
218 return *(enC.begin());
221 for (const auto& event : A) {
222 if (enC.contains(event)) {
229 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
231 const EventSet C_union_D = C.get_events().make_union(D);
232 const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
233 const EventSet Q_CDU = C_union_D.make_union(es_immediate_conflicts.get_local_config());
235 // Move {e} \ Q_CDU from U to G
236 if (Q_CDU.contains(e)) {
237 this->unfolding.remove(e);
240 // foreach ê in #ⁱ_U(e)
241 for (const auto* e_hat : es_immediate_conflicts) {
242 // Move [ê] \ Q_CDU from U to G
243 const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
244 this->unfolding.remove(to_remove);
248 RecordTrace UdporChecker::get_record_trace()
254 std::vector<std::string> UdporChecker::get_textual_trace()
256 // TODO: Topologically sort the events of the latest configuration
257 // and iterate through that topological sorting
258 std::vector<std::string> trace;
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