#ifndef SIMGRID_MC_UDPOR_CHECKER_HPP
#define SIMGRID_MC_UDPOR_CHECKER_HPP
+#include "src/mc/api/State.hpp"
#include "src/mc/explo/Exploration.hpp"
+#include "src/mc/explo/udpor/Configuration.hpp"
+#include "src/mc/explo/udpor/EventSet.hpp"
+#include "src/mc/explo/udpor/Unfolding.hpp"
+#include "src/mc/explo/udpor/UnfoldingEvent.hpp"
#include "src/mc/mc_record.hpp"
-#include "src/mc/udpor_global.hpp"
+#include <functional>
+#include <list>
#include <optional>
namespace simgrid::mc::udpor {
* current implementation of `tiny_simgrid`:
*
* 1. "Unfolding-based Partial Order Reduction" by Rodriguez et al.
- * 2. Quasi-Optimal Partial Order Reduction by Nguyen et al.
+ * 2. "Quasi-Optimal Partial Order Reduction" by Nguyen et al.
* 3. The Anh Pham's Thesis "Exploration efficace de l'espace ..."
*/
class XBT_PRIVATE UdporChecker : public Exploration {
void run() override;
RecordTrace get_record_trace() override;
- std::vector<std::string> get_textual_trace() override;
+ std::unique_ptr<State> get_current_state() { return std::make_unique<State>(get_remote_app()); }
private:
- /**
- * The total number of events created whilst exploring the unfolding
- */
- uint32_t nb_events = 0;
- uint32_t nb_traces = 0;
+ Unfolding unfolding = Unfolding();
+
+ // The current sequence of states that the checker has
+ // visited in order to reach the current configuration
+ std::list<std::unique_ptr<State>> state_stack;
/**
- * @brief The "relevant" portions of the unfolding that must be kept around to ensure that
- * UDPOR properly searches the state space
+ * @brief Explores the unfolding of the concurrent system
+ * represented by the ModelChecker instance "mcmodel_checker"
*
- * The set `U` is a global variable which is maintained by UDPOR
- * to keep track of "just enough" information about the unfolding
- * to compute *alternatives* (see the paper for more details).
+ * This function performs the actual search following the
+ * UDPOR algorithm according to [1].
*
- * @invariant: When a new event is created by UDPOR, it is inserted into
- * this set. All new events that are created by UDPOR have causes that
- * also exist in U and are valid for the duration of the search.
+ * @param C the current configuration from which UDPOR will be used
+ * to explore expansions of the concurrent system being modeled
+ * @param D the set of events that should not be considered by UDPOR
+ * while performing its searches, in order to avoid sleep-set blocked
+ * executions. See [1] for more details
+ * @param A the set of events to "guide" UDPOR in the correct direction
+ * when it returns back to a node in the unfolding and must decide among
+ * events to select from `ex(C)`. See [1] for more details
*
- * If an event is discarded instead of moved from set `U` to set `G`,
- * the event and its contents will be discarded.
+ * TODO: Add the optimization where we can check if e == e_prior
+ * to prevent repeated work when computing ex(C)
*/
- EventSet U;
+ void explore(const Configuration& C, EventSet D, EventSet A, EventSet prev_exC);
/**
- * @brief The "irrelevant" portions of the unfolding that do not need to be kept
- * around to ensure that UDPOR functions correctly
+ * @brief Identifies the next event from the unfolding of the concurrent system
+ * that should next be explored as an extension of a configuration with
+ * enabled events `enC`
*
- * The set `G` is another global variable maintained by the UDPOR algorithm which
- * is used to keep track of all events which used to be important to UDPOR
- */
- EventSet G;
-
-private:
- /**
- * @brief Explores the unfolding of the concurrent system
- * represented by the model checker instance
- * "model_checker"
+ * @param A The set of events `A` maintained by the UDPOR algorithm to help
+ * determine how events should be selected. See the original paper [1] for more details
*
- * TODO: Explain what this means here
+ * @param enC The set `enC` of enabled events from the extension set `exC` used
+ * by the UDPOR algorithm to select new events to search. See the original
+ * paper [1] for more details
*/
- void explore(Configuration C, std::list<EventSet> max_evt_history, EventSet D, EventSet A, UnfoldingEvent* cur_event,
- EventSet prev_exC);
+ UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
/**
* @brief Computes the sets `ex(C)` and `en(C)` of the given configuration
* SimGrid is apart, which allow for `ex(C)` to be computed much more efficiently.
* Intuitively, the idea is to take advantage of the fact that you can avoid a lot
* of repeated computation by exploiting the aforementioned properties (in [3]) in
- * what is effectively a dynamic programming optimization. See [3] for more details
+ * what is akin to a dynamic programming optimization. See [3] for more details
*
* @param C the configuration based on which the two sets `ex(C)` and `en(C)` are
* computed
- * @param cur_event the event where UDPOR currently "rests", viz. the event UDPOR
- * is now currently considering
+ * @param stateC the state of the program after having executed C (viz. `state(C)`)
* @param prev_exC the previous value of `ex(C)`, viz. that which was computed for
- * the configuration `C' := C - {cur_event}`
- * @returns a tuple containing the pair of sets `ex(C)` and `en(C)` respectively
+ * the configuration `C' := C - {e}`
+ * @returns the extension set `ex(C)` of `C`
*/
- std::tuple<EventSet, EventSet> extend(const Configuration& C, const std::list<EventSet>& max_evt_history,
- const UnfoldingEvent& cur_event, const EventSet& prev_exC) const;
+ EventSet compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC);
+ EventSet compute_enC(const Configuration& C, const EventSet& exC) const;
/**
- * @brief Identifies the next event from the unfolding of the concurrent system
- * that should next be explored as an extension of a configuration with
- * enabled events `enC`
*
- * @param A The set of events `A` maintained by the UDPOR algorithm to help
- * determine how events should be selected. See the original paper [1] for more details
- *
- * @param enC The set `enC` of enabled events from the extension set `exC` used
- * by the UDPOR algorithm to select new events to search. See the original
- * paper [1] for more details
*/
- UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC);
+ void move_to_stateCe(State* stateC, UnfoldingEvent* e);
- EventSet compute_partial_alternative(const EventSet& D, const EventSet& C, const unsigned k) const;
+ /**
+ * @brief Creates a new snapshot of the state of the application
+ * as it currently looks
+ */
+ std::unique_ptr<State> record_current_state();
/**
+ * @brief Move the application side into the state at the top of the
+ * state stack provided
+ *
+ * As UDPOR performs its search, it moves the application-side along with
+ * it so that the application is always providing the checker with
+ * the correct information about what each actor is running (and whether
+ * those actors are enabled) at the state reached by the configuration it
+ * decides to search.
*
+ * When UDPOR decides to "backtrack" (e.g. after reaching a configuration
+ * whose en(C) is empty), before it attempts to continue the search by taking
+ * a different path from a configuration it visited in the past, it must ensure
+ * that the application-side has moved back into `state(C)`.
+ *
+ * The search may have moved the application arbitrarily deep into its execution,
+ * and the search may backtrack arbitrarily closer to the beginning of the execution.
+ * The UDPOR implementation in SimGrid ensures that the stack is updated appropriately,
+ * but the process must still be regenerated.
+ */
+ void restore_program_state_with_current_stack();
+
+ /**
+ * @brief Perform the functionality of the `Remove(e, C, D)` function in [1]
*/
- void clean_up_explore(const UnfoldingEvent* e, const EventSet& C, const EventSet& D);
+ void clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D);
};
} // namespace simgrid::mc::udpor
