X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/ab8e2fe95944fb998edd6e95d1022a05175c4f92..c6b1e0d38db0abceafffdc80987bd3d7f92c12c2:/src/mc/mc_state.h diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h index 3fb62da892..a2bd0ed170 100644 --- a/src/mc/mc_state.h +++ b/src/mc/mc_state.h @@ -15,17 +15,28 @@ #include #include "src/simix/smx_private.h" +#include "src/kernel/activity/SynchroIo.hpp" +#include "src/kernel/activity/SynchroComm.hpp" +#include "src/kernel/activity/SynchroRaw.hpp" +#include "src/kernel/activity/SynchroSleep.hpp" +#include "src/kernel/activity/SynchroExec.hpp" #include "src/mc/mc_snapshot.h" +#include "src/mc/mc_record.h" +#include "src/mc/Transition.hpp" namespace simgrid { namespace mc { -extern XBT_PRIVATE std::unique_ptr initial_global_state; +enum class PatternCommunicationType { + none = 0, + send = 1, + receive = 2, +}; struct PatternCommunication { int num = 0; - smx_synchro_t comm_addr; - e_smx_comm_type_t type = SIMIX_COMM_SEND; + smx_activity_t comm_addr; + PatternCommunicationType type = PatternCommunicationType::send; unsigned long src_proc = 0; unsigned long dst_proc = 0; const char *src_host = nullptr; @@ -59,70 +70,93 @@ struct PatternCommunication { }; -/* Possible exploration status of a process in a state */ -enum class ProcessInterleaveState { - no_interleave=0, /* Do not interleave (do not execute) */ - interleave, /* Interleave the process (one or more request) */ - more_interleave, /* Interleave twice the process (for mc_random simcall) */ - done /* Already interleaved */ -}; +/* 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, + }; -/* On every state, each process has an entry of the following type */ -struct ProcessState { /** Exploration control information */ - ProcessInterleaveState state = ProcessInterleaveState::no_interleave; - /** Number of times that the process was interleaved */ - unsigned int interleave_count; - - bool done() const - { - return this->state == ProcessInterleaveState::done; + InterleavingType state = InterleavingType::disabled; +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 interleave() const { - return this->state == ProcessInterleaveState::interleave - || this->state == ProcessInterleaveState::more_interleave; + 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; } }; -/* An exploration state. - * - * The `executed_state` is sometimes transformed into another `internal_req`. - * For example WAITANY is transformes into a WAIT and TESTANY into TEST. - * See `MC_state_set_executed_request()`. +/* A node in the exploration graph (kind-of) */ struct XBT_PRIVATE State { + + /** Sequential state number (used for debugging) */ + int num = 0; + /** State's exploration status by process */ std::vector processStates; - s_smx_synchro_t internal_comm; /* To be referenced by the internal_req */ - s_smx_simcall_t internal_req; /* Internal translation of request */ - s_smx_simcall_t executed_req; /* The executed request of the state */ - int req_num = 0; /* The request number (in the case of a - multi-request like waitany ) */ - std::shared_ptr system_state = nullptr; /* Snapshot of system state */ - int num = 0; - int in_visited_states = 0; - // comm determinism verification (xbt_dynar_t): - std::vector> incomplete_comm_pattern; + Transition transition; + + /** The simcall which was executed, going out of that state */ + s_smx_simcall_t 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_t internal_req; - // For communication determinism verification: + /* Can be used as a copy of the remote synchro object */ + simgrid::mc::Remote internal_comm; + + /** Snapshot of system state (if needed) */ + std::shared_ptr system_state; + + // For CommunicationDeterminismChecker + std::vector> incomplete_comm_pattern; std::vector communicationIndices; - State(); + State(unsigned long state_number); std::size_t interleaveSize() const; + void interleave(smx_actor_t process) { + this->processStates[process->pid].consider(); + } + Transition getTransition() const; }; -XBT_PRIVATE void replay(std::list> const& stack); - } } -XBT_PRIVATE simgrid::mc::State* MC_state_new(void); -XBT_PRIVATE void MC_state_interleave_process(simgrid::mc::State* state, smx_process_t process); -XBT_PRIVATE void MC_state_set_executed_request(simgrid::mc::State* state, smx_simcall_t req, int value); -XBT_PRIVATE smx_simcall_t MC_state_get_executed_request(simgrid::mc::State* state, int *value); -XBT_PRIVATE smx_simcall_t MC_state_get_internal_request(simgrid::mc::State* state); -XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value); +XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state); #endif