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",
63 (*i)->num, current_state->num);
69 RecordTrace SafetyChecker::getRecordTrace() // override
72 for (auto const& state : stack_)
73 res.push_back(state->getTransition());
77 std::vector<std::string> SafetyChecker::getTextualTrace() // override
79 std::vector<std::string> trace;
80 for (auto const& state : stack_) {
81 int value = state->transition.argument;
82 smx_simcall_t req = &state->executed_req;
84 trace.push_back(simgrid::mc::request_to_string(
85 req, value, simgrid::mc::RequestType::executed));
90 int SafetyChecker::run()
94 while (!stack_.empty()) {
96 /* Get current state */
97 simgrid::mc::State* state = stack_.back().get();
99 XBT_DEBUG("**************************************************");
101 "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
102 stack_.size(), state, state->num,
103 state->interleaveSize());
105 mc_stats->visited_states++;
107 // The interleave set is empty or the maximum depth is reached,
109 smx_simcall_t req = nullptr;
110 if (stack_.size() > (std::size_t) _sg_mc_max_depth
111 || (req = MC_state_get_request(state)) == nullptr
112 || visitedState_ != nullptr) {
113 int res = this->backtrack();
120 // If there are processes to interleave and the maximum depth has not been
121 // reached then perform one step of the exploration algorithm.
122 XBT_DEBUG("Execute: %s",
123 simgrid::mc::request_to_string(
124 req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
127 if (dot_output != nullptr)
128 req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
130 mc_stats->executed_transitions++;
132 /* Answer the request */
133 this->getSession().execute(state->transition);
135 /* Create the new expanded state */
136 std::unique_ptr<simgrid::mc::State> next_state =
137 std::unique_ptr<simgrid::mc::State>(MC_state_new());
139 if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
140 MC_show_non_termination();
141 return SIMGRID_MC_EXIT_NON_TERMINATION;
144 if (_sg_mc_visited == 0
145 || (visitedState_ = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
147 /* Get an enabled process and insert it in the interleave set of the next state */
148 for (auto& p : mc_model_checker->process().simix_processes())
149 if (simgrid::mc::process_is_enabled(&p.copy)) {
150 next_state->interleave(&p.copy);
151 if (reductionMode_ != simgrid::mc::ReductionMode::none)
155 if (dot_output != nullptr)
156 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
157 state->num, next_state->num, req_str.c_str());
159 } else if (dot_output != nullptr)
160 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
162 visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str());
164 stack_.push_back(std::move(next_state));
167 XBT_INFO("No property violation found.");
168 simgrid::mc::session->logState();
169 initial_global_state = nullptr;
170 return SIMGRID_MC_EXIT_SUCCESS;
173 int SafetyChecker::backtrack()
175 if (stack_.size() > (std::size_t) _sg_mc_max_depth
176 || visitedState_ != nullptr) {
177 if (visitedState_ == nullptr)
178 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
180 XBT_DEBUG("State already visited (equal to state %d),"
181 " exploration stopped on this path.",
182 visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
184 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
189 visitedState_ = nullptr;
191 /* Check for deadlocks */
192 if (mc_model_checker->checkDeadlock()) {
194 return SIMGRID_MC_EXIT_DEADLOCK;
197 /* Traverse the stack backwards until a state with a non empty interleave
198 set is found, deleting all the states that have it empty in the way.
199 For each deleted state, check if the request that has generated it
200 (from it's predecesor state), depends on any other previous request
201 executed before it. If it does then add it to the interleave set of the
202 state that executed that previous request. */
204 while (!stack_.empty()) {
205 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
207 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
208 smx_simcall_t req = &state->internal_req;
209 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
210 xbt_die("Mutex is currently not supported with DPOR, "
211 "use --cfg=model-check/reduction:none");
212 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
213 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
214 simgrid::mc::State* prev_state = i->get();
215 if (reductionMode_ != simgrid::mc::ReductionMode::none
216 && 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 (!prev_state->processStates[issuer->pid].isDone())
234 prev_state->interleave(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_process_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
248 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
249 req->call, issuer->pid, state->num,
250 prev_state->internal_req.call,
251 previous_issuer->pid,
258 if (state->interleaveSize()
259 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
260 /* We found a back-tracking point, let's loop */
261 XBT_DEBUG("Back-tracking to state %d at depth %zi",
262 state->num, stack_.size() + 1);
263 stack_.push_back(std::move(state));
264 simgrid::mc::replay(stack_);
265 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
266 stack_.back()->num, stack_.size());
269 XBT_DEBUG("Delete state %d at depth %zi",
270 state->num, stack_.size() + 1);
273 return SIMGRID_MC_EXIT_SUCCESS;
276 void SafetyChecker::init()
278 reductionMode_ = simgrid::mc::reduction_mode;
279 if( _sg_mc_termination)
280 reductionMode_ = simgrid::mc::ReductionMode::none;
281 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
282 reductionMode_ = simgrid::mc::ReductionMode::dpor;
284 if (_sg_mc_termination)
285 XBT_INFO("Check non progressive cycles");
287 XBT_INFO("Check a safety property");
288 mc_model_checker->wait_for_requests();
290 XBT_DEBUG("Starting the safety algorithm");
292 std::unique_ptr<simgrid::mc::State> initial_state =
293 std::unique_ptr<simgrid::mc::State>(MC_state_new());
295 XBT_DEBUG("**************************************************");
296 XBT_DEBUG("Initial state");
298 /* Get an enabled process and insert it in the interleave set of the initial state */
299 for (auto& p : mc_model_checker->process().simix_processes())
300 if (simgrid::mc::process_is_enabled(&p.copy)) {
301 initial_state->interleave(&p.copy);
302 if (reductionMode_ != simgrid::mc::ReductionMode::none)
306 stack_.push_back(std::move(initial_state));
308 /* Save the initial state */
309 initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
310 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
313 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
317 SafetyChecker::~SafetyChecker()
321 Checker* createSafetyChecker(Session& session)
323 return new SafetyChecker(session);