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::checkNonDeterminism(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;
100 std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
102 while (!stack_.empty()) {
104 /* Get current state */
105 simgrid::mc::State* state = stack_.back().get();
107 XBT_DEBUG("**************************************************");
109 "Exploration depth=%zi (state=%p, num %d)(%u interleave, user_max_depth %d)",
110 stack_.size(), state, state->num,
111 MC_state_interleave_size(state), user_max_depth_reached);
113 /* Update statistics */
114 mc_stats->visited_states++;
116 /* If there are processes to interleave and the maximum depth has not been reached
117 then perform one step of the exploration algorithm */
118 if (stack_.size() <= (std::size_t) _sg_mc_max_depth && !user_max_depth_reached
119 && (req = MC_state_get_request(state, &value)) && visited_state == 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->checkNonDeterminism(next_state.get())){
143 MC_show_non_termination();
144 return SIMGRID_MC_EXIT_NON_TERMINATION;
147 if (_sg_mc_visited == 0
148 || (visited_state = 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, visited_state->other_num == -1 ? visited_state->num : visited_state->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 || user_max_depth_reached
176 || visited_state != nullptr) {
178 if (user_max_depth_reached && visited_state == nullptr)
179 XBT_DEBUG("User max depth reached !");
180 else if (visited_state == nullptr)
181 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
183 XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
186 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
189 /* Trash the current state, no longer needed */
190 XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size());
193 visited_state = nullptr;
195 /* Check for deadlocks */
196 if (mc_model_checker->checkDeadlock()) {
198 return SIMGRID_MC_EXIT_DEADLOCK;
201 /* Traverse the stack backwards until a state with a non empty interleave
202 set is found, deleting all the states that have it empty in the way.
203 For each deleted state, check if the request that has generated it
204 (from it's predecesor state), depends on any other previous request
205 executed before it. If it does then add it to the interleave set of the
206 state that executed that previous request. */
208 while (!stack_.empty()) {
209 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
211 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
212 req = MC_state_get_internal_request(state.get());
213 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
214 xbt_die("Mutex is currently not supported with DPOR, "
215 "use --cfg=model-check/reduction:none");
216 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
217 for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
218 simgrid::mc::State* prev_state = i->get();
219 if (reductionMode_ != simgrid::mc::ReductionMode::none
220 && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
221 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
222 XBT_DEBUG("Dependent Transitions:");
223 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
224 char* req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
225 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
227 prev_req = MC_state_get_executed_request(state.get(), &value);
228 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
229 XBT_DEBUG("%s (state=%d)", req_str, state->num);
233 if (!MC_state_process_is_done(prev_state, issuer))
234 MC_state_interleave_process(prev_state, issuer);
236 XBT_DEBUG("Process %p is in done set", req->issuer);
240 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
242 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
247 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
248 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
249 req->call, issuer->pid, state->num,
250 MC_state_get_internal_request(prev_state)->call,
251 previous_issuer->pid,
258 if (MC_state_interleave_size(state.get())
259 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
260 /* We found a back-tracking point, let's loop */
261 XBT_DEBUG("Back-tracking to state %d at depth %zi",
262 state->num, stack_.size() + 1);
263 stack_.push_back(std::move(state));
264 simgrid::mc::replay(stack_);
265 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
266 stack_.back()->num, stack_.size());
269 XBT_DEBUG("Delete state %d at depth %zi",
270 state->num, stack_.size() + 1);
276 XBT_INFO("No property violation found.");
277 MC_print_statistics(mc_stats);
278 initial_global_state = nullptr;
279 return SIMGRID_MC_EXIT_SUCCESS;
282 void SafetyChecker::init()
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");
294 mc_model_checker->wait_for_requests();
296 XBT_DEBUG("Starting the safety algorithm");
298 std::unique_ptr<simgrid::mc::State> initial_state =
299 std::unique_ptr<simgrid::mc::State>(MC_state_new());
301 XBT_DEBUG("**************************************************");
302 XBT_DEBUG("Initial state");
304 /* Wait for requests (schedules processes) */
305 mc_model_checker->wait_for_requests();
307 /* Get an enabled process and insert it in the interleave set of the initial state */
308 for (auto& p : mc_model_checker->process().simix_processes())
309 if (simgrid::mc::process_is_enabled(&p.copy)) {
310 MC_state_interleave_process(initial_state.get(), &p.copy);
311 if (reductionMode_ != simgrid::mc::ReductionMode::none)
315 stack_.push_back(std::move(initial_state));
317 /* Save the initial state */
318 initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
319 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
322 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
326 SafetyChecker::~SafetyChecker()
330 Checker* createSafetyChecker(Session& session)
332 return new SafetyChecker(session);