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/CompatibilityGraph.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 // Perform the incremental computation of exC
46 // TODO: This method will have side effects on
47 // the unfolding, but the naming of the method
48 // suggests it is doesn't have side effects. We should
49 // reconcile this in the future
50 auto [exC, enC] = compute_extension(C, *stateC, prev_exC);
52 // If enC is a subset of D, intuitively
53 // there aren't any enabled transitions
54 // which are "worth" exploring since their
55 // exploration would lead to a so-called
56 // "sleep-set blocked" trace.
57 if (enC.is_subset_of(D)) {
59 if (not C.get_events().empty()) {
61 // g_var::nb_traces++;
64 // When `en(C)` is empty, intuitively this means that there
65 // are no enabled transitions that can be executed from the
66 // state reached by `C` (denoted `state(C)`), i.e. by some
67 // execution of the transitions in C obeying the causality
68 // relation. Here, then, we would be in a deadlock.
70 get_remote_app().check_deadlock();
76 // TODO: Add verbose logging about which event is being explored
78 UnfoldingEvent* e = select_next_unfolding_event(A, enC);
79 xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
80 "UDPOR guarantees that an event will be chosen at each point in\n"
81 "the search, yet no events were actually chosen\n"
82 "*********************************\n\n");
84 // Move the application into stateCe and actually make note of that state
85 move_to_stateCe(*stateC, *e);
86 auto stateCe = record_current_state();
95 // Explore(C + {e}, D, A \ {e})
96 explore(Ce, D, std::move(A), std::move(stateCe), std::move(exC));
101 // TODO: Determine a value of K to use or don't use it at all
102 constexpr unsigned K = 10;
103 if (auto J = compute_partial_alternative(D, C, K); !J.empty()) {
104 J.subtract(C.get_events());
106 // Before searching the "right half", we need to make
107 // sure the program actually reflects the fact
108 // that we are searching again from `stateC` (the recursive
109 // search moved the program into `stateCe`)
110 restore_program_state_to(*stateC);
112 // Explore(C, D + {e}, J \ C)
113 explore(C, D, std::move(J), std::move(stateC), std::move(prev_exC));
120 clean_up_explore(e, C, D);
123 std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C, const State& stateC,
124 const EventSet& prev_exC) const
126 // See eqs. 5.7 of section 5.2 of [3]
127 // C = C' + {e_cur}, i.e. C' = C - {e_cur}
131 // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} +
132 // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at K }
133 UnfoldingEvent* e_cur = C.get_latest_event();
134 EventSet exC = prev_exC;
137 for (const auto& [aid, actor_state] : stateC.get_actors_list()) {
138 for (const auto& transition : actor_state.get_enabled_transitions()) {
139 // First check for a specialized function that can compute the extension
140 // set "quickly" based on its type. Otherwise, fall back to computing
142 const auto specialized_extension_function = incremental_extension_functions.find(transition->type_);
143 if (specialized_extension_function != incremental_extension_functions.end()) {
144 exC.form_union((specialized_extension_function->second)(C, *transition));
146 exC.form_union(this->compute_extension_by_enumeration(C, *transition));
152 // TODO: Compute enC based on conflict relations
154 return std::tuple<EventSet, EventSet>(exC, enC);
157 EventSet UdporChecker::compute_extension_by_enumeration(const Configuration& C, const Transition& action) const
159 // Here we're computing the following:
161 // U{<a, K> : K is maximal, `a` depends on all of K, `a` enabled at K }
163 // where `a` is the `action` given to us.
164 EventSet incremental_exC;
166 // We only consider those combinations of events for which `action` is dependent with
167 // the action associated with any given event ("`a` depends on all of K")
168 const std::unique_ptr<CompatibilityGraph> G = C.make_compatibility_graph_filtered_on([=](UnfoldingEvent* e) {
169 const auto e_transition = e->get_transition();
170 return action.depends(e_transition);
173 // TODO: Now that the graph has been constructed, enumerate
174 // all possible k-cliques of the complement of G
176 // TODO: For each enumeration, check all possible
177 // combinations of selecting a single event from
178 // each set associated with the graph nodes
180 return incremental_exC;
183 void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
185 const aid_t next_actor = e.get_transition()->aid_;
187 // TODO: Add the trace if possible for reporting a bug
188 xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
189 "In reaching this execution path, UDPOR ensures that at least one\n"
190 "one transition of the state of an visited event is enabled, yet no\n"
191 "state was actually enabled. Please report this as a bug.\n"
192 "*********************************\n\n");
193 state.execute_next(next_actor);
196 void UdporChecker::restore_program_state_to(const State& stateC)
198 // TODO: Perform state regeneration in the same manner as is done
199 // in the DFSChecker.cpp
202 std::unique_ptr<State> UdporChecker::record_current_state()
204 auto next_state = this->get_current_state();
206 // In UDPOR, we care about all enabled transitions in a given state
207 next_state->mark_all_enabled_todo();
212 UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
215 return *(enC.begin());
218 for (const auto& event : A) {
219 if (enC.contains(event)) {
226 EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
228 // TODO: Compute k-partial alternatives using [2]
232 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
234 // TODO: Perform clean up here
237 RecordTrace UdporChecker::get_record_trace()
243 std::vector<std::string> UdporChecker::get_textual_trace()
245 // TODO: Topologically sort the events of the latest configuration
246 // and iterate through that topological sorting
247 std::vector<std::string> trace;
251 } // namespace simgrid::mc::udpor
253 namespace simgrid::mc {
255 Exploration* create_udpor_checker(const std::vector<char*>& args)
257 return new simgrid::mc::udpor::UdporChecker(args);
260 } // namespace simgrid::mc