1 /* Copyright (c) 2016. The SimGrid Team.
2 * All rights reserved. */
4 /* This program is free software; you can redistribute it and/or modify it
5 * under the terms of the license (GNU LGPL) which comes with this package. */
15 #include <xbt/sysdep.h>
17 #include "src/mc/Session.hpp"
18 #include "src/mc/Transition.hpp"
19 #include "src/mc/VisitedState.hpp"
20 #include "src/mc/checker/SafetyChecker.hpp"
21 #include "src/mc/mc_exit.h"
22 #include "src/mc/mc_private.h"
23 #include "src/mc/mc_record.h"
24 #include "src/mc/mc_request.h"
25 #include "src/mc/mc_smx.h"
27 #include "src/xbt/mmalloc/mmprivate.h"
29 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
30 "Logging specific to MC safety verification ");
34 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
36 simgrid::mc::Snapshot* s1 = state1->system_state.get();
37 simgrid::mc::Snapshot* s2 = state2->system_state.get();
38 int num1 = state1->num;
39 int num2 = state2->num;
40 return snapshot_compare(num1, s1, num2, s2);
43 void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
45 for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
46 if (snapshot_compare(state->get(), current_state) == 0) {
47 XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num, current_state->num);
48 XBT_INFO("******************************************");
49 XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
50 XBT_INFO("******************************************");
51 XBT_INFO("Counter-example execution trace:");
52 for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
53 XBT_INFO("%s", s.c_str());
54 simgrid::mc::session->logState();
56 throw simgrid::mc::TerminationError();
60 RecordTrace SafetyChecker::getRecordTrace() // override
63 for (auto const& state : stack_)
64 res.push_back(state->getTransition());
68 std::vector<std::string> SafetyChecker::getTextualTrace() // override
70 std::vector<std::string> trace;
71 for (auto const& state : stack_) {
72 int value = state->transition.argument;
73 smx_simcall_t req = &state->executed_req;
75 trace.push_back(simgrid::mc::request_to_string(
76 req, value, simgrid::mc::RequestType::executed));
81 void SafetyChecker::logState() // override
84 XBT_INFO("Expanded states = %lu", expandedStatesCount_);
85 XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
86 XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
89 void SafetyChecker::run()
91 /* This function runs the DFS algorithm the state space.
92 * We do so iteratively instead of recursively, dealing with the call stack manually.
93 * This allows to explore the call stack at wish. */
95 while (not stack_.empty()) {
97 /* Get current state */
98 simgrid::mc::State* state = stack_.back().get();
100 XBT_DEBUG("**************************************************");
101 XBT_DEBUG("Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
102 stack_.size(), state, state->num, state->interleaveSize());
104 mc_model_checker->visited_states++;
106 // Backtrack if we reached the maximum depth
107 if (stack_.size() > (std::size_t)_sg_mc_max_depth) {
108 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
113 // Backtrack if we are revisiting a state we saw previously
114 if (visitedState_ != nullptr) {
115 XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
116 visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num);
118 visitedState_ = nullptr;
123 // Search an enabled transition in the current state; backtrack if the interleave set is empty
124 // get_request also sets state.transition to be the one corresponding to the returned req
125 smx_simcall_t req = MC_state_get_request(state);
126 // req is now the transition of the process that was selected to be executed
128 if (req == nullptr) {
129 XBT_DEBUG("There are no more processes to interleave. (depth %zi)", stack_.size() + 1);
135 // If there are processes to interleave and the maximum depth has not been
136 // reached then perform one step of the exploration algorithm.
137 XBT_DEBUG("Execute: %s",
138 simgrid::mc::request_to_string(
139 req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
142 if (dot_output != nullptr)
143 req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
145 mc_model_checker->executed_transitions++;
147 /* Actually answer the request: let execute the selected request (MCed does one step) */
148 this->getSession().execute(state->transition);
150 /* Create the new expanded state (copy the state of MCed into our MCer data) */
151 std::unique_ptr<simgrid::mc::State> next_state =
152 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
154 if (_sg_mc_termination)
155 this->checkNonTermination(next_state.get());
157 /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
158 if (_sg_mc_max_visited_states > 0)
159 visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true);
161 /* If this is a new state (or if we don't care about state-equality reduction) */
162 if (visitedState_ == nullptr) {
164 /* Get an enabled process and insert it in the interleave set of the next state */
165 for (auto& actor : mc_model_checker->process().actors())
166 if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
167 next_state->interleave(actor.copy.getBuffer());
168 if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
172 if (dot_output != nullptr)
173 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
174 state->num, next_state->num, req_str.c_str());
176 } else if (dot_output != nullptr)
177 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
178 visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num,
181 stack_.push_back(std::move(next_state));
184 XBT_INFO("No property violation found.");
185 simgrid::mc::session->logState();
188 void SafetyChecker::backtrack()
192 /* Check for deadlocks */
193 if (mc_model_checker->checkDeadlock()) {
195 throw simgrid::mc::DeadlockError();
198 /* Traverse the stack backwards until a state with a non empty interleave
199 set is found, deleting all the states that have it empty in the way.
200 For each deleted state, check if the request that has generated it
201 (from it's predecessor state), depends on any other previous request
202 executed before it. If it does then add it to the interleave set of the
203 state that executed that previous request. */
205 while (not stack_.empty()) {
206 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
208 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
209 smx_simcall_t req = &state->internal_req;
210 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
211 xbt_die("Mutex is currently not supported with DPOR, use --cfg=model-check/reduction:none");
213 const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
214 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
215 simgrid::mc::State* prev_state = i->get();
216 if (simgrid::mc::request_depend(req, &prev_state->internal_req)) {
217 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
218 XBT_DEBUG("Dependent Transitions:");
219 int value = prev_state->transition.argument;
220 smx_simcall_t prev_req = &prev_state->executed_req;
221 XBT_DEBUG("%s (state=%d)",
222 simgrid::mc::request_to_string(
223 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
225 value = state->transition.argument;
226 prev_req = &state->executed_req;
227 XBT_DEBUG("%s (state=%d)",
228 simgrid::mc::request_to_string(
229 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
233 if (not prev_state->actorStates[issuer->pid].isDone())
234 prev_state->interleave(issuer);
236 XBT_DEBUG("Process %p is in done set", req->issuer);
240 } else if (req->issuer == prev_state->internal_req.issuer) {
242 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, prev_state->internal_req.call);
247 const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
248 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independent",
249 req->call, issuer->pid, state->num,
250 prev_state->internal_req.call,
251 previous_issuer->pid,
258 if (state->interleaveSize()
259 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
260 /* We found a back-tracking point, let's loop */
261 XBT_DEBUG("Back-tracking to state %d at depth %zi", state->num, stack_.size() + 1);
262 stack_.push_back(std::move(state));
263 this->restoreState();
264 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
265 stack_.back()->num, stack_.size());
268 XBT_DEBUG("Delete state %d at depth %zi",
269 state->num, stack_.size() + 1);
274 void SafetyChecker::restoreState()
276 /* Intermediate backtracking */
277 simgrid::mc::State* state = stack_.back().get();
278 if (state->system_state) {
279 simgrid::mc::restore_snapshot(state->system_state);
283 /* Restore the initial state */
284 simgrid::mc::session->restoreInitialState();
286 /* Traverse the stack from the state at position start and re-execute the transitions */
287 for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
288 if (state == stack_.back())
290 session->execute(state->transition);
291 /* Update statistics */
292 mc_model_checker->visited_states++;
293 mc_model_checker->executed_transitions++;
297 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
299 reductionMode_ = simgrid::mc::reduction_mode;
300 if (_sg_mc_termination)
301 reductionMode_ = simgrid::mc::ReductionMode::none;
302 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
303 reductionMode_ = simgrid::mc::ReductionMode::dpor;
305 if (_sg_mc_termination)
306 XBT_INFO("Check non progressive cycles");
308 XBT_INFO("Check a safety property. Reduction is: %s.",
309 (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
310 (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
311 simgrid::mc::session->initialize();
313 XBT_DEBUG("Starting the safety algorithm");
315 std::unique_ptr<simgrid::mc::State> initial_state =
316 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
318 XBT_DEBUG("**************************************************");
319 XBT_DEBUG("Initial state");
321 /* Get an enabled actor and insert it in the interleave set of the initial state */
322 for (auto& actor : mc_model_checker->process().actors())
323 if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
324 initial_state->interleave(actor.copy.getBuffer());
325 if (reductionMode_ != simgrid::mc::ReductionMode::none)
329 stack_.push_back(std::move(initial_state));
332 Checker* createSafetyChecker(Session& session)
334 return new SafetyChecker(session);