A
lgorithmique
N
umérique
D
istribuée
Public GIT Repository
projects
/
simgrid.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
| inline |
side by side
Merge branch 'master' into 'master'
[simgrid.git]
/
src
/
mc
/
checker
/
SafetyChecker.cpp
diff --git
a/src/mc/checker/SafetyChecker.cpp
b/src/mc/checker/SafetyChecker.cpp
index
d64486a
..
c08ecaa
100644
(file)
--- a/
src/mc/checker/SafetyChecker.cpp
+++ b/
src/mc/checker/SafetyChecker.cpp
@@
-35,7
+35,7
@@
void SafetyChecker::check_non_termination(simgrid::mc::State* current_state)
{
for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
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("Non-progressive cycle: state %d -> state %d", (*state)->num
_, current_state->num_
);
XBT_INFO("******************************************");
XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
XBT_INFO("******************************************");
@@
-53,7
+53,7
@@
RecordTrace SafetyChecker::get_record_trace() // override
{
RecordTrace res;
for (auto const& state : stack_)
- res.push_back(state->get
T
ransition());
+ res.push_back(state->get
_t
ransition());
return res;
}
@@
-61,8
+61,8
@@
std::vector<std::string> SafetyChecker::get_textual_trace() // override
{
std::vector<std::string> trace;
for (auto const& state : stack_) {
- int value
= state->transition.argument
;
- smx_simcall_t req = &state->executed_req;
+ int value
= state->transition_.argument_
;
+ smx_simcall_t req = &state->executed_req
_
;
if (req)
trace.push_back(simgrid::mc::request_to_string(
req, value, simgrid::mc::RequestType::executed));
@@
-81,7
+81,7
@@
void SafetyChecker::run()
{
/* 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 at wish
. */
+ * This allows
one to explore the call stack at will
. */
while (not stack_.empty()) {
@@
-89,8
+89,8
@@
void SafetyChecker::run()
simgrid::mc::State* state = stack_.back().get();
XBT_DEBUG("**************************************************");
- XBT_
DEBUG("Exploration depth=%zu (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num
,
-
state->interleaveS
ize());
+ XBT_
VERB("Exploration depth=%zu (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num_
,
+
state->interleave_s
ize());
mc_model_checker->visited_states++;
@@
-113,7
+113,7
@@
void SafetyChecker::run()
// Search an enabled transition in the current state; backtrack if the interleave set is empty
// get_request also sets state.transition to be the one corresponding to the returned req
- smx_simcall_t req = MC_state_
get
_request(state);
+ smx_simcall_t req = MC_state_
choose
_request(state);
// req is now the transition of the process that was selected to be executed
if (req == nullptr) {
@@
-125,18
+125,18
@@
void SafetyChecker::run()
// 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, state->transition.argument
, simgrid::mc::RequestType::simix).c_str());
+ XBT_DEBUG(
+ "Execute: %s",
+
simgrid::mc::request_to_string(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, state->transition
.argument
);
+ req_str = simgrid::mc::request_get_dot_output(req, state->transition
_.argument_
);
mc_model_checker->executed_transitions++;
/* Actually answer the request: let execute the selected request (MCed does one step) */
- this->get_session().execute(state->transition);
+ this->get_session().execute(state->transition
_
);
/* Create the new expanded state (copy the state of MCed into our MCer data) */
std::unique_ptr<simgrid::mc::State> next_state =
@@
-156,18
+156,17
@@
void SafetyChecker::run()
for (auto& remoteActor : mc_model_checker->process().actors()) {
auto actor = remoteActor.copy.get_buffer();
if (simgrid::mc::actor_is_enabled(actor)) {
- next_state->add
InterleavingS
et(actor);
+ next_state->add
_interleaving_s
et(actor);
if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
break; // With DPOR, we take the first enabled transition
}
}
if (dot_output != nullptr)
- std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
- state->num, next_state->num, req_str.c_str());
+ std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num_, next_state->num_, req_str.c_str());
} else if (dot_output != nullptr)
- std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
+ std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num
_
,
visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num,
req_str.c_str());
@@
-200,7
+199,7
@@
void SafetyChecker::backtrack()
stack_.pop_back();
if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
smx_simcall_t req = &state->internal_req;
- if (req->call
== SIMCALL_MUTEX_LOCK || req->call
== SIMCALL_MUTEX_TRYLOCK)
+ 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_actor_t issuer = MC_smx_simcall_get_issuer(req);
@@
-209,52
+208,50
@@
void SafetyChecker::backtrack()
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
;
- smx_simcall_t prev_req = &prev_state->executed_req;
+ 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->transition.argument;
- prev_req = &state->executed_req;
+ simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal).c_str(),
+ prev_state->num_);
+ value = state->transition_.argument_;
+ prev_req = &state->executed_req_;
XBT_DEBUG("%s (state=%d)",
- simgrid::mc::request_to_string(
- prev_req, value, simgrid::mc::RequestType::executed).c_str(),
- state->num);
+ simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed).c_str(),
+ state->num_);
}
- if (not prev_state->actor
States[issuer->get_pid()].isD
one())
- prev_state->add
InterleavingS
et(issuer);
+ if (not prev_state->actor
_states_[issuer->get_pid()].is_d
one())
+ prev_state->add
_interleaving_s
et(issuer);
else
- XBT_DEBUG("Process %p is in done set", req->issuer);
+ 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 %d and %d with same issuer", req->call, prev_state->internal_req.call);
+ XBT_DEBUG("Simcall %s and %s with same issuer", SIMIX_simcall_name(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);
- XBT_DEBUG("Simcall %
d, process %ld (state %d) and simcall %d
, process %ld (state %d) are independent",
-
req->call, issuer->get_pid(), state->num, prev_state->internal_req.call, previous_issuer->get_pid()
,
-
prev_state->num
);
+ 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_
);
}
}
}
- if (state->interleaveSize()
- && stack_.size() < (std::size_t) _sg_mc_max_depth) {
+ if (state->interleave_size() && 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 %zu", state->num, stack_.size() + 1);
+ XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num
_
, stack_.size() + 1);
stack_.push_back(std::move(state));
this->restore_state();
- XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num, stack_.size());
+ XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num
_
, stack_.size());
break;
} else {
- XBT_DEBUG("Delete state %d at depth %zu", state->num, stack_.size() + 1);
+ XBT_DEBUG("Delete state %d at depth %zu", state->num
_
, stack_.size() + 1);
}
}
}
@@
-275,7
+272,7
@@
void SafetyChecker::restore_state()
for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
if (state == stack_.back())
break;
- session->execute(state->transition);
+ session->execute(state->transition
_
);
/* Update statistics */
mc_model_checker->visited_states++;
mc_model_checker->executed_transitions++;
@@
-309,7
+306,7
@@
SafetyChecker::SafetyChecker(Session& s) : Checker(s)
/* 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.get_buffer())) {
- initial_state->add
InterleavingS
et(actor.copy.get_buffer());
+ initial_state->add
_interleaving_s
et(actor.copy.get_buffer());
if (reductionMode_ != simgrid::mc::ReductionMode::none)
break;
}