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 may be in a deadlock (the other
66 // possibility is that we've finished running everything, and
67 // we wouldn't be in deadlock then)
69 get_remote_app().check_deadlock();
75 // TODO: Add verbose logging about which event is being explored
77 const UnfoldingEvent* e = select_next_unfolding_event(A, enC);
78 xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
79 "UDPOR guarantees that an event will be chosen at each point in\n"
80 "the search, yet no events were actually chosen\n"
81 "*********************************\n\n");
83 // Move the application into stateCe and make note of that state
84 move_to_stateCe(*stateC, *e);
85 auto stateCe = record_current_state();
94 // Explore(C + {e}, D, A \ {e})
95 explore(Ce, D, std::move(A), std::move(stateCe), std::move(exC));
100 constexpr unsigned K = 10;
101 if (auto J_minus_C = compute_k_partial_alternative(D, C, K); J_minus_C.has_value()) {
102 // Before searching the "right half", we need to make
103 // sure the program actually reflects the fact
104 // that we are searching again from `stateC` (the recursive
105 // search moved the program into `stateCe`)
106 restore_program_state_to(*stateC);
108 // Explore(C, D + {e}, J \ C)
109 explore(C, D, std::move(J_minus_C.value()), 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);
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->mark_all_enabled_todo();
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 std::vector<const UnfoldingEvent*> UdporChecker::pick_k_partial_alternative_events(const EventSet& D,
236 const unsigned k) const
238 const unsigned size = std::min(k, static_cast<unsigned>(D.size()));
239 std::vector<const UnfoldingEvent*> D_hat(size);
241 // Potentially select intelligently here (e.g. perhaps pick events
242 // with transitions that we know are totally independent)...
244 // For now, simply pick the first `k` events (any subset suffices)
245 std::copy_n(D.begin(), size, D_hat.begin());
249 std::optional<EventSet> UdporChecker::compute_k_partial_alternative(const EventSet& D, const Configuration& C,
250 const unsigned k) const
252 // 1. Select k (of |D|, whichever is smaller) arbitrary events e_1, ..., e_k from D
253 const auto D_hat = pick_k_partial_alternative_events(D, k);
255 // 2. Build a U-comb <s_1, ..., s_k> of size k, where spike `s_i` contains
256 // all events in conflict with `e_i`
258 // 3. EXCEPT those events e' for which [e'] + C is not a configuration or
261 // NOTE: This is an expensive operation as we must traverse the entire unfolding
262 // and compute `C.is_compatible_with(History)` for every event in the structure :/.
263 // A later performance improvement would be to incorporate the work of Nguyen et al.
264 // into SimGrid. Since that is a rather complicated addition, we defer to the addition
265 // for a later time...
268 for (const auto* e : this->unfolding) {
269 for (unsigned i = 0; i < k; i++) {
270 const auto& e_i = D_hat[i];
271 if (const auto e_local_config = History(e);
272 e_i->conflicts_with(e) and (not D.contains(e_local_config)) and C.is_compatible_with(e_local_config)) {
273 comb[i].push_back(e);
278 // 4. Find any such combination <e_1', ..., e_k'> in comb satisfying
279 // ~(e_i' # e_j') for i != j
281 // NOTE: This is a VERY expensive operation: it enumerates all possible
282 // ways to select an element from each spike. Unfortunately there's no
283 // way around the enumeration, as computing a full alternative in general is
284 // NP-complete (although computing the k-partial alternative is polynomial in n)
285 const auto map_events = [](const std::vector<Spike::const_iterator>& spikes) {
286 std::vector<const UnfoldingEvent*> events;
287 for (const auto& event_in_spike : spikes) {
288 events.push_back(*event_in_spike);
290 return EventSet(std::move(events));
292 const auto alternative =
293 std::find_if(comb.combinations_begin(), comb.combinations_end(),
294 [&map_events](const auto& vector) { return map_events(vector).is_conflict_free(); });
296 // No such alternative exists
297 if (alternative == comb.combinations_end()) {
301 // 5. J := [e_1] + [e_2] + ... + [e_k] is a k-partial alternative
302 // NOTE: This function computes J / C, which is what is actually used in UDPOR
303 return History(map_events(*alternative)).get_event_diff_with(C);
306 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
308 const EventSet C_union_D = C.get_events().make_union(D);
309 const EventSet es_immediate_conflicts = this->unfolding.get_immediate_conflicts_of(e);
310 const EventSet Q_CDU = C_union_D.make_union(es_immediate_conflicts.get_local_config());
312 // Move {e} \ Q_CDU from U to G
313 if (Q_CDU.contains(e)) {
314 this->unfolding.remove(e);
317 // foreach ê in #ⁱ_U(e)
318 for (const auto* e_hat : es_immediate_conflicts) {
319 // Move [ê] \ Q_CDU from U to G
320 const EventSet to_remove = e_hat->get_history().subtracting(Q_CDU);
321 this->unfolding.remove(to_remove);
325 RecordTrace UdporChecker::get_record_trace()
331 std::vector<std::string> UdporChecker::get_textual_trace()
333 // TODO: Topologically sort the events of the latest configuration
334 // and iterate through that topological sorting
335 std::vector<std::string> trace;
339 } // namespace simgrid::mc::udpor
341 namespace simgrid::mc {
343 Exploration* create_udpor_checker(const std::vector<char*>& args)
345 return new simgrid::mc::udpor::UdporChecker(args);
348 } // namespace simgrid::mc