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. */
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/mc_client.h"
22 #include "src/mc/mc_exit.h"
24 #include "src/xbt/mmalloc/mmprivate.h"
28 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
29 "Logging specific to MC safety verification ");
33 static int is_exploration_stack_state(mc_state_t current_state){
36 mc_state_t stack_state;
37 for(item = xbt_fifo_get_first_item(mc_stack); item != NULL; item = xbt_fifo_get_next_item(item)) {
38 stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
39 if(snapshot_compare(stack_state, current_state) == 0){
40 XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
47 static void MC_modelcheck_safety_init(void);
50 * \brief Initialize the DPOR exploration algorithm
52 static void MC_pre_modelcheck_safety()
54 if (_sg_mc_visited > 0)
55 visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
57 mc_state_t initial_state = MC_state_new();
59 XBT_DEBUG("**************************************************");
60 XBT_DEBUG("Initial state");
62 /* Wait for requests (schedules processes) */
63 mc_model_checker->wait_for_requests();
65 /* Get an enabled process and insert it in the interleave set of the initial state */
66 smx_process_t process;
67 MC_EACH_SIMIX_PROCESS(process,
68 if (MC_process_is_enabled(process)) {
69 MC_state_interleave_process(initial_state, process);
70 if (mc_reduce_kind != e_mc_reduce_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 int MC_modelcheck_safety(void)
84 MC_modelcheck_safety_init();
88 smx_simcall_t req = NULL;
89 mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
90 xbt_fifo_item_t item = NULL;
91 mc_visited_state_t visited_state = NULL;
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 == NULL) {
112 req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
113 XBT_DEBUG("Execute: %s", req_str);
116 if (dot_output != NULL) {
117 req_str = MC_request_get_dot_output(req, value);
120 MC_state_set_executed_request(state, req, value);
121 mc_stats->executed_transitions++;
123 // TODO, bundle both operations in a single message
124 // MC_execute_transition(req, value)
126 /* Answer the request */
127 MC_simcall_handle(req, value);
128 mc_model_checker->wait_for_requests();
130 /* Create the new expanded state */
131 next_state = MC_state_new();
133 if(_sg_mc_termination && is_exploration_stack_state(next_state)){
134 MC_show_non_termination();
135 return SIMGRID_MC_EXIT_NON_TERMINATION;
138 if ((visited_state = is_visited_state(next_state)) == NULL) {
140 /* Get an enabled process and insert it in the interleave set of the next state */
141 smx_process_t process = NULL;
142 MC_EACH_SIMIX_PROCESS(process,
143 if (MC_process_is_enabled(process)) {
144 MC_state_interleave_process(next_state, process);
145 if (mc_reduce_kind != e_mc_reduce_none)
150 if (dot_output != NULL)
151 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
155 if (dot_output != NULL)
156 std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
160 xbt_fifo_unshift(mc_stack, next_state);
162 if (dot_output != NULL)
165 /* Let's loop again */
167 /* The interleave set is empty or the maximum depth is reached, let's back-track */
170 if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != NULL) {
172 if (user_max_depth_reached && visited_state == NULL)
173 XBT_DEBUG("User max depth reached !");
174 else if (visited_state == NULL)
175 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
177 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);
181 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
185 /* Trash the current state, no longer needed */
186 xbt_fifo_shift(mc_stack);
187 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
188 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
190 visited_state = NULL;
192 /* Check for deadlocks */
193 if (MC_deadlock_check()) {
194 MC_show_deadlock(NULL);
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 ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) {
206 if (mc_reduce_kind == e_mc_reduce_dpor) {
207 req = MC_state_get_internal_request(state);
208 if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
209 xbt_die("Mutex is currently not supported with DPOR, "
210 "use --cfg=model-check/reduction:none");
211 const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
212 xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
213 if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
214 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
215 XBT_DEBUG("Dependent Transitions:");
216 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
217 req_str = MC_request_to_string(prev_req, value, MC_REQUEST_INTERNAL);
218 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
220 prev_req = MC_state_get_executed_request(state, &value);
221 req_str = MC_request_to_string(prev_req, value, MC_REQUEST_EXECUTED);
222 XBT_DEBUG("%s (state=%d)", req_str, state->num);
226 if (!MC_state_process_is_done(prev_state, issuer))
227 MC_state_interleave_process(prev_state, issuer);
229 XBT_DEBUG("Process %p is in done set", req->issuer);
233 } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
235 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
240 const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
241 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
242 req->call, issuer->pid, state->num,
243 MC_state_get_internal_request(prev_state)->call,
244 previous_issuer->pid,
251 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
252 /* We found a back-tracking point, let's loop */
253 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
254 xbt_fifo_unshift(mc_stack, state);
256 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
259 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
260 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
266 XBT_INFO("No property violation found.");
267 MC_print_statistics(mc_stats);
268 return SIMGRID_MC_EXIT_SUCCESS;
271 static void MC_modelcheck_safety_init(void)
273 if(_sg_mc_termination)
274 mc_reduce_kind = e_mc_reduce_none;
275 else if (mc_reduce_kind == e_mc_reduce_unset)
276 mc_reduce_kind = e_mc_reduce_dpor;
278 if (_sg_mc_termination)
279 XBT_INFO("Check non progressive cycles");
281 XBT_INFO("Check a safety property");
282 mc_model_checker->wait_for_requests();
284 XBT_DEBUG("Starting the safety algorithm");
288 /* Create exploration stack */
289 mc_stack = xbt_fifo_new();
291 MC_pre_modelcheck_safety();
293 /* Save the initial state */
294 initial_global_state = xbt_new0(s_mc_global_t, 1);
295 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);