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::session->logState();
55 throw simgrid::mc::TerminationError();
59 RecordTrace SafetyChecker::getRecordTrace() // override
62 for (auto const& state : stack_)
63 res.push_back(state->getTransition());
67 std::vector<std::string> SafetyChecker::getTextualTrace() // override
69 std::vector<std::string> trace;
70 for (auto const& state : stack_) {
71 int value = state->transition.argument;
72 smx_simcall_t req = &state->executed_req;
74 trace.push_back(simgrid::mc::request_to_string(
75 req, value, simgrid::mc::RequestType::executed));
80 void SafetyChecker::logState() // override
82 XBT_INFO("Expanded states = %lu", expandedStatesCount_);
83 XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
84 XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
87 void SafetyChecker::run()
89 /* This function runs the DFS algorithm the state space.
90 * We do so iteratively instead of recursively, dealing with the call stack manually.
91 * This allows to explore the call stack at wish. */
93 while (not stack_.empty()) {
95 /* Get current state */
96 simgrid::mc::State* state = stack_.back().get();
98 XBT_DEBUG("**************************************************");
99 XBT_DEBUG("Exploration depth=%zu (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num,
100 state->interleaveSize());
102 mc_model_checker->visited_states++;
104 // Backtrack if we reached the maximum depth
105 if (stack_.size() > (std::size_t)_sg_mc_max_depth) {
106 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
111 // Backtrack if we are revisiting a state we saw previously
112 if (visitedState_ != nullptr) {
113 XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
114 visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num);
116 visitedState_ = nullptr;
121 // Search an enabled transition in the current state; backtrack if the interleave set is empty
122 // get_request also sets state.transition to be the one corresponding to the returned req
123 smx_simcall_t req = MC_state_get_request(state);
124 // req is now the transition of the process that was selected to be executed
126 if (req == nullptr) {
127 XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size() + 1);
133 // If there are processes to interleave and the maximum depth has not been
134 // reached then perform one step of the exploration algorithm.
135 XBT_DEBUG("Execute: %s",
136 simgrid::mc::request_to_string(
137 req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
140 if (dot_output != nullptr)
141 req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
143 mc_model_checker->executed_transitions++;
145 /* Actually answer the request: let execute the selected request (MCed does one step) */
146 this->getSession().execute(state->transition);
148 /* Create the new expanded state (copy the state of MCed into our MCer data) */
149 std::unique_ptr<simgrid::mc::State> next_state =
150 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
152 if (_sg_mc_termination)
153 this->checkNonTermination(next_state.get());
155 /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
156 if (_sg_mc_max_visited_states > 0)
157 visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true);
159 /* If this is a new state (or if we don't care about state-equality reduction) */
160 if (visitedState_ == nullptr) {
162 /* Get an enabled process and insert it in the interleave set of the next state */
163 for (auto& remoteActor : mc_model_checker->process().actors()) {
164 auto actor = remoteActor.copy.getBuffer();
165 if (simgrid::mc::actor_is_enabled(actor)) {
166 next_state->addInterleavingSet(actor);
167 if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
168 break; // With DPOR, we take the first enabled transition
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->get_pid()].isDone())
234 prev_state->addInterleavingSet(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 %ld (state %d) and simcall %d, process %ld (state %d) are independent",
249 req->call, issuer->get_pid(), state->num, prev_state->internal_req.call, previous_issuer->get_pid(),
255 if (state->interleaveSize()
256 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
257 /* We found a back-tracking point, let's loop */
258 XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num, stack_.size() + 1);
259 stack_.push_back(std::move(state));
260 this->restoreState();
261 XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num, stack_.size());
264 XBT_DEBUG("Delete state %d at depth %zu", state->num, stack_.size() + 1);
269 void SafetyChecker::restoreState()
271 /* Intermediate backtracking */
272 simgrid::mc::State* state = stack_.back().get();
273 if (state->system_state) {
274 simgrid::mc::restore_snapshot(state->system_state);
278 /* Restore the initial state */
279 simgrid::mc::session->restoreInitialState();
281 /* Traverse the stack from the state at position start and re-execute the transitions */
282 for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
283 if (state == stack_.back())
285 session->execute(state->transition);
286 /* Update statistics */
287 mc_model_checker->visited_states++;
288 mc_model_checker->executed_transitions++;
292 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
294 reductionMode_ = simgrid::mc::reduction_mode;
295 if (_sg_mc_termination)
296 reductionMode_ = simgrid::mc::ReductionMode::none;
297 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
298 reductionMode_ = simgrid::mc::ReductionMode::dpor;
300 if (_sg_mc_termination)
301 XBT_INFO("Check non progressive cycles");
303 XBT_INFO("Check a safety property. Reduction is: %s.",
304 (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
305 (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
306 simgrid::mc::session->initialize();
308 XBT_DEBUG("Starting the safety algorithm");
310 std::unique_ptr<simgrid::mc::State> initial_state =
311 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
313 XBT_DEBUG("**************************************************");
314 XBT_DEBUG("Initial state");
316 /* Get an enabled actor and insert it in the interleave set of the initial state */
317 for (auto& actor : mc_model_checker->process().actors())
318 if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
319 initial_state->addInterleavingSet(actor.copy.getBuffer());
320 if (reductionMode_ != simgrid::mc::ReductionMode::none)
324 stack_.push_back(std::move(initial_state));
327 Checker* createSafetyChecker(Session& session)
329 return new SafetyChecker(session);