From: Gabriel Corona Date: Tue, 5 Apr 2016 10:20:17 +0000 (+0200) Subject: [mc] C++ification of State X-Git-Tag: v3_13~173 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/11ce6b59ec29ed55d422a0c97a7d734ac1eb7a39 [mc] C++ification of State --- diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index a817ff97a1..23c1d538eb 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -408,9 +408,9 @@ int CommunicationDeterminismChecker::main(void) simgrid::mc::State* state = stack_.back().get(); XBT_DEBUG("**************************************************"); - XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %d)", + XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)", stack_.size(), state->num, - MC_state_interleave_size(state)); + state->interleaveSize()); /* Update statistics */ mc_stats->visited_states++; @@ -505,7 +505,7 @@ int CommunicationDeterminismChecker::main(void) while (!stack_.empty()) { std::unique_ptr state = std::move(stack_.back()); stack_.pop_back(); - if (MC_state_interleave_size(state.get()) + if (state->interleaveSize() && stack_.size() < (std::size_t) _sg_mc_max_depth) { /* We found a back-tracking point, let's loop */ XBT_DEBUG("Back-tracking to state %d at depth %zi", diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index e41d3f54fd..086d12252a 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -345,9 +345,10 @@ int LivenessChecker::main(void) /* Update current state in buchi automaton */ simgrid::mc::property_automaton->current_state = current_pair->automaton_state; - XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size = %d, pair_num = %d, requests = %d)", + XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size = %zd, pair_num = %d, requests = %d)", current_pair->depth, current_pair->search_cycle, - MC_state_interleave_size(current_pair->graph_state.get()), current_pair->num, + current_pair->graph_state->interleaveSize(), + current_pair->num, current_pair->requests); if (current_pair->requests == 0) { @@ -448,7 +449,7 @@ std::shared_ptr LivenessChecker::newPair(Pair* current_pair, xbt_automaton 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->requests = MC_state_interleave_size(next_pair->graph_state.get()); + next_pair->requests = next_pair->graph_state->interleaveSize(); /* FIXME : get search_cycle value for each acceptant state */ if (next_pair->automaton_state->type == 1 || (current_pair && current_pair->search_cycle)) diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index b1929fc3fc..0f20188764 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -104,9 +104,9 @@ int SafetyChecker::run() XBT_DEBUG("**************************************************"); XBT_DEBUG( - "Exploration depth=%zi (state=%p, num %d)(%u interleave)", + "Exploration depth=%zi (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num, - MC_state_interleave_size(state)); + state->interleaveSize()); mc_stats->visited_states++; @@ -241,7 +241,7 @@ int SafetyChecker::backtrack() xbt_free(req_str); } - if (!MC_state_process_is_done(prev_state, issuer)) + if (!prev_state->processStates[issuer->pid].done()) MC_state_interleave_process(prev_state, issuer); else XBT_DEBUG("Process %p is in done set", req->issuer); @@ -266,7 +266,7 @@ int SafetyChecker::backtrack() } } - if (MC_state_interleave_size(state.get()) + if (state->interleaveSize() && stack_.size() < (std::size_t) _sg_mc_max_depth) { /* We found a back-tracking point, let's loop */ XBT_DEBUG("Back-tracking to state %d at depth %zi", diff --git a/src/mc/mc_comm_pattern.cpp b/src/mc/mc_comm_pattern.cpp index 35540c66e3..4dc30b9b43 100644 --- a/src/mc/mc_comm_pattern.cpp +++ b/src/mc/mc_comm_pattern.cpp @@ -76,7 +76,7 @@ void MC_restore_communications_pattern(simgrid::mc::State* state) unsigned int cursor; xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm) - list_process_comm->index_comm = (int)xbt_dynar_get_as(state->index_comm, cursor, int); + list_process_comm->index_comm = state->communicationIndices[cursor]; for (unsigned i = 0; i < MC_smx_get_maxpid(); i++) MC_patterns_copy( @@ -98,11 +98,11 @@ void MC_state_copy_incomplete_communications_pattern(simgrid::mc::State* state) void MC_state_copy_index_communications_pattern(simgrid::mc::State* state) { - state->index_comm = xbt_dynar_new(sizeof(unsigned int), nullptr); + state->communicationIndices.clear(); mc_list_comm_pattern_t list_process_comm; unsigned int cursor; xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm) - xbt_dynar_push_as(state->index_comm, unsigned int, list_process_comm->index_comm); + state->communicationIndices.push_back(list_process_comm->index_comm); } void MC_handle_comm_pattern( diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index 3ed4e6ceb1..2012bcd113 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -6,6 +6,8 @@ #include +#include + #include #include @@ -31,9 +33,7 @@ simgrid::mc::State* MC_state_new() std::memset(&state->internal_comm, 0, sizeof(state->internal_comm)); std::memset(&state->internal_req, 0, sizeof(state->internal_req)); std::memset(&state->executed_req, 0, sizeof(state->executed_req)); - - state->max_pid = MC_smx_get_maxpid(); - state->proc_status = xbt_new0(s_mc_procstate_t, state->max_pid); + state->processStates.resize(MC_smx_get_maxpid()); state->num = ++mc_stats->expanded_states; /* Stateful model checking */ if((_sg_mc_checkpoint > 0 && (mc_stats->expanded_states % _sg_mc_checkpoint == 0)) || _sg_mc_termination){ @@ -58,9 +58,13 @@ State::State() State::~State() { - xbt_free(this->index_comm); xbt_free(this->incomplete_comm_pattern); - xbt_free(this->proc_status); +} + +std::size_t State::interleaveSize() const +{ + return std::count_if(this->processStates.begin(), this->processStates.end(), + [](simgrid::mc::ProcessState const& state) { return state.interleave(); }); } } @@ -69,29 +73,14 @@ State::~State() void MC_state_interleave_process(simgrid::mc::State* state, smx_process_t process) { assert(state); - state->proc_status[process->pid].state = MC_INTERLEAVE; - state->proc_status[process->pid].interleave_count = 0; + state->processStates[process->pid].state = simgrid::mc::ProcessInterleaveState::interleave; + state->processStates[process->pid].interleave_count = 0; } void MC_state_remove_interleave_process(simgrid::mc::State* state, smx_process_t process) { - if (state->proc_status[process->pid].state == MC_INTERLEAVE) - state->proc_status[process->pid].state = MC_DONE; -} - -unsigned int MC_state_interleave_size(simgrid::mc::State* state) -{ - unsigned int i, size = 0; - for (i = 0; i < state->max_pid; i++) - if ((state->proc_status[i].state == MC_INTERLEAVE) - || (state->proc_status[i].state == MC_MORE_INTERLEAVE)) - size++; - return size; -} - -int MC_state_process_is_done(simgrid::mc::State* state, smx_process_t process) -{ - return state->proc_status[process->pid].state == MC_DONE ? TRUE : FALSE; + if (state->processStates[process->pid].state == simgrid::mc::ProcessInterleaveState::interleave) + state->processStates[process->pid].state = simgrid::mc::ProcessInterleaveState::done; } void MC_state_set_executed_request(simgrid::mc::State* state, smx_simcall_t req, @@ -154,10 +143,10 @@ void MC_state_set_executed_request(simgrid::mc::State* state, smx_simcall_t req, int random_max = simcall_mc_random__get__max(req); if (value != random_max) for (auto& p : mc_model_checker->process().simix_processes()) { - mc_procstate_t procstate = &state->proc_status[p.copy.pid]; + 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 = MC_MORE_INTERLEAVE; + procstate->state = simgrid::mc::ProcessInterleaveState::more_interleave; break; } } @@ -184,11 +173,10 @@ smx_simcall_t MC_state_get_internal_request(simgrid::mc::State* state) static inline smx_simcall_t MC_state_get_request_for_process( simgrid::mc::State* state, int*value, smx_process_t process) { - mc_procstate_t procstate = &state->proc_status[process->pid]; + simgrid::mc::ProcessState* procstate = &state->processStates[process->pid]; - if (procstate->state != MC_INTERLEAVE - && procstate->state != MC_MORE_INTERLEAVE) - return nullptr; + if (!procstate->interleave()) + return nullptr; if (!simgrid::mc::process_is_enabled(process)) return nullptr; @@ -209,7 +197,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 = MC_DONE; + procstate->state = simgrid::mc::ProcessInterleaveState::done; if (*value != -1) return &process->simcall; @@ -231,7 +219,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 = MC_DONE; + procstate->state = simgrid::mc::ProcessInterleaveState::done; if (*value != -1 || start_count == 0) return &process->simcall; @@ -251,20 +239,20 @@ static inline smx_simcall_t MC_state_get_request_for_process( *value = 0; else *value = -1; - procstate->state = MC_DONE; + procstate->state = simgrid::mc::ProcessInterleaveState::done; return &process->simcall; } case SIMCALL_MC_RANDOM: - if (procstate->state == MC_INTERLEAVE) + 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 = MC_DONE; + procstate->state = simgrid::mc::ProcessInterleaveState::done; return &process->simcall; default: - procstate->state = MC_DONE; + procstate->state = simgrid::mc::ProcessInterleaveState::done; *value = 0; return &process->simcall; } diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h index 1b8659fe21..90706daa4b 100644 --- a/src/mc/mc_state.h +++ b/src/mc/mc_state.h @@ -17,26 +17,36 @@ #include "src/simix/smx_private.h" #include "src/mc/mc_snapshot.h" -/* Possible exploration status of a process in a state */ -typedef enum { - MC_NOT_INTERLEAVE=0, /* Do not interleave (do not execute) */ - MC_INTERLEAVE, /* Interleave the process (one or more request) */ - MC_MORE_INTERLEAVE, /* Interleave twice the process (for mc_random simcall) */ - MC_DONE /* Already interleaved */ -} e_mc_process_state_t; - -/* On every state, each process has an entry of the following type */ -typedef struct mc_procstate{ - e_mc_process_state_t state; /* Exploration control information */ - unsigned int interleave_count; /* Number of times that the process was - interleaved */ -} s_mc_procstate_t, *mc_procstate_t; - namespace simgrid { namespace mc { extern XBT_PRIVATE std::unique_ptr initial_global_state; +/* 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 { + /** 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; + } + bool interleave() const { + return this->state == ProcessInterleaveState::interleave + || this->state == ProcessInterleaveState::more_interleave; + } +}; + /* An exploration state. * * The `executed_state` is sometimes transformed into another `internal_req`. @@ -44,9 +54,9 @@ extern XBT_PRIVATE std::unique_ptr initial_global_state; * See `MC_state_set_executed_request()`. */ struct XBT_PRIVATE State { - unsigned long max_pid = 0; /* Maximum pid at state's creation time */ - mc_procstate_t proc_status = 0; /* State's exploration status by process */ - s_smx_synchro_t internal_comm; /* To be referenced by the internal_req */ + /** 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 @@ -54,12 +64,17 @@ struct XBT_PRIVATE State { std::shared_ptr system_state = nullptr; /* Snapshot of system state */ int num = 0; int in_visited_states = 0; + // comm determinism verification (xbt_dynar_t): xbt_dynar_t incomplete_comm_pattern = nullptr; - xbt_dynar_t index_comm = nullptr; // comm determinism verification + + // For communication determinism verification: + std::vector communicationIndices; State(); ~State(); + + std::size_t interleaveSize() const; }; XBT_PRIVATE void replay(std::list> const& stack); @@ -69,8 +84,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 unsigned int MC_state_interleave_size(simgrid::mc::State* state); -XBT_PRIVATE int MC_state_process_is_done(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);