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
[mc] Get rid of the ugly "value" out parameter in MC_state_get_request()
[simgrid.git]
/
src
/
mc
/
SafetyChecker.cpp
diff --git
a/src/mc/SafetyChecker.cpp
b/src/mc/SafetyChecker.cpp
index
7cdceed
..
8055c65
100644
(file)
--- a/
src/mc/SafetyChecker.cpp
+++ b/
src/mc/SafetyChecker.cpp
@@
-76,8
+76,8
@@
std::vector<std::string> SafetyChecker::getTextualTrace() // override
{
std::vector<std::string> trace;
for (auto const& state : stack_) {
- int value;
- smx_simcall_t req =
MC_state_get_executed_request(state.get(), &value)
;
+ int value
= state->req_num
;
+ smx_simcall_t req =
&state->executed_req
;
if (req)
trace.push_back(simgrid::mc::request_to_string(
req, value, simgrid::mc::RequestType::executed));
@@
-89,8
+89,6
@@
int SafetyChecker::run()
{
this->init();
- int value;
-
while (!stack_.empty()) {
/* Get current state */
@@
-108,7
+106,7
@@
int SafetyChecker::run()
// 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
, &value
)) == nullptr
+ || (req = MC_state_get_request(state)) == nullptr
|| visitedState_ != nullptr) {
int res = this->backtrack();
if (res)
@@
-117,23
+115,25
@@
int SafetyChecker::run()
continue;
}
+ int req_num = state->req_num;
+
// 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,
value
, simgrid::mc::RequestType::simix).c_str());
+ req,
req_num
, simgrid::mc::RequestType::simix).c_str());
std::string req_str;
if (dot_output != nullptr)
- req_str = simgrid::mc::request_get_dot_output(req,
value
);
+ req_str = simgrid::mc::request_get_dot_output(req,
req_num
);
mc_stats->executed_transitions++;
// TODO, bundle both operations in a single message
- // MC_execute_transition(req,
value
)
+ // MC_execute_transition(req,
req_num
)
/* Answer the request */
- simgrid::mc::handle_simcall(req,
value
);
+ simgrid::mc::handle_simcall(req,
req_num
);
mc_model_checker->wait_for_requests();
/* Create the new expanded state */
@@
-209,7
+209,7
@@
int SafetyChecker::backtrack()
std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
stack_.pop_back();
if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
- smx_simcall_t req =
MC_state_get_internal_request(state.get())
;
+ smx_simcall_t req =
&state->internal_req
;
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");
@@
-217,16
+217,17
@@
int SafetyChecker::backtrack()
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)
)) {
+ && 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;
- smx_simcall_t prev_req =
MC_state_get_executed_request(prev_state, &value)
;
+ int value
= prev_state->req_num
;
+ 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);
- prev_req = MC_state_get_executed_request(state.get(), &value);
+ value = state->req_num;
+ prev_req = &state->executed_req;
XBT_DEBUG("%s (state=%d)",
simgrid::mc::request_to_string(
prev_req, value, simgrid::mc::RequestType::executed).c_str(),
@@
-240,17
+241,17
@@
int SafetyChecker::backtrack()
break;
- } else if (req->issuer ==
MC_state_get_internal_request(prev_state)->
issuer) {
+ } else if (req->issuer ==
prev_state->internal_req.
issuer) {
- XBT_DEBUG("Simcall %d and %d with same issuer", req->call,
MC_state_get_internal_request(prev_state)->
call);
+ XBT_DEBUG("Simcall %d and %d with same issuer", req->call,
prev_state->internal_req.
call);
break;
} else {
- const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(
MC_state_get_internal_request(prev_state)
);
+ const smx_process_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,
-
MC_state_get_internal_request(prev_state)->
call,
+
prev_state->internal_req.
call,
previous_issuer->pid,
prev_state->num);