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. */
12 #include <xbt/dynar.h>
13 #include <xbt/dynar.hpp>
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"
28 #include "src/xbt/mmalloc/mmprivate.h"
30 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
31 "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 static int is_exploration_stack_state(simgrid::mc::State* current_state){
59 simgrid::mc::State* stack_state;
60 for(item = xbt_fifo_get_first_item(mc_stack); item != nullptr; item = xbt_fifo_get_next_item(item)) {
61 stack_state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
62 if(snapshot_compare(stack_state, current_state) == 0){
63 XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
70 RecordTrace SafetyChecker::getRecordTrace() // override
74 xbt_fifo_item_t start = xbt_fifo_get_last_item(mc_stack);
75 for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) {
78 simgrid::mc::State* state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
80 smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
81 const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
82 const int pid = issuer->pid;
84 res.push_back(RecordTraceElement(pid, value));
90 std::vector<std::string> SafetyChecker::getTextualTrace() // override
92 std::vector<std::string> trace;
93 for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
94 item; item = xbt_fifo_get_prev_item(item)) {
95 simgrid::mc::State* state = (simgrid::mc::State*)xbt_fifo_get_item_content(item);
97 smx_simcall_t req = MC_state_get_executed_request(state, &value);
99 char* req_str = simgrid::mc::request_to_string(
100 req, value, simgrid::mc::RequestType::executed);
101 trace.push_back(req_str);
108 int SafetyChecker::run()
112 char *req_str = nullptr;
114 smx_simcall_t req = nullptr;
115 simgrid::mc::State* state = nullptr;
116 simgrid::mc::State* prev_state = nullptr;
117 simgrid::mc::State* next_state = nullptr;
118 xbt_fifo_item_t item = nullptr;
119 std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
121 while (xbt_fifo_size(mc_stack) > 0) {
123 /* Get current state */
124 state = (simgrid::mc::State*)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
126 XBT_DEBUG("**************************************************");
128 ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
129 xbt_fifo_size(mc_stack), state, state->num,
130 MC_state_interleave_size(state), user_max_depth_reached);
132 /* Update statistics */
133 mc_stats->visited_states++;
135 /* If there are processes to interleave and the maximum depth has not been reached
136 then perform one step of the exploration algorithm */
137 if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
138 && (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
140 req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
141 XBT_DEBUG("Execute: %s", req_str);
144 if (dot_output != nullptr)
145 req_str = simgrid::mc::request_get_dot_output(req, value);
147 MC_state_set_executed_request(state, req, value);
148 mc_stats->executed_transitions++;
150 // TODO, bundle both operations in a single message
151 // MC_execute_transition(req, value)
153 /* Answer the request */
154 simgrid::mc::handle_simcall(req, value);
155 mc_model_checker->wait_for_requests();
157 /* Create the new expanded state */
158 next_state = MC_state_new();
160 if(_sg_mc_termination && is_exploration_stack_state(next_state)){
161 MC_show_non_termination();
162 return SIMGRID_MC_EXIT_NON_TERMINATION;
165 if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, true)) == nullptr) {
167 /* Get an enabled process and insert it in the interleave set of the next state */
168 for (auto& p : mc_model_checker->process().simix_processes())
169 if (simgrid::mc::process_is_enabled(&p.copy)) {
170 MC_state_interleave_process(next_state, &p.copy);
171 if (reductionMode_ != simgrid::mc::ReductionMode::none)
175 if (dot_output != nullptr)
176 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
178 } else if (dot_output != nullptr)
179 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
182 xbt_fifo_unshift(mc_stack, next_state);
184 if (dot_output != nullptr)
187 /* Let's loop again */
189 /* The interleave set is empty or the maximum depth is reached, let's back-track */
192 if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != nullptr) {
194 if (user_max_depth_reached && visited_state == nullptr)
195 XBT_DEBUG("User max depth reached !");
196 else if (visited_state == nullptr)
197 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
199 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);
202 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
204 /* Trash the current state, no longer needed */
205 xbt_fifo_shift(mc_stack);
206 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
207 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
209 visited_state = nullptr;
211 /* Check for deadlocks */
212 if (mc_model_checker->checkDeadlock()) {
214 return SIMGRID_MC_EXIT_DEADLOCK;
217 /* Traverse the stack backwards until a state with a non empty interleave
218 set is found, deleting all the states that have it empty in the way.
219 For each deleted state, check if the request that has generated it
220 (from it's predecesor state), depends on any other previous request
221 executed before it. If it does then add it to the interleave set of the
222 state that executed that previous request. */
224 while ((state = (simgrid::mc::State*) xbt_fifo_shift(mc_stack))) {
225 if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
226 req = MC_state_get_internal_request(state);
227 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
228 xbt_die("Mutex is currently not supported with DPOR, "
229 "use --cfg=model-check/reduction:none");
230 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
231 xbt_fifo_foreach(mc_stack, item, prev_state, simgrid::mc::State*) {
232 if (reductionMode_ != simgrid::mc::ReductionMode::none
233 && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
234 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
235 XBT_DEBUG("Dependent Transitions:");
236 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
237 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
238 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
240 prev_req = MC_state_get_executed_request(state, &value);
241 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
242 XBT_DEBUG("%s (state=%d)", req_str, state->num);
246 if (!MC_state_process_is_done(prev_state, issuer))
247 MC_state_interleave_process(prev_state, issuer);
249 XBT_DEBUG("Process %p is in done set", req->issuer);
253 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
255 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
260 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
261 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
262 req->call, issuer->pid, state->num,
263 MC_state_get_internal_request(prev_state)->call,
264 previous_issuer->pid,
271 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
272 /* We found a back-tracking point, let's loop */
273 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
274 xbt_fifo_unshift(mc_stack, state);
276 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
279 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
280 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
286 XBT_INFO("No property violation found.");
287 MC_print_statistics(mc_stats);
288 initial_global_state = nullptr;
289 return SIMGRID_MC_EXIT_SUCCESS;
292 void SafetyChecker::init()
294 reductionMode_ = simgrid::mc::reduction_mode;
295 if( _sg_mc_termination)
296 reductionMode_ = simgrid::mc::ReductionMode::none;
297 else if (reductionMode_ == simgrid::mc::ReductionMode::unset)
298 reductionMode_ = simgrid::mc::ReductionMode::dpor;
300 if (_sg_mc_termination)
301 XBT_INFO("Check non progressive cycles");
303 XBT_INFO("Check a safety property");
304 mc_model_checker->wait_for_requests();
306 XBT_DEBUG("Starting the safety algorithm");
308 /* Create exploration stack */
309 mc_stack = xbt_fifo_new();
311 simgrid::mc::visited_states.clear();
313 simgrid::mc::State* initial_state = MC_state_new();
315 XBT_DEBUG("**************************************************");
316 XBT_DEBUG("Initial state");
318 /* Wait for requests (schedules processes) */
319 mc_model_checker->wait_for_requests();
321 /* Get an enabled process and insert it in the interleave set of the initial state */
322 for (auto& p : mc_model_checker->process().simix_processes())
323 if (simgrid::mc::process_is_enabled(&p.copy)) {
324 MC_state_interleave_process(initial_state, &p.copy);
325 if (reductionMode_ != simgrid::mc::ReductionMode::none)
329 xbt_fifo_unshift(mc_stack, initial_state);
331 /* Save the initial state */
332 initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
333 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
336 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
340 SafetyChecker::~SafetyChecker()