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/maximal_subsets_iterator.hpp"
9 #include <xbt/asserts.h>
12 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification using UDPOR");
14 namespace simgrid::mc::udpor {
16 UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args)
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)) {
54 if (not C.get_events().empty()) {
55 // Report information...
58 // When `en(C)` is empty, intuitively this means that there
59 // are no enabled transitions that can be executed from the
60 // state reached by `C` (denoted `state(C)`), i.e. by some
61 // execution of the transitions in C obeying the causality
62 // relation. Here, then, we would be in a deadlock.
64 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 // TODO: Determine a value of K to use or don't use it at all
97 constexpr unsigned K = 10;
98 if (auto J = compute_partial_alternative(D, C, K); !J.empty()) {
99 J.subtract(C.get_events());
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 explore(C, D, std::move(J), std::move(stateC), 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 // First check for a specialized function that can compute the extension
134 // set "quickly" based on its type. Otherwise, fall back to computing
136 const auto specialized_extension_function = incremental_extension_functions.find(transition->type_);
137 if (specialized_extension_function != incremental_extension_functions.end()) {
138 exC.form_union((specialized_extension_function->second)(C, transition));
140 exC.form_union(this->compute_exC_by_enumeration(C, transition));
147 EventSet UdporChecker::compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action)
149 // Here we're computing the following:
151 // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
153 // where `a` is the `action` given to us. Note that `a` is presumed to be enabled
154 EventSet incremental_exC;
157 maximal_subsets_iterator(C, {[&](const UnfoldingEvent* e) { return e->is_dependent_with(action.get()); }});
158 begin != maximal_subsets_iterator(); ++begin) {
159 const EventSet& maximal_subset = *begin;
161 // TODO: Determine if `a` is enabled here
162 const bool enabled_at_config_k = false;
164 if (enabled_at_config_k) {
165 auto candidate_handle = std::make_unique<UnfoldingEvent>(maximal_subset, action);
166 if (auto candidate_event = candidate_handle.get(); not unfolding.contains_event_equivalent_to(candidate_event)) {
167 // This is a new event (i.e. one we haven't yet seen)
168 unfolding.insert(std::move(candidate_handle));
169 incremental_exC.insert(candidate_event);
174 return incremental_exC;
177 EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const
180 for (const auto e : exC) {
181 if (not e->conflicts_with(C)) {
188 void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
190 const aid_t next_actor = e.get_transition()->aid_;
192 // TODO: Add the trace if possible for reporting a bug
193 xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
194 "In reaching this execution path, UDPOR ensures that at least one\n"
195 "one transition of the state of an visited event is enabled, yet no\n"
196 "state was actually enabled. Please report this as a bug.\n"
197 "*********************************\n\n");
198 state.execute_next(next_actor);
201 void UdporChecker::restore_program_state_to(const State& stateC)
203 get_remote_app().restore_initial_state();
204 // TODO: We need to have the stack of past states available at this
205 // point. Since the method is recursive, we'll need to keep track of
206 // this as we progress
209 std::unique_ptr<State> UdporChecker::record_current_state()
211 auto next_state = this->get_current_state();
213 // In UDPOR, we care about all enabled transitions in a given state
214 next_state->mark_all_enabled_todo();
219 const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
222 return *(enC.begin());
225 for (const auto& event : A) {
226 if (enC.contains(event)) {
233 EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
235 // TODO: Compute k-partial alternatives using [2]
239 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
241 const EventSet C_union_D = C.get_events().make_union(D);
242 const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
243 const EventSet Q_CDU = C_union_D.make_union(es_immediate_conflicts.get_local_config());
245 // Move {e} \ Q_CDU from U to G
246 if (Q_CDU.contains(e)) {
247 this->unfolding.remove(e);
250 // foreach ê in #ⁱ_U(e)
251 for (const auto* e_hat : es_immediate_conflicts) {
252 // Move [ê] \ Q_CDU from U to G
253 const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
254 this->unfolding.remove(to_remove);
258 RecordTrace UdporChecker::get_record_trace()
264 std::vector<std::string> UdporChecker::get_textual_trace()
266 // TODO: Topologically sort the events of the latest configuration
267 // and iterate through that topological sorting
268 std::vector<std::string> trace;
272 } // namespace simgrid::mc::udpor
274 namespace simgrid::mc {
276 Exploration* create_udpor_checker(const std::vector<char*>& args)
278 return new simgrid::mc::udpor::UdporChecker(args);
281 } // namespace simgrid::mc