1 /* Copyright (c) 2008-2015. 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/mc_client.h"
24 #include "src/mc/mc_exit.h"
26 #include "src/xbt/mmalloc/mmprivate.h"
30 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
31 "Logging specific to MC safety verification ");
38 static int is_exploration_stack_state(mc_state_t current_state){
41 mc_state_t stack_state;
42 for(item = xbt_fifo_get_first_item(mc_stack); item != nullptr; item = xbt_fifo_get_next_item(item)) {
43 stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
44 if(snapshot_compare(stack_state, current_state) == 0){
45 XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
52 static void modelcheck_safety_init(void);
55 * \brief Initialize the DPOR exploration algorithm
57 static void pre_modelcheck_safety()
59 if (_sg_mc_visited > 0)
60 simgrid::mc::visited_states = simgrid::xbt::newDeleteDynar<simgrid::mc::VisitedState>();
62 mc_state_t initial_state = MC_state_new();
64 XBT_DEBUG("**************************************************");
65 XBT_DEBUG("Initial state");
67 /* Wait for requests (schedules processes) */
68 mc_model_checker->wait_for_requests();
70 /* Get an enabled process and insert it in the interleave set of the initial state */
71 for (auto& p : mc_model_checker->process().simix_processes())
72 if (simgrid::mc::process_is_enabled(&p.copy)) {
73 MC_state_interleave_process(initial_state, &p.copy);
74 if (simgrid::mc::reduction_mode != simgrid::mc::ReductionMode::none)
78 xbt_fifo_unshift(mc_stack, initial_state);
82 /** \brief Model-check the application using a DFS exploration
83 * with DPOR (Dynamic Partial Order Reductions)
85 int modelcheck_safety(void)
87 modelcheck_safety_init();
89 char *req_str = nullptr;
91 smx_simcall_t req = nullptr;
92 mc_state_t state = nullptr, prev_state = NULL, next_state = NULL;
93 xbt_fifo_item_t item = nullptr;
94 simgrid::mc::VisitedState* visited_state = nullptr;
96 while (xbt_fifo_size(mc_stack) > 0) {
98 /* Get current state */
99 state = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
101 XBT_DEBUG("**************************************************");
103 ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
104 xbt_fifo_size(mc_stack), state, state->num,
105 MC_state_interleave_size(state), user_max_depth_reached);
107 /* Update statistics */
108 mc_stats->visited_states++;
110 /* If there are processes to interleave and the maximum depth has not been reached
111 then perform one step of the exploration algorithm */
112 if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
113 && (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
115 req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
116 XBT_DEBUG("Execute: %s", req_str);
119 if (dot_output != nullptr)
120 req_str = simgrid::mc::request_get_dot_output(req, value);
122 MC_state_set_executed_request(state, req, value);
123 mc_stats->executed_transitions++;
125 // TODO, bundle both operations in a single message
126 // MC_execute_transition(req, value)
128 /* Answer the request */
129 simgrid::mc::handle_simcall(req, value);
130 mc_model_checker->wait_for_requests();
132 /* Create the new expanded state */
133 next_state = MC_state_new();
135 if(_sg_mc_termination && is_exploration_stack_state(next_state)){
136 MC_show_non_termination();
137 return SIMGRID_MC_EXIT_NON_TERMINATION;
140 if ((visited_state = simgrid::mc::is_visited_state(next_state)) == nullptr) {
142 /* Get an enabled process and insert it in the interleave set of the next state */
143 for (auto& p : mc_model_checker->process().simix_processes())
144 if (simgrid::mc::process_is_enabled(&p.copy)) {
145 MC_state_interleave_process(next_state, &p.copy);
146 if (simgrid::mc::reduction_mode != simgrid::mc::ReductionMode::none)
150 if (dot_output != nullptr)
151 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
153 } else if (dot_output != nullptr)
154 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
157 xbt_fifo_unshift(mc_stack, next_state);
159 if (dot_output != nullptr)
162 /* Let's loop again */
164 /* The interleave set is empty or the maximum depth is reached, let's back-track */
167 if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != nullptr) {
169 if (user_max_depth_reached && visited_state == nullptr)
170 XBT_DEBUG("User max depth reached !");
171 else if (visited_state == nullptr)
172 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
174 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);
177 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
179 /* Trash the current state, no longer needed */
180 xbt_fifo_shift(mc_stack);
181 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
182 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
184 visited_state = nullptr;
186 /* Check for deadlocks */
187 if (MC_deadlock_check()) {
188 MC_show_deadlock(nullptr);
189 return SIMGRID_MC_EXIT_DEADLOCK;
192 /* Traverse the stack backwards until a state with a non empty interleave
193 set is found, deleting all the states that have it empty in the way.
194 For each deleted state, check if the request that has generated it
195 (from it's predecesor state), depends on any other previous request
196 executed before it. If it does then add it to the interleave set of the
197 state that executed that previous request. */
199 while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
200 if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::dpor) {
201 req = MC_state_get_internal_request(state);
202 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
203 xbt_die("Mutex is currently not supported with DPOR, "
204 "use --cfg=model-check/reduction:none");
205 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
206 xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
207 if (simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
208 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
209 XBT_DEBUG("Dependent Transitions:");
210 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
211 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
212 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
214 prev_req = MC_state_get_executed_request(state, &value);
215 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
216 XBT_DEBUG("%s (state=%d)", req_str, state->num);
220 if (!MC_state_process_is_done(prev_state, issuer))
221 MC_state_interleave_process(prev_state, issuer);
223 XBT_DEBUG("Process %p is in done set", req->issuer);
227 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
229 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
234 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
235 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
236 req->call, issuer->pid, state->num,
237 MC_state_get_internal_request(prev_state)->call,
238 previous_issuer->pid,
245 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
246 /* We found a back-tracking point, let's loop */
247 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
248 xbt_fifo_unshift(mc_stack, state);
250 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
253 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
254 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
260 XBT_INFO("No property violation found.");
261 MC_print_statistics(mc_stats);
262 return SIMGRID_MC_EXIT_SUCCESS;
265 static void modelcheck_safety_init(void)
267 if(_sg_mc_termination)
268 simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none;
269 else if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::unset)
270 simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::dpor;
272 if (_sg_mc_termination)
273 XBT_INFO("Check non progressive cycles");
275 XBT_INFO("Check a safety property");
276 mc_model_checker->wait_for_requests();
278 XBT_DEBUG("Starting the safety algorithm");
282 /* Create exploration stack */
283 mc_stack = xbt_fifo_new();
285 pre_modelcheck_safety();
287 /* Save the initial state */
288 initial_global_state = xbt_new0(s_mc_global_t, 1);
289 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);