-/* Copyright (c) 2016-2019. The SimGrid Team. All rights reserved. */
+/* Copyright (c) 2016-2020. 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. */
namespace simgrid {
namespace mc {
-void SafetyChecker::check_non_termination(State* current_state)
+void SafetyChecker::check_non_termination(const State* current_state)
{
for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
- if (snapshot_equal((*state)->system_state.get(), current_state->system_state.get())) {
+ if (snapshot_equal((*state)->system_state_.get(), current_state->system_state_.get())) {
XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num_, current_state->num_);
XBT_INFO("******************************************");
XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
for (auto const& state : stack_) {
int value = state->transition_.argument_;
smx_simcall_t req = &state->executed_req_;
- if (req)
- trace.push_back(request_to_string(req, value, RequestType::executed));
+ trace.push_back(request_to_string(req, value, RequestType::executed));
}
return trace;
}
this->get_session().execute(state->transition_);
/* Create the new expanded state (copy the state of MCed into our MCer data) */
- std::unique_ptr<State> next_state = std::unique_ptr<State>(new State(++expanded_states_count_));
+ ++expanded_states_count_;
+ auto next_state = std::make_unique<State>(expanded_states_count_);
if (_sg_mc_termination)
this->check_non_termination(next_state.get());
/* If this is a new state (or if we don't care about state-equality reduction) */
if (visited_state_ == nullptr) {
/* Get an enabled process and insert it in the interleave set of the next state */
- for (auto& remoteActor : mc_model_checker->process().actors()) {
+ for (auto& remoteActor : mc_model_checker->get_remote_simulation().actors()) {
auto actor = remoteActor.copy.get_buffer();
if (actor_is_enabled(actor)) {
next_state->add_interleaving_set(actor);
std::unique_ptr<State> state = std::move(stack_.back());
stack_.pop_back();
if (reductionMode_ == ReductionMode::dpor) {
- smx_simcall_t req = &state->internal_req;
- if (req->call_ == SIMCALL_MUTEX_LOCK || req->call_ == SIMCALL_MUTEX_TRYLOCK)
+ smx_simcall_t req = &state->internal_req_;
+ if (req->call_ == simix::Simcall::MUTEX_LOCK || req->call_ == simix::Simcall::MUTEX_TRYLOCK)
xbt_die("Mutex is currently not supported with DPOR, use --cfg=model-check/reduction:none");
- const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
+ const kernel::actor::ActorImpl* issuer = MC_smx_simcall_get_issuer(req);
for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
State* prev_state = i->get();
- if (request_depend(req, &prev_state->internal_req)) {
+ if (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
XBT_DEBUG("Process %p is in done set", req->issuer_);
break;
- } else if (req->issuer_ == prev_state->internal_req.issuer_) {
+ } else if (req->issuer_ == prev_state->internal_req_.issuer_) {
XBT_DEBUG("Simcall %s and %s with same issuer", SIMIX_simcall_name(req->call_),
- SIMIX_simcall_name(prev_state->internal_req.call_));
+ SIMIX_simcall_name(prev_state->internal_req_.call_));
break;
} else {
- const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
+ const kernel::actor::ActorImpl* previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req_);
XBT_DEBUG("Simcall %s, process %ld (state %d) and simcall %s, process %ld (state %d) are independent",
SIMIX_simcall_name(req->call_), issuer->get_pid(), state->num_,
- SIMIX_simcall_name(prev_state->internal_req.call_), previous_issuer->get_pid(), prev_state->num_);
+ SIMIX_simcall_name(prev_state->internal_req_.call_), previous_issuer->get_pid(), prev_state->num_);
}
}
}
void SafetyChecker::restore_state()
{
/* Intermediate backtracking */
- State* last_state = stack_.back().get();
- if (last_state->system_state) {
- last_state->system_state->restore(&mc_model_checker->process());
+ const State* last_state = stack_.back().get();
+ if (last_state->system_state_) {
+ last_state->system_state_->restore(&mc_model_checker->get_remote_simulation());
return;
}
XBT_DEBUG("Starting the safety algorithm");
- std::unique_ptr<State> initial_state = std::unique_ptr<State>(new State(++expanded_states_count_));
+ ++expanded_states_count_;
+ auto initial_state = std::make_unique<State>(expanded_states_count_);
XBT_DEBUG("**************************************************");
XBT_DEBUG("Initial state");
/* Get an enabled actor and insert it in the interleave set of the initial state */
- for (auto& actor : mc_model_checker->process().actors())
+ for (auto& actor : mc_model_checker->get_remote_simulation().actors())
if (actor_is_enabled(actor.copy.get_buffer())) {
initial_state->add_interleaving_set(actor.copy.get_buffer());
if (reductionMode_ != ReductionMode::none)