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;
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());
+ XBT_DEBUG("Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
+ stack_.size(), state, state->num, state->interleaveSize());
mc_model_checker->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) {
+ // 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;
+ else
+ continue;
+ }
+
+ // 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;
/* Create the new expanded state */
std::unique_ptr<simgrid::mc::State> next_state =
- std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
+ 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(expandedStatesCount_, 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;
}
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->transition.argument;
} 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,
void SafetyChecker::restoreState()
{
/* Intermediate backtracking */
- {
- simgrid::mc::State* state = stack_.back().get();
- if (state->system_state) {
- simgrid::mc::restore_snapshot(state->system_state);
- return;
- }
+ simgrid::mc::State* state = stack_.back().get();
+ if (state->system_state) {
+ simgrid::mc::restore_snapshot(state->system_state);
+ return;
}
/* Restore the initial state */
}
}
-void SafetyChecker::init()
+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_DEBUG("Starting the safety algorithm");
std::unique_ptr<simgrid::mc::State> initial_state =
- std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
+ std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
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)) {
- 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));
}
-SafetyChecker::SafetyChecker(Session& session) : Checker(session)
-{
-}
-
SafetyChecker::~SafetyChecker()
{
}