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/mc_state.h"
18 #include "src/mc/mc_request.h"
19 #include "src/mc/mc_safety.h"
20 #include "src/mc/mc_private.h"
21 #include "src/mc/mc_record.h"
22 #include "src/mc/mc_smx.h"
23 #include "src/mc/Client.hpp"
24 #include "src/mc/mc_exit.h"
25 #include "src/mc/Checker.hpp"
26 #include "src/mc/SafetyChecker.hpp"
27 #include "src/mc/VisitedState.hpp"
28 #include "src/mc/Transition.hpp"
29 #include "src/mc/Session.hpp"
31 #include "src/xbt/mmalloc/mmprivate.h"
33 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
34 "Logging specific to MC safety verification ");
38 static void MC_show_non_termination(void)
40 XBT_INFO("******************************************");
41 XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
42 XBT_INFO("******************************************");
43 XBT_INFO("Counter-example execution trace:");
44 for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
45 XBT_INFO("%s", s.c_str());
46 simgrid::mc::session->logState();
49 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
51 simgrid::mc::Snapshot* s1 = state1->system_state.get();
52 simgrid::mc::Snapshot* s2 = state2->system_state.get();
53 int num1 = state1->num;
54 int num2 = state2->num;
55 return snapshot_compare(num1, s1, num2, s2);
58 bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
60 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
61 if (snapshot_compare(i->get(), current_state) == 0){
62 XBT_INFO("Non-progressive cycle: state %d -> state %d", (*i)->num, current_state->num);
68 RecordTrace SafetyChecker::getRecordTrace() // override
71 for (auto const& state : stack_)
72 res.push_back(state->getTransition());
76 std::vector<std::string> SafetyChecker::getTextualTrace() // override
78 std::vector<std::string> trace;
79 for (auto const& state : stack_) {
80 int value = state->transition.argument;
81 smx_simcall_t req = &state->executed_req;
83 trace.push_back(simgrid::mc::request_to_string(
84 req, value, simgrid::mc::RequestType::executed));
89 void SafetyChecker::logState() // override
92 XBT_INFO("Expanded states = %lu", expandedStatesCount_);
93 XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
94 XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
97 int SafetyChecker::run()
99 while (!stack_.empty()) {
101 /* Get current state */
102 simgrid::mc::State* state = stack_.back().get();
104 XBT_DEBUG("**************************************************");
106 "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
107 stack_.size(), state, state->num,
108 state->interleaveSize());
110 mc_model_checker->visited_states++;
112 // The interleave set is empty or the maximum depth is reached,
114 smx_simcall_t req = nullptr;
115 if (stack_.size() > (std::size_t) _sg_mc_max_depth
116 || (req = MC_state_get_request(state)) == nullptr
117 || visitedState_ != nullptr) {
118 int res = this->backtrack();
125 // If there are processes to interleave and the maximum depth has not been
126 // reached then perform one step of the exploration algorithm.
127 XBT_DEBUG("Execute: %s",
128 simgrid::mc::request_to_string(
129 req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
132 if (dot_output != nullptr)
133 req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
135 mc_model_checker->executed_transitions++;
137 /* Answer the request */
138 this->getSession().execute(state->transition);
140 /* Create the new expanded state */
141 std::unique_ptr<simgrid::mc::State> next_state =
142 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
144 if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
145 MC_show_non_termination();
146 return SIMGRID_MC_EXIT_NON_TERMINATION;
149 if (_sg_mc_visited == 0
150 || (visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true)) == nullptr) {
152 /* Get an enabled process and insert it in the interleave set of the next state */
153 for (auto& p : mc_model_checker->process().actors())
154 if (simgrid::mc::actor_is_enabled(p.copy.getBuffer())) {
155 next_state->interleave(p.copy.getBuffer());
156 if (reductionMode_ != simgrid::mc::ReductionMode::none)
160 if (dot_output != nullptr)
161 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
162 state->num, next_state->num, req_str.c_str());
164 } else if (dot_output != nullptr)
165 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
167 visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str());
169 stack_.push_back(std::move(next_state));
172 XBT_INFO("No property violation found.");
173 simgrid::mc::session->logState();
174 return SIMGRID_MC_EXIT_SUCCESS;
177 int SafetyChecker::backtrack()
179 if (stack_.size() > (std::size_t) _sg_mc_max_depth
180 || visitedState_ != nullptr) {
181 if (visitedState_ == nullptr)
182 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
184 XBT_DEBUG("State already visited (equal to state %d),"
185 " exploration stopped on this path.",
186 visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
188 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
193 visitedState_ = nullptr;
195 /* Check for deadlocks */
196 if (mc_model_checker->checkDeadlock()) {
198 return SIMGRID_MC_EXIT_DEADLOCK;
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 predecesor 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, "
215 "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->processStates[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",
265 state->num, stack_.size() + 1);
266 stack_.push_back(std::move(state));
267 this->restoreState();
268 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
269 stack_.back()->num, stack_.size());
272 XBT_DEBUG("Delete state %d at depth %zi",
273 state->num, stack_.size() + 1);
276 return SIMGRID_MC_EXIT_SUCCESS;
279 void SafetyChecker::restoreState()
281 /* Intermediate backtracking */
283 simgrid::mc::State* state = stack_.back().get();
284 if (state->system_state) {
285 simgrid::mc::restore_snapshot(state->system_state);
290 /* Restore the initial state */
291 simgrid::mc::session->restoreInitialState();
293 /* Traverse the stack from the state at position start and re-execute the transitions */
294 for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
295 if (state == stack_.back())
297 session->execute(state->transition);
298 /* Update statistics */
299 mc_model_checker->visited_states++;
300 mc_model_checker->executed_transitions++;
304 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
306 reductionMode_ = simgrid::mc::reduction_mode;
307 if (_sg_mc_termination)
308 reductionMode_ = simgrid::mc::ReductionMode::none;
309 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
310 reductionMode_ = simgrid::mc::ReductionMode::dpor;
312 if (_sg_mc_termination)
313 XBT_INFO("Check non progressive cycles");
315 XBT_INFO("Check a safety property");
316 simgrid::mc::session->initialize();
318 XBT_DEBUG("Starting the safety algorithm");
320 std::unique_ptr<simgrid::mc::State> initial_state =
321 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
323 XBT_DEBUG("**************************************************");
324 XBT_DEBUG("Initial state");
326 /* Get an enabled actor and insert it in the interleave set of the initial state */
327 for (auto& actor : mc_model_checker->process().actors())
328 if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
329 initial_state->interleave(actor.copy.getBuffer());
330 if (reductionMode_ != simgrid::mc::ReductionMode::none)
334 stack_.push_back(std::move(initial_state));
337 SafetyChecker::~SafetyChecker()
341 Checker* createSafetyChecker(Session& session)
343 return new SafetyChecker(session);