#include "src/mc/Checker.hpp"
#include "src/mc/SafetyChecker.hpp"
#include "src/mc/VisitedState.hpp"
+#include "src/mc/Transition.hpp"
+#include "src/mc/Session.hpp"
#include "src/xbt/mmalloc/mmprivate.h"
XBT_INFO("Counter-example execution trace:");
for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
XBT_INFO("%s", s.c_str());
- MC_print_statistics(mc_stats);
+ simgrid::mc::session->logState();
}
static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
bool SafetyChecker::checkNonTermination(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);
+ for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
+ if (snapshot_compare(state->get(), current_state) == 0) {
+ XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num, current_state->num);
return true;
}
return false;
{
RecordTrace res;
for (auto const& state : stack_)
- res.push_back(state->getRecordElement());
+ res.push_back(state->getTransition());
return res;
}
{
std::vector<std::string> trace;
for (auto const& state : stack_) {
- int value = state->req_num;
+ int value = state->transition.argument;
smx_simcall_t req = &state->executed_req;
if (req)
trace.push_back(simgrid::mc::request_to_string(
return trace;
}
+void SafetyChecker::logState() // override
+{
+ Checker::logState();
+ XBT_INFO("Expanded states = %lu", expandedStatesCount_);
+ XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
+ XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
+}
+
int SafetyChecker::run()
{
- this->init();
+ /* This function runs the DFS algorithm the state space.
+ * We do so iteratively instead of recursively, dealing with the call stack manually.
+ * This allows to explore the call stack when we want to. */
while (!stack_.empty()) {
simgrid::mc::State* state = stack_.back().get();
XBT_DEBUG("**************************************************");
- XBT_DEBUG(
- "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
- stack_.size(), state, state->num,
- state->interleaveSize());
-
- mc_stats->visited_states++;
-
- // The interleave set is empty or the maximum depth is reached,
- // let's back-track.
- smx_simcall_t req = nullptr;
- if (stack_.size() > (std::size_t) _sg_mc_max_depth
- || (req = MC_state_get_request(state)) == nullptr
- || visitedState_ != nullptr) {
+ XBT_DEBUG("Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
+ stack_.size(), state, state->num, state->interleaveSize());
+
+ mc_model_checker->visited_states++;
+
+ // Backtrack if we reached the maximum depth
+ if (stack_.size() > (std::size_t)_sg_mc_max_depth) {
+ XBT_WARN("/!\\ Max depth reached ! /!\\ ");
int res = this->backtrack();
if (res)
return res;
continue;
}
- int req_num = state->req_num;
+ // Backtrack if we are revisiting a state we saw previously
+ if (visitedState_ != nullptr) {
+ XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
+ visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
+
+ visitedState_ = nullptr;
+ int res = this->backtrack();
+ if (res)
+ return res;
+ else
+ continue;
+ }
+
+ smx_simcall_t req = MC_state_get_request(state);
+ // Backtrack if the interleave set is empty
+ if (req == nullptr) {
+ XBT_DEBUG("There are no more processes to interleave. (depth %zi)", stack_.size() + 1);
+
+ int res = this->backtrack();
+ if (res)
+ return res;
+ else
+ continue;
+ }
// If there are processes to interleave and the maximum depth has not been
// reached then perform one step of the exploration algorithm.
XBT_DEBUG("Execute: %s",
simgrid::mc::request_to_string(
- req, req_num, simgrid::mc::RequestType::simix).c_str());
+ req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
std::string req_str;
if (dot_output != nullptr)
- req_str = simgrid::mc::request_get_dot_output(req, req_num);
-
- mc_stats->executed_transitions++;
+ req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
- // TODO, bundle both operations in a single message
- // MC_execute_transition(req, req_num)
+ mc_model_checker->executed_transitions++;
/* Answer the request */
- simgrid::mc::handle_simcall(req, req_num);
- mc_model_checker->wait_for_requests();
+ this->getSession().execute(state->transition);
/* Create the new expanded state */
std::unique_ptr<simgrid::mc::State> next_state =
- std::unique_ptr<simgrid::mc::State>(MC_state_new());
+ std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
MC_show_non_termination();
return SIMGRID_MC_EXIT_NON_TERMINATION;
}
- if (_sg_mc_visited == 0
- || (visitedState_ = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
+ /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
+ if (_sg_mc_visited == true)
+ visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true);
+
+ /* If this is a new state (or if we don't care about state-equality reduction) */
+ if (_sg_mc_visited == 0 || visitedState_ == 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)) {
- next_state->interleave(&p.copy);
- if (reductionMode_ != simgrid::mc::ReductionMode::none)
+ for (auto& actor : mc_model_checker->process().actors())
+ if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
+ next_state->interleave(actor.copy.getBuffer());
+ if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
break;
}
}
XBT_INFO("No property violation found.");
- MC_print_statistics(mc_stats);
- initial_global_state = nullptr;
+ simgrid::mc::session->logState();
return SIMGRID_MC_EXIT_SUCCESS;
}
int SafetyChecker::backtrack()
{
- if (stack_.size() > (std::size_t) _sg_mc_max_depth
- || visitedState_ != nullptr) {
- if (visitedState_ == nullptr)
- XBT_WARN("/!\\ Max depth reached ! /!\\ ");
- else
- XBT_DEBUG("State already visited (equal to state %d),"
- " exploration stopped on this path.",
- visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
- } else
- XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
- stack_.size() + 1);
-
stack_.pop_back();
- visitedState_ = nullptr;
-
/* Check for deadlocks */
if (mc_model_checker->checkDeadlock()) {
MC_show_deadlock();
/* Traverse the stack backwards until a state with a non empty interleave
set is found, deleting all the states that have it empty in the way.
- For each deleted state, check if the request that has generated it
- (from it's predecesor state), depends on any other previous request
+ For each deleted state, check if the request that has generated it
+ (from it's predecessor state), depends on any other previous request
executed before it. If it does then add it to the interleave set of the
state that executed that previous request. */
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);
+ 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();
- if (reductionMode_ != simgrid::mc::ReductionMode::none
- && simgrid::mc::request_depend(req, &prev_state->internal_req)) {
+ if (simgrid::mc::request_depend(req, &prev_state->internal_req)) {
if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
XBT_DEBUG("Dependent Transitions:");
- int value = prev_state->req_num;
+ int value = prev_state->transition.argument;
smx_simcall_t prev_req = &prev_state->executed_req;
XBT_DEBUG("%s (state=%d)",
simgrid::mc::request_to_string(
prev_req, value, simgrid::mc::RequestType::internal).c_str(),
prev_state->num);
- value = state->req_num;
+ value = state->transition.argument;
prev_req = &state->executed_req;
XBT_DEBUG("%s (state=%d)",
simgrid::mc::request_to_string(
} else {
- const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
+ const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
req->call, issuer->pid, state->num,
prev_state->internal_req.call,
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_);
+ this->restoreState();
XBT_DEBUG("Back-tracking to state %d at depth %zi done",
stack_.back()->num, stack_.size());
break;
return SIMGRID_MC_EXIT_SUCCESS;
}
-void SafetyChecker::init()
+void SafetyChecker::restoreState()
+{
+ /* Intermediate backtracking */
+ simgrid::mc::State* state = stack_.back().get();
+ if (state->system_state) {
+ simgrid::mc::restore_snapshot(state->system_state);
+ return;
+ }
+
+ /* Restore the initial state */
+ simgrid::mc::session->restoreInitialState();
+
+ /* Traverse the stack from the state at position start and re-execute the transitions */
+ for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
+ if (state == stack_.back())
+ break;
+ session->execute(state->transition);
+ /* Update statistics */
+ mc_model_checker->visited_states++;
+ mc_model_checker->executed_transitions++;
+ }
+}
+
+SafetyChecker::SafetyChecker(Session& session) : Checker(session)
{
reductionMode_ = simgrid::mc::reduction_mode;
- if( _sg_mc_termination)
+ if (_sg_mc_termination)
reductionMode_ = simgrid::mc::ReductionMode::none;
else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
reductionMode_ = simgrid::mc::ReductionMode::dpor;
XBT_INFO("Check non progressive cycles");
else
XBT_INFO("Check a safety property");
- mc_model_checker->wait_for_requests();
+ simgrid::mc::session->initialize();
XBT_DEBUG("Starting the safety algorithm");
std::unique_ptr<simgrid::mc::State> initial_state =
- std::unique_ptr<simgrid::mc::State>(MC_state_new());
+ std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
XBT_DEBUG("**************************************************");
XBT_DEBUG("Initial state");
- /* Wait for requests (schedules processes) */
- mc_model_checker->wait_for_requests();
-
- /* 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)) {
- initial_state->interleave(&p.copy);
+ /* Get an enabled actor and insert it in the interleave set of the initial state */
+ for (auto& actor : mc_model_checker->process().actors())
+ if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
+ initial_state->interleave(actor.copy.getBuffer());
if (reductionMode_ != simgrid::mc::ReductionMode::none)
break;
}
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());
- initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
-}
-
-SafetyChecker::SafetyChecker(Session& session) : Checker(session)
-{
}
SafetyChecker::~SafetyChecker()
