From c6b1e0d38db0abceafffdc80987bd3d7f92c12c2 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Wed, 25 Jan 2017 15:14:06 +0100 Subject: [PATCH 1/1] MC: comment, rename stuff, don't change anything profund --- src/mc/checker/SafetyChecker.cpp | 8 ++-- src/mc/mc_state.cpp | 70 ++++++++++++++++---------------- src/mc/mc_state.h | 46 ++++++++++----------- 3 files changed, 62 insertions(+), 62 deletions(-) diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index 21855771d7..600e5e236c 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -147,10 +147,10 @@ void SafetyChecker::run() mc_model_checker->executed_transitions++; - /* Actually answer the request: let the remote process do execute that request */ + /* Actually answer the request: let execute the selected request (MCed does one step) */ this->getSession().execute(state->transition); - /* Create the new expanded state */ + /* Create the new expanded state (copy the state of MCed into our MCer data) */ std::unique_ptr next_state = std::unique_ptr(new simgrid::mc::State(++expandedStatesCount_)); @@ -211,8 +211,8 @@ void SafetyChecker::backtrack() if (reductionMode_ == simgrid::mc::ReductionMode::dpor) { smx_simcall_t req = &state->internal_req; if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK) - xbt_die("Mutex is currently not supported with DPOR, " - "use --cfg=model-check/reduction:none"); + xbt_die("Mutex is currently not supported with DPOR, use --cfg=model-check/reduction:none"); + const smx_actor_t issuer = MC_smx_simcall_get_issuer(req); for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) { simgrid::mc::State* prev_state = i->get(); diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index e85574f899..47f86822a3 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -47,7 +47,7 @@ State::State(unsigned long state_number) std::size_t State::interleaveSize() const { return boost::range::count_if(this->processStates, - [](simgrid::mc::ProcessState const& p) { return p.isToInterleave(); }); + [](simgrid::mc::ProcessState const& p) { return p.isTodo(); }); } Transition State::getTransition() const @@ -63,7 +63,7 @@ Transition State::getTransition() const * This can be seen as an iterator returning the next transition of the process. * * We only consider the processes that are both - * - marked "to be interleaved" in their ProcessState (controled by the checker algo). + * - marked "to be interleaved" in their ProcessState (controlled by the checker algorithm). * - which simcall can currently be executed (like a comm where the other partner is already known) * Once we returned the last enabled transition of a process, it is marked done. * @@ -72,65 +72,65 @@ Transition State::getTransition() const * field to remember what was the last returned sub-transition. */ static inline smx_simcall_t MC_state_get_request_for_process( - simgrid::mc::State* state, smx_actor_t process) + simgrid::mc::State* state, smx_actor_t actor) { /* reset the outgoing transition */ - simgrid::mc::ProcessState* procstate = &state->processStates[process->pid]; + simgrid::mc::ProcessState* procstate = &state->processStates[actor->pid]; state->transition.pid = -1; state->transition.argument = -1; state->executed_req.call = SIMCALL_NONE; - if (!procstate->isToInterleave()) - return nullptr; - if (!simgrid::mc::actor_is_enabled(process)) - return nullptr; + if (!procstate->isTodo()) + return nullptr; // Not considered by the checker algorithm + if (!simgrid::mc::actor_is_enabled(actor)) + return nullptr; // Not executable in the application smx_simcall_t req = nullptr; - switch (process->simcall.call) { + switch (actor->simcall.call) { case SIMCALL_COMM_WAITANY: state->transition.argument = -1; - while (procstate->interleave_count < + while (procstate->times_considered < read_length(mc_model_checker->process(), - remote(simcall_comm_waitany__get__comms(&process->simcall)))) { - if (simgrid::mc::request_is_enabled_by_idx(&process->simcall, - procstate->interleave_count++)) { - state->transition.argument = procstate->interleave_count - 1; + remote(simcall_comm_waitany__get__comms(&actor->simcall)))) { + if (simgrid::mc::request_is_enabled_by_idx(&actor->simcall, + procstate->times_considered++)) { + state->transition.argument = procstate->times_considered - 1; break; } } - if (procstate->interleave_count >= + if (procstate->times_considered >= simgrid::mc::read_length(mc_model_checker->process(), - simgrid::mc::remote(simcall_comm_waitany__get__comms(&process->simcall)))) + simgrid::mc::remote(simcall_comm_waitany__get__comms(&actor->simcall)))) procstate->setDone(); if (state->transition.argument != -1) - req = &process->simcall; + req = &actor->simcall; break; case SIMCALL_COMM_TESTANY: { - unsigned start_count = procstate->interleave_count; + unsigned start_count = procstate->times_considered; state->transition.argument = -1; - while (procstate->interleave_count < - simcall_comm_testany__get__count(&process->simcall)) - if (simgrid::mc::request_is_enabled_by_idx(&process->simcall, - procstate->interleave_count++)) { - state->transition.argument = procstate->interleave_count - 1; + while (procstate->times_considered < + simcall_comm_testany__get__count(&actor->simcall)) + if (simgrid::mc::request_is_enabled_by_idx(&actor->simcall, + procstate->times_considered++)) { + state->transition.argument = procstate->times_considered - 1; break; } - if (procstate->interleave_count >= - simcall_comm_testany__get__count(&process->simcall)) + if (procstate->times_considered >= + simcall_comm_testany__get__count(&actor->simcall)) procstate->setDone(); if (state->transition.argument != -1 || start_count == 0) - req = &process->simcall; + req = &actor->simcall; break; } case SIMCALL_COMM_WAIT: { simgrid::mc::RemotePtr remote_act = remote( - static_cast(simcall_comm_wait__get__comm(&process->simcall))); + static_cast(simcall_comm_wait__get__comm(&actor->simcall))); simgrid::mc::Remote temp_act; mc_model_checker->process().read(temp_act, remote_act); simgrid::kernel::activity::Comm* act = temp_act.getBuffer(); @@ -142,30 +142,30 @@ static inline smx_simcall_t MC_state_get_request_for_process( else state->transition.argument = -1; procstate->setDone(); - req = &process->simcall; + req = &actor->simcall; break; } case SIMCALL_MC_RANDOM: { - int min_value = simcall_mc_random__get__min(&process->simcall); - state->transition.argument = procstate->interleave_count + min_value; - procstate->interleave_count++; - if (state->transition.argument == simcall_mc_random__get__max(&process->simcall)) + int min_value = simcall_mc_random__get__min(&actor->simcall); + state->transition.argument = procstate->times_considered + min_value; + procstate->times_considered++; + if (state->transition.argument == simcall_mc_random__get__max(&actor->simcall)) procstate->setDone(); - req = &process->simcall; + req = &actor->simcall; break; } default: procstate->setDone(); state->transition.argument = 0; - req = &process->simcall; + req = &actor->simcall; break; } if (!req) return nullptr; - state->transition.pid = process->pid; + state->transition.pid = actor->pid; state->executed_req = *req; // Fetch the data of the request and translate it: state->internal_req = *req; diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h index 9ee934f4a1..a2bd0ed170 100644 --- a/src/mc/mc_state.h +++ b/src/mc/mc_state.h @@ -70,45 +70,45 @@ struct PatternCommunication { }; -/* On every state, each process has an entry of the following type */ +/* 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 in a state */ + /* 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 { - /** We do not have to execute this process transitions */ + /** This process transition is not considered by the checker (yet?) */ disabled = 0, - /** We still have to execute (some of) this process transitions */ - interleave, - /** We have already executed this process transitions */ + /** 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; public: - - /** Number of times that the process was interleaved */ + /** Number of times that the process was considered to be executed */ // TODO, make this private - unsigned int interleave_count = 0; + unsigned int times_considered = 0; - bool isDisabled() const - { + bool isDisabled() const { return this->state == InterleavingType::disabled; } - bool isDone() const - { + bool isDone() const { return this->state == InterleavingType::done; } - bool isToInterleave() const - { - return this->state == InterleavingType::interleave; + bool isTodo() const { + return this->state == InterleavingType::todo; } - void interleave() - { - this->state = InterleavingType::interleave; - this->interleave_count = 0; + /** 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() - { + void setDone() { this->state = InterleavingType::done; } }; @@ -149,7 +149,7 @@ struct XBT_PRIVATE State { std::size_t interleaveSize() const; void interleave(smx_actor_t process) { - this->processStates[process->pid].interleave(); + this->processStates[process->pid].consider(); } Transition getTransition() const; }; -- 2.20.1