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)
24 void UdporChecker::run()
26 XBT_INFO("Starting a UDPOR exploration");
27 // NOTE: `A`, `D`, and `C` are derived from the
28 // original UDPOR paper [1], while `prev_exC` arises
29 // from the incremental computation of ex(C) from [3]
32 // TODO: Move computing the root configuration into a method on the Unfolding
33 auto initial_state = get_current_state();
34 auto root_event = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<Transition>());
35 auto* root_event_handle = root_event.get();
36 unfolding.insert(std::move(root_event));
37 C_root.add_event(root_event_handle);
39 explore(C_root, EventSet(), EventSet(), std::move(initial_state), EventSet());
41 XBT_INFO("UDPOR exploration terminated -- model checking completed");
44 void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, std::unique_ptr<State> stateC,
47 auto exC = compute_exC(C, *stateC, prev_exC);
48 const auto enC = compute_enC(C, exC);
50 // If enC is a subset of D, intuitively
51 // there aren't any enabled transitions
52 // which are "worth" exploring since their
53 // exploration would lead to a so-called
54 // "sleep-set blocked" trace.
55 if (enC.is_subset_of(D)) {
57 if (not C.get_events().empty()) {
58 // Report information...
61 // When `en(C)` is empty, intuitively this means that there
62 // are no enabled transitions that can be executed from the
63 // state reached by `C` (denoted `state(C)`), i.e. by some
64 // execution of the transitions in C obeying the causality
65 // relation. Here, then, we may be in a deadlock (the other
66 // possibility is that we've finished running everything, and
67 // we wouldn't be in deadlock then)
69 get_remote_app().check_deadlock();
75 // TODO: Add verbose logging about which event is being explored
77 const UnfoldingEvent* e = select_next_unfolding_event(A, enC);
78 xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
79 "UDPOR guarantees that an event will be chosen at each point in\n"
80 "the search, yet no events were actually chosen\n"
81 "*********************************\n\n");
83 // Move the application into stateCe and make note of that state
84 move_to_stateCe(*stateC, *e);
85 auto stateCe = record_current_state();
94 // Explore(C + {e}, D, A \ {e})
95 explore(Ce, D, std::move(A), std::move(stateCe), std::move(exC));
100 constexpr unsigned K = 10;
101 if (auto J = C.compute_k_partial_alternative_to(D, this->unfolding, K); J.has_value()) {
103 // Before searching the "right half", we need to make
104 // sure the program actually reflects the fact
105 // that we are searching again from `stateC` (the recursive
106 // search moved the program into `stateCe`)
107 restore_program_state_to(*stateC);
109 // Explore(C, D + {e}, J \ C)
110 auto J_minus_C = J.value().get_events().subtracting(C.get_events());
111 explore(C, D, std::move(J_minus_C), std::move(stateC), std::move(prev_exC));
118 clean_up_explore(e, C, D);
121 EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC)
123 // See eqs. 5.7 of section 5.2 of [3]
124 // C = C' + {e_cur}, i.e. C' = C - {e_cur}
128 // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
129 // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
130 const UnfoldingEvent* e_cur = C.get_latest_event();
131 EventSet exC = prev_exC;
134 for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
135 for (const auto& transition : actor_state.get_enabled_transitions()) {
136 // First check for a specialized function that can compute the extension
137 // set "quickly" based on its type. Otherwise, fall back to computing
139 const auto specialized_extension_function = incremental_extension_functions.find(transition->type_);
140 if (specialized_extension_function != incremental_extension_functions.end()) {
141 exC.form_union((specialized_extension_function->second)(C, transition));
143 exC.form_union(this->compute_exC_by_enumeration(C, transition));
150 EventSet UdporChecker::compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action)
152 // Here we're computing the following:
154 // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
156 // where `a` is the `action` given to us. Note that `a` is presumed to be enabled
157 EventSet incremental_exC;
160 maximal_subsets_iterator(C, {[&](const UnfoldingEvent* e) { return e->is_dependent_with(action.get()); }});
161 begin != maximal_subsets_iterator(); ++begin) {
162 const EventSet& maximal_subset = *begin;
164 // Determining if `a` is enabled here might not be possible while looking at `a` opaquely
165 // We leave the implementation as-is to ensure that any addition would be simple
166 // if it were ever added
167 const bool enabled_at_config_k = false;
169 if (enabled_at_config_k) {
170 auto candidate_handle = std::make_unique<UnfoldingEvent>(maximal_subset, action);
171 if (auto candidate_event = candidate_handle.get(); not unfolding.contains_event_equivalent_to(candidate_event)) {
172 // This is a new event (i.e. one we haven't yet seen)
173 unfolding.insert(std::move(candidate_handle));
174 incremental_exC.insert(candidate_event);
178 return incremental_exC;
181 EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const
184 for (const auto e : exC) {
185 if (not e->conflicts_with(C)) {
192 void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
194 const aid_t next_actor = e.get_transition()->aid_;
196 // TODO: Add the trace if possible for reporting a bug
197 xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
198 "In reaching this execution path, UDPOR ensures that at least one\n"
199 "one transition of the state of an visited event is enabled, yet no\n"
200 "state was actually enabled. Please report this as a bug.\n"
201 "*********************************\n\n");
202 state.execute_next(next_actor, get_remote_app());
205 void UdporChecker::restore_program_state_to(const State& stateC)
207 get_remote_app().restore_initial_state();
208 // TODO: We need to have the stack of past states available at this
209 // point. Since the method is recursive, we'll need to keep track of
210 // this as we progress
213 std::unique_ptr<State> UdporChecker::record_current_state()
215 auto next_state = this->get_current_state();
217 // In UDPOR, we care about all enabled transitions in a given state
218 next_state->consider_all();
223 const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
226 return *(enC.begin());
229 for (const auto& event : A) {
230 if (enC.contains(event)) {
237 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
239 const EventSet C_union_D = C.get_events().make_union(D);
240 const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
241 const EventSet Q_CDU = C_union_D.make_union(es_immediate_conflicts.get_local_config());
243 // Move {e} \ Q_CDU from U to G
244 if (Q_CDU.contains(e)) {
245 this->unfolding.remove(e);
248 // foreach ê in #ⁱ_U(e)
249 for (const auto* e_hat : es_immediate_conflicts) {
250 // Move [ê] \ Q_CDU from U to G
251 const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
252 this->unfolding.remove(to_remove);
256 RecordTrace UdporChecker::get_record_trace()
262 std::vector<std::string> UdporChecker::get_textual_trace()
264 // TODO: Topologically sort the events of the latest configuration
265 // and iterate through that topological sorting
266 std::vector<std::string> trace;
270 } // namespace simgrid::mc::udpor
272 namespace simgrid::mc {
274 Exploration* create_udpor_checker(const std::vector<char*>& args)
276 return new simgrid::mc::udpor::UdporChecker(args);
279 } // namespace simgrid::mc