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 %d and %d with same issuer", req->call_, prev_state->internal_req.call_);
237 const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req);
238 XBT_DEBUG("Simcall %d, process %ld (state %d) and simcall %d, process %ld (state %d) are independent",
239 req->call_, issuer->get_pid(), state->num_, prev_state->internal_req.call_,
240 previous_issuer->get_pid(), prev_state->num_);
245 if (state->interleave_size() && stack_.size() < (std::size_t)_sg_mc_max_depth) {
246 /* We found a back-tracking point, let's loop */
247 XBT_DEBUG("Back-tracking to state %d at depth %zu", state->num_, stack_.size() + 1);
248 stack_.push_back(std::move(state));
249 this->restore_state();
250 XBT_DEBUG("Back-tracking to state %d at depth %zu done", stack_.back()->num_, stack_.size());
253 XBT_DEBUG("Delete state %d at depth %zu", state->num_, stack_.size() + 1);
258 void SafetyChecker::restore_state()
260 /* Intermediate backtracking */
261 simgrid::mc::State* last_state = stack_.back().get();
262 if (last_state->system_state) {
263 last_state->system_state->restore(&mc_model_checker->process());
267 /* Restore the initial state */
268 simgrid::mc::session->restore_initial_state();
270 /* Traverse the stack from the state at position start and re-execute the transitions */
271 for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
272 if (state == stack_.back())
274 session->execute(state->transition_);
275 /* Update statistics */
276 mc_model_checker->visited_states++;
277 mc_model_checker->executed_transitions++;
281 SafetyChecker::SafetyChecker(Session& s) : Checker(s)
283 reductionMode_ = simgrid::mc::reduction_mode;
284 if (_sg_mc_termination)
285 reductionMode_ = simgrid::mc::ReductionMode::none;
286 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
287 reductionMode_ = simgrid::mc::ReductionMode::dpor;
289 if (_sg_mc_termination)
290 XBT_INFO("Check non progressive cycles");
292 XBT_INFO("Check a safety property. Reduction is: %s.",
293 (reductionMode_ == simgrid::mc::ReductionMode::none ? "none":
294 (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown")));
295 simgrid::mc::session->initialize();
297 XBT_DEBUG("Starting the safety algorithm");
299 std::unique_ptr<simgrid::mc::State> initial_state =
300 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expanded_states_count_));
302 XBT_DEBUG("**************************************************");
303 XBT_DEBUG("Initial state");
305 /* Get an enabled actor and insert it in the interleave set of the initial state */
306 for (auto& actor : mc_model_checker->process().actors())
307 if (simgrid::mc::actor_is_enabled(actor.copy.get_buffer())) {
308 initial_state->add_interleaving_set(actor.copy.get_buffer());
309 if (reductionMode_ != simgrid::mc::ReductionMode::none)
313 stack_.push_back(std::move(initial_state));
316 Checker* createSafetyChecker(Session& s)
318 return new SafetyChecker(s);