1 /* Copyright (c) 2016-2019. The SimGrid Team. All rights reserved. */
3 /* This program is free software; you can redistribute it and/or modify it
4 * under the terms of the license (GNU LGPL) which comes with this package. */
14 #include <xbt/sysdep.h>
16 #include "src/mc/Session.hpp"
17 #include "src/mc/Transition.hpp"
18 #include "src/mc/VisitedState.hpp"
19 #include "src/mc/checker/SafetyChecker.hpp"
20 #include "src/mc/mc_exit.hpp"
21 #include "src/mc/mc_private.hpp"
22 #include "src/mc/mc_record.hpp"
23 #include "src/mc/mc_request.hpp"
24 #include "src/mc/mc_smx.hpp"
26 #include "src/xbt/mmalloc/mmprivate.h"
28 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
29 "Logging specific to MC safety verification ");
33 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
35 simgrid::mc::Snapshot* s1 = state1->system_state.get();
36 simgrid::mc::Snapshot* s2 = state2->system_state.get();
37 return snapshot_compare(s1, s2);
40 void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
42 for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
43 if (snapshot_compare(state->get(), current_state) == 0) {
44 XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num, current_state->num);
45 XBT_INFO("******************************************");
46 XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
47 XBT_INFO("******************************************");
48 XBT_INFO("Counter-example execution trace:");
49 for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
50 XBT_INFO(" %s", s.c_str());
51 simgrid::mc::dumpRecordPath();
52 simgrid::mc::session->logState();
54 throw simgrid::mc::TerminationError();
58 RecordTrace SafetyChecker::getRecordTrace() // override
61 for (auto const& state : stack_)
62 res.push_back(state->getTransition());
66 std::vector<std::string> SafetyChecker::getTextualTrace() // override
68 std::vector<std::string> trace;
69 for (auto const& state : stack_) {
70 int value = state->transition.argument;
71 smx_simcall_t req = &state->executed_req;
73 trace.push_back(simgrid::mc::request_to_string(
74 req, value, simgrid::mc::RequestType::executed));
79 void SafetyChecker::logState() // override
81 XBT_INFO("Expanded states = %lu", expandedStatesCount_);
82 XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
83 XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
86 void SafetyChecker::run()
88 /* This function runs the DFS algorithm the state space.
89 * We do so iteratively instead of recursively, dealing with the call stack manually.
90 * This allows to explore the call stack at wish. */
92 while (not stack_.empty()) {
94 /* Get current state */
95 simgrid::mc::State* state = stack_.back().get();
97 XBT_DEBUG("**************************************************");
98 XBT_DEBUG("Exploration depth=%zu (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num,
99 state->interleaveSize());
101 mc_model_checker->visited_states++;
103 // Backtrack if we reached the maximum depth
104 if (stack_.size() > (std::size_t)_sg_mc_max_depth) {
105 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
110 // Backtrack if we are revisiting a state we saw previously
111 if (visitedState_ != nullptr) {
112 XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
113 visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num);
115 visitedState_ = nullptr;
120 // Search an enabled transition in the current state; backtrack if the interleave set is empty
121 // get_request also sets state.transition to be the one corresponding to the returned req
122 smx_simcall_t req = MC_state_get_request(state);
123 // req is now the transition of the process that was selected to be executed
125 if (req == nullptr) {
126 XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size() + 1);
132 // If there are processes to interleave and the maximum depth has not been
133 // reached then perform one step of the exploration algorithm.
134 XBT_DEBUG("Execute: %s",
135 simgrid::mc::request_to_string(
136 req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
139 if (dot_output != nullptr)
140 req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
142 mc_model_checker->executed_transitions++;
144 /* Actually answer the request: let execute the selected request (MCed does one step) */
145 this->getSession().execute(state->transition);
147 /* Create the new expanded state (copy the state of MCed into our MCer data) */
148 std::unique_ptr<simgrid::mc::State> next_state =
149 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
151 if (_sg_mc_termination)
152 this->checkNonTermination(next_state.get());
154 /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
155 if (_sg_mc_max_visited_states > 0)
156 visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true);
158 /* If this is a new state (or if we don't care about state-equality reduction) */
159 if (visitedState_ == nullptr) {
161 /* Get an enabled process and insert it in the interleave set of the next state */
162 for (auto& remoteActor : mc_model_checker->process().actors()) {
163 auto actor = remoteActor.copy.getBuffer();
164 if (simgrid::mc::actor_is_enabled(actor)) {
165 next_state->addInterleavingSet(actor);
166 if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
167 break; // With DPOR, we take the first enabled transition
171 if (dot_output != nullptr)
172 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
173 state->num, next_state->num, req_str.c_str());
175 } else if (dot_output != nullptr)
176 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
177 visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num,
180 stack_.push_back(std::move(next_state));
183 XBT_INFO("No property violation found.");
184 simgrid::mc::session->logState();
187 void SafetyChecker::backtrack()
191 /* Check for deadlocks */
192 if (mc_model_checker->checkDeadlock()) {
194 throw simgrid::mc::DeadlockError();
197 /* Traverse the stack backwards until a state with a non empty interleave
198 set is found, deleting all the states that have it empty in the way.
199 For each deleted state, check if the request that has generated it
200 (from it's predecessor state), depends on any other previous request
201 executed before it. If it does then add it to the interleave set of the
202 state that executed that previous request. */
204 while (not stack_.empty()) {
205 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
207 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
208 smx_simcall_t req = &state->internal_req;
209 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
210 xbt_die("Mutex is currently not supported with DPOR, use --cfg=model-check/reduction:none");
212 const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
213 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
214 simgrid::mc::State* prev_state = i->get();
215 if (simgrid::mc::request_depend(req, &prev_state->internal_req)) {
216 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
217 XBT_DEBUG("Dependent Transitions:");
218 int value = prev_state->transition.argument;
219 smx_simcall_t prev_req = &prev_state->executed_req;
220 XBT_DEBUG("%s (state=%d)",
221 simgrid::mc::request_to_string(
222 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
224 value = state->transition.argument;
225 prev_req = &state->executed_req;
226 XBT_DEBUG("%s (state=%d)",
227 simgrid::mc::request_to_string(
228 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
232 if (not prev_state->actorStates[issuer->get_pid()].isDone())
233 prev_state->addInterleavingSet(issuer);
235 XBT_DEBUG("Process %p is in done set", req->issuer);
239 } else if (req->issuer == prev_state->internal_req.issuer) {
241 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, prev_state->internal_req.call);
246 const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
247 XBT_DEBUG("Simcall %d, process %ld (state %d) and simcall %d, process %ld (state %d) are independent",
248 req->call, issuer->get_pid(), state->num, prev_state->internal_req.call, previous_issuer->get_pid(),
254 if (state->interleaveSize()
255 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
256 /* We found a back-tracking point, let's loop */
257 XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num, stack_.size() + 1);
258 stack_.push_back(std::move(state));
259 this->restoreState();
260 XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num, stack_.size());
263 XBT_DEBUG("Delete state %d at depth %zu", state->num, stack_.size() + 1);
268 void SafetyChecker::restoreState()
270 /* Intermediate backtracking */
271 simgrid::mc::State* last_state = stack_.back().get();
272 if (last_state->system_state) {
273 simgrid::mc::restore_snapshot(last_state->system_state);
277 /* Restore the initial state */
278 simgrid::mc::session->restoreInitialState();
280 /* Traverse the stack from the state at position start and re-execute the transitions */
281 for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
282 if (state == stack_.back())
284 session->execute(state->transition);
285 /* Update statistics */
286 mc_model_checker->visited_states++;
287 mc_model_checker->executed_transitions++;
291 SafetyChecker::SafetyChecker(Session& s) : Checker(s)
293 reductionMode_ = simgrid::mc::reduction_mode;
294 if (_sg_mc_termination)
295 reductionMode_ = simgrid::mc::ReductionMode::none;
296 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
297 reductionMode_ = simgrid::mc::ReductionMode::dpor;
299 if (_sg_mc_termination)
300 XBT_INFO("Check non progressive cycles");
302 XBT_INFO("Check a safety property. Reduction is: %s.",
303 (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
304 (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
305 simgrid::mc::session->initialize();
307 XBT_DEBUG("Starting the safety algorithm");
309 std::unique_ptr<simgrid::mc::State> initial_state =
310 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
312 XBT_DEBUG("**************************************************");
313 XBT_DEBUG("Initial state");
315 /* Get an enabled actor and insert it in the interleave set of the initial state */
316 for (auto& actor : mc_model_checker->process().actors())
317 if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
318 initial_state->addInterleavingSet(actor.copy.getBuffer());
319 if (reductionMode_ != simgrid::mc::ReductionMode::none)
323 stack_.push_back(std::move(initial_state));
326 Checker* createSafetyChecker(Session& s)
328 return new SafetyChecker(s);