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)
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 would be in a deadlock.
67 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_minus_C = compute_k_partial_alternative(D, C, K); J_minus_C.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 explore(C, D, std::move(J_minus_C.value()), 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);
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 get_remote_app().restore_initial_state();
203 // TODO: We need to have the stack of past states available at this
204 // point. Since the method is recursive, we'll need to keep track of
205 // this as we progress
208 std::unique_ptr<State> UdporChecker::record_current_state()
210 auto next_state = this->get_current_state();
212 // In UDPOR, we care about all enabled transitions in a given state
213 next_state->mark_all_enabled_todo();
218 const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
221 return *(enC.begin());
224 for (const auto& event : A) {
225 if (enC.contains(event)) {
232 std::vector<const UnfoldingEvent*> UdporChecker::pick_k_partial_alternative_events(const EventSet& D,
233 const unsigned k) const
235 const unsigned size = std::min(k, static_cast<unsigned>(D.size()));
236 std::vector<const UnfoldingEvent*> D_hat(size);
238 // Potentially select intelligently here (e.g. perhaps pick events
239 // with transitions that we know are totally independent)...
241 // For now, simply pick the first `k` events (any subset suffices)
242 std::copy_n(D.begin(), size, D_hat.begin());
246 std::optional<EventSet> UdporChecker::compute_k_partial_alternative(const EventSet& D, const Configuration& C,
247 const unsigned k) const
249 // 1. Select k (of |D|, whichever is smaller) arbitrary events e_1, ..., e_k from D
250 const auto D_hat = pick_k_partial_alternative_events(D, k);
252 // 2. Build a U-comb <s_1, ..., s_k> of size k, where spike `s_i` contains
253 // all events in conflict with `e_i`
255 // 3. EXCEPT those events e' for which [e'] + C is not a configuration or
259 for (const auto* e : this->unfolding) {
260 for (unsigned i = 0; i < k; i++) {
261 const auto& e_i = D_hat[i];
262 if (const auto e_local_config = History(e);
263 e_i->conflicts_with(e) and (not D.contains(e_local_config)) and C.is_compatible_with(e_local_config)) {
264 comb[i].push_back(e);
269 // 4. Find any such combination <e_1', ..., e_k'> in comb satisfying
270 // ~(e_i' # e_j') for i != j
271 // Note: This is a VERY expensive operation: it enumerates all possible
272 // ways to select an element from each spike
274 const auto map_events = [](const std::vector<Spike::const_iterator>& spikes) {
275 std::vector<const UnfoldingEvent*> events;
276 for (const auto& event_in_spike : spikes) {
277 events.push_back(*event_in_spike);
279 return EventSet(std::move(events));
281 const auto alternative =
282 std::find_if(comb.combinations_begin(), comb.combinations_end(),
283 [&map_events](const auto& vector) { return map_events(vector).is_conflict_free(); });
285 // No such alternative exists
286 if (alternative == comb.combinations_end()) {
290 // 5. J := [e_1] + [e_2] + ... + [e_k] is a k-partial alternative
291 return History(map_events(*alternative)).get_event_diff_with(C);
294 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
296 const EventSet C_union_D = C.get_events().make_union(D);
297 const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
298 const EventSet Q_CDU = C_union_D.make_union(es_immediate_conflicts.get_local_config());
300 // Move {e} \ Q_CDU from U to G
301 if (Q_CDU.contains(e)) {
302 this->unfolding.remove(e);
305 // foreach ê in #ⁱ_U(e)
306 for (const auto* e_hat : es_immediate_conflicts) {
307 // Move [ê] \ Q_CDU from U to G
308 const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
309 this->unfolding.remove(to_remove);
313 RecordTrace UdporChecker::get_record_trace()
319 std::vector<std::string> UdporChecker::get_textual_trace()
321 // TODO: Topologically sort the events of the latest configuration
322 // and iterate through that topological sorting
323 std::vector<std::string> trace;
327 } // namespace simgrid::mc::udpor
329 namespace simgrid::mc {
331 Exploration* create_udpor_checker(const std::vector<char*>& args)
333 return new simgrid::mc::udpor::UdporChecker(args);
336 } // namespace simgrid::mc