From bb7efba154782b821294cf933e12488d02a7802b Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Wed, 26 Apr 2023 15:57:28 +0200 Subject: [PATCH] Add `Execution` to represent series of transitions The Execution class represents a series of transitions taken by a process. An execution importantly also encodes the happens-before relation among the series of steps represented. The eventual implementation will leverage clock vectors to compute the relation between events. A more refined happens-before relation is left for as a future (complicated) exercise... --- src/mc/api/State.hpp | 1 + src/mc/explo/DFSExplorer.hpp | 8 ++- src/mc/explo/odpor/WakeupTree.cpp | 0 src/mc/explo/odpor/WakeupTree.hpp | 0 src/mc/explo/sdpor/Execution.hpp | 93 +++++++++++++++++++++++++++++ src/mc/explo/sdpor/Initials.cpp | 0 src/mc/explo/sdpor/Initials.hpp | 0 src/mc/explo/sdpor/WeakInitials.cpp | 0 src/mc/explo/sdpor/WeakInitials.hpp | 0 9 files changed, 101 insertions(+), 1 deletion(-) create mode 100644 src/mc/explo/odpor/WakeupTree.cpp create mode 100644 src/mc/explo/odpor/WakeupTree.hpp create mode 100644 src/mc/explo/sdpor/Execution.hpp create mode 100644 src/mc/explo/sdpor/Initials.cpp create mode 100644 src/mc/explo/sdpor/Initials.hpp create mode 100644 src/mc/explo/sdpor/WeakInitials.cpp create mode 100644 src/mc/explo/sdpor/WeakInitials.hpp diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp index e60e547b36..0bbc686b77 100644 --- a/src/mc/api/State.hpp +++ b/src/mc/api/State.hpp @@ -7,6 +7,7 @@ #define SIMGRID_MC_STATE_HPP #include "src/mc/api/ActorState.hpp" +#include "src/mc/api/ClockVector.hpp" #include "src/mc/api/RemoteApp.hpp" #include "src/mc/api/strategy/Strategy.hpp" #include "src/mc/transition/Transition.hpp" diff --git a/src/mc/explo/DFSExplorer.hpp b/src/mc/explo/DFSExplorer.hpp index 27194a8b46..087e06f13c 100644 --- a/src/mc/explo/DFSExplorer.hpp +++ b/src/mc/explo/DFSExplorer.hpp @@ -6,6 +6,7 @@ #ifndef SIMGRID_MC_SAFETY_CHECKER_HPP #define SIMGRID_MC_SAFETY_CHECKER_HPP +#include "src/mc/api/ClockVector.hpp" #include "src/mc/api/State.hpp" #include "src/mc/explo/Exploration.hpp" @@ -17,6 +18,7 @@ #include #include #include +#include #include namespace simgrid::mc { @@ -24,7 +26,7 @@ namespace simgrid::mc { using stack_t = std::list>; class XBT_PRIVATE DFSExplorer : public Exploration { - XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor); + XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor, sdpor); ReductionMode reduction_mode_; unsigned long backtrack_count_ = 0; // for statistics @@ -93,6 +95,10 @@ private: /** Stack representing the position in the exploration graph */ stack_t stack_; + + /** Per-actor clock vectors used to compute the "happens-before" relation */ + std::unordered_map per_actor_clocks_; + #if SIMGRID_HAVE_STATEFUL_MC VisitedStates visited_states_; std::unique_ptr visited_state_; diff --git a/src/mc/explo/odpor/WakeupTree.cpp b/src/mc/explo/odpor/WakeupTree.cpp new file mode 100644 index 0000000000..e69de29bb2 diff --git a/src/mc/explo/odpor/WakeupTree.hpp b/src/mc/explo/odpor/WakeupTree.hpp new file mode 100644 index 0000000000..e69de29bb2 diff --git a/src/mc/explo/sdpor/Execution.hpp b/src/mc/explo/sdpor/Execution.hpp new file mode 100644 index 0000000000..62af981943 --- /dev/null +++ b/src/mc/explo/sdpor/Execution.hpp @@ -0,0 +1,93 @@ +/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#ifndef SIMGRID_MC_ODPOR_EXECUTION_HPP +#define SIMGRID_MC_ODPOR_EXECUTION_HPP + +#include "src/mc/api/ClockVector.hpp" +#include "src/mc/transition/Transition.hpp" + +#include +#include + +namespace simgrid::mc::odpor { + +/** + * @brief An ordered sequence of actions + */ +class ExecutionSequence : public std::list {}; +using Hypothetical = ExecutionSequence; + +/** + * @brief The occurrence of a transition in an execution + */ +class Event { + std::pair contents_; + +public: + Event() = default; + Event(Event&&) = default; + Event(const Event&) = default; + Event& operator=(const Event&) = default; + Event& operator=(const Event&&) = default; + + explicit Event(std::pair pair) : contents_(std::move(pair)) {} + + const Transition* get_transition() const { return contents_.get<0>(); } + const ClockVector& get_clock_vector() const { return contents_.get<1>(); } +} + +/** + * @brief An ordered sequence of transitions which describe + * the evolution of a process undergoing model checking + * + * Executions are conceived based on the following papers: + * 1. "Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction" + * by Abdulla et al. + * + * In addition to representing an actual steps taken, + * an execution keeps track of the "happens-before" + * relation among the transitions in the execution + * by following the procedure outlined in the + * original DPOR paper with clock vectors + * + * @note: For more nuanced happens-before relations, clock + * vectors may not always suffice. Clock vectors work + * well with transition-based dependencies like that used in + * SimGrid; but to have a more refined independence relation, + * an event-based dependency approach is needed. See the section 2 + * in the ODPOR paper [1] concerning event-based dependencies and + * how the happens-before relation can be refined in a + * computation model much like that of SimGrid. In fact, the same issue + * arrises with UDPOR with context-sensitive dependencies: + * the two concepts are analogous if not identical + */ +class Execution { +private: + /** + * @brief The actual steps that are taken by the process + * during exploration. + */ + std::list contents_; + +public: + Execution() = default; + Execution(const Execution&) = default; + Execution& operator=(Execution const&) = default; + Execution(Execution&&) = default; + explicit Execution(ExecutionSequence&& seq); + explicit Execution(const ExecutionSequence& seq); + + std::unordered_set get_initials_after(const Hypothetical& w) const; + std::unordered_set get_weak_initials_after(const Hypothetical& w) const; + + bool is_initial(aid_t p, const Hypothetical& w) const; + bool is_weak_initial(aid_t p, const Hypothetical& w) const; + + void take_action(const Transition*); +}; + +} // namespace simgrid::mc::odpor +#endif diff --git a/src/mc/explo/sdpor/Initials.cpp b/src/mc/explo/sdpor/Initials.cpp new file mode 100644 index 0000000000..e69de29bb2 diff --git a/src/mc/explo/sdpor/Initials.hpp b/src/mc/explo/sdpor/Initials.hpp new file mode 100644 index 0000000000..e69de29bb2 diff --git a/src/mc/explo/sdpor/WeakInitials.cpp b/src/mc/explo/sdpor/WeakInitials.cpp new file mode 100644 index 0000000000..e69de29bb2 diff --git a/src/mc/explo/sdpor/WeakInitials.hpp b/src/mc/explo/sdpor/WeakInitials.hpp new file mode 100644 index 0000000000..e69de29bb2 -- 2.20.1