From 2bdd4ab1f667695dbf8aeedfe7d3d940991146cd Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Thu, 7 Apr 2016 10:58:44 +0200 Subject: [PATCH 1/1] [mc] Simplify/unify the interleeaving/exploration logic * MC_RANDOM was using a different mechanism from its friends in order to keep track of which transition was already executed; * document the different fields; * add methods. --- src/mc/CommunicationDeterminismChecker.cpp | 4 +- src/mc/LivenessChecker.cpp | 2 +- src/mc/SafetyChecker.cpp | 8 ++-- src/mc/mc_state.cpp | 47 +++++------------- src/mc/mc_state.h | 55 +++++++++++++++------- 5 files changed, 58 insertions(+), 58 deletions(-) diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index ea3ab38e09..3c0cd08bf2 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -360,7 +360,7 @@ void CommunicationDeterminismChecker::prepare() /* Get an enabled process and insert it in the interleave set of the initial state */ for (auto& p : mc_model_checker->process().simix_processes()) if (simgrid::mc::process_is_enabled(&p.copy)) - MC_state_interleave_process(initial_state.get(), &p.copy); + initial_state->interleave(&p.copy); stack_.push_back(std::move(initial_state)); } @@ -445,7 +445,7 @@ int CommunicationDeterminismChecker::main(void) /* Get enabled processes and insert them in the interleave set of the next state */ for (auto& p : mc_model_checker->process().simix_processes()) if (simgrid::mc::process_is_enabled(&p.copy)) - MC_state_interleave_process(next_state.get(), &p.copy); + next_state->interleave(&p.copy); if (dot_output != nullptr) fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index be0149b7f4..8dcb3b92eb 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -446,7 +446,7 @@ std::shared_ptr LivenessChecker::newPair(Pair* current_pair, xbt_automaton /* Get enabled processes and insert them in the interleave set of the next graph_state */ for (auto& p : mc_model_checker->process().simix_processes()) if (simgrid::mc::process_is_enabled(&p.copy)) - MC_state_interleave_process(next_pair->graph_state.get(), &p.copy); + next_pair->graph_state->interleave(&p.copy); next_pair->requests = next_pair->graph_state->interleaveSize(); /* FIXME : get search_cycle value for each acceptant state */ if (next_pair->automaton_state->type == 1 || diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index e7c62e8a3f..62a4f5c177 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -156,7 +156,7 @@ int SafetyChecker::run() /* Get an enabled process and insert it in the interleave set of the next state */ for (auto& p : mc_model_checker->process().simix_processes()) if (simgrid::mc::process_is_enabled(&p.copy)) { - MC_state_interleave_process(next_state.get(), &p.copy); + next_state->interleave(&p.copy); if (reductionMode_ != simgrid::mc::ReductionMode::none) break; } @@ -238,8 +238,8 @@ int SafetyChecker::backtrack() state->num); } - if (!prev_state->processStates[issuer->pid].done()) - MC_state_interleave_process(prev_state, issuer); + if (!prev_state->processStates[issuer->pid].isDone()) + prev_state->interleave(issuer); else XBT_DEBUG("Process %p is in done set", req->issuer); @@ -309,7 +309,7 @@ void SafetyChecker::init() /* Get an enabled process and insert it in the interleave set of the initial state */ for (auto& p : mc_model_checker->process().simix_processes()) if (simgrid::mc::process_is_enabled(&p.copy)) { - MC_state_interleave_process(initial_state.get(), &p.copy); + initial_state->interleave(&p.copy); if (reductionMode_ != simgrid::mc::ReductionMode::none) break; } diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index d6123a3e9f..1a88fb1abb 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -56,19 +56,12 @@ State::State() std::size_t State::interleaveSize() const { return std::count_if(this->processStates.begin(), this->processStates.end(), - [](simgrid::mc::ProcessState const& state) { return state.interleave(); }); + [](simgrid::mc::ProcessState const& state) { return state.isToInterleave(); }); } } } -void MC_state_interleave_process(simgrid::mc::State* state, smx_process_t process) -{ - assert(state); - state->processStates[process->pid].state = simgrid::mc::ProcessInterleaveState::interleave; - state->processStates[process->pid].interleave_count = 0; -} - smx_simcall_t MC_state_get_executed_request(simgrid::mc::State* state, int *value) { *value = state->req_num; @@ -85,7 +78,7 @@ static inline smx_simcall_t MC_state_get_request_for_process( { simgrid::mc::ProcessState* procstate = &state->processStates[process->pid]; - if (!procstate->interleave()) + if (!procstate->isToInterleave()) return nullptr; if (!simgrid::mc::process_is_enabled(process)) return nullptr; @@ -107,7 +100,7 @@ static inline smx_simcall_t MC_state_get_request_for_process( if (procstate->interleave_count >= simgrid::mc::read_length(mc_model_checker->process(), simgrid::mc::remote(simcall_comm_waitany__get__comms(&process->simcall)))) - procstate->state = simgrid::mc::ProcessInterleaveState::done; + procstate->setDone(); if (*value != -1) req = &process->simcall; break; @@ -127,7 +120,7 @@ static inline smx_simcall_t MC_state_get_request_for_process( if (procstate->interleave_count >= read_length(mc_model_checker->process(), remote(simcall_comm_testany__get__comms(&process->simcall)))) - procstate->state = simgrid::mc::ProcessInterleaveState::done; + procstate->setDone(); if (*value != -1 || start_count == 0) req = &process->simcall; @@ -147,22 +140,23 @@ static inline smx_simcall_t MC_state_get_request_for_process( *value = 0; else *value = -1; - procstate->state = simgrid::mc::ProcessInterleaveState::done; + procstate->setDone(); req = &process->simcall; break; } - case SIMCALL_MC_RANDOM: - if (procstate->state == simgrid::mc::ProcessInterleaveState::interleave) - *value = simcall_mc_random__get__min(&process->simcall); - else if (state->req_num < simcall_mc_random__get__max(&process->simcall)) - *value = state->req_num + 1; - procstate->state = simgrid::mc::ProcessInterleaveState::done; + case SIMCALL_MC_RANDOM: { + int min_value = simcall_mc_random__get__min(&process->simcall); + *value = procstate->interleave_count + min_value; + procstate->interleave_count++; + if (*value == simcall_mc_random__get__max(&process->simcall)) + procstate->setDone(); req = &process->simcall; break; + } default: - procstate->state = simgrid::mc::ProcessInterleaveState::done; + procstate->setDone(); *value = 0; req = &process->simcall; break; @@ -224,21 +218,6 @@ static inline smx_simcall_t MC_state_get_request_for_process( simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm); break; - case SIMCALL_MC_RANDOM: { - state->internal_req = *req; - int random_max = simcall_mc_random__get__max(req); - if (*value != random_max) - for (auto& p : mc_model_checker->process().simix_processes()) { - simgrid::mc::ProcessState* procstate = &state->processStates[p.copy.pid]; - const smx_process_t issuer = MC_smx_simcall_get_issuer(req); - if (p.copy.pid == issuer->pid) { - procstate->state = simgrid::mc::ProcessInterleaveState::more_interleave; - break; - } - } - break; - } - default: state->internal_req = *req; break; diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h index 032a6e5b4d..fa5ddb98d7 100644 --- a/src/mc/mc_state.h +++ b/src/mc/mc_state.h @@ -59,28 +59,46 @@ 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 */ -struct ProcessState { +class ProcessState { + /* Possible exploration status of a process in a state */ + enum class InterleavingType { + /** We do not have to execute this process transitions */ + disabled = 0, + /** We still have to execute (some of) this process transitions */ + interleave, + /** We have already executed this process transitions */ + done, + }; + /** Exploration control information */ - ProcessInterleaveState state = ProcessInterleaveState::no_interleave; + InterleavingType state = InterleavingType::disabled; +public: + /** Number of times that the process was interleaved */ - unsigned int interleave_count; + // TODO, make this private + unsigned int interleave_count = 0; - bool done() const + bool isDisabled() const { - return this->state == ProcessInterleaveState::done; + 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 isToInterleave() const + { + return this->state == InterleavingType::interleave; + } + void interleave() + { + this->state = InterleavingType::interleave; + this->interleave_count = 0; + } + void setDone() + { + this->state = InterleavingType::done; } }; @@ -134,6 +152,10 @@ struct XBT_PRIVATE State { State(); std::size_t interleaveSize() const; + void interleave(smx_process_t process) + { + this->processStates[process->pid].interleave(); + } }; XBT_PRIVATE void replay(std::list> const& stack); @@ -142,7 +164,6 @@ XBT_PRIVATE void replay(std::list> const& st } 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 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); -- 2.20.1