1 /* Copyright (c) 2016-2017. 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
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->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 %lu (state %d) and simcall %d, process %lu (state %d) are independent",
250 req->call, issuer->pid, state->num,
251 prev_state->internal_req.call,
252 previous_issuer->pid,
259 if (state->interleaveSize()
260 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
261 /* We found a back-tracking point, let's loop */
262 XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num, stack_.size() + 1);
263 stack_.push_back(std::move(state));
264 this->restoreState();
265 XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num, stack_.size());
268 XBT_DEBUG("Delete state %d at depth %zu", state->num, stack_.size() + 1);
273 void SafetyChecker::restoreState()
275 /* Intermediate backtracking */
276 simgrid::mc::State* state = stack_.back().get();
277 if (state->system_state) {
278 simgrid::mc::restore_snapshot(state->system_state);
282 /* Restore the initial state */
283 simgrid::mc::session->restoreInitialState();
285 /* Traverse the stack from the state at position start and re-execute the transitions */
286 for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
287 if (state == stack_.back())
289 session->execute(state->transition);
290 /* Update statistics */
291 mc_model_checker->visited_states++;
292 mc_model_checker->executed_transitions++;
296 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
298 reductionMode_ = simgrid::mc::reduction_mode;
299 if (_sg_mc_termination)
300 reductionMode_ = simgrid::mc::ReductionMode::none;
301 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
302 reductionMode_ = simgrid::mc::ReductionMode::dpor;
304 if (_sg_mc_termination)
305 XBT_INFO("Check non progressive cycles");
307 XBT_INFO("Check a safety property. Reduction is: %s.",
308 (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
309 (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
310 simgrid::mc::session->initialize();
312 XBT_DEBUG("Starting the safety algorithm");
314 std::unique_ptr<simgrid::mc::State> initial_state =
315 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
317 XBT_DEBUG("**************************************************");
318 XBT_DEBUG("Initial state");
320 /* Get an enabled actor and insert it in the interleave set of the initial state */
321 for (auto& actor : mc_model_checker->process().actors())
322 if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
323 initial_state->addInterleavingSet(actor.copy.getBuffer());
324 if (reductionMode_ != simgrid::mc::ReductionMode::none)
328 stack_.push_back(std::move(initial_state));
331 Checker* createSafetyChecker(Session& session)
333 return new SafetyChecker(session);