Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : remove useless debug message and add another one
[simgrid.git] / src / mc / mc_safety.c
1 /* Copyright (c) 2008-2014. The SimGrid Team.
2  * All rights reserved.                                                     */
3
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. */
6
7 #include "mc_private.h"
8
9 #include "xbt/mmalloc/mmprivate.h"
10
11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
12                                 "Logging specific to MC safety verification ");
13
14 xbt_dict_t first_enabled_state;
15
16 /**
17  *  \brief Initialize the DPOR exploration algorithm
18  */
19 void MC_pre_modelcheck_safety()
20 {
21
22   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
23
24   mc_state_t initial_state = NULL;
25   smx_process_t process;
26
27   /* Create the initial state and push it into the exploration stack */
28   if (!mc_mem_set)
29     MC_SET_MC_HEAP;
30
31   if (_sg_mc_visited > 0)
32     visited_states =
33         xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
34
35   if (mc_reduce_kind == e_mc_reduce_dpor)
36     first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
37
38   initial_state = MC_state_new();
39
40   MC_SET_STD_HEAP;
41
42   XBT_DEBUG("**************************************************");
43   XBT_DEBUG("Initial state");
44
45   /* Wait for requests (schedules processes) */
46   MC_wait_for_requests();
47
48   MC_SET_MC_HEAP;
49
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)
55         break;
56     }
57   }
58
59   xbt_fifo_unshift(mc_stack, initial_state);
60
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);
71         xbt_free(key);
72       }
73     }
74   }
75
76   if (!mc_mem_set)
77     MC_SET_STD_HEAP;
78 }
79
80
81 /** \brief Model-check the application using a DFS exploration
82  *         with DPOR (Dynamic Partial Order Reductions)
83  */
84 void MC_modelcheck_safety(void)
85 {
86
87   char *req_str = NULL;
88   int value;
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;
95   int pos;
96   int visited_state = -1;
97   int enabled = 0;
98
99   while (xbt_fifo_size(mc_stack) > 0) {
100
101     /* Get current state */
102     state = (mc_state_t)
103         xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
104
105     XBT_DEBUG("**************************************************");
106     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));
111
112     /* Update statistics */
113     mc_stats->visited_states++;
114
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) {
119
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);
124         xbt_free(req_str);
125       }
126
127       MC_SET_MC_HEAP;
128       if (dot_output != NULL)
129         req_str = MC_request_get_dot_output(req, value);
130       MC_SET_STD_HEAP;
131
132       MC_state_set_executed_request(state, req, value);
133       mc_stats->executed_transitions++;
134
135       if (mc_reduce_kind == e_mc_reduce_dpor) {
136         MC_SET_MC_HEAP;
137         char *key = bprintf("%lu", req->issuer->pid);
138         xbt_dict_remove(first_enabled_state, key);
139         xbt_free(key);
140         MC_SET_STD_HEAP;
141       }
142
143       /* Answer the request */
144       SIMIX_simcall_pre(req, value);
145
146       /* Wait for requests (schedules processes) */
147       MC_wait_for_requests();
148
149       /* Create the new expanded state */
150       MC_SET_MC_HEAP;
151
152       next_state = MC_state_new();
153
154       if ((visited_state = is_visited_state()) == -1) {
155
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)
161               break;
162           }
163         }
164
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);
168         }
169
170         if (dot_output != NULL)
171           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
172                   next_state->num, req_str);
173
174       } else {
175
176         if (dot_output != NULL)
177           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
178                   visited_state, req_str);
179
180       }
181
182       xbt_fifo_unshift(mc_stack, next_state);
183
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);
192             }
193             xbt_free(key);
194           }
195         }
196       }
197
198       if (dot_output != NULL)
199         xbt_free(req_str);
200
201       MC_SET_STD_HEAP;
202
203       /* Let's loop again */
204
205       /* The interleave set is empty or the maximum depth is reached, let's back-track */
206     } else {
207
208       if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached
209           || visited_state != -1) {
210
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 ! /!\\ ");
215         else
216           XBT_DEBUG("State already visited, exploration stopped on this path.");
217
218         if (mc_reduce_kind == e_mc_reduce_dpor) {
219           /* Interleave enabled processes in the state in which they have been enabled for the first time */
220           xbt_swag_foreach(process, simix_global->process_list) {
221             if (MC_process_is_enabled(process)) {
222               char *key = bprintf("%lu", process->pid);
223               enabled =
224                   (int) strtoul(xbt_dict_get_or_null(first_enabled_state, key),
225                                 0, 10);
226               xbt_free(key);
227               int cursor = xbt_fifo_size(mc_stack);
228               xbt_fifo_foreach(mc_stack, item, state_test, mc_state_t) {
229                 if (cursor-- == enabled) {
230                   if (!MC_state_process_is_done(state_test, process)
231                       && state_test->num != state->num) {
232                     XBT_DEBUG("Interleave process %lu in state %d",
233                               process->pid, state_test->num);
234                     MC_state_interleave_process(state_test, process);
235                     break;
236                   }
237                 }
238               }
239             }
240           }
241         }
242
243       } else {
244
245         XBT_DEBUG("There are no more processes to interleave. (depth %d)",
246                   xbt_fifo_size(mc_stack) + 1);
247
248       }
249
250       MC_SET_MC_HEAP;
251
252       /* Trash the current state, no longer needed */
253       xbt_fifo_shift(mc_stack);
254       MC_state_delete(state);
255       XBT_DEBUG("Delete state %d at depth %d", state->num,
256                 xbt_fifo_size(mc_stack) + 1);
257
258       MC_SET_STD_HEAP;
259
260       visited_state = -1;
261
262       /* Check for deadlocks */
263       if (MC_deadlock_check()) {
264         MC_show_deadlock(NULL);
265         return;
266       }
267
268       MC_SET_MC_HEAP;
269       /* Traverse the stack backwards until a state with a non empty interleave
270          set is found, deleting all the states that have it empty in the way.
271          For each deleted state, check if the request that has generated it 
272          (from it's predecesor state), depends on any other previous request 
273          executed before it. If it does then add it to the interleave set of the
274          state that executed that previous request. */
275
276       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
277         if (mc_reduce_kind == e_mc_reduce_dpor) {
278           req = MC_state_get_internal_request(state);
279           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
280             if (MC_request_depend
281                 (req, MC_state_get_internal_request(prev_state))) {
282               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
283                 XBT_DEBUG("Dependent Transitions:");
284                 prev_req = MC_state_get_executed_request(prev_state, &value);
285                 req_str = MC_request_to_string(prev_req, value);
286                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
287                 xbt_free(req_str);
288                 prev_req = MC_state_get_executed_request(state, &value);
289                 req_str = MC_request_to_string(prev_req, value);
290                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
291                 xbt_free(req_str);
292               }
293
294               if (!MC_state_process_is_done(prev_state, req->issuer))
295                 MC_state_interleave_process(prev_state, req->issuer);
296               else
297                 XBT_DEBUG("Process %p is in done set", req->issuer);
298
299               break;
300
301             } else if (req->issuer ==
302                        MC_state_get_internal_request(prev_state)->issuer) {
303
304               XBT_DEBUG("Simcall %d and %d with same issuer", req->call,
305                         MC_state_get_internal_request(prev_state)->call);
306               break;
307
308             } else {
309
310               XBT_DEBUG
311                   ("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
312                    req->call, req->issuer->pid, state->num,
313                    MC_state_get_internal_request(prev_state)->call,
314                    MC_state_get_internal_request(prev_state)->issuer->pid,
315                    prev_state->num);
316
317             }
318           }
319         }
320
321         if (MC_state_interleave_size(state)
322             && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
323           /* We found a back-tracking point, let's loop */
324           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num,
325                     xbt_fifo_size(mc_stack) + 1);
326           if (_sg_mc_checkpoint) {
327             if (state->system_state != NULL) {
328               MC_restore_snapshot(state->system_state);
329               xbt_fifo_unshift(mc_stack, state);
330               MC_SET_STD_HEAP;
331             } else {
332               pos = xbt_fifo_size(mc_stack);
333               item = xbt_fifo_get_first_item(mc_stack);
334               while (pos > 0) {
335                 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
336                 if (restored_state->system_state != NULL) {
337                   break;
338                 } else {
339                   item = xbt_fifo_get_next_item(item);
340                   pos--;
341                 }
342               }
343               MC_restore_snapshot(restored_state->system_state);
344               xbt_fifo_unshift(mc_stack, state);
345               MC_SET_STD_HEAP;
346               MC_replay(mc_stack, pos);
347             }
348           } else {
349             xbt_fifo_unshift(mc_stack, state);
350             MC_SET_STD_HEAP;
351             MC_replay(mc_stack, -1);
352           }
353           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
354                     xbt_fifo_size(mc_stack));
355           break;
356         } else {
357           XBT_DEBUG("Delete state %d at depth %d", state->num,
358                     xbt_fifo_size(mc_stack) + 1);
359           MC_state_delete(state);
360         }
361       }
362       MC_SET_STD_HEAP;
363     }
364   }
365   MC_print_statistics(mc_stats);
366   MC_SET_STD_HEAP;
367
368   return;
369 }