#include "simgrid/msg.h"
#include "mc/mc.h"
-#include "xbt/automaton.h"
#include "bugged1_liveness.h"
XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages");
#include "simgrid/msg.h"
#include "mc/mc.h"
-#include "xbt/automaton.h"
#include "bugged2_liveness.h"
XBT_LOG_NEW_DEFAULT_CATEGORY(bugged3, "my log messages");
#include <simgrid_config.h> /* HAVE_MC ? */
#include <xbt/base.h>
-#include <xbt/automaton.h>
SG_BEGIN_DECL()
};
XBT_PUBLIC() Checker* createLivenessChecker(Session& session);
+XBT_PUBLIC() Checker* createSafetyChecker(Session& session);
+XBT_PUBLIC() Checker* createCommunicationDeterminismChecker(Session& session);
}
}
#include <xbt/dynar.h>
#include <xbt/dynar.hpp>
-#include <xbt/fifo.h>
#include <xbt/log.h>
#include <xbt/sysdep.h>
#include "src/mc/Client.hpp"
#include "src/mc/CommunicationDeterminismChecker.hpp"
#include "src/mc/mc_exit.h"
+#include "src/mc/VisitedState.hpp"
using simgrid::mc::remote;
RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
{
RecordTrace res;
-
- xbt_fifo_item_t start = xbt_fifo_get_last_item(mc_stack);
- for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) {
-
- // Find (pid, value):
- simgrid::mc::State* state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
+ for (auto const& state : stack_) {
int value = 0;
- smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
+ smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
const int pid = issuer->pid;
-
res.push_back(RecordTraceElement(pid, value));
}
-
return res;
}
// TODO, deduplicate with SafetyChecker
std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
{
- 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)) {
- simgrid::mc::State* state = (simgrid::mc::State*)xbt_fifo_get_item_content(item);
+ std::vector<std::string> trace;
+ for (auto const& state : stack_) {
int value;
- smx_simcall_t req = MC_state_get_executed_request(state, &value);
+ smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
if (req) {
char* req_str = simgrid::mc::request_to_string(
req, value, simgrid::mc::RequestType::executed);
- res.push_back(req_str);
+ trace.push_back(req_str);
xbt_free(req_str);
}
}
- return res;
+ return trace;
}
void CommunicationDeterminismChecker::prepare()
{
- simgrid::mc::State* initial_state = nullptr;
+
int i;
const int maxpid = MC_smx_get_maxpid();
- simgrid::mc::visited_states.clear();
-
// Create initial_communications_pattern elements:
initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), MC_list_comm_pattern_free_voidp);
for (i=0; i < maxpid; i++){
xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
}
- initial_state = MC_state_new();
+ std::unique_ptr<simgrid::mc::State> initial_state =
+ std::unique_ptr<simgrid::mc::State>(MC_state_new());
XBT_DEBUG("********* Start communication determinism verification *********");
/* 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, &p.copy);
+ MC_state_interleave_process(initial_state.get(), &p.copy);
- xbt_fifo_unshift(mc_stack, initial_state);
+ stack_.push_back(std::move(initial_state));
}
static inline
int value;
std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
smx_simcall_t req = nullptr;
- simgrid::mc::State* state = nullptr;
- simgrid::mc::State* next_state = nullptr;
- while (xbt_fifo_size(mc_stack) > 0) {
+ while (!stack_.empty()) {
/* Get current state */
- state = (simgrid::mc::State*) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+ simgrid::mc::State* state = stack_.back().get();
XBT_DEBUG("**************************************************");
- XBT_DEBUG("Exploration depth = %d (state = %d, interleaved processes = %d)",
- xbt_fifo_size(mc_stack), state->num,
+ XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %d)",
+ stack_.size(), state->num,
MC_state_interleave_size(state));
/* Update statistics */
mc_stats->visited_states++;
- if ((xbt_fifo_size(mc_stack) <= _sg_mc_max_depth)
+ if (stack_.size() <= (std::size_t) _sg_mc_max_depth
&& (req = MC_state_get_request(state, &value))
&& (visited_state == nullptr)) {
mc_model_checker->wait_for_requests();
/* Create the new expanded state */
- next_state = MC_state_new();
+ std::unique_ptr<simgrid::mc::State> next_state =
+ std::unique_ptr<simgrid::mc::State>(MC_state_new());
/* If comm determinism verification, we cannot stop the exploration if
some communications are not finished (at least, data are transfered).
bool compare_snapshots = all_communications_are_finished()
&& initial_global_state->initial_communications_pattern_done;
- if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, compare_snapshots)) == nullptr) {
+ if (_sg_mc_visited == 0
+ || (visited_state = visitedStates_.addVisitedState(next_state.get(), compare_snapshots)) == nullptr) {
/* 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, &p.copy);
+ MC_state_interleave_process(next_state.get(), &p.copy);
if (dot_output != nullptr)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
- xbt_fifo_unshift(mc_stack, next_state);
+ stack_.push_back(std::move(next_state));
if (dot_output != nullptr)
xbt_free(req_str);
} else {
- if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth)
+ if (stack_.size() > (std::size_t) _sg_mc_max_depth)
XBT_WARN("/!\\ Max depth reached ! /!\\ ");
else if (visited_state != nullptr)
XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
else
- XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack));
+ XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
+ stack_.size());
if (!initial_global_state->initial_communications_pattern_done)
initial_global_state->initial_communications_pattern_done = 1;
/* Trash the current state, no longer needed */
- xbt_fifo_shift(mc_stack);
- MC_state_delete(state, !state->in_visited_states ? 1 : 0);
- XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
+ XBT_DEBUG("Delete state %d at depth %zi",
+ state->num, stack_.size());
+ stack_.pop_back();
visited_state = nullptr;
return SIMGRID_MC_EXIT_DEADLOCK;
}
- 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) {
+ while (!stack_.empty()) {
+ std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
+ stack_.pop_back();
+ if (MC_state_interleave_size(state.get())
+ && 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 %d", state->num, xbt_fifo_size(mc_stack) + 1);
- xbt_fifo_unshift(mc_stack, state);
+ XBT_DEBUG("Back-tracking to state %d at depth %zi",
+ state->num, stack_.size() + 1);
+ stack_.push_back(std::move(state));
- MC_replay(mc_stack);
+ simgrid::mc::replay(stack_);
- XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
+ XBT_DEBUG("Back-tracking to state %d at depth %zi done",
+ stack_.back()->num, stack_.size());
break;
} else {
- XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
- MC_state_delete(state, !state->in_visited_states ? 1 : 0);
+ XBT_DEBUG("Delete state %d at depth %zi",
+ state->num, stack_.size() + 1);
}
-
+ }
}
}
// This will move somehwere else:
simgrid::mc::Client::get()->handleMessages();
- /* Create exploration stack */
- mc_stack = xbt_fifo_new();
-
this->prepare();
initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
return res;
}
+Checker* createCommunicationDeterminismChecker(Session& session)
+{
+ return new CommunicationDeterminismChecker(session);
+}
+
}
}
\ No newline at end of file
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
+#include <list>
+#include <memory>
+#include <string>
+#include <vector>
+
#include "src/mc/mc_forward.hpp"
#include "src/mc/Checker.hpp"
+#include "src/mc/VisitedState.hpp"
#ifndef SIMGRID_MC_COMMUNICATION_DETERMINISM_CHECKER_HPP
#define SIMGRID_MC_COMMUNICATION_DETERMINISM_CHECKER_HPP
namespace simgrid {
namespace mc {
-class CommunicationDeterminismChecker : public Checker {
+class XBT_PRIVATE CommunicationDeterminismChecker : public Checker {
public:
CommunicationDeterminismChecker(Session& session);
~CommunicationDeterminismChecker();
private:
void prepare();
int main();
+private:
+ /** Stack representing the position in the exploration graph */
+ std::list<std::unique_ptr<simgrid::mc::State>> stack_;
+ simgrid::mc::VisitedStates visitedStates_;
};
#endif
VisitedPair::VisitedPair(
int pair_num, xbt_automaton_state_t automaton_state,
- std::vector<int> const& atomic_propositions, std::shared_ptr<simgrid::mc::State> graph_state)
+ std::shared_ptr<const std::vector<int>> atomic_propositions,
+ std::shared_ptr<simgrid::mc::State> graph_state)
{
simgrid::mc::Process* process = &(mc_model_checker->process());
this->automaton_state = automaton_state;
this->num = pair_num;
this->other_num = -1;
- this->atomic_propositions = atomic_propositions;
+ this->atomic_propositions = std::move(atomic_propositions);
}
VisitedPair::~VisitedPair()
Pair::~Pair() {}
-std::vector<int> LivenessChecker::getPropositionValues()
+std::shared_ptr<const std::vector<int>> LivenessChecker::getPropositionValues()
{
std::vector<int> values;
unsigned int cursor = 0;
xbt_automaton_propositional_symbol_t ps = nullptr;
xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, ps)
values.push_back(xbt_automaton_propositional_symbol_evaluate(ps));
- return values;
+ return std::make_shared<const std::vector<int>>(std::move(values));
}
int LivenessChecker::compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2)
std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
if (xbt_automaton_state_compare(
pair_test->automaton_state, new_pair->automaton_state) != 0
- || pair_test->atomic_propositions != new_pair->atomic_propositions
+ || *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions)
|| this->compare(pair_test.get(), new_pair.get()) != 0)
continue;
XBT_INFO("Pair %d already reached (equal to pair %d) !",
initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
initial_global_state->prev_pair = 0;
+ std::shared_ptr<const std::vector<int>> propos = this->getPropositionValues();
+
// For each initial state of the property automaton, push a
// (application_state, automaton_state) pair to the exploration stack:
unsigned int cursor = 0;
xbt_automaton_state_t automaton_state;
xbt_dynar_foreach(simgrid::mc::property_automaton->states, cursor, automaton_state)
if (automaton_state->type == -1)
- explorationStack_.push_back(this->newPair(nullptr, automaton_state));
+ explorationStack_.push_back(this->newPair(nullptr, automaton_state, propos));
}
VisitedPair* pair_test = i->get();
if (xbt_automaton_state_compare(
pair_test->automaton_state, visited_pair->automaton_state) != 0
- || pair_test->atomic_propositions != visited_pair->atomic_propositions
+ || *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions)
|| this->compare(pair_test, visited_pair.get()) != 0)
continue;
if (pair_test->other_num == -1)
current_pair->exploration_started = true;
/* Get values of atomic propositions (variables used in the property formula) */
- std::vector<int> prop_values = this->getPropositionValues();
+ std::shared_ptr<const std::vector<int>> prop_values = this->getPropositionValues();
// For each enabled transition in the property automaton, push a
// (application_state, automaton_state) pair to the exploration stack:
int cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1;
while (cursor >= 0) {
xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t);
- if (evaluate_label(transition_succ->label, prop_values))
+ if (evaluate_label(transition_succ->label, *prop_values))
explorationStack_.push_back(this->newPair(
- current_pair.get(), transition_succ->dst));
+ current_pair.get(), transition_succ->dst, prop_values));
cursor--;
}
return SIMGRID_MC_EXIT_SUCCESS;
}
-std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state)
+std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state, std::shared_ptr<const std::vector<int>> propositions)
{
std::shared_ptr<Pair> next_pair = std::make_shared<Pair>();
next_pair->automaton_state = state;
next_pair->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new());
- next_pair->atomic_propositions = this->getPropositionValues();
+ next_pair->atomic_propositions = std::move(propositions);
if (current_pair)
next_pair->depth = current_pair->depth + 1;
else
bool search_cycle = false;
std::shared_ptr<simgrid::mc::State> graph_state = nullptr; /* System state included */
xbt_automaton_state_t automaton_state = nullptr;
- std::vector<int> atomic_propositions;
+ std::shared_ptr<const std::vector<int>> atomic_propositions;
int requests = 0;
int depth = 0;
bool exploration_started = false;
int other_num = 0; /* Dot output for */
std::shared_ptr<simgrid::mc::State> graph_state = nullptr; /* System state included */
xbt_automaton_state_t automaton_state = nullptr;
- std::vector<int> atomic_propositions;
+ std::shared_ptr<const std::vector<int>> atomic_propositions;
std::size_t heap_bytes_used = 0;
int nb_processes = 0;
VisitedPair(
int pair_num, xbt_automaton_state_t automaton_state,
- std::vector<int> const& atomic_propositions,
+ std::shared_ptr<const std::vector<int>> atomic_propositions,
std::shared_ptr<simgrid::mc::State> graph_state);
~VisitedPair();
};
int main();
void prepare();
int compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2);
- std::vector<int> getPropositionValues();
+ std::shared_ptr<const std::vector<int>> getPropositionValues();
std::shared_ptr<VisitedPair> insertAcceptancePair(simgrid::mc::Pair* pair);
int insertVisitedPair(std::shared_ptr<VisitedPair> visited_pair, simgrid::mc::Pair* pair);
void showAcceptanceCycle(std::size_t depth);
void removeAcceptancePair(int pair_num);
void purgeVisitedPairs();
void backtrack();
- std::shared_ptr<Pair> newPair(Pair* pair, xbt_automaton_state_t state);
+ std::shared_ptr<Pair> newPair(Pair* pair, xbt_automaton_state_t state, std::shared_ptr<const std::vector<int>> propositions);
public:
// A stack of (application_state, automaton_state) pairs for DFS exploration:
std::list<std::shared_ptr<Pair>> explorationStack_;
* under the terms of the license (GNU LGPL) which comes with this package. */
#include <cassert>
-
#include <cstdio>
+#include <list>
+
#include <xbt/log.h>
-#include <xbt/dynar.h>
-#include <xbt/dynar.hpp>
-#include <xbt/fifo.h>
#include <xbt/sysdep.h>
#include "src/mc/mc_state.h"
#include "src/mc/mc_exit.h"
#include "src/mc/Checker.hpp"
#include "src/mc/SafetyChecker.hpp"
+#include "src/mc/VisitedState.hpp"
#include "src/xbt/mmalloc/mmprivate.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
"Logging specific to MC safety verification ");
-
namespace simgrid {
namespace mc {
return snapshot_compare(num1, s1, num2, s2);
}
-static int is_exploration_stack_state(simgrid::mc::State* current_state){
-
- xbt_fifo_item_t item;
- 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 = (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;
+bool SafetyChecker::checkNonDeterminism(simgrid::mc::State* current_state)
+{
+ for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
+ if (snapshot_compare(i->get(), current_state) == 0){
+ XBT_INFO("Non-progressive cycle : state %d -> state %d",
+ (*i)->num, current_state->num);
+ return true;
}
- }
- return 0;
+ return false;
}
RecordTrace SafetyChecker::getRecordTrace() // override
{
RecordTrace res;
-
- xbt_fifo_item_t start = xbt_fifo_get_last_item(mc_stack);
- for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) {
-
- // Find (pid, value):
- simgrid::mc::State* state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
+ for (auto const& state : stack_) {
int value = 0;
- smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
+ smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
const int pid = issuer->pid;
-
res.push_back(RecordTraceElement(pid, value));
}
-
return res;
}
std::vector<std::string> SafetyChecker::getTextualTrace() // override
{
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)) {
- simgrid::mc::State* state = (simgrid::mc::State*)xbt_fifo_get_item_content(item);
+ for (auto const& state : stack_) {
int value;
- smx_simcall_t req = MC_state_get_executed_request(state, &value);
+ smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
if (req) {
char* req_str = simgrid::mc::request_to_string(
req, value, simgrid::mc::RequestType::executed);
{
this->init();
- char *req_str = nullptr;
int value;
smx_simcall_t req = nullptr;
- 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) {
+ while (!stack_.empty()) {
/* Get current state */
- state = (simgrid::mc::State*)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+ simgrid::mc::State* state = stack_.back().get();
XBT_DEBUG("**************************************************");
- XBT_DEBUG
- ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
- xbt_fifo_size(mc_stack), state, state->num,
- MC_state_interleave_size(state), user_max_depth_reached);
+ XBT_DEBUG(
+ "Exploration depth=%zi (state=%p, num %d)(%u interleave, user_max_depth %d)",
+ stack_.size(), state, state->num,
+ MC_state_interleave_size(state), user_max_depth_reached);
/* Update statistics */
mc_stats->visited_states++;
/* If there are processes to interleave and the maximum depth has not been reached
then perform one step of the exploration algorithm */
- if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
+ if (stack_.size() <= (std::size_t) _sg_mc_max_depth && !user_max_depth_reached
&& (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
- req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
+ char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
XBT_DEBUG("Execute: %s", req_str);
xbt_free(req_str);
mc_model_checker->wait_for_requests();
/* Create the new expanded state */
- next_state = MC_state_new();
+ std::unique_ptr<simgrid::mc::State> next_state =
+ std::unique_ptr<simgrid::mc::State>(MC_state_new());
- if(_sg_mc_termination && is_exploration_stack_state(next_state)){
+ if (_sg_mc_termination && this->checkNonDeterminism(next_state.get())){
MC_show_non_termination();
return SIMGRID_MC_EXIT_NON_TERMINATION;
}
- if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, true)) == nullptr) {
+ if (_sg_mc_visited == 0
+ || (visited_state = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
/* 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, &p.copy);
+ MC_state_interleave_process(next_state.get(), &p.copy);
if (reductionMode_ != simgrid::mc::ReductionMode::none)
break;
}
} else if (dot_output != nullptr)
std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
-
- xbt_fifo_unshift(mc_stack, next_state);
+ stack_.push_back(std::move(next_state));
if (dot_output != nullptr)
xbt_free(req_str);
/* The interleave set is empty or the maximum depth is reached, let's back-track */
} else {
- if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != nullptr) {
+ if (stack_.size() > (std::size_t) _sg_mc_max_depth
+ || user_max_depth_reached
+ || visited_state != nullptr) {
if (user_max_depth_reached && visited_state == nullptr)
XBT_DEBUG("User max depth reached !");
XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
} else
- XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
+ XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
+ stack_.size() + 1);
/* Trash the current state, no longer needed */
- xbt_fifo_shift(mc_stack);
- XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
- MC_state_delete(state, !state->in_visited_states ? 1 : 0);
+ XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size());
+ stack_.pop_back();
visited_state = nullptr;
executed before it. If it does then add it to the interleave set of the
state that executed that previous request. */
- while ((state = (simgrid::mc::State*) xbt_fifo_shift(mc_stack))) {
+ while (!stack_.empty()) {
+ std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
+ stack_.pop_back();
if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
- req = MC_state_get_internal_request(state);
+ req = MC_state_get_internal_request(state.get());
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, simgrid::mc::State*) {
+ for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
+ simgrid::mc::State* prev_state = i->get();
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)) {
XBT_DEBUG("Dependent Transitions:");
smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
- req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
+ char* req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
xbt_free(req_str);
- prev_req = MC_state_get_executed_request(state, &value);
+ prev_req = MC_state_get_executed_request(state.get(), &value);
req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
XBT_DEBUG("%s (state=%d)", req_str, state->num);
xbt_free(req_str);
}
}
- if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
+ if (MC_state_interleave_size(state.get())
+ && 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 %d", state->num, xbt_fifo_size(mc_stack) + 1);
- xbt_fifo_unshift(mc_stack, state);
- MC_replay(mc_stack);
- XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
+ XBT_DEBUG("Back-tracking to state %d at depth %zi",
+ state->num, stack_.size() + 1);
+ stack_.push_back(std::move(state));
+ simgrid::mc::replay(stack_);
+ XBT_DEBUG("Back-tracking to state %d at depth %zi done",
+ stack_.back()->num, stack_.size());
break;
} else {
- XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
- MC_state_delete(state, !state->in_visited_states ? 1 : 0);
+ XBT_DEBUG("Delete state %d at depth %zi",
+ state->num, stack_.size() + 1);
}
}
}
XBT_DEBUG("Starting the safety algorithm");
- /* Create exploration stack */
- mc_stack = xbt_fifo_new();
-
- simgrid::mc::visited_states.clear();
-
- simgrid::mc::State* initial_state = MC_state_new();
+ std::unique_ptr<simgrid::mc::State> initial_state =
+ std::unique_ptr<simgrid::mc::State>(MC_state_new());
XBT_DEBUG("**************************************************");
XBT_DEBUG("Initial state");
/* 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, &p.copy);
+ MC_state_interleave_process(initial_state.get(), &p.copy);
if (reductionMode_ != simgrid::mc::ReductionMode::none)
break;
}
- xbt_fifo_unshift(mc_stack, initial_state);
+ stack_.push_back(std::move(initial_state));
/* Save the initial state */
initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
SafetyChecker::~SafetyChecker()
{
}
+
+Checker* createSafetyChecker(Session& session)
+{
+ return new SafetyChecker(session);
+}
}
}
#ifndef SIMGRID_MC_SAFETY_CHECKER_HPP
#define SIMGRID_MC_SAFETY_CHECKER_HPP
+#include <list>
+#include <memory>
+#include <string>
+#include <vector>
+
#include "src/mc/mc_forward.hpp"
#include "src/mc/Checker.hpp"
+#include "src/mc/VisitedState.hpp"
namespace simgrid {
namespace mc {
-class SafetyChecker : public Checker {
+class XBT_PRIVATE SafetyChecker : public Checker {
simgrid::mc::ReductionMode reductionMode_ = simgrid::mc::ReductionMode::unset;
public:
SafetyChecker(Session& session);
private:
// Temp
void init();
+ bool checkNonDeterminism(simgrid::mc::State* current_state);
+private:
+ /** Stack representing the position in the exploration graph */
+ std::list<std::unique_ptr<simgrid::mc::State>> stack_;
+ simgrid::mc::VisitedStates visitedStates_;
};
}
#include <memory>
#include <algorithm>
-#include <xbt/automaton.h>
#include <xbt/log.h>
#include <xbt/sysdep.h>
#include <xbt/dynar.h>
#include "src/mc/mc_private.h"
#include "src/mc/Process.hpp"
#include "src/mc/mc_smx.h"
+#include "src/mc/VisitedState.hpp"
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_VisitedState, mc,
"Logging specific to state equaity detection mechanisms");
namespace simgrid {
namespace mc {
-std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
+static int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::VisitedState* state2)
+{
+ simgrid::mc::Snapshot* s1 = state1->system_state.get();
+ simgrid::mc::Snapshot* s2 = state2->system_state.get();
+ int num1 = state1->num;
+ int num2 = state2->num;
+ return snapshot_compare(num1, s1, num2, s2);
+}
/**
* \brief Save the current state
{
}
-static void prune_visited_states()
+void VisitedStates::prune()
{
- while (visited_states.size() > (std::size_t) _sg_mc_visited) {
+ while (states_.size() > (std::size_t) _sg_mc_visited) {
XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
- auto min_element = std::min_element(visited_states.begin(), visited_states.end(),
+ auto min_element = std::min_element(states_.begin(), states_.end(),
[](std::unique_ptr<simgrid::mc::VisitedState>& a, std::unique_ptr<simgrid::mc::VisitedState>& b) {
return a->num < b->num;
});
- xbt_assert(min_element != visited_states.end());
+ xbt_assert(min_element != states_.end());
// and drop it:
- visited_states.erase(min_element);
+ states_.erase(min_element);
XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
}
}
-static int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::VisitedState* state2)
-{
- simgrid::mc::Snapshot* s1 = state1->system_state.get();
- simgrid::mc::Snapshot* s2 = state2->system_state.get();
- int num1 = state1->num;
- int num2 = state2->num;
- return snapshot_compare(num1, s1, num2, s2);
-}
-
/**
* \brief Checks whether a given state has already been visited by the algorithm.
*/
-std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(simgrid::mc::State* graph_state, bool compare_snpashots)
+std::unique_ptr<simgrid::mc::VisitedState> VisitedStates::addVisitedState(simgrid::mc::State* graph_state, bool compare_snpashots)
{
-
-
std::unique_ptr<simgrid::mc::VisitedState> new_state =
std::unique_ptr<simgrid::mc::VisitedState>(new VisitedState());
graph_state->system_state = new_state->system_state;
XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)",
new_state->system_state.get(), new_state->num, graph_state->num);
- auto range = std::equal_range(visited_states.begin(), visited_states.end(),
+ auto range = std::equal_range(states_.begin(), states_.end(),
new_state.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
- if (compare_snpashots) {
-
- for (auto i = range.first; i != range.second; ++i) {
- auto& visited_state = *i;
- if (snapshot_compare(visited_state.get(), new_state.get()) == 0) {
- // The state has been visited:
-
- std::unique_ptr<simgrid::mc::VisitedState> old_state =
- std::move(visited_state);
-
- if (old_state->other_num == -1)
- new_state->other_num = old_state->num;
- else
- new_state->other_num = old_state->other_num;
-
- if (dot_output == nullptr)
- XBT_DEBUG("State %d already visited ! (equal to state %d)",
- new_state->num, old_state->num);
- else
- XBT_DEBUG(
- "State %d already visited ! (equal to state %d (state %d in dot_output))",
- new_state->num, old_state->num, new_state->other_num);
-
- /* Replace the old state with the new one (with a bigger num)
- (when the max number of visited states is reached, the oldest
- one is removed according to its number (= with the min number) */
- XBT_DEBUG("Replace visited state %d with the new visited state %d",
- old_state->num, new_state->num);
-
- visited_state = std::move(new_state);
- return std::move(old_state);
- }
- }
+ if (compare_snpashots)
+ for (auto i = range.first; i != range.second; ++i) {
+ auto& visited_state = *i;
+ if (snapshot_compare(visited_state.get(), new_state.get()) == 0) {
+ // The state has been visited:
+
+ std::unique_ptr<simgrid::mc::VisitedState> old_state =
+ std::move(visited_state);
+
+ if (old_state->other_num == -1)
+ new_state->other_num = old_state->num;
+ else
+ new_state->other_num = old_state->other_num;
+
+ if (dot_output == nullptr)
+ XBT_DEBUG("State %d already visited ! (equal to state %d)",
+ new_state->num, old_state->num);
+ else
+ XBT_DEBUG(
+ "State %d already visited ! (equal to state %d (state %d in dot_output))",
+ new_state->num, old_state->num, new_state->other_num);
+
+ /* Replace the old state with the new one (with a bigger num)
+ (when the max number of visited states is reached, the oldest
+ one is removed according to its number (= with the min number) */
+ XBT_DEBUG("Replace visited state %d with the new visited state %d",
+ old_state->num, new_state->num);
+
+ visited_state = std::move(new_state);
+ return std::move(old_state);
}
+ }
- XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, (unsigned long) visited_states.size());
- visited_states.insert(range.first, std::move(new_state));
- prune_visited_states();
+ XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, (unsigned long) states_.size());
+ states_.insert(range.first, std::move(new_state));
+ this->prune();
return nullptr;
}
--- /dev/null
+/* Copyright (c) 2007-2016. The SimGrid Team.
+ * All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_VISITED_STATE_HPP
+#define SIMGRID_MC_VISITED_STATE_HPP
+
+#include <cstddef>
+
+#include <memory>
+
+#include "src/mc/mc_snapshot.h"
+
+namespace simgrid {
+namespace mc {
+
+struct XBT_PRIVATE VisitedState {
+ std::shared_ptr<simgrid::mc::Snapshot> system_state = nullptr;
+ std::size_t heap_bytes_used = 0;
+ int nb_processes = 0;
+ int num = 0;
+ int other_num = 0; // dot_output for
+
+ VisitedState();
+ ~VisitedState();
+};
+
+class XBT_PRIVATE VisitedStates {
+ std::vector<std::unique_ptr<simgrid::mc::VisitedState>> states_;
+public:
+ void clear() { states_.clear(); }
+ std::unique_ptr<simgrid::mc::VisitedState> addVisitedState(simgrid::mc::State* graph_state, bool compare_snpashots);
+private:
+ void prune();
+};
+
+}
+}
+
+#endif
char mc_replay_mode = false;
mc_stats_t mc_stats = nullptr;
-xbt_fifo_t mc_stack = nullptr;
/* Liveness */
simgrid::mc::processes_time.clear();
}
+namespace simgrid {
+namespace mc {
+
/**
* \brief Re-executes from the state at position start all the transitions indicated by
* a given model-checker stack.
* \param stack The stack with the transitions to execute.
* \param start Start index to begin the re-execution.
*/
-void MC_replay(xbt_fifo_t stack)
+void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack)
{
- int value, count = 1;
- char *req_str;
- smx_simcall_t req = nullptr, saved_req = NULL;
- xbt_fifo_item_t item, start_item;
- 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 = (simgrid::mc::State*)xbt_fifo_get_item_content(start_item);
- if(state->system_state){
+ simgrid::mc::State* state = stack.back().get();
+ if (state->system_state) {
simgrid::mc::restore_snapshot(state->system_state);
if(_sg_mc_comms_determinism || _sg_mc_send_determinism)
MC_restore_communications_pattern(state);
/* At the moment of taking the snapshot the raw heap was set, so restoring
* it will set it back again, we have to unset it to continue */
- start_item = xbt_fifo_get_last_item(stack);
-
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
// int n = xbt_dynar_length(incomplete_communications_pattern);
unsigned n = MC_smx_get_maxpid();
}
}
+ int count = 1;
+
/* Traverse the stack from the state at position start and re-execute the transitions */
- for (item = start_item;
- item != xbt_fifo_get_first_item(stack);
- item = xbt_fifo_get_prev_item(item)) {
+ for (std::unique_ptr<simgrid::mc::State> const& state : stack) {
+ if (state == stack.back())
+ break;
- state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
- saved_req = MC_state_get_executed_request(state, &value);
+ int value;
+ smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
if (saved_req) {
/* because we got a copy of the executed request, we have to fetch the
real one, pointed by the request field of the issuer process */
const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
- req = &issuer->simcall;
+ smx_simcall_t req = &issuer->simcall;
/* Debug information */
if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
- req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
- XBT_DEBUG("Replay: %s (%p)", req_str, state);
+ char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
+ XBT_DEBUG("Replay: %s (%p)", req_str, state.get());
xbt_free(req_str);
}
XBT_DEBUG("**** End Replay ****");
}
+}
+}
+
void MC_show_deadlock(void)
{
XBT_INFO("**************************");
#include <xbt/fifo.h>
#include <xbt/config.h>
#include <xbt/base.h>
+#include <xbt/automaton.h>
#include "mc/mc.h"
#include "mc/datatypes.h"
XBT_PRIVATE extern int user_max_depth_reached;
-XBT_PRIVATE void MC_replay(xbt_fifo_t stack);
XBT_PRIVATE void MC_show_deadlock(void);
-/** 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`).
- */
-XBT_PRIVATE extern xbt_fifo_t mc_stack;
-
/****************************** Statistics ************************************/
typedef struct mc_stats {
extern XBT_PRIVATE simgrid::mc::ReductionMode reduction_mode;
-struct XBT_PRIVATE VisitedState {
- std::shared_ptr<simgrid::mc::Snapshot> system_state = nullptr;
- size_t heap_bytes_used = 0;
- int nb_processes = 0;
- int num = 0;
- int other_num = 0; // dot_output for
-
- VisitedState();
- ~VisitedState();
-};
-
-extern XBT_PRIVATE std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
-XBT_PRIVATE std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(simgrid::mc::State* graph_state, bool compare_snpashots);
-
}
}
#ifndef SIMGRID_MC_STATE_H
#define SIMGRID_MC_STATE_H
+#include <list>
#include <memory>
#include <xbt/base.h>
~State();
};
+XBT_PRIVATE void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack);
+
}
}
#include "src/mc/mc_exit.h"
#include "src/mc/Session.hpp"
#include "src/mc/Checker.hpp"
-#include "src/mc/CommunicationDeterminismChecker.hpp"
-#include "src/mc/SafetyChecker.hpp"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
{
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
return std::unique_ptr<simgrid::mc::Checker>(
- new simgrid::mc::CommunicationDeterminismChecker(session));
+ simgrid::mc::createCommunicationDeterminismChecker(session));
else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
return std::unique_ptr<simgrid::mc::Checker>(
- new simgrid::mc::SafetyChecker(session));
+ simgrid::mc::createSafetyChecker(session));
else
return std::unique_ptr<simgrid::mc::Checker>(
simgrid::mc::createLivenessChecker(session));
XBT_LOG_CONNECT(mc_page_snapshot);
XBT_LOG_CONNECT(mc_request);
XBT_LOG_CONNECT(mc_safety);
- XBT_LOG_CONNECT(mc_visited);
+ XBT_LOG_CONNECT(mc_VisitedState);
XBT_LOG_CONNECT(mc_client);
XBT_LOG_CONNECT(mc_client_api);
XBT_LOG_CONNECT(mc_comm_pattern);
src/mc/mc_safety.h
src/mc/mc_state.h
src/mc/mc_state.cpp
- src/mc/mc_visited.cpp
+ src/mc/VisitedState.cpp
+ src/mc/VisitedState.hpp
src/mc/mc_client_api.cpp
src/mc/mc_protocol.h
src/mc/mc_protocol.cpp
