Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
83460ff5da51d240831bf7882ea587e952a77faf
[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_state.h"
8 #include "mc_request.h"
9 #include "mc_safety.h"
10 #include "mc_private.h"
11 #include "mc_record.h"
12
13 #include "xbt/mmalloc/mmprivate.h"
14
15 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
16                                 "Logging specific to MC safety verification ");
17
18 /**
19  *  \brief Initialize the DPOR exploration algorithm
20  */
21 void MC_pre_modelcheck_safety()
22 {
23
24   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
25
26   mc_state_t initial_state = NULL;
27   smx_process_t process;
28
29   /* Create the initial state and push it into the exploration stack */
30   if (!mc_mem_set)
31     MC_SET_MC_HEAP;
32
33   if (_sg_mc_visited > 0)
34     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
35
36   initial_state = MC_state_new();
37
38   MC_SET_STD_HEAP;
39
40   XBT_DEBUG("**************************************************");
41   XBT_DEBUG("Initial state");
42
43   /* Wait for requests (schedules processes) */
44   MC_wait_for_requests();
45
46   MC_SET_MC_HEAP;
47
48   /* Get an enabled process and insert it in the interleave set of the initial state */
49   xbt_swag_foreach(process, simix_global->process_list) {
50     if (MC_process_is_enabled(process)) {
51       MC_state_interleave_process(initial_state, process);
52       if (mc_reduce_kind != e_mc_reduce_none)
53         break;
54     }
55   }
56
57   xbt_fifo_unshift(mc_stack, initial_state);
58
59   if (!mc_mem_set)
60     MC_SET_STD_HEAP;
61 }
62
63
64 /** \brief Model-check the application using a DFS exploration
65  *         with DPOR (Dynamic Partial Order Reductions)
66  */
67 void MC_modelcheck_safety(void)
68 {
69
70   char *req_str = NULL;
71   int value;
72   smx_simcall_t req = NULL, prev_req = NULL;
73   mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
74   smx_process_t process = NULL;
75   xbt_fifo_item_t item = NULL;
76   mc_visited_state_t visited_state = NULL;
77
78   while (xbt_fifo_size(mc_stack) > 0) {
79
80     /* Get current state */
81     state = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
82
83     XBT_DEBUG("**************************************************");
84     XBT_DEBUG
85         ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
86          xbt_fifo_size(mc_stack), state, state->num,
87          MC_state_interleave_size(state), user_max_depth_reached);
88
89     /* Update statistics */
90     mc_stats->visited_states++;
91
92     /* If there are processes to interleave and the maximum depth has not been reached
93        then perform one step of the exploration algorithm */
94     if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
95         && (req = MC_state_get_request(state, &value)) && visited_state == NULL) {
96
97       char* req_str = MC_request_to_string(req, value);  
98       XBT_DEBUG("Execute: %s", req_str);                 
99       xbt_free(req_str);
100
101       if (dot_output != NULL) {
102         MC_SET_MC_HEAP;
103         req_str = MC_request_get_dot_output(req, value);
104         MC_SET_STD_HEAP;
105       }
106
107       MC_state_set_executed_request(state, req, value);
108       mc_stats->executed_transitions++;
109
110       /* Answer the request */
111       SIMIX_simcall_handle(req, value);
112
113       /* Wait for requests (schedules processes) */
114       MC_wait_for_requests();
115
116       /* Create the new expanded state */
117       MC_SET_MC_HEAP;
118
119       next_state = MC_state_new();
120
121       if ((visited_state = is_visited_state(next_state)) == NULL) {
122
123         /* Get an enabled process and insert it in the interleave set of the next state */
124         xbt_swag_foreach(process, simix_global->process_list) {
125           if (MC_process_is_enabled(process)) {
126             MC_state_interleave_process(next_state, process);
127             if (mc_reduce_kind != e_mc_reduce_none)
128               break;
129           }
130         }
131
132         if (dot_output != NULL)
133           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
134
135       } else {
136
137         if (dot_output != NULL)
138           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
139
140       }
141
142       xbt_fifo_unshift(mc_stack, next_state);
143
144       if (dot_output != NULL)
145         xbt_free(req_str);
146
147       MC_SET_STD_HEAP;
148
149       /* Let's loop again */
150
151       /* The interleave set is empty or the maximum depth is reached, let's back-track */
152     } else {
153
154       if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != NULL) {
155
156         if (user_max_depth_reached && visited_state == NULL)
157           XBT_DEBUG("User max depth reached !");
158         else if (visited_state == NULL)
159           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
160         else
161           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);
162
163       } else {
164
165         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
166
167       }
168
169       MC_SET_MC_HEAP;
170
171       /* Trash the current state, no longer needed */
172       xbt_fifo_shift(mc_stack);
173       MC_state_delete(state, !state->in_visited_states ? 1 : 0);
174       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
175
176       MC_SET_STD_HEAP;
177
178       visited_state = NULL;
179
180       /* Check for deadlocks */
181       if (MC_deadlock_check()) {
182         MC_show_deadlock(NULL);
183         return;
184       }
185
186       MC_SET_MC_HEAP;
187       /* Traverse the stack backwards until a state with a non empty interleave
188          set is found, deleting all the states that have it empty in the way.
189          For each deleted state, check if the request that has generated it 
190          (from it's predecesor state), depends on any other previous request 
191          executed before it. If it does then add it to the interleave set of the
192          state that executed that previous request. */
193
194       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
195         if (mc_reduce_kind == e_mc_reduce_dpor) {
196           req = MC_state_get_internal_request(state);
197           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
198             if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
199               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
200                 XBT_DEBUG("Dependent Transitions:");
201                 prev_req = MC_state_get_executed_request(prev_state, &value);
202                 req_str = MC_request_to_string(prev_req, value);
203                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
204                 xbt_free(req_str);
205                 prev_req = MC_state_get_executed_request(state, &value);
206                 req_str = MC_request_to_string(prev_req, value);
207                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
208                 xbt_free(req_str);
209               }
210
211               if (!MC_state_process_is_done(prev_state, req->issuer))
212                 MC_state_interleave_process(prev_state, req->issuer);
213               else
214                 XBT_DEBUG("Process %p is in done set", req->issuer);
215
216               break;
217
218             } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
219
220               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
221               break;
222
223             } else {
224
225               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
226                         req->call, req->issuer->pid, state->num,
227                         MC_state_get_internal_request(prev_state)->call,
228                         MC_state_get_internal_request(prev_state)->issuer->pid,
229                         prev_state->num);
230
231             }
232           }
233         }
234
235         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
236           /* We found a back-tracking point, let's loop */
237           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
238           xbt_fifo_unshift(mc_stack, state);
239           MC_replay(mc_stack);
240           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
241           break;
242         } else {
243           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
244           MC_state_delete(state, !state->in_visited_states ? 1 : 0);
245         }
246       }
247       MC_SET_STD_HEAP;
248     }
249   }
250   MC_print_statistics(mc_stats);
251   MC_SET_STD_HEAP;
252
253   return;
254 }