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()
100 while (!stack_.empty()) {
102 /* Get current state */
103 simgrid::mc::State* state = stack_.back().get();
105 XBT_DEBUG("**************************************************");
107 "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
108 stack_.size(), state, state->num,
109 state->interleaveSize());
111 mc_model_checker->visited_states++;
113 // The interleave set is empty or the maximum depth is reached,
115 smx_simcall_t req = nullptr;
116 if (stack_.size() > (std::size_t) _sg_mc_max_depth
117 || (req = MC_state_get_request(state)) == nullptr
118 || visitedState_ != nullptr) {
119 int res = this->backtrack();
126 // If there are processes to interleave and the maximum depth has not been
127 // reached then perform one step of the exploration algorithm.
128 XBT_DEBUG("Execute: %s",
129 simgrid::mc::request_to_string(
130 req, state->transition.argument, simgrid::mc::RequestType::simix).c_str());
133 if (dot_output != nullptr)
134 req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument);
136 mc_model_checker->executed_transitions++;
138 /* Answer the request */
139 this->getSession().execute(state->transition);
141 /* Create the new expanded state */
142 std::unique_ptr<simgrid::mc::State> next_state =
143 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
145 if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
146 MC_show_non_termination();
147 return SIMGRID_MC_EXIT_NON_TERMINATION;
150 if (_sg_mc_visited == 0
151 || (visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true)) == nullptr) {
153 /* Get an enabled process and insert it in the interleave set of the next state */
154 for (auto& p : mc_model_checker->process().simix_processes())
155 if (simgrid::mc::process_is_enabled(p.copy.getBuffer())) {
156 next_state->interleave(p.copy.getBuffer());
157 if (reductionMode_ != simgrid::mc::ReductionMode::none)
161 if (dot_output != nullptr)
162 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
163 state->num, next_state->num, req_str.c_str());
165 } else if (dot_output != nullptr)
166 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
168 visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str());
170 stack_.push_back(std::move(next_state));
173 XBT_INFO("No property violation found.");
174 simgrid::mc::session->logState();
175 return SIMGRID_MC_EXIT_SUCCESS;
178 int SafetyChecker::backtrack()
180 if (stack_.size() > (std::size_t) _sg_mc_max_depth
181 || visitedState_ != nullptr) {
182 if (visitedState_ == nullptr)
183 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
185 XBT_DEBUG("State already visited (equal to state %d),"
186 " exploration stopped on this path.",
187 visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
189 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
194 visitedState_ = nullptr;
196 /* Check for deadlocks */
197 if (mc_model_checker->checkDeadlock()) {
199 return SIMGRID_MC_EXIT_DEADLOCK;
202 /* Traverse the stack backwards until a state with a non empty interleave
203 set is found, deleting all the states that have it empty in the way.
204 For each deleted state, check if the request that has generated it
205 (from it's predecesor state), depends on any other previous request
206 executed before it. If it does then add it to the interleave set of the
207 state that executed that previous request. */
209 while (!stack_.empty()) {
210 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
212 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
213 smx_simcall_t req = &state->internal_req;
214 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
215 xbt_die("Mutex is currently not supported with DPOR, "
216 "use --cfg=model-check/reduction:none");
217 const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
218 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
219 simgrid::mc::State* prev_state = i->get();
220 if (simgrid::mc::request_depend(req, &prev_state->internal_req)) {
221 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
222 XBT_DEBUG("Dependent Transitions:");
223 int value = prev_state->transition.argument;
224 smx_simcall_t prev_req = &prev_state->executed_req;
225 XBT_DEBUG("%s (state=%d)",
226 simgrid::mc::request_to_string(
227 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
229 value = state->transition.argument;
230 prev_req = &state->executed_req;
231 XBT_DEBUG("%s (state=%d)",
232 simgrid::mc::request_to_string(
233 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
237 if (!prev_state->processStates[issuer->pid].isDone())
238 prev_state->interleave(issuer);
240 XBT_DEBUG("Process %p is in done set", req->issuer);
244 } else if (req->issuer == prev_state->internal_req.issuer) {
246 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, prev_state->internal_req.call);
251 const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
252 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
253 req->call, issuer->pid, state->num,
254 prev_state->internal_req.call,
255 previous_issuer->pid,
262 if (state->interleaveSize()
263 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
264 /* We found a back-tracking point, let's loop */
265 XBT_DEBUG("Back-tracking to state %d at depth %zi",
266 state->num, stack_.size() + 1);
267 stack_.push_back(std::move(state));
268 this->restoreState();
269 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
270 stack_.back()->num, stack_.size());
273 XBT_DEBUG("Delete state %d at depth %zi",
274 state->num, stack_.size() + 1);
277 return SIMGRID_MC_EXIT_SUCCESS;
280 void SafetyChecker::restoreState()
282 /* Intermediate backtracking */
284 simgrid::mc::State* state = stack_.back().get();
285 if (state->system_state) {
286 simgrid::mc::restore_snapshot(state->system_state);
291 /* Restore the initial state */
292 simgrid::mc::session->restoreInitialState();
294 /* Traverse the stack from the state at position start and re-execute the transitions */
295 for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
296 if (state == stack_.back())
298 session->execute(state->transition);
299 /* Update statistics */
300 mc_model_checker->visited_states++;
301 mc_model_checker->executed_transitions++;
305 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
307 reductionMode_ = simgrid::mc::reduction_mode;
308 if (_sg_mc_termination)
309 reductionMode_ = simgrid::mc::ReductionMode::none;
310 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
311 reductionMode_ = simgrid::mc::ReductionMode::dpor;
313 if (_sg_mc_termination)
314 XBT_INFO("Check non progressive cycles");
316 XBT_INFO("Check a safety property");
317 simgrid::mc::session->initialize();
319 XBT_DEBUG("Starting the safety algorithm");
321 std::unique_ptr<simgrid::mc::State> initial_state =
322 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
324 XBT_DEBUG("**************************************************");
325 XBT_DEBUG("Initial state");
327 /* Get an enabled process and insert it in the interleave set of the initial state */
328 for (auto& p : mc_model_checker->process().simix_processes())
329 if (simgrid::mc::process_is_enabled(p.copy.getBuffer())) {
330 initial_state->interleave(p.copy.getBuffer());
331 if (reductionMode_ != simgrid::mc::ReductionMode::none)
335 stack_.push_back(std::move(initial_state));
338 SafetyChecker::~SafetyChecker()
342 Checker* createSafetyChecker(Session& session)
344 return new SafetyChecker(session);