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. */
13 #include <xbt/sysdep.h>
15 #include "src/mc/mc_state.h"
16 #include "src/mc/mc_request.h"
17 #include "src/mc/mc_safety.h"
18 #include "src/mc/mc_private.h"
19 #include "src/mc/mc_record.h"
20 #include "src/mc/mc_smx.h"
21 #include "src/mc/Client.hpp"
22 #include "src/mc/mc_exit.h"
23 #include "src/mc/Checker.hpp"
24 #include "src/mc/SafetyChecker.hpp"
25 #include "src/mc/VisitedState.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 static void MC_show_non_termination(void)
36 XBT_INFO("******************************************");
37 XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
38 XBT_INFO("******************************************");
39 XBT_INFO("Counter-example execution trace:");
40 for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
41 XBT_INFO("%s", s.c_str());
42 MC_print_statistics(mc_stats);
45 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
47 simgrid::mc::Snapshot* s1 = state1->system_state.get();
48 simgrid::mc::Snapshot* s2 = state2->system_state.get();
49 int num1 = state1->num;
50 int num2 = state2->num;
51 return snapshot_compare(num1, s1, num2, s2);
54 bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
56 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
57 if (snapshot_compare(i->get(), current_state) == 0){
58 XBT_INFO("Non-progressive cycle : state %d -> state %d",
59 (*i)->num, current_state->num);
65 RecordTrace SafetyChecker::getRecordTrace() // override
68 for (auto const& state : stack_) {
70 smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
71 const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
72 const int pid = issuer->pid;
73 res.push_back(RecordTraceElement(pid, value));
78 std::vector<std::string> SafetyChecker::getTextualTrace() // override
80 std::vector<std::string> trace;
81 for (auto const& state : stack_) {
83 smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
85 trace.push_back(simgrid::mc::request_to_string(
86 req, value, simgrid::mc::RequestType::executed));
91 int SafetyChecker::run()
97 while (!stack_.empty()) {
99 /* Get current state */
100 simgrid::mc::State* state = stack_.back().get();
102 XBT_DEBUG("**************************************************");
104 "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
105 stack_.size(), state, state->num,
106 state->interleaveSize());
108 mc_stats->visited_states++;
110 // The interleave set is empty or the maximum depth is reached,
112 smx_simcall_t req = nullptr;
113 if (stack_.size() > (std::size_t) _sg_mc_max_depth
114 || (req = MC_state_get_request(state, &value)) == nullptr
115 || visitedState_ != nullptr) {
116 int res = this->backtrack();
123 // If there are processes to interleave and the maximum depth has not been
124 // reached then perform one step of the exploration algorithm.
125 XBT_DEBUG("Execute: %s",
126 simgrid::mc::request_to_string(
127 req, value, simgrid::mc::RequestType::simix).c_str());
130 if (dot_output != nullptr)
131 req_str = simgrid::mc::request_get_dot_output(req, value);
133 MC_state_set_executed_request(state, req, value);
134 mc_stats->executed_transitions++;
136 // TODO, bundle both operations in a single message
137 // MC_execute_transition(req, value)
139 /* Answer the request */
140 simgrid::mc::handle_simcall(req, value);
141 mc_model_checker->wait_for_requests();
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());
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(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 MC_state_interleave_process(next_state.get(), &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 MC_print_statistics(mc_stats);
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 = MC_state_get_internal_request(state.get());
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, MC_state_get_internal_request(prev_state))) {
225 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
226 XBT_DEBUG("Dependent Transitions:");
228 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
229 XBT_DEBUG("%s (state=%d)",
230 simgrid::mc::request_to_string(
231 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
233 prev_req = MC_state_get_executed_request(state.get(), &value);
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].done())
241 MC_state_interleave_process(prev_state, issuer);
243 XBT_DEBUG("Process %p is in done set", req->issuer);
247 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
249 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
254 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
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 MC_state_get_internal_request(prev_state)->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 simgrid::mc::replay(stack_);
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::init()
285 reductionMode_ = simgrid::mc::reduction_mode;
286 if( _sg_mc_termination)
287 reductionMode_ = simgrid::mc::ReductionMode::none;
288 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
289 reductionMode_ = simgrid::mc::ReductionMode::dpor;
291 if (_sg_mc_termination)
292 XBT_INFO("Check non progressive cycles");
294 XBT_INFO("Check a safety property");
295 mc_model_checker->wait_for_requests();
297 XBT_DEBUG("Starting the safety algorithm");
299 std::unique_ptr<simgrid::mc::State> initial_state =
300 std::unique_ptr<simgrid::mc::State>(MC_state_new());
302 XBT_DEBUG("**************************************************");
303 XBT_DEBUG("Initial state");
305 /* Wait for requests (schedules processes) */
306 mc_model_checker->wait_for_requests();
308 /* Get an enabled process and insert it in the interleave set of the initial state */
309 for (auto& p : mc_model_checker->process().simix_processes())
310 if (simgrid::mc::process_is_enabled(&p.copy)) {
311 MC_state_interleave_process(initial_state.get(), &p.copy);
312 if (reductionMode_ != simgrid::mc::ReductionMode::none)
316 stack_.push_back(std::move(initial_state));
318 /* Save the initial state */
319 initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
320 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
323 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
327 SafetyChecker::~SafetyChecker()
331 Checker* createSafetyChecker(Session& session)
333 return new SafetyChecker(session);