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 int num1 = state1->num;
38 int num2 = state2->num;
39 return snapshot_compare(num1, s1, num2, s2);
42 void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
44 for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
45 if (snapshot_compare(state->get(), current_state) == 0) {
46 XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num, current_state->num);
47 XBT_INFO("******************************************");
48 XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
49 XBT_INFO("******************************************");
50 XBT_INFO("Counter-example execution trace:");
51 for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
52 XBT_INFO(" %s", s.c_str());
53 simgrid::mc::dumpRecordPath();
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
83 XBT_INFO("Expanded states = %lu", expandedStatesCount_);
84 XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
85 XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
88 void SafetyChecker::run()
90 /* This function runs the DFS algorithm the state space.
91 * We do so iteratively instead of recursively, dealing with the call stack manually.
92 * This allows to explore the call stack at wish. */
94 while (not stack_.empty()) {
96 /* Get current state */
97 simgrid::mc::State* state = stack_.back().get();
99 XBT_DEBUG("**************************************************");
100 XBT_DEBUG("Exploration depth=%zu (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num,
101 state->interleaveSize());
103 mc_model_checker->visited_states++;
105 // Backtrack if we reached the maximum depth
106 if (stack_.size() > (std::size_t)_sg_mc_max_depth) {
107 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
112 // Backtrack if we are revisiting a state we saw previously
113 if (visitedState_ != nullptr) {
114 XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
115 visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num);
117 visitedState_ = nullptr;
122 // Search an enabled transition in the current state; backtrack if the interleave set is empty
123 // get_request also sets state.transition to be the one corresponding to the returned req
124 smx_simcall_t req = MC_state_get_request(state);
125 // req is now the transition of the process that was selected to be executed
127 if (req == nullptr) {
128 XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size() + 1);
134 // If there are processes to interleave and the maximum depth has not been
135 // reached then perform one step of the exploration algorithm.
136 XBT_DEBUG("Execute: %s",
137 simgrid::mc::request_to_string(
138 req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
141 if (dot_output != nullptr)
142 req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
144 mc_model_checker->executed_transitions++;
146 /* Actually answer the request: let execute the selected request (MCed does one step) */
147 this->getSession().execute(state->transition);
149 /* Create the new expanded state (copy the state of MCed into our MCer data) */
150 std::unique_ptr<simgrid::mc::State> next_state =
151 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
153 if (_sg_mc_termination)
154 this->checkNonTermination(next_state.get());
156 /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
157 if (_sg_mc_max_visited_states > 0)
158 visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true);
160 /* If this is a new state (or if we don't care about state-equality reduction) */
161 if (visitedState_ == nullptr) {
163 /* Get an enabled process and insert it in the interleave set of the next state */
164 for (auto& remoteActor : mc_model_checker->process().actors()) {
165 auto actor = remoteActor.copy.getBuffer();
166 if (simgrid::mc::actor_is_enabled(actor)) {
167 next_state->addInterleavingSet(actor);
168 if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
169 break; // With DPOR, we take the first enabled transition
173 if (dot_output != nullptr)
174 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
175 state->num, next_state->num, req_str.c_str());
177 } else if (dot_output != nullptr)
178 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
179 visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num,
182 stack_.push_back(std::move(next_state));
185 XBT_INFO("No property violation found.");
186 simgrid::mc::session->logState();
189 void SafetyChecker::backtrack()
193 /* Check for deadlocks */
194 if (mc_model_checker->checkDeadlock()) {
196 throw simgrid::mc::DeadlockError();
199 /* Traverse the stack backwards until a state with a non empty interleave
200 set is found, deleting all the states that have it empty in the way.
201 For each deleted state, check if the request that has generated it
202 (from it's predecessor state), depends on any other previous request
203 executed before it. If it does then add it to the interleave set of the
204 state that executed that previous request. */
206 while (not stack_.empty()) {
207 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
209 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
210 smx_simcall_t req = &state->internal_req;
211 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
212 xbt_die("Mutex is currently not supported with DPOR, use --cfg=model-check/reduction:none");
214 const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
215 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
216 simgrid::mc::State* prev_state = i->get();
217 if (simgrid::mc::request_depend(req, &prev_state->internal_req)) {
218 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
219 XBT_DEBUG("Dependent Transitions:");
220 int value = prev_state->transition.argument;
221 smx_simcall_t prev_req = &prev_state->executed_req;
222 XBT_DEBUG("%s (state=%d)",
223 simgrid::mc::request_to_string(
224 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
226 value = state->transition.argument;
227 prev_req = &state->executed_req;
228 XBT_DEBUG("%s (state=%d)",
229 simgrid::mc::request_to_string(
230 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
234 if (not prev_state->actorStates[issuer->get_pid()].isDone())
235 prev_state->addInterleavingSet(issuer);
237 XBT_DEBUG("Process %p is in done set", req->issuer);
241 } else if (req->issuer == prev_state->internal_req.issuer) {
243 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, prev_state->internal_req.call);
248 const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
249 XBT_DEBUG("Simcall %d, process %ld (state %d) and simcall %d, process %ld (state %d) are independent",
250 req->call, issuer->get_pid(), state->num, prev_state->internal_req.call, previous_issuer->get_pid(),
256 if (state->interleaveSize()
257 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
258 /* We found a back-tracking point, let's loop */
259 XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num, stack_.size() + 1);
260 stack_.push_back(std::move(state));
261 this->restoreState();
262 XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num, stack_.size());
265 XBT_DEBUG("Delete state %d at depth %zu", state->num, stack_.size() + 1);
270 void SafetyChecker::restoreState()
272 /* Intermediate backtracking */
273 simgrid::mc::State* last_state = stack_.back().get();
274 if (last_state->system_state) {
275 simgrid::mc::restore_snapshot(last_state->system_state);
279 /* Restore the initial state */
280 simgrid::mc::session->restoreInitialState();
282 /* Traverse the stack from the state at position start and re-execute the transitions */
283 for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
284 if (state == stack_.back())
286 session->execute(state->transition);
287 /* Update statistics */
288 mc_model_checker->visited_states++;
289 mc_model_checker->executed_transitions++;
293 SafetyChecker::SafetyChecker(Session& s) : Checker(s)
295 reductionMode_ = simgrid::mc::reduction_mode;
296 if (_sg_mc_termination)
297 reductionMode_ = simgrid::mc::ReductionMode::none;
298 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
299 reductionMode_ = simgrid::mc::ReductionMode::dpor;
301 if (_sg_mc_termination)
302 XBT_INFO("Check non progressive cycles");
304 XBT_INFO("Check a safety property. Reduction is: %s.",
305 (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
306 (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
307 simgrid::mc::session->initialize();
309 XBT_DEBUG("Starting the safety algorithm");
311 std::unique_ptr<simgrid::mc::State> initial_state =
312 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
314 XBT_DEBUG("**************************************************");
315 XBT_DEBUG("Initial state");
317 /* Get an enabled actor and insert it in the interleave set of the initial state */
318 for (auto& actor : mc_model_checker->process().actors())
319 if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
320 initial_state->addInterleavingSet(actor.copy.getBuffer());
321 if (reductionMode_ != simgrid::mc::ReductionMode::none)
325 stack_.push_back(std::move(initial_state));
328 Checker* createSafetyChecker(Session& s)
330 return new SafetyChecker(s);