Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
ac5e674325cbe3241d18adff79f7104a2147f075
[simgrid.git] / src / mc / mc_dpor.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_dpor, mc,
12                                 "Logging specific to MC DPOR exploration");
13
14 /********** Global variables **********/
15
16 xbt_dynar_t visited_states;
17 xbt_dict_t first_enabled_state;
18 xbt_dynar_t initial_communications_pattern;
19 xbt_dynar_t incomplete_communications_pattern;
20 xbt_dynar_t communications_pattern;
21 int nb_comm_pattern;
22
23 /********** Static functions ***********/
24
25 static void comm_pattern_free(mc_comm_pattern_t p){
26   xbt_free(p->rdv);
27   xbt_free(p->data);
28   xbt_free(p);
29   p = NULL;
30 }
31
32 static void comm_pattern_free_voidp( void *p){
33   comm_pattern_free((mc_comm_pattern_t) * (void **)p);
34 }
35
36 static mc_comm_pattern_t get_comm_pattern_from_idx(xbt_dynar_t pattern, unsigned int *idx, e_smx_comm_type_t type, unsigned long proc){
37   mc_comm_pattern_t current_comm;
38   while(*idx < xbt_dynar_length(pattern)){
39     current_comm = (mc_comm_pattern_t)xbt_dynar_get_as(pattern, *idx, mc_comm_pattern_t);
40     if(current_comm->type == type && type == SIMIX_COMM_SEND){
41       if(current_comm->src_proc == proc)
42         return current_comm;
43     }else if(current_comm->type == type && type == SIMIX_COMM_RECEIVE){
44       if(current_comm->dst_proc == proc)
45         return current_comm;
46     }
47     (*idx)++;
48   }
49   return NULL;
50 }
51
52 static int compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2){
53   if(strcmp(comm1->rdv, comm2->rdv) != 0)
54     return 1;
55   if(comm1->src_proc != comm2->src_proc)
56     return 1;
57   if(comm1->dst_proc != comm2->dst_proc)
58     return 1;
59   if(comm1->data_size != comm2->data_size)
60     return 1;
61   if(memcmp(comm1->data, comm2->data, comm1->data_size) != 0)
62     return 1;
63   return 0;
64 }
65
66 static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t pattern){
67
68   if(!xbt_dynar_is_empty(incomplete_communications_pattern))
69     xbt_die("Damn ! Some communications are incomplete that means one or several simcalls are not handle ... ");
70
71   unsigned int cursor = 0, send_index = 0, recv_index = 0;
72   mc_comm_pattern_t comm1, comm2;
73   int comm_comparison = 0;
74   int current_process = 0;
75   while(current_process < simix_process_maxpid){
76     while(cursor < xbt_dynar_length(initial_pattern)){
77       comm1 = (mc_comm_pattern_t)xbt_dynar_get_as(initial_pattern, cursor, mc_comm_pattern_t);
78       if(comm1->type == SIMIX_COMM_SEND && comm1->src_proc == current_process){
79         comm2 = get_comm_pattern_from_idx(pattern, &send_index, comm1->type, current_process);
80         comm_comparison = compare_comm_pattern(comm1, comm2);
81         if(comm_comparison == 1){
82           initial_state_safety->send_deterministic = 0;
83           initial_state_safety->comm_deterministic = 0;
84           return;
85         }
86         send_index++;
87       }else if(comm1->type == SIMIX_COMM_RECEIVE && comm1->dst_proc == current_process){
88         comm2 = get_comm_pattern_from_idx(pattern, &recv_index, comm1->type, current_process);
89         comm_comparison = compare_comm_pattern(comm1, comm2);
90         if(comm_comparison == 1){
91           initial_state_safety->comm_deterministic = 0;
92           if(!_sg_mc_send_determinism)
93             return;
94         }
95         recv_index++;
96       }
97       cursor++;
98     }
99     cursor = 0;
100     send_index = 0;
101     recv_index = 0;
102     current_process++;
103   }
104 }
105
106 void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm){
107   mc_comm_pattern_t current_pattern;
108   unsigned int cursor = 0;
109   int index;
110   int completed = 0;
111   void *addr_pointed;
112   xbt_dynar_foreach(incomplete_communications_pattern, cursor, index){
113     current_pattern = (mc_comm_pattern_t)xbt_dynar_get_as(list, index, mc_comm_pattern_t);
114     if(current_pattern->comm == comm){
115       current_pattern->src_proc = comm->comm.src_proc->pid;
116       current_pattern->dst_proc = comm->comm.dst_proc->pid;
117       current_pattern->src_host = simcall_host_get_name(comm->comm.src_proc->smx_host);
118       current_pattern->dst_host = simcall_host_get_name(comm->comm.dst_proc->smx_host);
119       if(current_pattern->data_size == -1){
120         current_pattern->data_size = *(comm->comm.dst_buff_size);
121         current_pattern->data = xbt_malloc0(current_pattern->data_size);
122         addr_pointed = *(void **)comm->comm.src_buff;
123         if(addr_pointed > std_heap && addr_pointed < ((xbt_mheap_t)std_heap)->breakval)
124           memcpy(current_pattern->data, addr_pointed, current_pattern->data_size);
125         else
126           memcpy(current_pattern->data, comm->comm.src_buff, current_pattern->data_size);
127       }
128       xbt_dynar_remove_at(incomplete_communications_pattern, cursor, NULL);
129       completed++;
130       if(completed == 2)
131         return;
132       cursor--;
133     }
134   }
135 }
136
137 void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
138   mc_comm_pattern_t pattern = NULL;
139   pattern = xbt_new0(s_mc_comm_pattern_t, 1);
140   pattern->num = ++nb_comm_pattern;
141   pattern->data_size = -1;
142   void * addr_pointed;
143   if(call == 1){ // ISEND
144     pattern->comm = simcall_comm_isend__get__result(request);
145     pattern->type = SIMIX_COMM_SEND;
146     pattern->src_proc = pattern->comm->comm.src_proc->pid;
147     pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
148     pattern->data_size = pattern->comm->comm.src_buff_size;
149     pattern->data = xbt_malloc0(pattern->data_size);
150     addr_pointed = *(void **)pattern->comm->comm.src_buff;
151     if(addr_pointed > std_heap && addr_pointed < ((xbt_mheap_t)std_heap)->breakval)
152       memcpy(pattern->data, addr_pointed, pattern->data_size);
153     else
154       memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
155   }else{ // IRECV
156     pattern->comm = simcall_comm_irecv__get__result(request);
157     pattern->type = SIMIX_COMM_RECEIVE;
158     pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
159     pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
160   }
161   
162   if(pattern->comm->comm.rdv != NULL)
163     pattern->rdv = strdup(pattern->comm->comm.rdv->name);
164   else
165     pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name);
166   
167   xbt_dynar_push(list, &pattern);
168
169   xbt_dynar_push_as(incomplete_communications_pattern, int, xbt_dynar_length(list) - 1);
170
171 }
172
173 static void print_communications_pattern(xbt_dynar_t comms_pattern){
174   unsigned int cursor = 0;
175   mc_comm_pattern_t current_comm;
176   xbt_dynar_foreach(comms_pattern, cursor, current_comm){
177     if(current_comm->type == SIMIX_COMM_SEND)
178       XBT_INFO("[(%lu) %s -> (%lu) %s] %s ", current_comm->src_proc, current_comm->src_host, current_comm->dst_proc, current_comm->dst_host, "iSend");
179     else
180       XBT_INFO("[(%lu) %s <- (%lu) %s] %s ", current_comm->dst_proc, current_comm->dst_host, current_comm->src_proc, current_comm->src_host, "iRecv");
181   }
182 }
183
184 static void visited_state_free(mc_visited_state_t state){
185   if(state){
186     MC_free_snapshot(state->system_state);
187     xbt_free(state);
188   }
189 }
190
191 static void visited_state_free_voidp(void *s){
192   visited_state_free((mc_visited_state_t) * (void **) s);
193 }
194
195 /** \brief Save the current state
196  *
197  *  \return Snapshot of the current state.
198  */
199 static mc_visited_state_t visited_state_new(){
200
201   mc_visited_state_t new_state = NULL;
202   new_state = xbt_new0(s_mc_visited_state_t, 1);
203   new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
204   new_state->nb_processes = xbt_swag_size(simix_global->process_list);
205   new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
206   new_state->num = mc_stats->expanded_states;
207   new_state->other_num = -1;
208
209   return new_state;
210   
211 }
212
213 /** \brief Find a suitable subrange of candidate duplicates for a given state
214  *
215  *  \param all_ pairs dynamic array of states with candidate duplicates of the current state;
216  *  \param pair current state;
217  *  \param min (output) index of the beginning of the the subrange
218  *  \param max (output) index of the enf of the subrange
219  *
220  *  Given a suitably ordered array of state, this function extracts a subrange
221  *  (with index *min <= i <= *max) with candidate duplicates of the given state.
222  *  This function uses only fast discriminating criterions and does not use the
223  *  full state comparison algorithms.
224  *
225  *  The states in all_pairs MUST be ordered using a (given) weak order
226  *  (based on nb_processes and heap_bytes_used).
227  *  The subrange is the subrange of "equivalence" of the given state.
228  */
229 static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, int *min, int *max){
230   XBT_VERB("Searching interval for state %i: nd_processes=%zu heap_bytes_used=%zu",
231     state->num, (size_t)state->nb_processes, (size_t)state->heap_bytes_used);
232
233   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
234
235   MC_SET_MC_HEAP;
236
237   int cursor = 0, previous_cursor, next_cursor;
238   mc_visited_state_t state_test;
239   int start = 0;
240   int end = xbt_dynar_length(all_states) - 1;
241   
242   while(start <= end){
243     cursor = (start + end) / 2;
244     state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, cursor, mc_visited_state_t);
245     if(state_test->nb_processes < state->nb_processes){
246       start = cursor + 1;
247     }else if(state_test->nb_processes > state->nb_processes){
248       end = cursor - 1;
249     }else{
250       if(state_test->heap_bytes_used < state->heap_bytes_used){
251         start = cursor +1;
252       }else if(state_test->heap_bytes_used > state->heap_bytes_used){
253         end = cursor - 1;
254       }else{
255         *min = *max = cursor;
256         previous_cursor = cursor - 1;
257         while(previous_cursor >= 0){
258           state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, previous_cursor, mc_visited_state_t);
259           if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
260             break;
261           *min = previous_cursor;
262           previous_cursor--;
263         }
264         next_cursor = cursor + 1;
265         while(next_cursor < xbt_dynar_length(all_states)){
266           state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, next_cursor, mc_visited_state_t);
267           if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
268             break;
269           *max = next_cursor;
270           next_cursor++;
271         }
272         if(!raw_mem_set)
273           MC_SET_STD_HEAP;
274         return -1;
275       }
276      }
277   }
278
279   if(!raw_mem_set)
280     MC_SET_STD_HEAP;
281
282   return cursor;
283 }
284
285 /** \brief Take a snapshot the current state and process it.
286  *
287  *  \return number of the duplicate state or -1 (not visited)
288  */
289 static int is_visited_state(){
290
291   if(_sg_mc_visited == 0)
292     return -1;
293
294   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
295
296   MC_SET_MC_HEAP;
297
298   mc_visited_state_t new_state = visited_state_new();
299   
300   if(xbt_dynar_is_empty(visited_states)){
301
302     xbt_dynar_push(visited_states, &new_state); 
303
304     if(!raw_mem_set)
305       MC_SET_STD_HEAP;
306
307     return -1;
308
309   }else{
310
311     int min = -1, max = -1, index;
312     //int res;
313     mc_visited_state_t state_test;
314     int cursor;
315
316     index = get_search_interval(visited_states, new_state, &min, &max);
317
318     if(min != -1 && max != -1){
319
320       // Parallell implementation
321       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
322       if(res != -1){
323         state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
324         if(state_test->other_num == -1)
325           new_state->other_num = state_test->num;
326         else
327           new_state->other_num = state_test->other_num;
328         if(dot_output == NULL)
329           XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
330         else
331           XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
332         xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
333         xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
334         if(!raw_mem_set)
335           MC_SET_STD_HEAP;
336         return new_state->other_num;
337         }*/
338
339       cursor = min;
340       while(cursor <= max){
341         state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
342         if(snapshot_compare(state_test, new_state) == 0){
343           // The state has been visited:
344
345           if(state_test->other_num == -1)
346             new_state->other_num = state_test->num;
347           else
348             new_state->other_num = state_test->other_num;
349           if(dot_output == NULL)
350             XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
351           else
352             XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
353
354           // Replace the old state with the new one (why?):
355           xbt_dynar_remove_at(visited_states, cursor, NULL);
356           xbt_dynar_insert_at(visited_states, cursor, &new_state);
357
358           if(!raw_mem_set)
359             MC_SET_STD_HEAP;
360           return new_state->other_num;
361         }
362         cursor++;
363       }
364
365       // The state has not been visited, add it to the list:
366       xbt_dynar_insert_at(visited_states, min, &new_state);
367
368     }else{
369
370       // The state has not been visited: insert the state in the dynamic array.
371       state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
372       if(state_test->nb_processes < new_state->nb_processes){
373         xbt_dynar_insert_at(visited_states, index+1, &new_state);
374       }else{
375         if(state_test->heap_bytes_used < new_state->heap_bytes_used)
376           xbt_dynar_insert_at(visited_states, index + 1, &new_state);
377         else
378           xbt_dynar_insert_at(visited_states, index, &new_state);
379       }
380
381     }
382
383     // We have reached the maximum number of stored states;
384     if(xbt_dynar_length(visited_states) > _sg_mc_visited){
385
386       // Find the (index of the) older state:
387       int min2 = mc_stats->expanded_states;
388       unsigned int cursor2 = 0;
389       unsigned int index2 = 0;
390       xbt_dynar_foreach(visited_states, cursor2, state_test){
391         if(state_test->num < min2){
392           index2 = cursor2;
393           min2 = state_test->num;
394         }
395       }
396
397       // and drop it:
398       xbt_dynar_remove_at(visited_states, index2, NULL);
399     }
400
401     if(!raw_mem_set)
402       MC_SET_STD_HEAP;
403     
404     return -1;
405     
406   }
407 }
408
409 /**
410  *  \brief Initialize the DPOR exploration algorithm
411  */
412 void MC_dpor_init()
413 {
414   
415   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
416
417   mc_state_t initial_state = NULL;
418   smx_process_t process;
419   
420   /* Create the initial state and push it into the exploration stack */
421   MC_SET_MC_HEAP;
422
423   if(_sg_mc_visited > 0)
424     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
425
426   if(mc_reduce_kind == e_mc_reduce_dpor)
427     first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
428
429   if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
430     initial_communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
431     communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
432     incomplete_communications_pattern = xbt_dynar_new(sizeof(int), NULL);
433     nb_comm_pattern = 0;
434   }
435
436   initial_state = MC_state_new();
437
438   MC_SET_STD_HEAP;
439
440   XBT_DEBUG("**************************************************");
441   XBT_DEBUG("Initial state");
442
443   /* Wait for requests (schedules processes) */
444   MC_wait_for_requests();
445
446   MC_ignore_heap(simix_global->process_to_run->data, 0);
447   MC_ignore_heap(simix_global->process_that_ran->data, 0);
448
449   MC_SET_MC_HEAP;
450  
451   /* Get an enabled process and insert it in the interleave set of the initial state */
452   xbt_swag_foreach(process, simix_global->process_list){
453     if(MC_process_is_enabled(process)){
454       MC_state_interleave_process(initial_state, process);
455       if(mc_reduce_kind != e_mc_reduce_none)
456         break;
457     }
458   }
459
460   xbt_fifo_unshift(mc_stack_safety, initial_state);
461
462   if(mc_reduce_kind == e_mc_reduce_dpor){
463     /* To ensure the soundness of DPOR, we have to keep a list of 
464        processes which are still enabled at each step of the exploration. 
465        If max depth is reached, we interleave them in the state in which they have 
466        been enabled for the first time. */
467     xbt_swag_foreach(process, simix_global->process_list){
468       if(MC_process_is_enabled(process)){
469         char *key = bprintf("%lu", process->pid);
470         char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
471         xbt_dict_set(first_enabled_state, key, data, NULL);
472         xbt_free(key);
473       }
474     }
475   }
476
477   MC_SET_STD_HEAP;
478
479   if(raw_mem_set)
480     MC_SET_MC_HEAP;
481   else
482     MC_SET_STD_HEAP;
483   
484 }
485
486
487 /** \brief Model-check the application using a DFS exploration
488  *         with DPOR (Dynamic Partial Order Reductions)
489  */
490 void MC_dpor(void)
491 {
492
493   char *req_str = NULL;
494   int value;
495   smx_simcall_t req = NULL, prev_req = NULL;
496   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restored_state=NULL;
497   smx_process_t process = NULL;
498   xbt_fifo_item_t item = NULL;
499   mc_state_t state_test = NULL;
500   int pos;
501   int visited_state = -1;
502   int enabled = 0;
503   int interleave_size = 0;
504   int comm_pattern = 0;
505   smx_action_t current_comm;
506
507   while (xbt_fifo_size(mc_stack_safety) > 0) {
508
509     /* Get current state */
510     state = (mc_state_t) 
511       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
512
513     XBT_DEBUG("**************************************************");
514     XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
515               xbt_fifo_size(mc_stack_safety), state, state->num,
516               MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state));
517       
518     interleave_size = MC_state_interleave_size(state);
519
520     /* Update statistics */
521     mc_stats->visited_states++;
522
523     /* If there are processes to interleave and the maximum depth has not been reached
524        then perform one step of the exploration algorithm */
525     if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
526         (req = MC_state_get_request(state, &value)) && visited_state == -1) {
527
528       /* Debug information */
529       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
530         req_str = MC_request_to_string(req, value);
531         XBT_DEBUG("Execute: %s", req_str);
532         xbt_free(req_str);
533       }
534       
535       MC_SET_MC_HEAP;
536       if(dot_output != NULL)
537         req_str = MC_request_get_dot_output(req, value);
538       MC_SET_STD_HEAP;
539
540       MC_state_set_executed_request(state, req, value);
541       mc_stats->executed_transitions++;
542
543       if(mc_reduce_kind ==  e_mc_reduce_dpor){
544         MC_SET_MC_HEAP;
545         char *key = bprintf("%lu", req->issuer->pid);
546         xbt_dict_remove(first_enabled_state, key); 
547         xbt_free(key);
548         MC_SET_STD_HEAP;
549       }
550
551       /* TODO : handle test and testany simcalls */
552       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
553         if(req->call == SIMCALL_COMM_ISEND)
554           comm_pattern = 1;
555         else if(req->call == SIMCALL_COMM_IRECV)
556           comm_pattern = 2;
557         else if(req->call == SIMCALL_COMM_WAIT)
558           comm_pattern = 3;
559         else if(req->call == SIMCALL_COMM_WAITANY)
560           comm_pattern = 4;
561       }
562
563       /* Answer the request */
564       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
565
566       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
567         MC_SET_MC_HEAP;
568         if(comm_pattern == 1 || comm_pattern == 2){
569           if(!initial_state_safety->initial_communications_pattern_done)
570             get_comm_pattern(initial_communications_pattern, req, comm_pattern);
571           else
572             get_comm_pattern(communications_pattern, req, comm_pattern);
573         }else if(comm_pattern == 3){
574           current_comm = simcall_comm_wait__get__comm(req);
575           if(current_comm->comm.refcount == 1){ /* First wait only must be considered */
576             if(!initial_state_safety->initial_communications_pattern_done)
577               complete_comm_pattern(initial_communications_pattern, current_comm);
578             else
579               complete_comm_pattern(communications_pattern, current_comm);
580           }
581         }else if(comm_pattern == 4){
582           current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t);
583           if(current_comm->comm.refcount == 1){ /* First wait only must be considered */
584             if(!initial_state_safety->initial_communications_pattern_done)
585               complete_comm_pattern(initial_communications_pattern, current_comm);
586             else
587               complete_comm_pattern(communications_pattern, current_comm);
588           }
589         }
590         MC_SET_STD_HEAP;
591         comm_pattern = 0;
592       }
593
594       /* Wait for requests (schedules processes) */
595       MC_wait_for_requests();
596
597       /* Create the new expanded state */
598       MC_SET_MC_HEAP;
599
600       next_state = MC_state_new();
601
602       if((visited_state = is_visited_state()) == -1){
603      
604         /* Get an enabled process and insert it in the interleave set of the next state */
605         xbt_swag_foreach(process, simix_global->process_list){
606           if(MC_process_is_enabled(process)){
607             MC_state_interleave_process(next_state, process);
608             if(mc_reduce_kind != e_mc_reduce_none)
609               break;
610           }
611         }
612
613         if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
614           next_state->system_state = MC_take_snapshot(next_state->num);
615         }
616
617         if(dot_output != NULL)
618           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
619
620       }else{
621
622         if(dot_output != NULL)
623           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
624
625       }
626
627       xbt_fifo_unshift(mc_stack_safety, next_state);
628
629       if(mc_reduce_kind ==  e_mc_reduce_dpor){
630         /* Insert in dict all enabled processes, if not included yet */
631         xbt_swag_foreach(process, simix_global->process_list){
632           if(MC_process_is_enabled(process)){
633             char *key = bprintf("%lu", process->pid);
634             if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
635               char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
636               xbt_dict_set(first_enabled_state, key, data, NULL); 
637             }
638             xbt_free(key);
639           }
640         }
641       }
642       
643       if(dot_output != NULL)
644         xbt_free(req_str);
645
646       MC_SET_STD_HEAP;
647
648       /* Let's loop again */
649
650       /* The interleave set is empty or the maximum depth is reached, let's back-track */
651     } else {
652
653       if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){  
654
655         if(user_max_depth_reached && visited_state == -1)
656           XBT_DEBUG("User max depth reached !");
657         else if(visited_state == -1)
658           XBT_WARN("/!\\ Max depth reached ! /!\\ ");
659
660         visited_state = -1;
661
662         if(mc_reduce_kind ==  e_mc_reduce_dpor){
663           /* Interleave enabled processes in the state in which they have been enabled for the first time */
664           xbt_swag_foreach(process, simix_global->process_list){
665             if(MC_process_is_enabled(process)){
666               char *key = bprintf("%lu", process->pid);
667               enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
668               xbt_free(key);
669               int cursor = xbt_fifo_size(mc_stack_safety);
670               xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
671                 if(cursor-- == enabled){ 
672                   if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){ 
673                     XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
674                     MC_state_interleave_process(state_test, process);
675                     break;
676                   }
677                 }
678               }
679             }
680           }
681         }
682
683       }else{
684
685         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
686
687       }
688
689       MC_SET_MC_HEAP;
690
691       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
692         if(initial_state_safety->initial_communications_pattern_done){
693           if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
694             deterministic_pattern(initial_communications_pattern, communications_pattern);
695             if(initial_state_safety->comm_deterministic == 0 && _sg_mc_comms_determinism){
696               XBT_INFO("****************************************************");
697               XBT_INFO("***** Non-deterministic communications pattern *****");
698               XBT_INFO("****************************************************");
699               XBT_INFO("Initial communications pattern:");
700               print_communications_pattern(initial_communications_pattern);
701               XBT_INFO("Communications pattern counter-example:");
702               print_communications_pattern(communications_pattern);
703               MC_print_statistics(mc_stats);
704               return;
705             }else if(initial_state_safety->send_deterministic == 0 && _sg_mc_send_determinism){
706               XBT_INFO("*********************************************************");
707               XBT_INFO("***** Non-send-deterministic communications pattern *****");
708               XBT_INFO("*********************************************************");
709               XBT_INFO("Initial communications pattern:");
710               print_communications_pattern(initial_communications_pattern);
711               XBT_INFO("Communications pattern counter-example:");
712               print_communications_pattern(communications_pattern);
713               MC_print_statistics(mc_stats);
714               return;
715             }
716           }
717         }else{
718           initial_state_safety->initial_communications_pattern_done = 1;
719         }
720       }
721
722       /* Trash the current state, no longer needed */
723       xbt_fifo_shift(mc_stack_safety);
724       MC_state_delete(state);
725       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
726
727       MC_SET_STD_HEAP;
728       
729       /* Check for deadlocks */
730       if(MC_deadlock_check()){
731         MC_show_deadlock(NULL);
732         return;
733       }
734
735       MC_SET_MC_HEAP;
736       /* Traverse the stack backwards until a state with a non empty interleave
737          set is found, deleting all the states that have it empty in the way.
738          For each deleted state, check if the request that has generated it 
739          (from it's predecesor state), depends on any other previous request 
740          executed before it. If it does then add it to the interleave set of the
741          state that executed that previous request. */
742       
743       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
744         if(mc_reduce_kind == e_mc_reduce_dpor){
745           req = MC_state_get_internal_request(state);
746           xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
747             if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
748               if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
749                 XBT_DEBUG("Dependent Transitions:");
750                 prev_req = MC_state_get_executed_request(prev_state, &value);
751                 req_str = MC_request_to_string(prev_req, value);
752                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
753                 xbt_free(req_str);
754                 prev_req = MC_state_get_executed_request(state, &value);
755                 req_str = MC_request_to_string(prev_req, value);
756                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
757                 xbt_free(req_str);              
758               }
759
760               if(!MC_state_process_is_done(prev_state, req->issuer))
761                 MC_state_interleave_process(prev_state, req->issuer);
762               else
763                 XBT_DEBUG("Process %p is in done set", req->issuer);
764
765               break;
766
767             }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
768
769               XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
770               break;
771
772             }else{
773
774               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant", req->call, req->issuer->pid, state->num, MC_state_get_internal_request(prev_state)->call, MC_state_get_internal_request(prev_state)->issuer->pid, prev_state->num);
775
776             }
777           }
778         }
779              
780         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
781           /* We found a back-tracking point, let's loop */
782           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
783           if(_sg_mc_checkpoint){
784             if(state->system_state != NULL){
785               MC_restore_snapshot(state->system_state);
786               xbt_fifo_unshift(mc_stack_safety, state);
787               MC_SET_STD_HEAP;
788             }else{
789               pos = xbt_fifo_size(mc_stack_safety);
790               item = xbt_fifo_get_first_item(mc_stack_safety);
791               while(pos>0){
792                 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
793                 if(restored_state->system_state != NULL){
794                   break;
795                 }else{
796                   item = xbt_fifo_get_next_item(item);
797                   pos--;
798                 }
799               }
800               MC_restore_snapshot(restored_state->system_state);
801               xbt_fifo_unshift(mc_stack_safety, state);
802               MC_SET_STD_HEAP;
803               MC_replay(mc_stack_safety, pos);
804             }
805           }else{
806             xbt_fifo_unshift(mc_stack_safety, state);
807             MC_SET_STD_HEAP;
808             MC_replay(mc_stack_safety, -1);
809           }
810           XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
811           break;
812         } else {
813           /*req = MC_state_get_internal_request(state);
814           if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
815             if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
816               if(!xbt_dynar_is_empty(communications_pattern))
817                 xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
818             }
819             }*/
820           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1); 
821           MC_state_delete(state);
822         }
823       }
824       MC_SET_STD_HEAP;
825     }
826   }
827   MC_print_statistics(mc_stats);
828   MC_SET_STD_HEAP;
829
830   return;
831 }
832
833
834
835