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 char* req_str = simgrid::mc::request_to_string(
86 req, value, simgrid::mc::RequestType::executed);
87 trace.push_back(req_str);
94 int SafetyChecker::run()
99 smx_simcall_t req = nullptr;
101 while (!stack_.empty()) {
103 /* Get current state */
104 simgrid::mc::State* state = stack_.back().get();
106 XBT_DEBUG("**************************************************");
108 "Exploration depth=%zi (state=%p, num %d)(%u interleave)",
109 stack_.size(), state, state->num,
110 MC_state_interleave_size(state));
112 /* Update statistics */
113 mc_stats->visited_states++;
115 /* If there are processes to interleave and the maximum depth has not been reached
116 then perform one step of the exploration algorithm */
117 if (stack_.size() <= (std::size_t) _sg_mc_max_depth
118 && (req = MC_state_get_request(state, &value)) != nullptr
119 && visitedState_ == nullptr) {
121 char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
122 XBT_DEBUG("Execute: %s", req_str);
125 if (dot_output != nullptr)
126 req_str = simgrid::mc::request_get_dot_output(req, value);
128 MC_state_set_executed_request(state, req, value);
129 mc_stats->executed_transitions++;
131 // TODO, bundle both operations in a single message
132 // MC_execute_transition(req, value)
134 /* Answer the request */
135 simgrid::mc::handle_simcall(req, value);
136 mc_model_checker->wait_for_requests();
138 /* Create the new expanded state */
139 std::unique_ptr<simgrid::mc::State> next_state =
140 std::unique_ptr<simgrid::mc::State>(MC_state_new());
142 if (_sg_mc_termination && this->checkNonTermination(next_state.get())) {
143 MC_show_non_termination();
144 return SIMGRID_MC_EXIT_NON_TERMINATION;
147 if (_sg_mc_visited == 0
148 || (visitedState_ = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
150 /* Get an enabled process and insert it in the interleave set of the next state */
151 for (auto& p : mc_model_checker->process().simix_processes())
152 if (simgrid::mc::process_is_enabled(&p.copy)) {
153 MC_state_interleave_process(next_state.get(), &p.copy);
154 if (reductionMode_ != simgrid::mc::ReductionMode::none)
158 if (dot_output != nullptr)
159 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
161 } else if (dot_output != nullptr)
162 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str);
164 stack_.push_back(std::move(next_state));
166 if (dot_output != nullptr)
169 /* Let's loop again */
171 /* The interleave set is empty or the maximum depth is reached, let's back-track */
174 if (stack_.size() > (std::size_t) _sg_mc_max_depth
175 || visitedState_ != nullptr) {
176 if (visitedState_ == nullptr)
177 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
179 XBT_DEBUG("State already visited (equal to state %d),"
180 " exploration stopped on this path.",
181 visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num);
183 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
186 /* Trash the current state, no longer needed */
187 XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size());
190 visitedState_ = nullptr;
192 /* Check for deadlocks */
193 if (mc_model_checker->checkDeadlock()) {
195 return SIMGRID_MC_EXIT_DEADLOCK;
198 /* Traverse the stack backwards until a state with a non empty interleave
199 set is found, deleting all the states that have it empty in the way.
200 For each deleted state, check if the request that has generated it
201 (from it's predecesor state), depends on any other previous request
202 executed before it. If it does then add it to the interleave set of the
203 state that executed that previous request. */
205 while (!stack_.empty()) {
206 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
208 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
209 req = MC_state_get_internal_request(state.get());
210 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
211 xbt_die("Mutex is currently not supported with DPOR, "
212 "use --cfg=model-check/reduction:none");
213 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
214 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
215 simgrid::mc::State* prev_state = i->get();
216 if (reductionMode_ != simgrid::mc::ReductionMode::none
217 && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
218 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
219 XBT_DEBUG("Dependent Transitions:");
220 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
221 char* req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
222 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
224 prev_req = MC_state_get_executed_request(state.get(), &value);
225 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
226 XBT_DEBUG("%s (state=%d)", req_str, state->num);
230 if (!MC_state_process_is_done(prev_state, issuer))
231 MC_state_interleave_process(prev_state, issuer);
233 XBT_DEBUG("Process %p is in done set", req->issuer);
237 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
239 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
244 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
245 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
246 req->call, issuer->pid, state->num,
247 MC_state_get_internal_request(prev_state)->call,
248 previous_issuer->pid,
255 if (MC_state_interleave_size(state.get())
256 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
257 /* We found a back-tracking point, let's loop */
258 XBT_DEBUG("Back-tracking to state %d at depth %zi",
259 state->num, stack_.size() + 1);
260 stack_.push_back(std::move(state));
261 simgrid::mc::replay(stack_);
262 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
263 stack_.back()->num, stack_.size());
266 XBT_DEBUG("Delete state %d at depth %zi",
267 state->num, stack_.size() + 1);
273 XBT_INFO("No property violation found.");
274 MC_print_statistics(mc_stats);
275 initial_global_state = nullptr;
276 return SIMGRID_MC_EXIT_SUCCESS;
279 void SafetyChecker::init()
281 reductionMode_ = simgrid::mc::reduction_mode;
282 if( _sg_mc_termination)
283 reductionMode_ = simgrid::mc::ReductionMode::none;
284 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
285 reductionMode_ = simgrid::mc::ReductionMode::dpor;
287 if (_sg_mc_termination)
288 XBT_INFO("Check non progressive cycles");
290 XBT_INFO("Check a safety property");
291 mc_model_checker->wait_for_requests();
293 XBT_DEBUG("Starting the safety algorithm");
295 std::unique_ptr<simgrid::mc::State> initial_state =
296 std::unique_ptr<simgrid::mc::State>(MC_state_new());
298 XBT_DEBUG("**************************************************");
299 XBT_DEBUG("Initial state");
301 /* Wait for requests (schedules processes) */
302 mc_model_checker->wait_for_requests();
304 /* Get an enabled process and insert it in the interleave set of the initial state */
305 for (auto& p : mc_model_checker->process().simix_processes())
306 if (simgrid::mc::process_is_enabled(&p.copy)) {
307 MC_state_interleave_process(initial_state.get(), &p.copy);
308 if (reductionMode_ != simgrid::mc::ReductionMode::none)
312 stack_.push_back(std::move(initial_state));
314 /* Save the initial state */
315 initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
316 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
319 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
323 SafetyChecker::~SafetyChecker()
327 Checker* createSafetyChecker(Session& session)
329 return new SafetyChecker(session);