X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/fe304706848f0a64477d4687b3ea97d5b9a0c35c..7f0516d66943c1fa8f64946cf159eb37bc7ef41f:/src/mc/mc_state.hpp diff --git a/src/mc/mc_state.hpp b/src/mc/mc_state.hpp index a7a0fb3c7a..858f00bfe1 100644 --- a/src/mc/mc_state.hpp +++ b/src/mc/mc_state.hpp @@ -1,4 +1,4 @@ -/* Copyright (c) 2007-2019. The SimGrid Team. All rights reserved. */ +/* Copyright (c) 2007-2022. 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. */ @@ -6,131 +6,61 @@ #ifndef SIMGRID_MC_STATE_HPP #define SIMGRID_MC_STATE_HPP -#include "src/mc/sosp/mc_snapshot.hpp" -#include "src/kernel/activity/CommImpl.hpp" #include "src/mc/Transition.hpp" +#include "src/mc/sosp/Snapshot.hpp" +#include "src/mc/mc_comm_pattern.hpp" namespace simgrid { namespace mc { -enum class PatternCommunicationType { - none = 0, - send = 1, - receive = 2, -}; - -class PatternCommunication { -public: - int num = 0; - simgrid::kernel::activity::CommImpl* comm_addr; - PatternCommunicationType type = PatternCommunicationType::send; - unsigned long src_proc = 0; - unsigned long dst_proc = 0; - const char* src_host = nullptr; - const char* dst_host = nullptr; - std::string rdv; - std::vector data; - int tag = 0; - int index = 0; - - PatternCommunication() { std::memset(&comm_addr, 0, sizeof(comm_addr)); } - - PatternCommunication dup() const - { - simgrid::mc::PatternCommunication res; - // num? - res.comm_addr = this->comm_addr; - res.type = this->type; - // src_proc? - // dst_proc? - res.dst_proc = this->dst_proc; - res.dst_host = this->dst_host; - res.rdv = this->rdv; - res.data = this->data; - // tag? - res.index = this->index; - return res; - } -}; +/* A node in the exploration graph (kind-of) */ +class XBT_PRIVATE State { + static long expended_states_; /* Count total amount of states, for stats */ -/* On every state, each process has an entry of the following type. - * This represents both the process and its transition because - * a process cannot have more than one enabled transition at a given time. - */ -class ProcessState { - /* Possible exploration status of a process transition in a state. - * Either the checker did not consider the transition, or it was considered and to do, or considered and done. - */ - enum class InterleavingType { - /** This process transition is not considered by the checker (yet?) */ - disabled = 0, - /** The checker algorithm decided that this process transitions should be done at some point */ - todo, - /** The checker algorithm decided that this should be done, but it was done in the meanwhile */ - done, - }; - - /** Exploration control information */ - InterleavingType state = InterleavingType::disabled; + /* Outgoing transition: what was the last transition that we took to leave this state? Useful for replay */ + Transition transition_; public: - /** Number of times that the process was considered to be executed */ - // TODO, make this private - unsigned int times_considered = 0; - - bool isDisabled() const { return this->state == InterleavingType::disabled; } - bool isDone() const { return this->state == InterleavingType::done; } - bool isTodo() const { return this->state == InterleavingType::todo; } - /** Mark that we should try executing this process at some point in the future of the checker algorithm */ - void consider() - { - this->state = InterleavingType::todo; - this->times_considered = 0; - } - void setDone() { this->state = InterleavingType::done; } -}; + explicit State(); -/* A node in the exploration graph (kind-of) - */ -class XBT_PRIVATE State { -public: /** Sequential state number (used for debugging) */ - int num = 0; + long num_ = 0; /** State's exploration status by process */ - std::vector actorStates; - - Transition transition; + std::vector actor_states_; /** The simcall which was executed, going out of that state */ - s_smx_simcall executed_req; - - /* Internal translation of the executed_req simcall - * - * SIMCALL_COMM_TESTANY is translated to a SIMCALL_COMM_TEST - * and SIMCALL_COMM_WAITANY to a SIMCALL_COMM_WAIT. - */ - s_smx_simcall internal_req; + s_smx_simcall executed_req_; - /* Can be used as a copy of the remote synchro object */ - simgrid::mc::Remote internal_comm; + /** Observer of the transition leading to that sate */ + RemotePtr remote_observer_; /** Snapshot of system state (if needed) */ - std::shared_ptr system_state; + std::shared_ptr system_state_; // For CommunicationDeterminismChecker - std::vector> incomplete_comm_pattern; - std::vector communicationIndices; + std::vector> incomplete_comm_pattern_; + std::vector communication_indices_; + + + /* Returns a positive number if there is another transition to pick, or -1 if not */ + int next_transition() const; - explicit State(unsigned long state_number); + /* Explore a new path */ + RemotePtr execute_next(int next); - std::size_t interleaveSize() const; - void addInterleavingSet(smx_actor_t actor) { this->actorStates[actor->get_pid()].consider(); } - Transition getTransition() const; + std::size_t count_todo() const; + void mark_todo(aid_t actor) { this->actor_states_[actor].mark_todo(); } + Transition* get_transition() const; + + /* Returns the total amount of states created so far (for statistics) */ + static long get_expanded_states() { return expended_states_; } + +private: + void copy_incomplete_comm_pattern(); + void copy_index_comm_pattern(); }; } } -XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state); - #endif