Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
New trace replayer, as fast as hell, and as boring as hell, too
[simgrid.git] / src / mc / mc_global.c
1 #include <unistd.h>
2 #include <sys/types.h>
3 #include <sys/wait.h>
4
5 #include "../surf/surf_private.h"
6 #include "../simix/private.h"
7 #include "xbt/fifo.h"
8 #include "private.h"
9
10
11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
12                                 "Logging specific to MC (global)");
13
14 /* MC global data structures */
15 mc_snapshot_t initial_snapshot = NULL;
16 xbt_fifo_t mc_stack = NULL;
17 xbt_setset_t mc_setset = NULL;
18 mc_stats_t mc_stats = NULL;
19 mc_state_t mc_current_state = NULL;
20 char mc_replay_mode = FALSE;
21
22 /**
23  *  \brief Initialize the model-checker data structures
24  */
25 void MC_init(void)
26 {
27   smx_process_t process;
28   
29   /* Check if MC is already initialized */
30   if (initial_snapshot)
31     return;
32
33   /* Initialize the data structures that must be persistent across every
34      iteration of the model-checker (in RAW memory) */
35   MC_SET_RAW_MEM;
36
37   /* Initialize statistics */
38   mc_stats = xbt_new0(s_mc_stats_t, 1);
39   mc_stats->state_size = 1;
40
41   /* Create exploration stack */
42   mc_stack = xbt_fifo_new();
43
44   /* Create the container for the sets */
45   mc_setset = xbt_setset_new(20);
46
47   /* Add the existing processes to mc's setset so they have an ID designated */
48   xbt_swag_foreach(process, simix_global->process_list){
49     xbt_setset_elm_add(mc_setset, process);
50   }
51   
52   /* Initialize the control variable */
53   mc_exp_ctl = xbt_new0(e_mc_exp_ctl_t, 1);
54   *mc_exp_ctl = MC_EXPLORE;
55   
56   MC_UNSET_RAW_MEM;
57   
58
59
60   /* Save the initial state */
61 /*  MC_SET_RAW_MEM;
62   initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
63   MC_take_snapshot(initial_snapshot);
64   MC_UNSET_RAW_MEM;*/
65 }
66
67 void MC_modelcheck(void)
68 {
69   int status;
70   pid_t pid;
71
72   /* Compute initial state */
73   MC_init();
74   
75   /* Fork an mc's slave exploration process and wait for it. */
76   /* The forked process will explore a trace until:
77        - a back-tracking point is found (it sets mc_expl_ctl to MC_explore)
78        - there are no more states to explore (it sets mc_expl_ctl to MC_STOP)
79        - a property is invalid (or dead-lock)
80    */
81   while(*mc_exp_ctl == MC_EXPLORE){
82     if((pid = fork())){
83       waitpid(pid, &status, 0);
84       mmalloc_detach(raw_heap);
85       raw_heap = mmalloc_attach(raw_heap_fd, (char*)(std_heap) + STD_HEAP_SIZE + getpagesize());
86
87     if (WIFSIGNALED(status)) {
88       INFO1("killed by signal %d\n", WTERMSIG(status));
89       break;
90     }else if (WIFSTOPPED(status)) {
91       INFO1("stopped by signal %d\n", WSTOPSIG(status));
92       break;
93     }else if (WIFCONTINUED(status)) {
94       INFO0("continued\n");
95       break;
96     }
97      
98     if(*mc_exp_ctl == MC_DEADLOCK){
99       INFO0("**************************");
100       INFO0("*** DEAD-LOCK DETECTED ***");
101       INFO0("**************************");
102       MC_dump_stack(mc_stack);
103       MC_print_statistics(mc_stats);
104       break;
105     }
106       
107     }else{
108       /* if mc_stack is empty then create first state, otherwise replay */
109       if(xbt_fifo_size(mc_stack) == 0)
110         MC_dpor_init();
111       else
112         MC_replay(mc_stack);
113
114       MC_dpor();
115       MC_memory_exit();
116       break;
117     }
118   }    
119   
120   /* If we are the mc's master process then exit */
121   if(pid)
122     MC_exit();
123 }
124
125 void MC_exit(void)
126 {
127   mmalloc_detach(raw_heap);
128   shm_unlink("raw_heap");
129 }
130
131 int MC_random(int min, int max)
132 {
133   /*FIXME: return mc_current_state->executed_transition->random.value;*/
134   return 0;
135 }
136
137 /**
138  * \brief Re-executes from the initial state all the transitions indicated by
139  *        a given model-checker stack.
140  * \param stack The stack with the transitions to execute.
141 */
142 void MC_replay(xbt_fifo_t stack)
143 {
144   char *req_str;
145   smx_req_t req = NULL, saved_req = NULL;
146   xbt_fifo_item_t item;
147   mc_state_t state;
148
149   DEBUG0("**** Begin Replay ****");
150
151   /* Restore the initial state */
152   /*MC_restore_snapshot(initial_snapshot);*/
153
154   MC_wait_for_requests();
155
156   /* Traverse the stack from the initial state and re-execute the transitions */
157   for (item = xbt_fifo_get_last_item(stack);
158        item != xbt_fifo_get_first_item(stack);
159        item = xbt_fifo_get_prev_item(item)) {
160
161     state = (mc_state_t) xbt_fifo_get_item_content(item);
162     saved_req = MC_state_get_executed_request(state);
163    
164     if(saved_req){
165       /* because we got a copy of the executed request, we have to fetch the  
166          real one, pointed by the request field of the issuer process */
167       req = saved_req->issuer->request;
168
169       /* Debug information */
170       if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
171         req_str = MC_request_to_string(req); 
172         DEBUG1("Replay: %s", req_str);
173         xbt_free(req_str);
174       }
175     }
176          
177     SIMIX_request_pre(req);
178     MC_wait_for_requests();
179          
180     /* Update statistics */
181     mc_stats->visited_states++;
182     mc_stats->executed_transitions++;
183   }
184   DEBUG0("**** End Replay ****");
185 }
186
187 /**
188  * \brief Dumps the contents of a model-checker's stack and shows the actual
189  *        execution trace
190  * \param stack The stack to dump
191 */
192 void MC_dump_stack(xbt_fifo_t stack)
193 {
194   mc_state_t state;
195
196   MC_show_stack(stack);
197
198   MC_SET_RAW_MEM;
199   while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
200     MC_state_delete(state);
201   MC_UNSET_RAW_MEM;
202 }
203
204 void MC_show_stack(xbt_fifo_t stack)
205 {
206   mc_state_t state;
207   xbt_fifo_item_t item;
208   smx_req_t req;
209   char *req_str = NULL;
210   
211   for (item = xbt_fifo_get_last_item(stack);
212        (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
213         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
214     req = MC_state_get_executed_request(state);
215     if(req){
216       req_str = MC_request_to_string(req); 
217       INFO1("%s", req_str);
218       xbt_free(req_str);
219     }
220   }
221 }
222
223 /**
224  * \brief Schedules all the process that are ready to run
225  */
226 void MC_wait_for_requests(void)
227 {
228   char *req_str = NULL;
229   smx_req_t req = NULL;
230
231   do {
232     SIMIX_context_runall(simix_global->process_to_run);
233     while((req = SIMIX_request_pop())){
234       if(!SIMIX_request_is_visible(req))
235         SIMIX_request_pre(req);
236       else if(req->call == REQ_COMM_WAITANY)
237         THROW_UNIMPLEMENTED;
238       else if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
239         req_str = MC_request_to_string(req);
240         DEBUG1("Got: %s", req_str);
241         xbt_free(req_str);
242       }
243     }
244   } while (xbt_swag_size(simix_global->process_to_run));
245 }
246
247 /****************************** Statistics ************************************/
248 void MC_print_statistics(mc_stats_t stats)
249 {
250   INFO1("State space size ~= %lu", stats->state_size);
251   INFO1("Expanded states = %lu", stats->expanded_states);
252   INFO1("Visited states = %lu", stats->visited_states);
253   INFO1("Executed transitions = %lu", stats->executed_transitions);
254   INFO1("Expanded / Visited = %lf",
255         (double) stats->visited_states / stats->expanded_states);
256   /*INFO1("Exploration coverage = %lf", 
257      (double)stats->expanded_states / stats->state_size); */
258 }
259
260 /************************* Assertion Checking *********************************/
261 void MC_assert(int prop)
262 {
263   if (MC_IS_ENABLED && !prop) {
264     INFO0("**************************");
265     INFO0("*** PROPERTY NOT VALID ***");
266     INFO0("**************************");
267     INFO0("Counter-example execution trace:");
268     MC_dump_stack(mc_stack);
269     MC_print_statistics(mc_stats);
270     xbt_abort();
271   }
272 }
273
274 void MC_show_deadlock(smx_req_t req)
275 {
276   char *req_str = NULL;
277   INFO0("**************************");
278   INFO0("*** DEAD-LOCK DETECTED ***");
279   INFO0("**************************");
280   INFO0("Locked request:");
281   req_str = MC_request_to_string(req);
282   INFO1("%s", req_str);
283   xbt_free(req_str);
284   INFO0("Counter-example execution trace:");
285   MC_dump_stack(mc_stack);
286 }