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_safety.h"
26 #include "src/mc/mc_smx.h"
27 #include "src/mc/mc_state.h"
28 #include "src/mc/remote/Client.hpp"
30 #include "src/xbt/mmalloc/mmprivate.h"
32 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
33 "Logging specific to MC safety verification ");
37 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
39 simgrid::mc::Snapshot* s1 = state1->system_state.get();
40 simgrid::mc::Snapshot* s2 = state2->system_state.get();
41 int num1 = state1->num;
42 int num2 = state2->num;
43 return snapshot_compare(num1, s1, num2, s2);
46 void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
48 for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
49 if (snapshot_compare(state->get(), current_state) == 0) {
50 XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num, current_state->num);
51 XBT_INFO("******************************************");
52 XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
53 XBT_INFO("******************************************");
54 XBT_INFO("Counter-example execution trace:");
55 for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
56 XBT_INFO("%s", s.c_str());
57 simgrid::mc::session->logState();
59 throw simgrid::mc::TerminationError();
63 RecordTrace SafetyChecker::getRecordTrace() // override
66 for (auto const& state : stack_)
67 res.push_back(state->getTransition());
71 std::vector<std::string> SafetyChecker::getTextualTrace() // override
73 std::vector<std::string> trace;
74 for (auto const& state : stack_) {
75 int value = state->transition.argument;
76 smx_simcall_t req = &state->executed_req;
78 trace.push_back(simgrid::mc::request_to_string(
79 req, value, simgrid::mc::RequestType::executed));
84 void SafetyChecker::logState() // override
87 XBT_INFO("Expanded states = %lu", expandedStatesCount_);
88 XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
89 XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
92 void SafetyChecker::run()
94 /* This function runs the DFS algorithm the state space.
95 * We do so iteratively instead of recursively, dealing with the call stack manually.
96 * This allows to explore the call stack at wish. */
98 while (!stack_.empty()) {
100 /* Get current state */
101 simgrid::mc::State* state = stack_.back().get();
103 XBT_DEBUG("**************************************************");
104 XBT_DEBUG("Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
105 stack_.size(), state, state->num, state->interleaveSize());
107 mc_model_checker->visited_states++;
109 // Backtrack if we reached the maximum depth
110 if (stack_.size() > (std::size_t)_sg_mc_max_depth) {
111 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
116 // Backtrack if we are revisiting a state we saw previously
117 if (visitedState_ != nullptr) {
118 XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
119 visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num);
121 visitedState_ = nullptr;
126 // Search an enabled transition in the current state; backtrack if the interleave set is empty
127 // get_request also sets state.transition to be the one corresponding to the returned req
128 smx_simcall_t req = MC_state_get_request(state);
129 // req is now the transition of the process that was selected to be executed
131 if (req == nullptr) {
132 XBT_DEBUG("There are no more processes to interleave. (depth %zi)", stack_.size() + 1);
138 // If there are processes to interleave and the maximum depth has not been
139 // reached then perform one step of the exploration algorithm.
140 XBT_DEBUG("Execute: %s",
141 simgrid::mc::request_to_string(
142 req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
145 if (dot_output != nullptr)
146 req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
148 mc_model_checker->executed_transitions++;
150 /* Actually answer the request: let execute the selected request (MCed does one step) */
151 this->getSession().execute(state->transition);
153 /* Create the new expanded state (copy the state of MCed into our MCer data) */
154 std::unique_ptr<simgrid::mc::State> next_state =
155 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
157 if (_sg_mc_termination)
158 this->checkNonTermination(next_state.get());
160 /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
161 if (_sg_mc_max_visited_states == true)
162 visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true);
164 /* If this is a new state (or if we don't care about state-equality reduction) */
165 if (visitedState_ == nullptr) {
167 /* Get an enabled process and insert it in the interleave set of the next state */
168 for (auto& actor : mc_model_checker->process().actors())
169 if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
170 next_state->interleave(actor.copy.getBuffer());
171 if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
175 if (dot_output != nullptr)
176 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
177 state->num, next_state->num, req_str.c_str());
179 } else if (dot_output != nullptr)
180 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
181 visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num,
184 stack_.push_back(std::move(next_state));
187 XBT_INFO("No property violation found.");
188 simgrid::mc::session->logState();
191 void SafetyChecker::backtrack()
195 /* Check for deadlocks */
196 if (mc_model_checker->checkDeadlock()) {
198 throw simgrid::mc::DeadlockError();
201 /* Traverse the stack backwards until a state with a non empty interleave
202 set is found, deleting all the states that have it empty in the way.
203 For each deleted state, check if the request that has generated it
204 (from it's predecessor state), depends on any other previous request
205 executed before it. If it does then add it to the interleave set of the
206 state that executed that previous request. */
208 while (!stack_.empty()) {
209 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
211 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
212 smx_simcall_t req = &state->internal_req;
213 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
214 xbt_die("Mutex is currently not supported with DPOR, use --cfg=model-check/reduction:none");
216 const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
217 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
218 simgrid::mc::State* prev_state = i->get();
219 if (simgrid::mc::request_depend(req, &prev_state->internal_req)) {
220 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
221 XBT_DEBUG("Dependent Transitions:");
222 int value = prev_state->transition.argument;
223 smx_simcall_t prev_req = &prev_state->executed_req;
224 XBT_DEBUG("%s (state=%d)",
225 simgrid::mc::request_to_string(
226 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
228 value = state->transition.argument;
229 prev_req = &state->executed_req;
230 XBT_DEBUG("%s (state=%d)",
231 simgrid::mc::request_to_string(
232 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
236 if (!prev_state->actorStates[issuer->pid].isDone())
237 prev_state->interleave(issuer);
239 XBT_DEBUG("Process %p is in done set", req->issuer);
243 } else if (req->issuer == prev_state->internal_req.issuer) {
245 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, prev_state->internal_req.call);
250 const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
251 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
252 req->call, issuer->pid, state->num,
253 prev_state->internal_req.call,
254 previous_issuer->pid,
261 if (state->interleaveSize()
262 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
263 /* We found a back-tracking point, let's loop */
264 XBT_DEBUG("Back-tracking to state %d at depth %zi", state->num, stack_.size() + 1);
265 stack_.push_back(std::move(state));
266 this->restoreState();
267 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
268 stack_.back()->num, stack_.size());
271 XBT_DEBUG("Delete state %d at depth %zi",
272 state->num, stack_.size() + 1);
277 void SafetyChecker::restoreState()
279 /* Intermediate backtracking */
280 simgrid::mc::State* state = stack_.back().get();
281 if (state->system_state) {
282 simgrid::mc::restore_snapshot(state->system_state);
286 /* Restore the initial state */
287 simgrid::mc::session->restoreInitialState();
289 /* Traverse the stack from the state at position start and re-execute the transitions */
290 for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
291 if (state == stack_.back())
293 session->execute(state->transition);
294 /* Update statistics */
295 mc_model_checker->visited_states++;
296 mc_model_checker->executed_transitions++;
300 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
302 reductionMode_ = simgrid::mc::reduction_mode;
303 if (_sg_mc_termination)
304 reductionMode_ = simgrid::mc::ReductionMode::none;
305 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
306 reductionMode_ = simgrid::mc::ReductionMode::dpor;
308 if (_sg_mc_termination)
309 XBT_INFO("Check non progressive cycles");
311 XBT_INFO("Check a safety property. Reduction is: %s.",
312 (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
313 (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
314 simgrid::mc::session->initialize();
316 XBT_DEBUG("Starting the safety algorithm");
318 std::unique_ptr<simgrid::mc::State> initial_state =
319 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
321 XBT_DEBUG("**************************************************");
322 XBT_DEBUG("Initial state");
324 /* Get an enabled actor and insert it in the interleave set of the initial state */
325 for (auto& actor : mc_model_checker->process().actors())
326 if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
327 initial_state->interleave(actor.copy.getBuffer());
328 if (reductionMode_ != simgrid::mc::ReductionMode::none)
332 stack_.push_back(std::move(initial_state));
335 SafetyChecker::~SafetyChecker()
339 Checker* createSafetyChecker(Session& session)
341 return new SafetyChecker(session);