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"
29 #include "src/xbt/mmalloc/mmprivate.h"
31 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
32 "Logging specific to MC safety verification ");
36 static void MC_show_non_termination(void)
38 XBT_INFO("******************************************");
39 XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
40 XBT_INFO("******************************************");
41 XBT_INFO("Counter-example execution trace:");
42 for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
43 XBT_INFO("%s", s.c_str());
44 MC_print_statistics(mc_stats);
47 static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2)
49 simgrid::mc::Snapshot* s1 = state1->system_state.get();
50 simgrid::mc::Snapshot* s2 = state2->system_state.get();
51 int num1 = state1->num;
52 int num2 = state2->num;
53 return snapshot_compare(num1, s1, num2, s2);
56 bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
58 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
59 if (snapshot_compare(i->get(), current_state) == 0){
60 XBT_INFO("Non-progressive cycle : state %d -> state %d",
61 (*i)->num, current_state->num);
67 RecordTrace SafetyChecker::getRecordTrace() // override
70 for (auto const& state : stack_) {
72 smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
73 const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
74 const int pid = issuer->pid;
75 res.push_back(RecordTraceElement(pid, value));
80 std::vector<std::string> SafetyChecker::getTextualTrace() // override
82 std::vector<std::string> trace;
83 for (auto const& state : stack_) {
85 smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
87 trace.push_back(simgrid::mc::request_to_string(
88 req, value, simgrid::mc::RequestType::executed));
93 int SafetyChecker::run()
99 while (!stack_.empty()) {
101 /* Get current state */
102 simgrid::mc::State* state = stack_.back().get();
104 XBT_DEBUG("**************************************************");
106 "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
107 stack_.size(), state, state->num,
108 state->interleaveSize());
110 mc_stats->visited_states++;
112 // The interleave set is empty or the maximum depth is reached,
114 smx_simcall_t req = nullptr;
115 if (stack_.size() > (std::size_t) _sg_mc_max_depth
116 || (req = MC_state_get_request(state, &value)) == nullptr
117 || visitedState_ != nullptr) {
118 int res = this->backtrack();
125 // If there are processes to interleave and the maximum depth has not been
126 // reached then perform one step of the exploration algorithm.
127 XBT_DEBUG("Execute: %s",
128 simgrid::mc::request_to_string(
129 req, value, simgrid::mc::RequestType::simix).c_str());
132 if (dot_output != nullptr)
133 req_str = simgrid::mc::request_get_dot_output(req, value);
135 MC_state_set_executed_request(state, req, value);
136 mc_stats->executed_transitions++;
138 // TODO, bundle both operations in a single message
139 // MC_execute_transition(req, value)
141 /* Answer the request */
142 simgrid::mc::handle_simcall(req, value);
143 mc_model_checker->wait_for_requests();
145 /* Create the new expanded state */
146 std::unique_ptr<simgrid::mc::State> next_state =
147 std::unique_ptr<simgrid::mc::State>(MC_state_new());
149 if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
150 MC_show_non_termination();
151 return SIMGRID_MC_EXIT_NON_TERMINATION;
154 if (_sg_mc_visited == 0
155 || (visitedState_ = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
157 /* Get an enabled process and insert it in the interleave set of the next state */
158 for (auto& p : mc_model_checker->process().simix_processes())
159 if (simgrid::mc::process_is_enabled(&p.copy)) {
160 MC_state_interleave_process(next_state.get(), &p.copy);
161 if (reductionMode_ != simgrid::mc::ReductionMode::none)
165 if (dot_output != nullptr)
166 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
167 state->num, next_state->num, req_str.c_str());
169 } else if (dot_output != nullptr)
170 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
172 visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str());
174 stack_.push_back(std::move(next_state));
177 XBT_INFO("No property violation found.");
178 MC_print_statistics(mc_stats);
179 initial_global_state = nullptr;
180 return SIMGRID_MC_EXIT_SUCCESS;
183 int SafetyChecker::backtrack()
185 if (stack_.size() > (std::size_t) _sg_mc_max_depth
186 || visitedState_ != nullptr) {
187 if (visitedState_ == nullptr)
188 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
190 XBT_DEBUG("State already visited (equal to state %d),"
191 " exploration stopped on this path.",
192 visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
194 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
199 visitedState_ = nullptr;
201 /* Check for deadlocks */
202 if (mc_model_checker->checkDeadlock()) {
204 return SIMGRID_MC_EXIT_DEADLOCK;
207 /* Traverse the stack backwards until a state with a non empty interleave
208 set is found, deleting all the states that have it empty in the way.
209 For each deleted state, check if the request that has generated it
210 (from it's predecesor state), depends on any other previous request
211 executed before it. If it does then add it to the interleave set of the
212 state that executed that previous request. */
214 while (!stack_.empty()) {
215 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
217 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
218 smx_simcall_t req = MC_state_get_internal_request(state.get());
219 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
220 xbt_die("Mutex is currently not supported with DPOR, "
221 "use --cfg=model-check/reduction:none");
222 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
223 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
224 simgrid::mc::State* prev_state = i->get();
225 if (reductionMode_ != simgrid::mc::ReductionMode::none
226 && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
227 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
228 XBT_DEBUG("Dependent Transitions:");
230 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
231 XBT_DEBUG("%s (state=%d)",
232 simgrid::mc::request_to_string(
233 prev_req, value, simgrid::mc::RequestType::internal).c_str(),
235 prev_req = MC_state_get_executed_request(state.get(), &value);
236 XBT_DEBUG("%s (state=%d)",
237 simgrid::mc::request_to_string(
238 prev_req, value, simgrid::mc::RequestType::executed).c_str(),
242 if (!prev_state->processStates[issuer->pid].done())
243 MC_state_interleave_process(prev_state, issuer);
245 XBT_DEBUG("Process %p is in done set", req->issuer);
249 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
251 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
256 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
257 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
258 req->call, issuer->pid, state->num,
259 MC_state_get_internal_request(prev_state)->call,
260 previous_issuer->pid,
267 if (state->interleaveSize()
268 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
269 /* We found a back-tracking point, let's loop */
270 XBT_DEBUG("Back-tracking to state %d at depth %zi",
271 state->num, stack_.size() + 1);
272 stack_.push_back(std::move(state));
273 simgrid::mc::replay(stack_);
274 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
275 stack_.back()->num, stack_.size());
278 XBT_DEBUG("Delete state %d at depth %zi",
279 state->num, stack_.size() + 1);
282 return SIMGRID_MC_EXIT_SUCCESS;
285 void SafetyChecker::init()
287 reductionMode_ = simgrid::mc::reduction_mode;
288 if( _sg_mc_termination)
289 reductionMode_ = simgrid::mc::ReductionMode::none;
290 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
291 reductionMode_ = simgrid::mc::ReductionMode::dpor;
293 if (_sg_mc_termination)
294 XBT_INFO("Check non progressive cycles");
296 XBT_INFO("Check a safety property");
297 mc_model_checker->wait_for_requests();
299 XBT_DEBUG("Starting the safety algorithm");
301 std::unique_ptr<simgrid::mc::State> initial_state =
302 std::unique_ptr<simgrid::mc::State>(MC_state_new());
304 XBT_DEBUG("**************************************************");
305 XBT_DEBUG("Initial state");
307 /* Wait for requests (schedules processes) */
308 mc_model_checker->wait_for_requests();
310 /* Get an enabled process and insert it in the interleave set of the initial state */
311 for (auto& p : mc_model_checker->process().simix_processes())
312 if (simgrid::mc::process_is_enabled(&p.copy)) {
313 MC_state_interleave_process(initial_state.get(), &p.copy);
314 if (reductionMode_ != simgrid::mc::ReductionMode::none)
318 stack_.push_back(std::move(initial_state));
320 /* Save the initial state */
321 initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
322 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
325 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
329 SafetyChecker::~SafetyChecker()
333 Checker* createSafetyChecker(Session& session)
335 return new SafetyChecker(session);