Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : cleanups, refactoring and apply indent script
[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   if (_sg_mc_visited > 0) {
49     MC_ignore_heap(simix_global->process_to_run->data, 0);
50     MC_ignore_heap(simix_global->process_that_ran->data, 0);
51   }
52
53   MC_SET_MC_HEAP;
54
55   /* Get an enabled process and insert it in the interleave set of the initial state */
56   xbt_swag_foreach(process, simix_global->process_list) {
57     if (MC_process_is_enabled(process)) {
58       MC_state_interleave_process(initial_state, process);
59       if (mc_reduce_kind != e_mc_reduce_none)
60         break;
61     }
62   }
63
64   xbt_fifo_unshift(mc_stack, initial_state);
65
66   if (mc_reduce_kind == e_mc_reduce_dpor) {
67     /* To ensure the soundness of DPOR, we have to keep a list of 
68        processes which are still enabled at each step of the exploration. 
69        If max depth is reached, we interleave them in the state in which they have 
70        been enabled for the first time. */
71     xbt_swag_foreach(process, simix_global->process_list) {
72       if (MC_process_is_enabled(process)) {
73         char *key = bprintf("%lu", process->pid);
74         char *data = bprintf("%d", xbt_fifo_size(mc_stack));
75         xbt_dict_set(first_enabled_state, key, data, NULL);
76         xbt_free(key);
77       }
78     }
79   }
80
81   if (!mc_mem_set)
82     MC_SET_STD_HEAP;
83 }
84
85
86 /** \brief Model-check the application using a DFS exploration
87  *         with DPOR (Dynamic Partial Order Reductions)
88  */
89 void MC_modelcheck_safety(void)
90 {
91
92   char *req_str = NULL;
93   int value;
94   smx_simcall_t req = NULL, prev_req = NULL;
95   mc_state_t state = NULL, prev_state = NULL, next_state =
96       NULL, restored_state = NULL;
97   smx_process_t process = NULL;
98   xbt_fifo_item_t item = NULL;
99   mc_state_t state_test = NULL;
100   int pos;
101   int visited_state = -1;
102   int enabled = 0;
103
104   while (xbt_fifo_size(mc_stack) > 0) {
105
106     /* Get current state */
107     state = (mc_state_t)
108         xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
109
110     XBT_DEBUG("**************************************************");
111     XBT_DEBUG
112         ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
113          xbt_fifo_size(mc_stack), state, state->num,
114          MC_state_interleave_size(state), user_max_depth_reached,
115          xbt_dict_size(first_enabled_state));
116
117     /* Update statistics */
118     mc_stats->visited_states++;
119
120     /* If there are processes to interleave and the maximum depth has not been reached
121        then perform one step of the exploration algorithm */
122     if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
123         && (req = MC_state_get_request(state, &value)) && visited_state == -1) {
124
125       /* Debug information */
126       if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
127         req_str = MC_request_to_string(req, value);
128         XBT_DEBUG("Execute: %s", req_str);
129         xbt_free(req_str);
130       }
131
132       MC_SET_MC_HEAP;
133       if (dot_output != NULL)
134         req_str = MC_request_get_dot_output(req, value);
135       MC_SET_STD_HEAP;
136
137       MC_state_set_executed_request(state, req, value);
138       mc_stats->executed_transitions++;
139
140       if (mc_reduce_kind == e_mc_reduce_dpor) {
141         MC_SET_MC_HEAP;
142         char *key = bprintf("%lu", req->issuer->pid);
143         xbt_dict_remove(first_enabled_state, key);
144         xbt_free(key);
145         MC_SET_STD_HEAP;
146       }
147
148       /* Answer the request */
149       SIMIX_simcall_pre(req, value);
150
151       /* Wait for requests (schedules processes) */
152       MC_wait_for_requests();
153
154       /* Create the new expanded state */
155       MC_SET_MC_HEAP;
156
157       next_state = MC_state_new();
158
159       if ((visited_state = is_visited_state()) == -1) {
160
161         /* Get an enabled process and insert it in the interleave set of the next state */
162         xbt_swag_foreach(process, simix_global->process_list) {
163           if (MC_process_is_enabled(process)) {
164             MC_state_interleave_process(next_state, process);
165             if (mc_reduce_kind != e_mc_reduce_none)
166               break;
167           }
168         }
169
170         if (_sg_mc_checkpoint
171             && ((xbt_fifo_size(mc_stack) + 1) % _sg_mc_checkpoint == 0)) {
172           next_state->system_state = MC_take_snapshot(next_state->num);
173         }
174
175         if (dot_output != NULL)
176           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
177                   next_state->num, req_str);
178
179       } else {
180
181         if (dot_output != NULL)
182           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
183                   visited_state, req_str);
184
185       }
186
187       xbt_fifo_unshift(mc_stack, next_state);
188
189       if (mc_reduce_kind == e_mc_reduce_dpor) {
190         /* Insert in dict all enabled processes, if not included yet */
191         xbt_swag_foreach(process, simix_global->process_list) {
192           if (MC_process_is_enabled(process)) {
193             char *key = bprintf("%lu", process->pid);
194             if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) {
195               char *data = bprintf("%d", xbt_fifo_size(mc_stack));
196               xbt_dict_set(first_enabled_state, key, data, NULL);
197             }
198             xbt_free(key);
199           }
200         }
201       }
202
203       if (dot_output != NULL)
204         xbt_free(req_str);
205
206       MC_SET_STD_HEAP;
207
208       /* Let's loop again */
209
210       /* The interleave set is empty or the maximum depth is reached, let's back-track */
211     } else {
212
213       if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached
214           || visited_state != -1) {
215
216         if (user_max_depth_reached && visited_state == -1)
217           XBT_DEBUG("User max depth reached !");
218         else if (visited_state == -1)
219           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
220
221         if (mc_reduce_kind == e_mc_reduce_dpor) {
222           /* Interleave enabled processes in the state in which they have been enabled for the first time */
223           xbt_swag_foreach(process, simix_global->process_list) {
224             if (MC_process_is_enabled(process)) {
225               char *key = bprintf("%lu", process->pid);
226               enabled =
227                   (int) strtoul(xbt_dict_get_or_null(first_enabled_state, key),
228                                 0, 10);
229               xbt_free(key);
230               int cursor = xbt_fifo_size(mc_stack);
231               xbt_fifo_foreach(mc_stack, item, state_test, mc_state_t) {
232                 if (cursor-- == enabled) {
233                   if (!MC_state_process_is_done(state_test, process)
234                       && state_test->num != state->num) {
235                     XBT_DEBUG("Interleave process %lu in state %d",
236                               process->pid, state_test->num);
237                     MC_state_interleave_process(state_test, process);
238                     break;
239                   }
240                 }
241               }
242             }
243           }
244         }
245
246       } else {
247
248         XBT_DEBUG("There are no more processes to interleave. (depth %d)",
249                   xbt_fifo_size(mc_stack) + 1);
250
251       }
252
253       MC_SET_MC_HEAP;
254
255       /* Trash the current state, no longer needed */
256       xbt_fifo_shift(mc_stack);
257       MC_state_delete(state);
258       XBT_DEBUG("Delete state %d at depth %d", state->num,
259                 xbt_fifo_size(mc_stack) + 1);
260
261       MC_SET_STD_HEAP;
262
263       visited_state = -1;
264
265       /* Check for deadlocks */
266       if (MC_deadlock_check()) {
267         MC_show_deadlock(NULL);
268         return;
269       }
270
271       MC_SET_MC_HEAP;
272       /* Traverse the stack backwards until a state with a non empty interleave
273          set is found, deleting all the states that have it empty in the way.
274          For each deleted state, check if the request that has generated it 
275          (from it's predecesor state), depends on any other previous request 
276          executed before it. If it does then add it to the interleave set of the
277          state that executed that previous request. */
278
279       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
280         if (mc_reduce_kind == e_mc_reduce_dpor) {
281           req = MC_state_get_internal_request(state);
282           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
283             if (MC_request_depend
284                 (req, MC_state_get_internal_request(prev_state))) {
285               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
286                 XBT_DEBUG("Dependent Transitions:");
287                 prev_req = MC_state_get_executed_request(prev_state, &value);
288                 req_str = MC_request_to_string(prev_req, value);
289                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
290                 xbt_free(req_str);
291                 prev_req = MC_state_get_executed_request(state, &value);
292                 req_str = MC_request_to_string(prev_req, value);
293                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
294                 xbt_free(req_str);
295               }
296
297               if (!MC_state_process_is_done(prev_state, req->issuer))
298                 MC_state_interleave_process(prev_state, req->issuer);
299               else
300                 XBT_DEBUG("Process %p is in done set", req->issuer);
301
302               break;
303
304             } else if (req->issuer ==
305                        MC_state_get_internal_request(prev_state)->issuer) {
306
307               XBT_DEBUG("Simcall %d and %d with same issuer", req->call,
308                         MC_state_get_internal_request(prev_state)->call);
309               break;
310
311             } else {
312
313               XBT_DEBUG
314                   ("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
315                    req->call, req->issuer->pid, state->num,
316                    MC_state_get_internal_request(prev_state)->call,
317                    MC_state_get_internal_request(prev_state)->issuer->pid,
318                    prev_state->num);
319
320             }
321           }
322         }
323
324         if (MC_state_interleave_size(state)
325             && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
326           /* We found a back-tracking point, let's loop */
327           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num,
328                     xbt_fifo_size(mc_stack) + 1);
329           if (_sg_mc_checkpoint) {
330             if (state->system_state != NULL) {
331               MC_restore_snapshot(state->system_state);
332               xbt_fifo_unshift(mc_stack, state);
333               MC_SET_STD_HEAP;
334             } else {
335               pos = xbt_fifo_size(mc_stack);
336               item = xbt_fifo_get_first_item(mc_stack);
337               while (pos > 0) {
338                 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
339                 if (restored_state->system_state != NULL) {
340                   break;
341                 } else {
342                   item = xbt_fifo_get_next_item(item);
343                   pos--;
344                 }
345               }
346               MC_restore_snapshot(restored_state->system_state);
347               xbt_fifo_unshift(mc_stack, state);
348               MC_SET_STD_HEAP;
349               MC_replay(mc_stack, pos);
350             }
351           } else {
352             xbt_fifo_unshift(mc_stack, state);
353             MC_SET_STD_HEAP;
354             MC_replay(mc_stack, -1);
355           }
356           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
357                     xbt_fifo_size(mc_stack));
358           break;
359         } else {
360           XBT_DEBUG("Delete state %d at depth %d", state->num,
361                     xbt_fifo_size(mc_stack) + 1);
362           MC_state_delete(state);
363         }
364       }
365       MC_SET_STD_HEAP;
366     }
367   }
368   MC_print_statistics(mc_stats);
369   MC_SET_STD_HEAP;
370
371   return;
372 }