1 /* Copyright (c) 2007-2023. The SimGrid Team.
2 * All rights reserved. */
4 /* This program is free software; you can redistribute it and/or modify it
5 * under the terms of the license (GNU LGPL) which comes with this package. */
7 #ifndef SIMGRID_MC_UDPOR_CHECKER_HPP
8 #define SIMGRID_MC_UDPOR_CHECKER_HPP
10 #include "src/mc/explo/Exploration.hpp"
11 #include "src/mc/explo/udpor/Configuration.hpp"
12 #include "src/mc/explo/udpor/EventSet.hpp"
13 #include "src/mc/explo/udpor/StateManager.hpp"
14 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
15 #include "src/mc/mc_record.hpp"
19 namespace simgrid::mc::udpor {
22 * @brief Performs exploration of a concurrent system via the
25 * The `UdporChecker` implementation is based primarily off three papers,
26 * herein referred to as [1], [2], and [3] respectively, as well as the
27 * current implementation of `tiny_simgrid`:
29 * 1. "Unfolding-based Partial Order Reduction" by Rodriguez et al.
30 * 2. Quasi-Optimal Partial Order Reduction by Nguyen et al.
31 * 3. The Anh Pham's Thesis "Exploration efficace de l'espace ..."
33 class XBT_PRIVATE UdporChecker : public Exploration {
35 explicit UdporChecker(const std::vector<char*>& args);
38 RecordTrace get_record_trace() override;
39 std::vector<std::string> get_textual_trace() override;
41 inline std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
45 * The total number of events created whilst exploring the unfolding
47 uint32_t nb_events = 0;
48 uint32_t nb_traces = 0;
51 * @brief The "relevant" portions of the unfolding that must be kept around to ensure that
52 * UDPOR properly searches the state space
54 * The set `U` is a global variable which is maintained by UDPOR
55 * to keep track of "just enough" information about the unfolding
56 * to compute *alternatives* (see the paper for more details).
58 * @invariant: When a new event is created by UDPOR, it is inserted into
59 * this set. All new events that are created by UDPOR have causes that
60 * also exist in U and are valid for the duration of the search.
62 * If an event is discarded instead of moved from set `U` to set `G`,
63 * the event and its contents will be discarded.
68 * @brief The "irrelevant" portions of the unfolding that do not need to be kept
69 * around to ensure that UDPOR functions correctly
71 * The set `G` is another global variable maintained by the UDPOR algorithm which
72 * is used to keep track of all events which used to be important to UDPOR
77 * Maintains the mapping between handles referenced by events in
78 * the current state of the unfolding
80 StateManager state_manager_;
84 * @brief Explores the unfolding of the concurrent system
85 * represented by the ModelChecker instance "mcmodel_checker"
87 * This function performs the actual search following the
88 * UDPOR algorithm according to [1].
90 * @param C the current configuration from which UDPOR will be used
91 * to explore expansions of the concurrent system being modeled
92 * @param D the set of events that should not be considered by UDPOR
93 * while performing its searches, in order to avoid sleep-set blocked
94 * executions. See [1] for more details
95 * @param A the set of events to "guide" UDPOR in the correct direction
96 * when it returns back to a node in the unfolding and must decide among
97 * events to select from `ex(C)`. See [1] for more details
98 * @param max_evt_history
100 * @param e the event where UDPOR currently "rests", viz. the event UDPOR
101 * is now currently considering. This event is contained in the set `C`
102 * and is the last event that was added to C
105 * TODO: Add the optimization where we can check if e == e_prior
106 * to prevent repeated work when computing ex(C)
108 void explore(Configuration C, EventSet D, EventSet A, std::list<EventSet> max_evt_history, UnfoldingEvent* e_cur,
112 * @brief Computes the sets `ex(C)` and `en(C)` of the given configuration
113 * `C` as an incremental computation from the the previous computation of `ex(C)`
115 * A central component to UDPOR is the computation of the set `ex(C)`. The
116 * extension set `ex(C)` of a configuration `C` is defined as the set of events
117 * outside of `C` whose full dependency chain is contained in `C` (see [1]
120 * In general, computing `ex(C)` is very expensive. In paper [3], The Anh Pham
121 * shows a method of incremental computation of the set `ex(C)` under the
122 * conclusions afforded under the computation model in consideration, of which
123 * SimGrid is apart, which allow for `ex(C)` to be computed much more efficiently.
124 * Intuitively, the idea is to take advantage of the fact that you can avoid a lot
125 * of repeated computation by exploiting the aforementioned properties (in [3]) in
126 * what is effectively a dynamic programming optimization. See [3] for more details
128 * @param C the configuration based on which the two sets `ex(C)` and `en(C)` are
130 * @param e the event where UDPOR currently "rests", viz. the event UDPOR
131 * is now currently considering
132 * @param prev_exC the previous value of `ex(C)`, viz. that which was computed for
133 * the configuration `C' := C - {e}`
134 * @returns a tuple containing the pair of sets `ex(C)` and `en(C)` respectively
136 std::tuple<EventSet, EventSet> compute_extension(const Configuration& C, const std::list<EventSet>& max_evt_history,
137 UnfoldingEvent* e, const EventSet& prev_exC) const;
142 StateHandle observe_unfolding_event(const UnfoldingEvent& event);
145 * @brief Resolves the state handle maintained by an event
146 * into a concrete reference to a state
148 State& get_state_referenced_by(const UnfoldingEvent& event);
151 * @brief Creates a new snapshot of the state of the progam undergoing
154 * @returns the handle used to uniquely identify this state later in the
155 * exploration of the unfolding. You provide this handle to an event in the
156 * unfolding to regenerate past states
158 StateHandle record_current_state();
161 * @brief Identifies the next event from the unfolding of the concurrent system
162 * that should next be explored as an extension of a configuration with
163 * enabled events `enC`
165 * @param A The set of events `A` maintained by the UDPOR algorithm to help
166 * determine how events should be selected. See the original paper [1] for more details
168 * @param enC The set `enC` of enabled events from the extension set `exC` used
169 * by the UDPOR algorithm to select new events to search. See the original
170 * paper [1] for more details
172 UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
177 EventSet compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const;
182 void clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D);
184 } // namespace simgrid::mc::udpor