X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/a123c47d727be0441ca0702d10a3ef63437deca7..7e625e5e848a284b522d69ec28cb111f1f88515b:/src/mc/explo/UdporChecker.hpp diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp index 28c9d1955b..02f2a8e1d1 100644 --- a/src/mc/explo/UdporChecker.hpp +++ b/src/mc/explo/UdporChecker.hpp @@ -7,13 +7,16 @@ #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/StateManager.hpp" +#include "src/mc/explo/udpor/Unfolding.hpp" #include "src/mc/explo/udpor/UnfoldingEvent.hpp" #include "src/mc/mc_record.hpp" +#include +#include #include namespace simgrid::mc::udpor { @@ -27,7 +30,7 @@ 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 { @@ -36,50 +39,15 @@ public: void run() override; RecordTrace get_record_trace() override; - std::vector get_textual_trace() override; - - inline std::unique_ptr get_current_state() { return std::make_unique(get_remote_app()); } + std::unique_ptr get_current_state() { return std::make_unique(get_remote_app()); } private: - /** - * The total number of events created whilst exploring the unfolding - */ - uint32_t nb_events = 0; - uint32_t nb_traces = 0; - - /** - * @brief The "relevant" portions of the unfolding that must be kept around to ensure that - * UDPOR properly searches the state space - * - * 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). - * - * @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. - * - * If an event is discarded instead of moved from set `U` to set `G`, - * the event and its contents will be discarded. - */ - EventSet U; - - /** - * @brief The "irrelevant" portions of the unfolding that do not need to be kept - * around to ensure that UDPOR functions correctly - * - * 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; + Unfolding unfolding = Unfolding(); - /** - * Maintains the mapping between handles referenced by events in - * the current state of the unfolding - */ - StateManager state_manager_; + // The current sequence of states that the checker has + // visited in order to reach the current configuration + std::list> state_stack; -private: /** * @brief Explores the unfolding of the concurrent system * represented by the ModelChecker instance "mcmodel_checker" @@ -95,18 +63,25 @@ private: * @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 - * @param max_evt_history - * - * @param e the event where UDPOR currently "rests", viz. the event UDPOR - * is now currently considering. This event is contained in the set `C` - * and is the last event that was added to C - * * * TODO: Add the optimization where we can check if e == e_prior * to prevent repeated work when computing ex(C) */ - void explore(Configuration C, EventSet D, EventSet A, std::list max_evt_history, UnfoldingEvent* e_cur, - EventSet prev_exC); + void explore(const Configuration& C, EventSet D, EventSet A, EventSet prev_exC); + + /** + * @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); /** * @brief Computes the sets `ex(C)` and `en(C)` of the given configuration @@ -123,61 +98,53 @@ private: * 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 e 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 - {e}` - * @returns a tuple containing the pair of sets `ex(C)` and `en(C)` respectively - */ - std::tuple compute_extension(const Configuration& C, const std::list& max_evt_history, - UnfoldingEvent* e, const EventSet& prev_exC) const; - - /** - * - */ - StateHandle observe_unfolding_event(const UnfoldingEvent& event); - - /** - * @brief Resolves the state handle maintained by an event - * into a concrete reference to a state + * @returns the extension set `ex(C)` of `C` */ - State& get_state_referenced_by(const UnfoldingEvent& event); + EventSet compute_exC(const Configuration& C, const State& stateC, const EventSet& prev_exC); + EventSet compute_enC(const Configuration& C, const EventSet& exC) const; /** - * @brief Creates a new snapshot of the state of the progam undergoing - * model checking * - * @returns the handle used to uniquely identify this state later in the - * exploration of the unfolding. You provide this handle to an event in the - * unfolding to regenerate past states */ - StateHandle record_current_state(); + void move_to_stateCe(State* stateC, UnfoldingEvent* e); /** - * @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 + * @brief Creates a new snapshot of the state of the application + * as it currently looks */ - UnfoldingEvent* select_next_unfolding_event(const EventSet& A, const EventSet& enC); + std::unique_ptr 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. */ - EventSet compute_partial_alternative(const EventSet& D, const Configuration& C, const unsigned k) const; + 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 Configuration& C, const EventSet& D); };