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)) {
56 if (not C.get_events().empty()) {
57 // Report information...
60 // When `en(C)` is empty, intuitively this means that there
61 // are no enabled transitions that can be executed from the
62 // state reached by `C` (denoted `state(C)`), i.e. by some
63 // execution of the transitions in C obeying the causality
64 // relation. Here, then, we may be in a deadlock (the other
65 // possibility is that we've finished running everything, and
66 // we wouldn't be in deadlock then)
68 get_remote_app().check_deadlock();
74 // TODO: Add verbose logging about which event is being explored
76 const UnfoldingEvent* e = select_next_unfolding_event(A, enC);
77 xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
78 "UDPOR guarantees that an event will be chosen at each point in\n"
79 "the search, yet no events were actually chosen\n"
80 "*********************************\n\n");
82 // Move the application into stateCe and make note of that state
83 move_to_stateCe(*stateC, *e);
84 auto stateCe = record_current_state();
93 // Explore(C + {e}, D, A \ {e})
94 explore(Ce, D, std::move(A), std::move(stateCe), std::move(exC));
99 constexpr unsigned K = 10;
100 if (auto J = C.compute_k_partial_alternative_to(D, this->unfolding, K); J.has_value()) {
101 // Before searching the "right half", we need to make
102 // sure the program actually reflects the fact
103 // that we are searching again from `stateC` (the recursive
104 // search moved the program into `stateCe`)
105 restore_program_state_to(*stateC);
107 // Explore(C, D + {e}, J \ C)
108 auto J_minus_C = J.value().get_events().subtracting(C.get_events());
109 explore(C, D, std::move(J_minus_C), std::move(stateC), std::move(prev_exC));
116 clean_up_explore(e, C, D);
119 EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC)
121 // See eqs. 5.7 of section 5.2 of [3]
122 // C = C' + {e_cur}, i.e. C' = C - {e_cur}
126 // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
127 // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
128 const UnfoldingEvent* e_cur = C.get_latest_event();
129 EventSet exC = prev_exC;
132 for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
133 for (const auto& transition : actor_state.get_enabled_transitions()) {
134 // First check for a specialized function that can compute the extension
135 // set "quickly" based on its type. Otherwise, fall back to computing
137 const auto specialized_extension_function = incremental_extension_functions.find(transition->type_);
138 if (specialized_extension_function != incremental_extension_functions.end()) {
139 exC.form_union((specialized_extension_function->second)(C, transition));
141 exC.form_union(this->compute_exC_by_enumeration(C, transition));
148 EventSet UdporChecker::compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action)
150 // Here we're computing the following:
152 // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
154 // where `a` is the `action` given to us. Note that `a` is presumed to be enabled
155 EventSet incremental_exC;
158 maximal_subsets_iterator(C, {[&](const UnfoldingEvent* e) { return e->is_dependent_with(action.get()); }});
159 begin != maximal_subsets_iterator(); ++begin) {
160 const EventSet& maximal_subset = *begin;
162 // Determining if `a` is enabled here might not be possible while looking at `a` opaquely
163 // We leave the implementation as-is to ensure that any addition would be simple
164 // if it were ever added
165 const bool enabled_at_config_k = false;
167 if (enabled_at_config_k) {
168 auto candidate_handle = std::make_unique<UnfoldingEvent>(maximal_subset, action);
169 if (auto candidate_event = candidate_handle.get(); not unfolding.contains_event_equivalent_to(candidate_event)) {
170 // This is a new event (i.e. one we haven't yet seen)
171 unfolding.insert(std::move(candidate_handle));
172 incremental_exC.insert(candidate_event);
176 return incremental_exC;
179 EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const
182 for (const auto e : exC) {
183 if (not e->conflicts_with(C)) {
190 void UdporChecker::move_to_stateCe(State& state, const 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 state.execute_next(next_actor, get_remote_app());
203 void UdporChecker::restore_program_state_to(const State& stateC)
205 get_remote_app().restore_initial_state();
206 // TODO: We need to have the stack of past states available at this
207 // point. Since the method is recursive, we'll need to keep track of
208 // this as we progress
211 std::unique_ptr<State> UdporChecker::record_current_state()
213 auto next_state = this->get_current_state();
215 // In UDPOR, we care about all enabled transitions in a given state
216 next_state->consider_all();
221 const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
224 return *(enC.begin());
227 for (const auto& event : A) {
228 if (enC.contains(event)) {
235 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
237 const EventSet C_union_D = C.get_events().make_union(D);
238 const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
239 const EventSet Q_CDU = C_union_D.make_union(es_immediate_conflicts.get_local_config());
241 // Move {e} \ Q_CDU from U to G
242 if (Q_CDU.contains(e)) {
243 this->unfolding.remove(e);
246 // foreach ê in #ⁱ_U(e)
247 for (const auto* e_hat : es_immediate_conflicts) {
248 // Move [ê] \ Q_CDU from U to G
249 const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
250 this->unfolding.remove(to_remove);
254 RecordTrace UdporChecker::get_record_trace()
260 std::vector<std::string> UdporChecker::get_textual_trace()
262 // TODO: Topologically sort the events of the latest configuration
263 // and iterate through that topological sorting
264 std::vector<std::string> trace;
268 } // namespace simgrid::mc::udpor
270 namespace simgrid::mc {
272 Exploration* create_udpor_checker(const std::vector<char*>& args)
274 return new simgrid::mc::udpor::UdporChecker(args);
277 } // namespace simgrid::mc