Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : compare the pid of enabled processes before memory introspection
[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
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);
221               enabled =
222                   (int) strtoul(xbt_dict_get_or_null(first_enabled_state, key),
223                                 0, 10);
224               xbt_free(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);
233                     break;
234                   }
235                 }
236               }
237             }
238           }
239         }
240
241       } else {
242
243         XBT_DEBUG("There are no more processes to interleave. (depth %d)",
244                   xbt_fifo_size(mc_stack) + 1);
245
246       }
247
248       MC_SET_MC_HEAP;
249
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);
255
256       MC_SET_STD_HEAP;
257
258       visited_state = -1;
259
260       /* Check for deadlocks */
261       if (MC_deadlock_check()) {
262         MC_show_deadlock(NULL);
263         return;
264       }
265
266       MC_SET_MC_HEAP;
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. */
273
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);
285                 xbt_free(req_str);
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);
289                 xbt_free(req_str);
290               }
291
292               if (!MC_state_process_is_done(prev_state, req->issuer))
293                 MC_state_interleave_process(prev_state, req->issuer);
294               else
295                 XBT_DEBUG("Process %p is in done set", req->issuer);
296
297               break;
298
299             } else if (req->issuer ==
300                        MC_state_get_internal_request(prev_state)->issuer) {
301
302               XBT_DEBUG("Simcall %d and %d with same issuer", req->call,
303                         MC_state_get_internal_request(prev_state)->call);
304               break;
305
306             } else {
307
308               XBT_DEBUG
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,
313                    prev_state->num);
314
315             }
316           }
317         }
318
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);
328               MC_SET_STD_HEAP;
329             } else {
330               pos = xbt_fifo_size(mc_stack);
331               item = xbt_fifo_get_first_item(mc_stack);
332               while (pos > 0) {
333                 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
334                 if (restored_state->system_state != NULL) {
335                   break;
336                 } else {
337                   item = xbt_fifo_get_next_item(item);
338                   pos--;
339                 }
340               }
341               MC_restore_snapshot(restored_state->system_state);
342               xbt_fifo_unshift(mc_stack, state);
343               MC_SET_STD_HEAP;
344               MC_replay(mc_stack, pos);
345             }
346           } else {
347             xbt_fifo_unshift(mc_stack, state);
348             MC_SET_STD_HEAP;
349             MC_replay(mc_stack, -1);
350           }
351           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
352                     xbt_fifo_size(mc_stack));
353           break;
354         } else {
355           XBT_DEBUG("Delete state %d at depth %d", state->num,
356                     xbt_fifo_size(mc_stack) + 1);
357           MC_state_delete(state);
358         }
359       }
360       MC_SET_STD_HEAP;
361     }
362   }
363   MC_print_statistics(mc_stats);
364   MC_SET_STD_HEAP;
365
366   return;
367 }