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();
70 // TODO: Add verbose logging about which event is being explored
72 const UnfoldingEvent* e = select_next_unfolding_event(A, enC);
73 xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
74 "UDPOR guarantees that an event will be chosen at each point in\n"
75 "the search, yet no events were actually chosen\n"
76 "*********************************\n\n");
78 // Move the application into stateCe and actually make note of that state
79 move_to_stateCe(*stateC, *e);
80 auto stateCe = record_current_state();
89 // Explore(C + {e}, D, A \ {e})
90 explore(Ce, D, std::move(A), std::move(stateCe), std::move(exC));
95 // TODO: Determine a value of K to use or don't use it at all
96 constexpr unsigned K = 10;
97 if (auto J = compute_partial_alternative(D, C, K); !J.empty()) {
98 J.subtract(C.get_events());
100 // Before searching the "right half", we need to make
101 // sure the program actually reflects the fact
102 // that we are searching again from `stateC` (the recursive
103 // search moved the program into `stateCe`)
104 restore_program_state_to(*stateC);
106 // Explore(C, D + {e}, J \ C)
107 explore(C, D, std::move(J), std::move(stateC), std::move(prev_exC));
114 clean_up_explore(e, C, D);
117 EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC)
119 // See eqs. 5.7 of section 5.2 of [3]
120 // C = C' + {e_cur}, i.e. C' = C - {e_cur}
124 // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
125 // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
126 const UnfoldingEvent* e_cur = C.get_latest_event();
127 EventSet exC = prev_exC;
130 for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
131 for (const auto& transition : actor_state.get_enabled_transitions()) {
132 // First check for a specialized function that can compute the extension
133 // set "quickly" based on its type. Otherwise, fall back to computing
135 const auto specialized_extension_function = incremental_extension_functions.find(transition->type_);
136 if (specialized_extension_function != incremental_extension_functions.end()) {
137 exC.form_union((specialized_extension_function->second)(C, transition));
139 exC.form_union(this->compute_exC_by_enumeration(C, transition));
146 EventSet UdporChecker::compute_exC_by_enumeration(const Configuration& C, const std::shared_ptr<Transition> action)
148 // Here we're computing the following:
150 // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at config(K) }
152 // where `a` is the `action` given to us. Note that `a` is presumed to be enabled
153 EventSet incremental_exC;
156 maximal_subsets_iterator(C, {[&](const UnfoldingEvent* e) { return e->is_dependent_with(action.get()); }});
157 begin != maximal_subsets_iterator(); ++begin) {
158 const EventSet& maximal_subset = *begin;
160 // TODO: Determine if `a` is enabled here
161 const bool enabled_at_config_k = false;
163 if (enabled_at_config_k) {
164 auto candidate_handle = std::make_unique<UnfoldingEvent>(maximal_subset, action);
165 if (auto candidate_event = candidate_handle.get(); not unfolding.contains_event_equivalent_to(candidate_event)) {
166 // This is a new event (i.e. one we haven't yet seen)
167 unfolding.insert(std::move(candidate_handle));
168 incremental_exC.insert(candidate_event);
173 return incremental_exC;
176 EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const
179 for (const auto e : exC) {
180 if (not e->conflicts_with(C)) {
187 void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
189 const aid_t next_actor = e.get_transition()->aid_;
191 // TODO: Add the trace if possible for reporting a bug
192 xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
193 "In reaching this execution path, UDPOR ensures that at least one\n"
194 "one transition of the state of an visited event is enabled, yet no\n"
195 "state was actually enabled. Please report this as a bug.\n"
196 "*********************************\n\n");
197 state.execute_next(next_actor);
200 void UdporChecker::restore_program_state_to(const State& stateC)
202 // TODO: Perform state regeneration in the same manner as is done
203 // in the DFSChecker.cpp
206 std::unique_ptr<State> UdporChecker::record_current_state()
208 auto next_state = this->get_current_state();
210 // In UDPOR, we care about all enabled transitions in a given state
211 next_state->mark_all_enabled_todo();
216 const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
219 return *(enC.begin());
222 for (const auto& event : A) {
223 if (enC.contains(event)) {
230 EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
232 // TODO: Compute k-partial alternatives using [2]
236 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
238 // TODO: Perform clean up here
241 RecordTrace UdporChecker::get_record_trace()
247 std::vector<std::string> UdporChecker::get_textual_trace()
249 // TODO: Topologically sort the events of the latest configuration
250 // and iterate through that topological sorting
251 std::vector<std::string> trace;
255 } // namespace simgrid::mc::udpor
257 namespace simgrid::mc {
259 Exploration* create_udpor_checker(const std::vector<char*>& args)
261 return new simgrid::mc::udpor::UdporChecker(args);
264 } // namespace simgrid::mc