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"
10 #include "xbt/mmalloc/mmprivate.h"
12 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
13 "Logging specific to MC safety verification ");
15 xbt_dict_t first_enabled_state;
18 * \brief Initialize the DPOR exploration algorithm
20 void MC_pre_modelcheck_safety()
23 int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
25 mc_state_t initial_state = NULL;
26 smx_process_t process;
28 /* Create the initial state and push it into the exploration stack */
32 if (_sg_mc_visited > 0)
34 xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
36 if (mc_reduce_kind == e_mc_reduce_dpor)
37 first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
39 initial_state = MC_state_new();
43 XBT_DEBUG("**************************************************");
44 XBT_DEBUG("Initial state");
46 /* Wait for requests (schedules processes) */
47 MC_wait_for_requests();
51 /* Get an enabled process and insert it in the interleave set of the initial state */
52 xbt_swag_foreach(process, simix_global->process_list) {
53 if (MC_process_is_enabled(process)) {
54 MC_state_interleave_process(initial_state, process);
55 if (mc_reduce_kind != e_mc_reduce_none)
60 xbt_fifo_unshift(mc_stack, initial_state);
62 if (mc_reduce_kind == e_mc_reduce_dpor) {
63 /* To ensure the soundness of DPOR, we have to keep a list of
64 processes which are still enabled at each step of the exploration.
65 If max depth is reached, we interleave them in the state in which they have
66 been enabled for the first time. */
67 xbt_swag_foreach(process, simix_global->process_list) {
68 if (MC_process_is_enabled(process)) {
69 char *key = bprintf("%lu", process->pid);
70 char *data = bprintf("%d", xbt_fifo_size(mc_stack));
71 xbt_dict_set(first_enabled_state, key, data, NULL);
82 /** \brief Model-check the application using a DFS exploration
83 * with DPOR (Dynamic Partial Order Reductions)
85 void MC_modelcheck_safety(void)
90 smx_simcall_t req = NULL, prev_req = NULL;
91 mc_state_t state = NULL, prev_state = NULL, next_state =
92 NULL, restored_state = NULL;
93 smx_process_t process = NULL;
94 xbt_fifo_item_t item = NULL;
95 mc_state_t state_test = NULL;
97 mc_visited_state_t visited_state = NULL;
100 while (xbt_fifo_size(mc_stack) > 0) {
102 /* Get current state */
104 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
106 XBT_DEBUG("**************************************************");
108 ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
109 xbt_fifo_size(mc_stack), state, state->num,
110 MC_state_interleave_size(state), user_max_depth_reached,
111 xbt_dict_size(first_enabled_state));
113 /* Update statistics */
114 mc_stats->visited_states++;
116 /* If there are processes to interleave and the maximum depth has not been reached
117 then perform one step of the exploration algorithm */
118 if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
119 && (req = MC_state_get_request(state, &value)) && visited_state == NULL) {
121 MC_LOG_REQUEST(mc_safety, req, value);
123 if (dot_output != NULL) {
125 req_str = MC_request_get_dot_output(req, value);
129 MC_state_set_executed_request(state, req, value);
130 mc_stats->executed_transitions++;
132 if (mc_reduce_kind == e_mc_reduce_dpor) {
134 char *key = bprintf("%lu", req->issuer->pid);
135 xbt_dict_remove(first_enabled_state, key);
140 /* Answer the request */
141 SIMIX_simcall_handle(req, value);
143 /* Wait for requests (schedules processes) */
144 MC_wait_for_requests();
146 /* Create the new expanded state */
149 next_state = MC_state_new();
151 if ((visited_state = is_visited_state()) == NULL) {
153 /* Get an enabled process and insert it in the interleave set of the next state */
154 xbt_swag_foreach(process, simix_global->process_list) {
155 if (MC_process_is_enabled(process)) {
156 MC_state_interleave_process(next_state, process);
157 if (mc_reduce_kind != e_mc_reduce_none)
162 if (_sg_mc_checkpoint
163 && ((xbt_fifo_size(mc_stack) + 1) % _sg_mc_checkpoint == 0)) {
164 next_state->system_state = MC_take_snapshot(next_state->num);
167 if (dot_output != NULL)
168 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
169 next_state->num, req_str);
173 if (dot_output != NULL)
174 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
175 visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
179 xbt_fifo_unshift(mc_stack, next_state);
181 if (mc_reduce_kind == e_mc_reduce_dpor) {
182 /* Insert in dict all enabled processes, if not included yet */
183 xbt_swag_foreach(process, simix_global->process_list) {
184 if (MC_process_is_enabled(process)) {
185 char *key = bprintf("%lu", process->pid);
186 if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) {
187 char *data = bprintf("%d", xbt_fifo_size(mc_stack));
188 xbt_dict_set(first_enabled_state, key, data, NULL);
195 if (dot_output != NULL)
200 /* Let's loop again */
202 /* The interleave set is empty or the maximum depth is reached, let's back-track */
205 if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached
206 || visited_state != NULL) {
208 if (user_max_depth_reached && visited_state == NULL)
209 XBT_DEBUG("User max depth reached !");
210 else if (visited_state == NULL)
211 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
213 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);
215 if (mc_reduce_kind == e_mc_reduce_dpor) {
216 /* Interleave enabled processes in the state in which they have been enabled for the first time */
217 xbt_swag_foreach(process, simix_global->process_list) {
218 if (MC_process_is_enabled(process)) {
219 char *key = bprintf("%lu", process->pid);
221 (int) strtoul(xbt_dict_get_or_null(first_enabled_state, key),
224 int cursor = xbt_fifo_size(mc_stack);
225 xbt_fifo_foreach(mc_stack, item, state_test, mc_state_t) {
226 if (cursor-- == enabled) {
227 if (!MC_state_process_is_done(state_test, process)
228 && state_test->num != state->num) {
229 XBT_DEBUG("Interleave process %lu in state %d",
230 process->pid, state_test->num);
231 MC_state_interleave_process(state_test, process);
242 XBT_DEBUG("There are no more processes to interleave. (depth %d)",
243 xbt_fifo_size(mc_stack) + 1);
249 /* Trash the current state, no longer needed */
250 xbt_fifo_shift(mc_stack);
251 MC_state_delete(state);
252 XBT_DEBUG("Delete state %d at depth %d", state->num,
253 xbt_fifo_size(mc_stack) + 1);
257 visited_state = NULL;
259 /* Check for deadlocks */
260 if (MC_deadlock_check()) {
261 MC_show_deadlock(NULL);
266 /* Traverse the stack backwards until a state with a non empty interleave
267 set is found, deleting all the states that have it empty in the way.
268 For each deleted state, check if the request that has generated it
269 (from it's predecesor state), depends on any other previous request
270 executed before it. If it does then add it to the interleave set of the
271 state that executed that previous request. */
273 while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
274 if (mc_reduce_kind == e_mc_reduce_dpor) {
275 req = MC_state_get_internal_request(state);
276 xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
277 if (MC_request_depend
278 (req, MC_state_get_internal_request(prev_state))) {
279 if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
280 XBT_DEBUG("Dependent Transitions:");
281 prev_req = MC_state_get_executed_request(prev_state, &value);
282 req_str = MC_request_to_string(prev_req, value);
283 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
285 prev_req = MC_state_get_executed_request(state, &value);
286 req_str = MC_request_to_string(prev_req, value);
287 XBT_DEBUG("%s (state=%d)", req_str, state->num);
291 if (!MC_state_process_is_done(prev_state, req->issuer))
292 MC_state_interleave_process(prev_state, req->issuer);
294 XBT_DEBUG("Process %p is in done set", req->issuer);
298 } else if (req->issuer ==
299 MC_state_get_internal_request(prev_state)->issuer) {
301 XBT_DEBUG("Simcall %d and %d with same issuer", req->call,
302 MC_state_get_internal_request(prev_state)->call);
308 ("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
309 req->call, req->issuer->pid, state->num,
310 MC_state_get_internal_request(prev_state)->call,
311 MC_state_get_internal_request(prev_state)->issuer->pid,
318 if (MC_state_interleave_size(state)
319 && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
320 /* We found a back-tracking point, let's loop */
321 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num,
322 xbt_fifo_size(mc_stack) + 1);
323 if (_sg_mc_checkpoint) {
324 if (state->system_state != NULL) {
325 MC_restore_snapshot(state->system_state);
326 xbt_fifo_unshift(mc_stack, state);
329 pos = xbt_fifo_size(mc_stack);
330 item = xbt_fifo_get_first_item(mc_stack);
332 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
333 if (restored_state->system_state != NULL) {
336 item = xbt_fifo_get_next_item(item);
340 MC_restore_snapshot(restored_state->system_state);
341 xbt_fifo_unshift(mc_stack, state);
343 MC_replay(mc_stack, pos);
346 xbt_fifo_unshift(mc_stack, state);
348 MC_replay(mc_stack, -1);
350 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
351 xbt_fifo_size(mc_stack));
354 XBT_DEBUG("Delete state %d at depth %d", state->num,
355 xbt_fifo_size(mc_stack) + 1);
356 MC_state_delete(state);
362 MC_print_statistics(mc_stats);