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 void SafetyChecker::logState() // override
93 XBT_INFO("Expanded states = %lu", expandedStatesCount_);
94 XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
95 XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
98 int SafetyChecker::run()
102 while (!stack_.empty()) {
104 /* Get current state */
105 simgrid::mc::State* state = stack_.back().get();
107 XBT_DEBUG("**************************************************");
109 "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
110 stack_.size(), state, state->num,
111 state->interleaveSize());
113 mc_model_checker->visited_states++;
115 // The interleave set is empty or the maximum depth is reached,
117 smx_simcall_t req = nullptr;
118 if (stack_.size() > (std::size_t) _sg_mc_max_depth
119 || (req = MC_state_get_request(state)) == nullptr
120 || visitedState_ != nullptr) {
121 int res = this->backtrack();
128 // If there are processes to interleave and the maximum depth has not been
129 // reached then perform one step of the exploration algorithm.
130 XBT_DEBUG("Execute: %s",
131 simgrid::mc::request_to_string(
132 req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
135 if (dot_output != nullptr)
136 req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
138 mc_model_checker->executed_transitions++;
140 /* Answer the request */
141 this->getSession().execute(state->transition);
143 /* Create the new expanded state */
144 std::unique_ptr<simgrid::mc::State> next_state =
145 std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
147 if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
148 MC_show_non_termination();
149 return SIMGRID_MC_EXIT_NON_TERMINATION;
152 if (_sg_mc_visited == 0
153 || (visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true)) == nullptr) {
155 /* Get an enabled process and insert it in the interleave set of the next state */
156 for (auto& p : mc_model_checker->process().simix_processes())
157 if (simgrid::mc::process_is_enabled(&p.copy)) {
158 next_state->interleave(&p.copy);
159 if (reductionMode_ != simgrid::mc::ReductionMode::none)
163 if (dot_output != nullptr)
164 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
165 state->num, next_state->num, req_str.c_str());
167 } else if (dot_output != nullptr)
168 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
170 visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str());
172 stack_.push_back(std::move(next_state));
175 XBT_INFO("No property violation found.");
176 simgrid::mc::session->logState();
177 return SIMGRID_MC_EXIT_SUCCESS;
180 int SafetyChecker::backtrack()
182 if (stack_.size() > (std::size_t) _sg_mc_max_depth
183 || visitedState_ != nullptr) {
184 if (visitedState_ == nullptr)
185 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
187 XBT_DEBUG("State already visited (equal to state %d),"
188 " exploration stopped on this path.",
189 visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
191 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
196 visitedState_ = nullptr;
198 /* Check for deadlocks */
199 if (mc_model_checker->checkDeadlock()) {
201 return SIMGRID_MC_EXIT_DEADLOCK;
204 /* Traverse the stack backwards until a state with a non empty interleave
205 set is found, deleting all the states that have it empty in the way.
206 For each deleted state, check if the request that has generated it
207 (from it's predecesor state), depends on any other previous request
208 executed before it. If it does then add it to the interleave set of the
209 state that executed that previous request. */
211 while (!stack_.empty()) {
212 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
214 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
215 smx_simcall_t req = &state->internal_req;
216 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
217 xbt_die("Mutex is currently not supported with DPOR, "
218 "use --cfg=model-check/reduction:none");
219 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
220 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
221 simgrid::mc::State* prev_state = i->get();
222 if (reductionMode_ != simgrid::mc::ReductionMode::none
223 && simgrid::mc::request_depend(req, &prev_state->internal_req)) {
224 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
225 XBT_DEBUG("Dependent Transitions:");
226 int value = prev_state->transition.argument;
227 smx_simcall_t prev_req = &prev_state->executed_req;
228 XBT_DEBUG("%s (state=%d)",
229 simgrid::mc::request_to_string(
230 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
232 value = state->transition.argument;
233 prev_req = &state->executed_req;
234 XBT_DEBUG("%s (state=%d)",
235 simgrid::mc::request_to_string(
236 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
240 if (!prev_state->processStates[issuer->pid].isDone())
241 prev_state->interleave(issuer);
243 XBT_DEBUG("Process %p is in done set", req->issuer);
247 } else if (req->issuer == prev_state->internal_req.issuer) {
249 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, prev_state->internal_req.call);
254 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
255 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
256 req->call, issuer->pid, state->num,
257 prev_state->internal_req.call,
258 previous_issuer->pid,
265 if (state->interleaveSize()
266 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
267 /* We found a back-tracking point, let's loop */
268 XBT_DEBUG("Back-tracking to state %d at depth %zi",
269 state->num, stack_.size() + 1);
270 stack_.push_back(std::move(state));
271 this->restoreState();
272 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
273 stack_.back()->num, stack_.size());
276 XBT_DEBUG("Delete state %d at depth %zi",
277 state->num, stack_.size() + 1);
280 return SIMGRID_MC_EXIT_SUCCESS;
283 void SafetyChecker::restoreState()
285 /* Intermediate backtracking */
287 simgrid::mc::State* state = stack_.back().get();
288 if (state->system_state) {
289 simgrid::mc::restore_snapshot(state->system_state);
294 /* Restore the initial state */
295 simgrid::mc::session->restoreInitialState();
297 /* Traverse the stack from the state at position start and re-execute the transitions */
298 for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
299 if (state == stack_.back())
301 session->execute(state->transition);
302 /* Update statistics */
303 mc_model_checker->visited_states++;
304 mc_model_checker->executed_transitions++;
308 void SafetyChecker::init()
310 reductionMode_ = simgrid::mc::reduction_mode;
311 if( _sg_mc_termination)
312 reductionMode_ = simgrid::mc::ReductionMode::none;
313 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
314 reductionMode_ = simgrid::mc::ReductionMode::dpor;
316 if (_sg_mc_termination)
317 XBT_INFO("Check non progressive cycles");
319 XBT_INFO("Check a safety property");
320 simgrid::mc::session->initialize();
322 XBT_DEBUG("Starting the safety algorithm");
324 std::unique_ptr<simgrid::mc::State> initial_state =
325 std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
327 XBT_DEBUG("**************************************************");
328 XBT_DEBUG("Initial state");
330 /* Get an enabled process and insert it in the interleave set of the initial state */
331 for (auto& p : mc_model_checker->process().simix_processes())
332 if (simgrid::mc::process_is_enabled(&p.copy)) {
333 initial_state->interleave(&p.copy);
334 if (reductionMode_ != simgrid::mc::ReductionMode::none)
338 stack_.push_back(std::move(initial_state));
341 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
345 SafetyChecker::~SafetyChecker()
349 Checker* createSafetyChecker(Session& session)
351 return new SafetyChecker(session);