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 int is_exploration_stack_state(mc_state_t current_state){
39 mc_state_t stack_state;
40 for(item = xbt_fifo_get_first_item(mc_stack); item != nullptr; item = xbt_fifo_get_next_item(item)) {
41 stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
42 if(snapshot_compare(stack_state, current_state) == 0){
43 XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
50 static void modelcheck_safety_init(void);
53 * \brief Initialize the DPOR exploration algorithm
55 static void pre_modelcheck_safety()
57 simgrid::mc::visited_states.clear();
59 mc_state_t initial_state = MC_state_new();
61 XBT_DEBUG("**************************************************");
62 XBT_DEBUG("Initial state");
64 /* Wait for requests (schedules processes) */
65 mc_model_checker->wait_for_requests();
67 /* Get an enabled process and insert it in the interleave set of the initial state */
68 for (auto& p : mc_model_checker->process().simix_processes())
69 if (simgrid::mc::process_is_enabled(&p.copy)) {
70 MC_state_interleave_process(initial_state, &p.copy);
71 if (simgrid::mc::reduction_mode != simgrid::mc::ReductionMode::none)
75 xbt_fifo_unshift(mc_stack, initial_state);
79 /** \brief Model-check the application using a DFS exploration
80 * with DPOR (Dynamic Partial Order Reductions)
82 static int modelcheck_safety(void)
84 modelcheck_safety_init();
86 char *req_str = nullptr;
88 smx_simcall_t req = nullptr;
89 mc_state_t state = nullptr, prev_state = NULL, next_state = NULL;
90 xbt_fifo_item_t item = nullptr;
91 std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
93 while (xbt_fifo_size(mc_stack) > 0) {
95 /* Get current state */
96 state = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
98 XBT_DEBUG("**************************************************");
100 ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
101 xbt_fifo_size(mc_stack), state, state->num,
102 MC_state_interleave_size(state), user_max_depth_reached);
104 /* Update statistics */
105 mc_stats->visited_states++;
107 /* If there are processes to interleave and the maximum depth has not been reached
108 then perform one step of the exploration algorithm */
109 if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
110 && (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
112 req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
113 XBT_DEBUG("Execute: %s", req_str);
116 if (dot_output != nullptr)
117 req_str = simgrid::mc::request_get_dot_output(req, value);
119 MC_state_set_executed_request(state, req, value);
120 mc_stats->executed_transitions++;
122 // TODO, bundle both operations in a single message
123 // MC_execute_transition(req, value)
125 /* Answer the request */
126 simgrid::mc::handle_simcall(req, value);
127 mc_model_checker->wait_for_requests();
129 /* Create the new expanded state */
130 next_state = MC_state_new();
132 if(_sg_mc_termination && is_exploration_stack_state(next_state)){
133 MC_show_non_termination();
134 return SIMGRID_MC_EXIT_NON_TERMINATION;
137 if ((visited_state = simgrid::mc::is_visited_state(next_state)) == nullptr) {
139 /* Get an enabled process and insert it in the interleave set of the next state */
140 for (auto& p : mc_model_checker->process().simix_processes())
141 if (simgrid::mc::process_is_enabled(&p.copy)) {
142 MC_state_interleave_process(next_state, &p.copy);
143 if (simgrid::mc::reduction_mode != simgrid::mc::ReductionMode::none)
147 if (dot_output != nullptr)
148 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
150 } else if (dot_output != nullptr)
151 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
154 xbt_fifo_unshift(mc_stack, next_state);
156 if (dot_output != nullptr)
159 /* Let's loop again */
161 /* The interleave set is empty or the maximum depth is reached, let's back-track */
164 if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != nullptr) {
166 if (user_max_depth_reached && visited_state == nullptr)
167 XBT_DEBUG("User max depth reached !");
168 else if (visited_state == nullptr)
169 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
171 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);
174 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
176 /* Trash the current state, no longer needed */
177 xbt_fifo_shift(mc_stack);
178 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
179 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
181 visited_state = nullptr;
183 /* Check for deadlocks */
184 if (mc_model_checker->checkDeadlock()) {
185 MC_show_deadlock(nullptr);
186 return SIMGRID_MC_EXIT_DEADLOCK;
189 /* Traverse the stack backwards until a state with a non empty interleave
190 set is found, deleting all the states that have it empty in the way.
191 For each deleted state, check if the request that has generated it
192 (from it's predecesor state), depends on any other previous request
193 executed before it. If it does then add it to the interleave set of the
194 state that executed that previous request. */
196 while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
197 if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::dpor) {
198 req = MC_state_get_internal_request(state);
199 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
200 xbt_die("Mutex is currently not supported with DPOR, "
201 "use --cfg=model-check/reduction:none");
202 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
203 xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
204 if (simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
205 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
206 XBT_DEBUG("Dependent Transitions:");
207 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
208 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
209 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
211 prev_req = MC_state_get_executed_request(state, &value);
212 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
213 XBT_DEBUG("%s (state=%d)", req_str, state->num);
217 if (!MC_state_process_is_done(prev_state, issuer))
218 MC_state_interleave_process(prev_state, issuer);
220 XBT_DEBUG("Process %p is in done set", req->issuer);
224 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
226 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
231 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
232 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
233 req->call, issuer->pid, state->num,
234 MC_state_get_internal_request(prev_state)->call,
235 previous_issuer->pid,
242 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
243 /* We found a back-tracking point, let's loop */
244 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
245 xbt_fifo_unshift(mc_stack, state);
247 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
250 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
251 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
257 XBT_INFO("No property violation found.");
258 MC_print_statistics(mc_stats);
259 return SIMGRID_MC_EXIT_SUCCESS;
262 static void modelcheck_safety_init(void)
264 if(_sg_mc_termination)
265 simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
266 else if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::unset)
267 simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::dpor;
269 if (_sg_mc_termination)
270 XBT_INFO("Check non progressive cycles");
272 XBT_INFO("Check a safety property");
273 mc_model_checker->wait_for_requests();
275 XBT_DEBUG("Starting the safety algorithm");
279 /* Create exploration stack */
280 mc_stack = xbt_fifo_new();
282 pre_modelcheck_safety();
284 /* Save the initial state */
285 initial_global_state = xbt_new0(s_mc_global_t, 1);
286 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
289 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
293 SafetyChecker::~SafetyChecker()
297 int SafetyChecker::run()
299 return simgrid::mc::modelcheck_safety();