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 initial_global_state = nullptr;
178 return SIMGRID_MC_EXIT_SUCCESS;
181 int SafetyChecker::backtrack()
183 if (stack_.size() > (std::size_t) _sg_mc_max_depth
184 || visitedState_ != nullptr) {
185 if (visitedState_ == nullptr)
186 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
188 XBT_DEBUG("State already visited (equal to state %d),"
189 " exploration stopped on this path.",
190 visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
192 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
197 visitedState_ = nullptr;
199 /* Check for deadlocks */
200 if (mc_model_checker->checkDeadlock()) {
202 return SIMGRID_MC_EXIT_DEADLOCK;
205 /* Traverse the stack backwards until a state with a non empty interleave
206 set is found, deleting all the states that have it empty in the way.
207 For each deleted state, check if the request that has generated it
208 (from it's predecesor state), depends on any other previous request
209 executed before it. If it does then add it to the interleave set of the
210 state that executed that previous request. */
212 while (!stack_.empty()) {
213 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
215 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
216 smx_simcall_t req = &state->internal_req;
217 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
218 xbt_die("Mutex is currently not supported with DPOR, "
219 "use --cfg=model-check/reduction:none");
220 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
221 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
222 simgrid::mc::State* prev_state = i->get();
223 if (reductionMode_ != simgrid::mc::ReductionMode::none
224 && simgrid::mc::request_depend(req, &prev_state->internal_req)) {
225 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
226 XBT_DEBUG("Dependent Transitions:");
227 int value = prev_state->transition.argument;
228 smx_simcall_t prev_req = &prev_state->executed_req;
229 XBT_DEBUG("%s (state=%d)",
230 simgrid::mc::request_to_string(
231 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
233 value = state->transition.argument;
234 prev_req = &state->executed_req;
235 XBT_DEBUG("%s (state=%d)",
236 simgrid::mc::request_to_string(
237 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
241 if (!prev_state->processStates[issuer->pid].isDone())
242 prev_state->interleave(issuer);
244 XBT_DEBUG("Process %p is in done set", req->issuer);
248 } else if (req->issuer == prev_state->internal_req.issuer) {
250 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, prev_state->internal_req.call);
255 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
256 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
257 req->call, issuer->pid, state->num,
258 prev_state->internal_req.call,
259 previous_issuer->pid,
266 if (state->interleaveSize()
267 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
268 /* We found a back-tracking point, let's loop */
269 XBT_DEBUG("Back-tracking to state %d at depth %zi",
270 state->num, stack_.size() + 1);
271 stack_.push_back(std::move(state));
272 simgrid::mc::replay(stack_);
273 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
274 stack_.back()->num, stack_.size());
277 XBT_DEBUG("Delete state %d at depth %zi",
278 state->num, stack_.size() + 1);
281 return SIMGRID_MC_EXIT_SUCCESS;
284 void SafetyChecker::init()
286 reductionMode_ = simgrid::mc::reduction_mode;
287 if( _sg_mc_termination)
288 reductionMode_ = simgrid::mc::ReductionMode::none;
289 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
290 reductionMode_ = simgrid::mc::ReductionMode::dpor;
292 if (_sg_mc_termination)
293 XBT_INFO("Check non progressive cycles");
295 XBT_INFO("Check a safety property");
296 mc_model_checker->wait_for_requests();
298 XBT_DEBUG("Starting the safety algorithm");
300 std::unique_ptr<simgrid::mc::State> initial_state =
301 std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
303 XBT_DEBUG("**************************************************");
304 XBT_DEBUG("Initial state");
306 /* Get an enabled process and insert it in the interleave set of the initial state */
307 for (auto& p : mc_model_checker->process().simix_processes())
308 if (simgrid::mc::process_is_enabled(&p.copy)) {
309 initial_state->interleave(&p.copy);
310 if (reductionMode_ != simgrid::mc::ReductionMode::none)
314 stack_.push_back(std::move(initial_state));
316 /* Save the initial state */
317 initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
318 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
321 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
325 SafetyChecker::~SafetyChecker()
329 Checker* createSafetyChecker(Session& session)
331 return new SafetyChecker(session);