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++;
while (!stack_.empty()) {
std::unique_ptr<simgrid::mc::State> 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",
/* 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) {
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))
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++;
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);
}
}
- 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",
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(
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(
#include <assert.h>
+#include <algorithm>
+
#include <xbt/log.h>
#include <xbt/sysdep.h>
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){
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(); });
}
}
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,
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;
}
}
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;
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;
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;
*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;
}
#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<s_mc_global_t> 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`.
* 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<ProcessState> 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
std::shared_ptr<simgrid::mc::Snapshot> system_state = nullptr; /* Snapshot of system state */
int num = 0;
int in_visited_states = 0;
+
// comm determinism verification (xbt_dynar_t<xbt_dynar_t<mc_comm_pattern_t>):
xbt_dynar_t incomplete_comm_pattern = nullptr;
- xbt_dynar_t index_comm = nullptr; // comm determinism verification
+
+ // For communication determinism verification:
+ std::vector<unsigned> communicationIndices;
State();
~State();
+
+ std::size_t interleaveSize() const;
};
XBT_PRIVATE void replay(std::list<std::unique_ptr<simgrid::mc::State>> 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 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);
