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 <xbt/asserts.h>
11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification using UDPOR");
13 namespace simgrid::mc::udpor {
15 UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args)
17 /* Create initial data structures, if any ...*/
19 // TODO: Initialize state structures for the search
22 void UdporChecker::run()
24 XBT_INFO("Starting a UDPOR exploration");
25 // NOTE: `A`, `D`, and `C` are derived from the
26 // original UDPOR paper [1], while `prev_exC` arises
27 // from the incremental computation of ex(C) from [3]
30 // TODO: Move computing the root configuration into a method on the Unfolding
31 auto initial_state = get_current_state();
32 auto root_event = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<Transition>());
33 auto* root_event_handle = root_event.get();
34 unfolding.insert(std::move(root_event));
35 C_root.add_event(root_event_handle);
37 explore(std::move(C_root), EventSet(), EventSet(), std::move(initial_state), EventSet());
39 XBT_INFO("UDPOR exploration terminated -- model checking completed");
42 void UdporChecker::explore(Configuration C, EventSet D, EventSet A, std::unique_ptr<State> stateC, EventSet prev_exC)
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, 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 (C.get_events().size() > 0) {
61 // g_var::nb_traces++;
63 // TODO: Log here correctly
64 // XBT_DEBUG("\n Exploring executions: %d : \n", g_var::nb_traces);
69 // When `en(C)` is empty, intuitively this means that there
70 // are no enabled transitions that can be executed from the
71 // state reached by `C` (denoted `state(C)`), i.e. by some
72 // execution of the transitions in C obeying the causality
73 // relation. Here, then, we would be in a deadlock.
75 get_remote_app().check_deadlock();
81 // TODO: Add verbose logging about which event is being explored
83 UnfoldingEvent* e = select_next_unfolding_event(A, enC);
84 xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
85 "UDPOR guarantees that an event will be chosen at each point in\n"
86 "the search, yet no events were actually chosen\n"
87 "*********************************\n\n");
89 // Move the application into stateCe and actually make note of that state
90 move_to_stateCe(*stateC, *e);
91 auto stateCe = record_current_state();
100 // Explore(C + {e}, D, A \ {e})
101 explore(Ce, D, std::move(A), std::move(stateCe), std::move(exC));
106 // TODO: Determine a value of K to use or don't use it at all
107 constexpr unsigned K = 10;
108 auto J = compute_partial_alternative(D, C, K);
110 J.subtract(C.get_events());
112 // Before searching the "right half", we need to make
113 // sure the program actually reflects the fact
114 // that we are searching again from `stateC` (the recursive
115 // search moved the program into `stateCe`)
116 restore_program_state_to(*stateC);
118 // Explore(C, D + {e}, J \ C)
119 explore(C, D, std::move(J), std::move(stateC), std::move(prev_exC));
126 clean_up_explore(e, C, D);
129 std::tuple<EventSet, EventSet> UdporChecker::compute_extension(const Configuration& C, const EventSet& prev_exC) const
131 // See eqs. 5.7 of section 5.2 of [3]
132 // C = C' + {e_cur}, i.e. C' = C - {e_cur}
136 // ex(C) = ex(C' + {e_cur}) = ex(C') / {e_cur} + U{<a, > : H }
137 UnfoldingEvent* e_cur = C.get_latest_event();
138 EventSet exC = prev_exC;
141 // ... fancy computations
144 return std::tuple<EventSet, EventSet>(exC, enC);
147 void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
149 const aid_t next_actor = e.get_transition()->aid_;
151 // TODO: Add the trace if possible for reporting a bug
152 xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
153 "In reaching this execution path, UDPOR ensures that at least one\n"
154 "one transition of the state of an visited event is enabled, yet no\n"
155 "state was actually enabled. Please report this as a bug.\n"
156 "*********************************\n\n");
157 state.execute_next(next_actor);
160 void UdporChecker::restore_program_state_to(const State& stateC)
162 // TODO: Perform state regeneration in the same manner as is done
163 // in the DFSChecker.cpp
166 std::unique_ptr<State> UdporChecker::record_current_state()
168 auto next_state = this->get_current_state();
170 // In UDPOR, we care about all enabled transitions in a given state
171 next_state->mark_all_enabled_todo();
176 UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
179 return *(enC.begin());
182 for (const auto& event : A) {
183 if (enC.contains(event)) {
190 EventSet UdporChecker::compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const
192 // TODO: Compute k-partial alternatives using [2]
196 void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D)
198 // TODO: Perform clean up here
201 RecordTrace UdporChecker::get_record_trace()
207 std::vector<std::string> UdporChecker::get_textual_trace()
209 // TODO: Topologically sort the events of the latest configuration
210 // and iterate through that topological sorting
211 std::vector<std::string> trace;
215 } // namespace simgrid::mc::udpor
217 namespace simgrid::mc {
219 Exploration* create_udpor_checker(const std::vector<char*>& args)
221 return new simgrid::mc::udpor::UdporChecker(args);
224 } // namespace simgrid::mc