1 /* Copyright (c) 2008-2014. 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. */
7 #include "mc_private.h"
9 #include "xbt/mmalloc/mmprivate.h"
11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
12 "Logging specific to MC safety verification ");
14 xbt_dict_t first_enabled_state;
17 * \brief Initialize the DPOR exploration algorithm
19 void MC_pre_modelcheck_safety()
22 int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
24 mc_state_t initial_state = NULL;
25 smx_process_t process;
27 /* Create the initial state and push it into the exploration stack */
31 if (_sg_mc_visited > 0)
33 xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
35 if (mc_reduce_kind == e_mc_reduce_dpor)
36 first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
38 initial_state = MC_state_new();
42 XBT_DEBUG("**************************************************");
43 XBT_DEBUG("Initial state");
45 /* Wait for requests (schedules processes) */
46 MC_wait_for_requests();
50 /* Get an enabled process and insert it in the interleave set of the initial state */
51 xbt_swag_foreach(process, simix_global->process_list) {
52 if (MC_process_is_enabled(process)) {
53 MC_state_interleave_process(initial_state, process);
54 if (mc_reduce_kind != e_mc_reduce_none)
59 xbt_fifo_unshift(mc_stack, initial_state);
61 if (mc_reduce_kind == e_mc_reduce_dpor) {
62 /* To ensure the soundness of DPOR, we have to keep a list of
63 processes which are still enabled at each step of the exploration.
64 If max depth is reached, we interleave them in the state in which they have
65 been enabled for the first time. */
66 xbt_swag_foreach(process, simix_global->process_list) {
67 if (MC_process_is_enabled(process)) {
68 char *key = bprintf("%lu", process->pid);
69 char *data = bprintf("%d", xbt_fifo_size(mc_stack));
70 xbt_dict_set(first_enabled_state, key, data, NULL);
81 /** \brief Model-check the application using a DFS exploration
82 * with DPOR (Dynamic Partial Order Reductions)
84 void MC_modelcheck_safety(void)
89 smx_simcall_t req = NULL, prev_req = NULL;
90 mc_state_t state = NULL, prev_state = NULL, next_state =
91 NULL, restored_state = NULL;
92 smx_process_t process = NULL;
93 xbt_fifo_item_t item = NULL;
94 mc_state_t state_test = NULL;
96 int visited_state = -1;
99 while (xbt_fifo_size(mc_stack) > 0) {
101 /* Get current state */
103 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
105 XBT_DEBUG("**************************************************");
107 ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
108 xbt_fifo_size(mc_stack), state, state->num,
109 MC_state_interleave_size(state), user_max_depth_reached,
110 xbt_dict_size(first_enabled_state));
112 /* Update statistics */
113 mc_stats->visited_states++;
115 /* If there are processes to interleave and the maximum depth has not been reached
116 then perform one step of the exploration algorithm */
117 if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
118 && (req = MC_state_get_request(state, &value)) && visited_state == -1) {
120 /* Debug information */
121 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
122 req_str = MC_request_to_string(req, value);
123 XBT_DEBUG("Execute: %s", req_str);
128 if (dot_output != NULL)
129 req_str = MC_request_get_dot_output(req, value);
132 MC_state_set_executed_request(state, req, value);
133 mc_stats->executed_transitions++;
135 if (mc_reduce_kind == e_mc_reduce_dpor) {
137 char *key = bprintf("%lu", req->issuer->pid);
138 xbt_dict_remove(first_enabled_state, key);
143 /* Answer the request */
144 SIMIX_simcall_pre(req, value);
146 /* Wait for requests (schedules processes) */
147 MC_wait_for_requests();
149 /* Create the new expanded state */
152 next_state = MC_state_new();
154 if ((visited_state = is_visited_state()) == -1) {
156 /* Get an enabled process and insert it in the interleave set of the next state */
157 xbt_swag_foreach(process, simix_global->process_list) {
158 if (MC_process_is_enabled(process)) {
159 MC_state_interleave_process(next_state, process);
160 if (mc_reduce_kind != e_mc_reduce_none)
165 if (_sg_mc_checkpoint
166 && ((xbt_fifo_size(mc_stack) + 1) % _sg_mc_checkpoint == 0)) {
167 next_state->system_state = MC_take_snapshot(next_state->num);
170 if (dot_output != NULL)
171 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
172 next_state->num, req_str);
176 if (dot_output != NULL)
177 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
178 visited_state, req_str);
182 xbt_fifo_unshift(mc_stack, next_state);
184 if (mc_reduce_kind == e_mc_reduce_dpor) {
185 /* Insert in dict all enabled processes, if not included yet */
186 xbt_swag_foreach(process, simix_global->process_list) {
187 if (MC_process_is_enabled(process)) {
188 char *key = bprintf("%lu", process->pid);
189 if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) {
190 char *data = bprintf("%d", xbt_fifo_size(mc_stack));
191 xbt_dict_set(first_enabled_state, key, data, NULL);
198 if (dot_output != NULL)
203 /* Let's loop again */
205 /* The interleave set is empty or the maximum depth is reached, let's back-track */
208 if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached
209 || visited_state != -1) {
211 if (user_max_depth_reached && visited_state == -1)
212 XBT_DEBUG("User max depth reached !");
213 else if (visited_state == -1)
214 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
216 if (mc_reduce_kind == e_mc_reduce_dpor) {
217 /* Interleave enabled processes in the state in which they have been enabled for the first time */
218 xbt_swag_foreach(process, simix_global->process_list) {
219 if (MC_process_is_enabled(process)) {
220 char *key = bprintf("%lu", process->pid);
222 (int) strtoul(xbt_dict_get_or_null(first_enabled_state, key),
225 int cursor = xbt_fifo_size(mc_stack);
226 xbt_fifo_foreach(mc_stack, item, state_test, mc_state_t) {
227 if (cursor-- == enabled) {
228 if (!MC_state_process_is_done(state_test, process)
229 && state_test->num != state->num) {
230 XBT_DEBUG("Interleave process %lu in state %d",
231 process->pid, state_test->num);
232 MC_state_interleave_process(state_test, process);
243 XBT_DEBUG("There are no more processes to interleave. (depth %d)",
244 xbt_fifo_size(mc_stack) + 1);
250 /* Trash the current state, no longer needed */
251 xbt_fifo_shift(mc_stack);
252 MC_state_delete(state);
253 XBT_DEBUG("Delete state %d at depth %d", state->num,
254 xbt_fifo_size(mc_stack) + 1);
260 /* Check for deadlocks */
261 if (MC_deadlock_check()) {
262 MC_show_deadlock(NULL);
267 /* Traverse the stack backwards until a state with a non empty interleave
268 set is found, deleting all the states that have it empty in the way.
269 For each deleted state, check if the request that has generated it
270 (from it's predecesor state), depends on any other previous request
271 executed before it. If it does then add it to the interleave set of the
272 state that executed that previous request. */
274 while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
275 if (mc_reduce_kind == e_mc_reduce_dpor) {
276 req = MC_state_get_internal_request(state);
277 xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
278 if (MC_request_depend
279 (req, MC_state_get_internal_request(prev_state))) {
280 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
281 XBT_DEBUG("Dependent Transitions:");
282 prev_req = MC_state_get_executed_request(prev_state, &value);
283 req_str = MC_request_to_string(prev_req, value);
284 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
286 prev_req = MC_state_get_executed_request(state, &value);
287 req_str = MC_request_to_string(prev_req, value);
288 XBT_DEBUG("%s (state=%d)", req_str, state->num);
292 if (!MC_state_process_is_done(prev_state, req->issuer))
293 MC_state_interleave_process(prev_state, req->issuer);
295 XBT_DEBUG("Process %p is in done set", req->issuer);
299 } else if (req->issuer ==
300 MC_state_get_internal_request(prev_state)->issuer) {
302 XBT_DEBUG("Simcall %d and %d with same issuer", req->call,
303 MC_state_get_internal_request(prev_state)->call);
309 ("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
310 req->call, req->issuer->pid, state->num,
311 MC_state_get_internal_request(prev_state)->call,
312 MC_state_get_internal_request(prev_state)->issuer->pid,
319 if (MC_state_interleave_size(state)
320 && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
321 /* We found a back-tracking point, let's loop */
322 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num,
323 xbt_fifo_size(mc_stack) + 1);
324 if (_sg_mc_checkpoint) {
325 if (state->system_state != NULL) {
326 MC_restore_snapshot(state->system_state);
327 xbt_fifo_unshift(mc_stack, state);
330 pos = xbt_fifo_size(mc_stack);
331 item = xbt_fifo_get_first_item(mc_stack);
333 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
334 if (restored_state->system_state != NULL) {
337 item = xbt_fifo_get_next_item(item);
341 MC_restore_snapshot(restored_state->system_state);
342 xbt_fifo_unshift(mc_stack, state);
344 MC_replay(mc_stack, pos);
347 xbt_fifo_unshift(mc_stack, state);
349 MC_replay(mc_stack, -1);
351 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
352 xbt_fifo_size(mc_stack));
355 XBT_DEBUG("Delete state %d at depth %d", state->num,
356 xbt_fifo_size(mc_stack) + 1);
357 MC_state_delete(state);
363 MC_print_statistics(mc_stats);