From: Maxwell Pirtle Date: Tue, 2 May 2023 06:58:21 +0000 (+0200) Subject: Add Execution concept without ExecutionViews X-Git-Tag: v3.34~68^2~61 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/a05b37852a57f94f75cbd4da7dc9e75a88a69f35 Add Execution concept without ExecutionViews The Execution is the key concept in ODPOR and SDPOR for generating new traces. Executions for the basis off of which new search paths are created --- diff --git a/MANIFEST.in b/MANIFEST.in index 74943c16d7..5bcbb3499d 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -2189,6 +2189,8 @@ include src/mc/explo/Exploration.cpp include src/mc/explo/Exploration.hpp include src/mc/explo/LivenessChecker.cpp include src/mc/explo/LivenessChecker.hpp +include src/mc/explo/odpor/Execution.cpp +include src/mc/explo/odpor/Execution.hpp include src/mc/explo/UdporChecker.cpp include src/mc/explo/UdporChecker.hpp include src/mc/explo/simgrid_mc.cpp diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp new file mode 100644 index 0000000000..e69de29bb2 diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp index 62af981943..3b8ebca348 100644 --- a/src/mc/explo/odpor/Execution.hpp +++ b/src/mc/explo/odpor/Execution.hpp @@ -9,16 +9,15 @@ #include "src/mc/api/ClockVector.hpp" #include "src/mc/transition/Transition.hpp" +#include #include #include namespace simgrid::mc::odpor { -/** - * @brief An ordered sequence of actions - */ -class ExecutionSequence : public std::list {}; -using Hypothetical = ExecutionSequence; +using ProcessSequence = std::list; +using ExecutionSequence = std::list; +using Hypothetical = ExecutionSequence; /** * @brief The occurrence of a transition in an execution @@ -43,6 +42,13 @@ public: * @brief An ordered sequence of transitions which describe * the evolution of a process undergoing model checking * + * An execution conceptually is just a string of actors + * ids (e.g. "1.2.3.1.2.2.1.1"), where the `i`th occurrence + * of actor id `j` corresponds to the `i`th action executed + * by the actor with id `j` (viz. the `i`th step of actor `j`). + * Executions can stand alone on their own or can extend + * the execution of other sequences + * * Executions are conceived based on the following papers: * 1. "Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction" * by Abdulla et al. @@ -65,20 +71,16 @@ public: * 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: + using Handle = decltype(contents_)::const_iterator; + Execution() = default; Execution(const Execution&) = default; Execution& operator=(Execution const&) = default; Execution(Execution&&) = default; - explicit Execution(ExecutionSequence&& seq); - explicit Execution(const ExecutionSequence& seq); + + Execution(ExecutionSequence&& seq, std::optional base = {}); + Execution(const ExecutionSequence& seq, std::optional base = {}); std::unordered_set get_initials_after(const Hypothetical& w) const; std::unordered_set get_weak_initials_after(const Hypothetical& w) const; @@ -86,7 +88,43 @@ public: 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*); + /** + * @brief Removes the last event of the execution, + * if such an event exists + * + * @note: When you remove events from an execution, any views + * of the execution referring to those removed events + * become invalidated + */ + void pop_latest(); + + /** + * @brief Extends the execution by one more step + * + * Intutively, pushing a transition `t` onto execution `E` + * is equivalent to making the execution become (using the + * notation of [1]) `E.proc(t)` where `proc(t)` is the + * actor which executed transition `t`. + */ + void push_transition(const Transition*); + + size_t size() const { return this->contents_.size(); } + size_t size() const { return this->contents_.size(); } + +private: + /** + * @brief A pointer into the execution off of which this + * execution extends computation + * + * Conceptually, the `prior` + */ + std::optional prior; + + /** + * @brief The actual steps that are taken by the process + * during exploration, relative to the + */ + std::list contents_; }; } // namespace simgrid::mc::odpor diff --git a/src/mc/explo/odpor/odpor_forward.hpp b/src/mc/explo/odpor/odpor_forward.hpp new file mode 100644 index 0000000000..65810615b9 --- /dev/null +++ b/src/mc/explo/odpor/odpor_forward.hpp @@ -0,0 +1,27 @@ +/* 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. */ + +/** @file odpor_forward.hpp + * + * Forward definitions for MC types specific to ODPOR + */ + +#ifndef SIMGRID_MC_ODPOR_FORWARD_HPP +#define SIMGRID_MC_ODPOR_FORWARD_HPP + +#include "src/mc/mc_forward.hpp" +#include + +namespace simgrid::mc::odpor { + +class Event; +class Execution; +class ExecutionSequence; +class ExecutionView; +class WakeupTree; + +} // namespace simgrid::mc::odpor + +#endif diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index d1a6d6738c..1eae1244ca 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -565,6 +565,9 @@ set(MC_SRC_STATEFUL src/mc/explo/LivenessChecker.hpp src/mc/explo/UdporChecker.cpp src/mc/explo/UdporChecker.hpp + + src/mc/explo/odpor/Execution.cpp + src/mc/explo/odpor/Execution.hpp src/mc/explo/udpor/Comb.hpp src/mc/explo/udpor/Configuration.hpp