for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) {
// Find (pid, value):
- mc_state_t state = (mc_state_t) xbt_fifo_get_item_content(item);
+ simgrid::mc::State* state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
int value = 0;
smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
std::vector<std::string> res;
for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
item; item = xbt_fifo_get_prev_item(item)) {
- mc_state_t state = (mc_state_t)xbt_fifo_get_item_content(item);
+ simgrid::mc::State* state = (simgrid::mc::State*)xbt_fifo_get_item_content(item);
int value;
smx_simcall_t req = MC_state_get_executed_request(state, &value);
if (req) {
void CommunicationDeterminismChecker::prepare()
{
- mc_state_t initial_state = nullptr;
+ simgrid::mc::State* initial_state = nullptr;
int i;
const int maxpid = MC_smx_get_maxpid();
int value;
std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
smx_simcall_t req = nullptr;
- mc_state_t state = nullptr, next_state = NULL;
+ simgrid::mc::State* state = nullptr;
+ simgrid::mc::State* next_state = nullptr;
while (xbt_fifo_size(mc_stack) > 0) {
/* Get current state */
- state = (mc_state_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+ state = (simgrid::mc::State*) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
XBT_DEBUG("**************************************************");
XBT_DEBUG("Exploration depth = %d (state = %d, interleaved processes = %d)",
return SIMGRID_MC_EXIT_DEADLOCK;
}
- while ((state = (mc_state_t) xbt_fifo_shift(mc_stack)) != nullptr)
+ while ((state = (simgrid::mc::State*) xbt_fifo_shift(mc_stack)) != nullptr)
if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
/* We found a back-tracking point, let's loop */
XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
namespace simgrid {
namespace mc {
-VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state)
+VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, simgrid::mc::State* graph_state)
{
simgrid::mc::Process* process = &(mc_model_checker->process());
{
xbt_fifo_item_t item;
simgrid::mc::Pair* pair = nullptr;
- mc_state_t state = nullptr;
+ simgrid::mc::State* state = nullptr;
smx_simcall_t req = nullptr, saved_req = NULL;
int value, depth = 1;
char *req_str;
pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
- state = (mc_state_t) pair->graph_state;
+ state = (simgrid::mc::State*) pair->graph_state;
if (pair->exploration_started) {
struct XBT_PRIVATE Pair {
int num = 0;
int search_cycle = 0;
- mc_state_t graph_state = nullptr; /* System state included */
+ simgrid::mc::State* graph_state = nullptr; /* System state included */
xbt_automaton_state_t automaton_state = nullptr;
simgrid::xbt::unique_ptr<s_xbt_dynar_t> atomic_propositions;
int requests = 0;
int num = 0;
int other_num = 0; /* Dot output for */
int acceptance_pair = 0;
- mc_state_t graph_state = nullptr; /* System state included */
+ simgrid::mc::State* graph_state = nullptr; /* System state included */
xbt_automaton_state_t automaton_state = nullptr;
simgrid::xbt::unique_ptr<s_xbt_dynar_t> atomic_propositions;
size_t heap_bytes_used = 0;
int acceptance_removed = 0;
int visited_removed = 0;
- VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state);
+ VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, simgrid::mc::State* graph_state);
~VisitedPair();
};
MC_print_statistics(mc_stats);
}
-static int snapshot_compare(mc_state_t state1, mc_state_t state2)
+static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
{
simgrid::mc::Snapshot* s1 = state1->system_state;
simgrid::mc::Snapshot* s2 = state2->system_state;
return snapshot_compare(num1, s1, num2, s2);
}
-static int is_exploration_stack_state(mc_state_t current_state){
+static int is_exploration_stack_state(simgrid::mc::State* current_state){
xbt_fifo_item_t item;
- mc_state_t stack_state;
+ simgrid::mc::State* stack_state;
for(item = xbt_fifo_get_first_item(mc_stack); item != nullptr; item = xbt_fifo_get_next_item(item)) {
- stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
+ stack_state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
if(snapshot_compare(stack_state, current_state) == 0){
XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
return 1;
for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) {
// Find (pid, value):
- mc_state_t state = (mc_state_t) xbt_fifo_get_item_content(item);
+ simgrid::mc::State* state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
int value = 0;
smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
std::vector<std::string> trace;
for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
item; item = xbt_fifo_get_prev_item(item)) {
- mc_state_t state = (mc_state_t)xbt_fifo_get_item_content(item);
+ simgrid::mc::State* state = (simgrid::mc::State*)xbt_fifo_get_item_content(item);
int value;
smx_simcall_t req = MC_state_get_executed_request(state, &value);
if (req) {
char *req_str = nullptr;
int value;
smx_simcall_t req = nullptr;
- mc_state_t state = nullptr, prev_state = NULL, next_state = NULL;
+ simgrid::mc::State* state = nullptr;
+ simgrid::mc::State* prev_state = nullptr;
+ simgrid::mc::State* next_state = nullptr;
xbt_fifo_item_t item = nullptr;
std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
while (xbt_fifo_size(mc_stack) > 0) {
/* Get current state */
- state = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+ state = (simgrid::mc::State*)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
XBT_DEBUG("**************************************************");
XBT_DEBUG
executed before it. If it does then add it to the interleave set of the
state that executed that previous request. */
- while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
+ while ((state = (simgrid::mc::State*) xbt_fifo_shift(mc_stack))) {
if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
req = MC_state_get_internal_request(state);
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");
const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
- xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
+ xbt_fifo_foreach(mc_stack, item, prev_state, simgrid::mc::State*) {
if (reductionMode_ != simgrid::mc::ReductionMode::none
&& simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
simgrid::mc::visited_states.clear();
- mc_state_t initial_state = MC_state_new();
+ simgrid::mc::State* initial_state = MC_state_new();
XBT_DEBUG("**************************************************");
XBT_DEBUG("Initial state");
}
}
-void MC_restore_communications_pattern(mc_state_t state)
+void MC_restore_communications_pattern(simgrid::mc::State* state)
{
mc_list_comm_pattern_t list_process_comm;
unsigned int cursor;
);
}
-void MC_state_copy_incomplete_communications_pattern(mc_state_t state)
+void MC_state_copy_incomplete_communications_pattern(simgrid::mc::State* state)
{
state->incomplete_comm_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
}
}
-void MC_state_copy_index_communications_pattern(mc_state_t state)
+void MC_state_copy_index_communications_pattern(simgrid::mc::State* state)
{
state->index_comm = xbt_dynar_new(sizeof(unsigned int), nullptr);
mc_list_comm_pattern_t list_process_comm;
XBT_PRIVATE void MC_list_comm_pattern_free_voidp(void *p);
XBT_PRIVATE void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking);
-XBT_PRIVATE void MC_restore_communications_pattern(mc_state_t state);
+XBT_PRIVATE void MC_restore_communications_pattern(simgrid::mc::State* state);
XBT_PRIVATE mc_comm_pattern_t MC_comm_pattern_dup(mc_comm_pattern_t comm);
XBT_PRIVATE xbt_dynar_t MC_comm_patterns_dup(xbt_dynar_t state);
-XBT_PRIVATE void MC_state_copy_incomplete_communications_pattern(mc_state_t state);
-XBT_PRIVATE void MC_state_copy_index_communications_pattern(mc_state_t state);
+XBT_PRIVATE void MC_state_copy_incomplete_communications_pattern(simgrid::mc::State* state);
+XBT_PRIVATE void MC_state_copy_index_communications_pattern(simgrid::mc::State* state);
XBT_PRIVATE void MC_comm_pattern_free(mc_comm_pattern_t p);
int user_max_depth_reached = 0;
/* MC global data structures */
-mc_state_t mc_current_state = nullptr;
+simgrid::mc::State* mc_current_state = nullptr;
char mc_replay_mode = false;
mc_stats_t mc_stats = nullptr;
char *req_str;
smx_simcall_t req = nullptr, saved_req = NULL;
xbt_fifo_item_t item, start_item;
- mc_state_t state;
+ simgrid::mc::State* state;
XBT_DEBUG("**** Begin Replay ****");
/* Intermediate backtracking */
if(_sg_mc_checkpoint > 0 || _sg_mc_termination || _sg_mc_visited > 0) {
start_item = xbt_fifo_get_first_item(stack);
- state = (mc_state_t)xbt_fifo_get_item_content(start_item);
+ state = (simgrid::mc::State*)xbt_fifo_get_item_content(start_item);
if(state->system_state){
simgrid::mc::restore_snapshot(state->system_state);
if(_sg_mc_comms_determinism || _sg_mc_send_determinism)
item != xbt_fifo_get_first_item(stack);
item = xbt_fifo_get_prev_item(item)) {
- state = (mc_state_t) xbt_fifo_get_item_content(item);
+ state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
saved_req = MC_state_get_executed_request(state, &value);
if (saved_req) {
XBT_PRIVATE void MC_replay(xbt_fifo_t stack);
XBT_PRIVATE void MC_show_deadlock(void);
-/** Stack (of `mc_state_t`) representing the current position of the
+/** Stack (of `simgrid::mc::State*`) representing the current position of the
* the MC in the exploration graph
*
* It is managed by its head (`xbt_fifo_shift` and `xbt_fifo_unshift`).
};
extern XBT_PRIVATE std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
-XBT_PRIVATE std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state, bool compare_snpashots);
+XBT_PRIVATE std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(simgrid::mc::State* graph_state, bool compare_snpashots);
}
}
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_state, mc,
"Logging specific to MC (state)");
-extern "C" {
-
/**
* \brief Creates a state data structure used by the exploration algorithm
*/
-mc_state_t MC_state_new()
+simgrid::mc::State* MC_state_new()
{
- mc_state_t state = xbt_new0(s_mc_state_t, 1);
+ simgrid::mc::State* state = new simgrid::mc::State();
+ 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->system_state = nullptr;
state->num = ++mc_stats->expanded_states;
- state->in_visited_states = 0;
- state->incomplete_comm_pattern = nullptr;
/* Stateful model checking */
if((_sg_mc_checkpoint > 0 && (mc_stats->expanded_states % _sg_mc_checkpoint == 0)) || _sg_mc_termination){
state->system_state = simgrid::mc::take_snapshot(state->num);
return state;
}
+namespace simgrid {
+namespace mc {
+
+State::State()
+{
+ std::memset(&this->internal_comm, 0, sizeof(this->internal_comm));
+ std::memset(&this->internal_req, 0, sizeof(this->internal_req));
+ std::memset(&this->executed_req, 0, sizeof(this->executed_req));
+}
+
+State::~State()
+{
+ xbt_free(this->index_comm);
+ xbt_free(this->incomplete_comm_pattern);
+ xbt_free(this->proc_status);
+}
+
+}
+}
+
/**
* \brief Deletes a state data structure
* \param trans The state to be deleted
*/
-void MC_state_delete(mc_state_t state, int free_snapshot){
+void MC_state_delete(simgrid::mc::State* state, int free_snapshot)
+{
if (state->system_state && free_snapshot)
delete state->system_state;
- if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
- xbt_free(state->index_comm);
- xbt_free(state->incomplete_comm_pattern);
- }
- xbt_free(state->proc_status);
- xbt_free(state);
+ delete state;
}
-void MC_state_interleave_process(mc_state_t state, smx_process_t process)
+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;
}
-void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process)
+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(mc_state_t state)
+unsigned int MC_state_interleave_size(simgrid::mc::State* state)
{
unsigned int i, size = 0;
for (i = 0; i < state->max_pid; i++)
return size;
}
-int MC_state_process_is_done(mc_state_t state, smx_process_t process)
+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;
}
-void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req,
+void MC_state_set_executed_request(simgrid::mc::State* state, smx_simcall_t req,
int value)
{
state->executed_req = *req;
}
}
-smx_simcall_t MC_state_get_executed_request(mc_state_t state, int *value)
+smx_simcall_t MC_state_get_executed_request(simgrid::mc::State* state, int *value)
{
*value = state->req_num;
return &state->executed_req;
}
-smx_simcall_t MC_state_get_internal_request(mc_state_t state)
+smx_simcall_t MC_state_get_internal_request(simgrid::mc::State* state)
{
return &state->internal_req;
}
static inline smx_simcall_t MC_state_get_request_for_process(
- mc_state_t state, int*value, smx_process_t process)
+ simgrid::mc::State* state, int*value, smx_process_t process)
{
mc_procstate_t procstate = &state->proc_status[process->pid];
return nullptr;
}
-smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
+smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value)
{
for (auto& p : mc_model_checker->process().simix_processes()) {
smx_simcall_t res = MC_state_get_request_for_process(state, value, &p.copy);
}
return nullptr;
}
-
-}
#include "src/simix/smx_private.h"
#include "src/mc/mc_snapshot.h"
-SG_BEGIN_DECL()
-
extern XBT_PRIVATE mc_global_t initial_global_state;
/* Possible exploration status of a process in a state */
interleaved */
} s_mc_procstate_t, *mc_procstate_t;
+namespace simgrid {
+namespace mc {
+
/* 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()`.
*/
-typedef struct XBT_PRIVATE mc_state {
- unsigned long max_pid; /* Maximum pid at state's creation time */
- mc_procstate_t proc_status; /* State's exploration status by process */
+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 */
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; /* The request number (in the case of a
+ int req_num = 0; /* The request number (in the case of a
multi-request like waitany ) */
- simgrid::mc::Snapshot* system_state; /* Snapshot of system state */
- int num;
- int in_visited_states;
+ simgrid::mc::Snapshot* system_state = 0; /* 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;
- xbt_dynar_t index_comm; // comm determinism verification
-} s_mc_state_t, *mc_state_t;
+ xbt_dynar_t incomplete_comm_pattern = nullptr;
+ xbt_dynar_t index_comm = nullptr; // comm determinism verification
+
+ State();
+ ~State();
+};
-XBT_PRIVATE mc_state_t MC_state_new(void);
-XBT_PRIVATE void MC_state_delete(mc_state_t state, int free_snapshot);
-XBT_PRIVATE void MC_state_interleave_process(mc_state_t state, smx_process_t process);
-XBT_PRIVATE unsigned int MC_state_interleave_size(mc_state_t state);
-XBT_PRIVATE int MC_state_process_is_done(mc_state_t state, smx_process_t process);
-XBT_PRIVATE void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, int value);
-XBT_PRIVATE smx_simcall_t MC_state_get_executed_request(mc_state_t state, int *value);
-XBT_PRIVATE smx_simcall_t MC_state_get_internal_request(mc_state_t state);
-XBT_PRIVATE smx_simcall_t MC_state_get_request(mc_state_t state, int *value);
-XBT_PRIVATE void MC_state_remove_interleave_process(mc_state_t state, smx_process_t process);
+}
+}
-SG_END_DECL()
+XBT_PRIVATE simgrid::mc::State* MC_state_new(void);
+XBT_PRIVATE void MC_state_delete(simgrid::mc::State* state, int free_snapshot);
+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);
+XBT_PRIVATE smx_simcall_t MC_state_get_request(simgrid::mc::State* state, int *value);
+XBT_PRIVATE void MC_state_remove_interleave_process(simgrid::mc::State* state, smx_process_t process);
#endif
static int is_exploration_stack_state(simgrid::mc::VisitedState* state){
xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
while (item) {
- if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
- ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
+ if (((simgrid::mc::State*)xbt_fifo_get_item_content(item))->num == state->num){
+ ((simgrid::mc::State*)xbt_fifo_get_item_content(item))->in_visited_states = 0;
return 1;
}
item = xbt_fifo_get_next_item(item);
/**
* \brief Checks whether a given state has already been visited by the algorithm.
*/
-std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state, bool compare_snpashots)
+std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(simgrid::mc::State* graph_state, bool compare_snpashots)
{
