1 /* Copyright (c) 2016-2019. The SimGrid Team. All rights reserved. */
3 /* This program is free software; you can redistribute it and/or modify it
4 * under the terms of the license (GNU LGPL) which comes with this package. */
14 #include <xbt/sysdep.h>
16 #include "src/mc/Session.hpp"
17 #include "src/mc/Transition.hpp"
18 #include "src/mc/VisitedState.hpp"
19 #include "src/mc/checker/SafetyChecker.hpp"
20 #include "src/mc/mc_config.hpp"
21 #include "src/mc/mc_exit.hpp"
22 #include "src/mc/mc_private.hpp"
23 #include "src/mc/mc_record.hpp"
24 #include "src/mc/mc_request.hpp"
25 #include "src/mc/mc_smx.hpp"
27 #include "src/xbt/mmalloc/mmprivate.h"
29 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
30 "Logging specific to MC safety verification ");
34 void SafetyChecker::check_non_termination(simgrid::mc::State* current_state)
36 for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
37 if (snapshot_equal((*state)->system_state.get(), current_state->system_state.get())) {
38 XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num_, current_state->num_);
39 XBT_INFO("******************************************");
40 XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
41 XBT_INFO("******************************************");
42 XBT_INFO("Counter-example execution trace:");
43 for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
44 XBT_INFO(" %s", s.c_str());
45 simgrid::mc::dumpRecordPath();
46 simgrid::mc::session->log_state();
48 throw simgrid::mc::TerminationError();
52 RecordTrace SafetyChecker::get_record_trace() // override
55 for (auto const& state : stack_)
56 res.push_back(state->get_transition());
60 std::vector<std::string> SafetyChecker::get_textual_trace() // override
62 std::vector<std::string> trace;
63 for (auto const& state : stack_) {
64 int value = state->transition_.argument_;
65 smx_simcall_t req = &state->executed_req_;
67 trace.push_back(simgrid::mc::request_to_string(
68 req, value, simgrid::mc::RequestType::executed));
73 void SafetyChecker::log_state() // override
75 XBT_INFO("Expanded states = %lu", expanded_states_count_);
76 XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
77 XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
80 void SafetyChecker::run()
82 /* This function runs the DFS algorithm the state space.
83 * We do so iteratively instead of recursively, dealing with the call stack manually.
84 * This allows to explore the call stack at wish. */
86 while (not stack_.empty()) {
88 /* Get current state */
89 simgrid::mc::State* state = stack_.back().get();
91 XBT_DEBUG("**************************************************");
92 XBT_VERB("Exploration depth=%zu (state=%p, num %d)(%zu interleave)", stack_.size(), state, state->num_,
93 state->interleave_size());
95 mc_model_checker->visited_states++;
97 // Backtrack if we reached the maximum depth
98 if (stack_.size() > (std::size_t)_sg_mc_max_depth) {
99 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
104 // Backtrack if we are revisiting a state we saw previously
105 if (visited_state_ != nullptr) {
106 XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
107 visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num);
109 visited_state_ = nullptr;
114 // Search an enabled transition in the current state; backtrack if the interleave set is empty
115 // get_request also sets state.transition to be the one corresponding to the returned req
116 smx_simcall_t req = MC_state_get_request(state);
117 // req is now the transition of the process that was selected to be executed
119 if (req == nullptr) {
120 XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size() + 1);
126 // If there are processes to interleave and the maximum depth has not been
127 // reached then perform one step of the exploration algorithm.
130 simgrid::mc::request_to_string(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 /* Actually answer the request: let execute the selected request (MCed does one step) */
139 this->get_session().execute(state->transition_);
141 /* Create the new expanded state (copy the state of MCed into our MCer data) */
142 std::unique_ptr<simgrid::mc::State> next_state =
143 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expanded_states_count_));
145 if (_sg_mc_termination)
146 this->check_non_termination(next_state.get());
148 /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
149 if (_sg_mc_max_visited_states > 0)
150 visited_state_ = visited_states_.addVisitedState(expanded_states_count_, next_state.get(), true);
152 /* If this is a new state (or if we don't care about state-equality reduction) */
153 if (visited_state_ == nullptr) {
155 /* Get an enabled process and insert it in the interleave set of the next state */
156 for (auto& remoteActor : mc_model_checker->process().actors()) {
157 auto actor = remoteActor.copy.get_buffer();
158 if (simgrid::mc::actor_is_enabled(actor)) {
159 next_state->add_interleaving_set(actor);
160 if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
161 break; // With DPOR, we take the first enabled transition
165 if (dot_output != nullptr)
166 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num_, next_state->num_, req_str.c_str());
168 } else if (dot_output != nullptr)
169 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num_,
170 visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num,
173 stack_.push_back(std::move(next_state));
176 XBT_INFO("No property violation found.");
177 simgrid::mc::session->log_state();
180 void SafetyChecker::backtrack()
184 /* Check for deadlocks */
185 if (mc_model_checker->checkDeadlock()) {
187 throw simgrid::mc::DeadlockError();
190 /* Traverse the stack backwards until a state with a non empty interleave
191 set is found, deleting all the states that have it empty in the way.
192 For each deleted state, check if the request that has generated it
193 (from it's predecessor state), depends on any other previous request
194 executed before it. If it does then add it to the interleave set of the
195 state that executed that previous request. */
197 while (not stack_.empty()) {
198 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
200 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
201 smx_simcall_t req = &state->internal_req;
202 if (req->call_ == SIMCALL_MUTEX_LOCK || req->call_ == SIMCALL_MUTEX_TRYLOCK)
203 xbt_die("Mutex is currently not supported with DPOR, use --cfg=model-check/reduction:none");
205 const smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
206 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
207 simgrid::mc::State* prev_state = i->get();
208 if (simgrid::mc::request_depend(req, &prev_state->internal_req)) {
209 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
210 XBT_DEBUG("Dependent Transitions:");
211 int value = prev_state->transition_.argument_;
212 smx_simcall_t prev_req = &prev_state->executed_req_;
213 XBT_DEBUG("%s (state=%d)",
214 simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal).c_str(),
216 value = state->transition_.argument_;
217 prev_req = &state->executed_req_;
218 XBT_DEBUG("%s (state=%d)",
219 simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed).c_str(),
223 if (not prev_state->actor_states_[issuer->get_pid()].is_done())
224 prev_state->add_interleaving_set(issuer);
226 XBT_DEBUG("Process %p is in done set", req->issuer_);
230 } else if (req->issuer_ == prev_state->internal_req.issuer_) {
232 XBT_DEBUG("Simcall %s and %s with same issuer", SIMIX_simcall_name(req->call_),
233 SIMIX_simcall_name(prev_state->internal_req.call_));
238 const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
239 XBT_DEBUG("Simcall %s, process %ld (state %d) and simcall %s, process %ld (state %d) are independent",
240 SIMIX_simcall_name(req->call_), issuer->get_pid(), state->num_,
241 SIMIX_simcall_name(prev_state->internal_req.call_), previous_issuer->get_pid(), prev_state->num_);
246 if (state->interleave_size() && stack_.size() < (std::size_t)_sg_mc_max_depth) {
247 /* We found a back-tracking point, let's loop */
248 XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num_, stack_.size() + 1);
249 stack_.push_back(std::move(state));
250 this->restore_state();
251 XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num_, stack_.size());
254 XBT_DEBUG("Delete state %d at depth %zu", state->num_, stack_.size() + 1);
259 void SafetyChecker::restore_state()
261 /* Intermediate backtracking */
262 simgrid::mc::State* last_state = stack_.back().get();
263 if (last_state->system_state) {
264 last_state->system_state->restore(&mc_model_checker->process());
268 /* Restore the initial state */
269 simgrid::mc::session->restore_initial_state();
271 /* Traverse the stack from the state at position start and re-execute the transitions */
272 for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
273 if (state == stack_.back())
275 session->execute(state->transition_);
276 /* Update statistics */
277 mc_model_checker->visited_states++;
278 mc_model_checker->executed_transitions++;
282 SafetyChecker::SafetyChecker(Session& s) : Checker(s)
284 reductionMode_ = simgrid::mc::reduction_mode;
285 if (_sg_mc_termination)
286 reductionMode_ = simgrid::mc::ReductionMode::none;
287 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
288 reductionMode_ = simgrid::mc::ReductionMode::dpor;
290 if (_sg_mc_termination)
291 XBT_INFO("Check non progressive cycles");
293 XBT_INFO("Check a safety property. Reduction is: %s.",
294 (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
295 (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
296 simgrid::mc::session->initialize();
298 XBT_DEBUG("Starting the safety algorithm");
300 std::unique_ptr<simgrid::mc::State> initial_state =
301 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expanded_states_count_));
303 XBT_DEBUG("**************************************************");
304 XBT_DEBUG("Initial state");
306 /* Get an enabled actor and insert it in the interleave set of the initial state */
307 for (auto& actor : mc_model_checker->process().actors())
308 if (simgrid::mc::actor_is_enabled(actor.copy.get_buffer())) {
309 initial_state->add_interleaving_set(actor.copy.get_buffer());
310 if (reductionMode_ != simgrid::mc::ReductionMode::none)
314 stack_.push_back(std::move(initial_state));
317 Checker* createSafetyChecker(Session& s)
319 return new SafetyChecker(s);