Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : move functions about snapshot comparison in a separate file mc_compare.c
[simgrid.git] / src / mc / mc_dpor.c
1 /* Copyright (c) 2008-2012. Da SimGrid Team. All rights reserved.           */
2
3 /* This program is free software; you can redistribute it and/or modify it
4  * under the terms of the license (GNU LGPL) which comes with this package. */
5
6 #include "mc_private.h"
7
8 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
9                                 "Logging specific to MC DPOR exploration");
10
11 /**
12  *  \brief Initialize the DPOR exploration algorithm
13  */
14 void MC_dpor_init()
15 {
16   
17   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
18
19   mc_state_t initial_state = NULL;
20   smx_process_t process;
21   
22   /* Create the initial state and push it into the exploration stack */
23   MC_SET_RAW_MEM;
24   initial_state = MC_state_new();
25   MC_UNSET_RAW_MEM;
26
27   XBT_DEBUG("**************************************************");
28   XBT_DEBUG("Initial state");
29
30   /* Wait for requests (schedules processes) */
31   MC_wait_for_requests();
32
33   MC_SET_RAW_MEM;
34   /* Get an enabled process and insert it in the interleave set of the initial state */
35   xbt_swag_foreach(process, simix_global->process_list){
36     if(MC_process_is_enabled(process)){
37       MC_state_interleave_process(initial_state, process);
38       break;
39     }
40   }
41
42   xbt_fifo_unshift(mc_stack_safety, initial_state);
43
44   MC_UNSET_RAW_MEM;
45
46   if(raw_mem_set)
47     MC_SET_RAW_MEM;
48   else
49     MC_UNSET_RAW_MEM;
50   
51     
52   /* FIXME: Update Statistics 
53      mc_stats->state_size +=
54      xbt_setset_set_size(initial_state->enabled_transitions); */
55 }
56
57
58 /**
59  *   \brief Perform the model-checking operation using a depth-first search exploration
60  *         with Dynamic Partial Order Reductions
61  */
62 void MC_dpor(void)
63 {
64
65   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
66
67   char *req_str;
68   int value;
69   smx_simcall_t req = NULL, prev_req = NULL;
70   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
71   smx_process_t process = NULL;
72   xbt_fifo_item_t item = NULL;
73   int pos;
74
75   while (xbt_fifo_size(mc_stack_safety) > 0) {
76
77     /* Get current state */
78     state = (mc_state_t) 
79       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
80
81     XBT_DEBUG("**************************************************");
82     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
83               xbt_fifo_size(mc_stack_safety), state,
84               MC_state_interleave_size(state));
85
86     /* Update statistics */
87     mc_stats->visited_states++;
88
89     /* If there are processes to interleave and the maximum depth has not been reached
90        then perform one step of the exploration algorithm */
91     if (xbt_fifo_size(mc_stack_safety) < MAX_DEPTH &&
92         (req = MC_state_get_request(state, &value))) {
93
94       /* Debug information */
95       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
96         req_str = MC_request_to_string(req, value);
97         XBT_DEBUG("Execute: %s", req_str);
98         xbt_free(req_str);
99       }
100
101       MC_state_set_executed_request(state, req, value);
102       mc_stats->executed_transitions++;
103
104       /* Answer the request */
105       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
106
107       /* Wait for requests (schedules processes) */
108       MC_wait_for_requests();
109
110       /* Create the new expanded state */
111       MC_SET_RAW_MEM;
112
113       next_state = MC_state_new();
114       
115       /* Get an enabled process and insert it in the interleave set of the next state */
116       xbt_swag_foreach(process, simix_global->process_list){
117         if(MC_process_is_enabled(process)){
118           MC_state_interleave_process(next_state, process);
119           break;
120         }
121       }
122
123       if(_surf_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_mc_checkpoint == 0)){
124         next_state->system_state = xbt_new0(s_mc_snapshot_t, 1);
125         MC_take_snapshot(next_state->system_state);
126       }
127
128       xbt_fifo_unshift(mc_stack_safety, next_state);
129       MC_UNSET_RAW_MEM;
130
131       /* FIXME: Update Statistics
132          mc_stats->state_size +=
133          xbt_setset_set_size(next_state->enabled_transitions);*/
134
135       /* Let's loop again */
136
137       /* The interleave set is empty or the maximum depth is reached, let's back-track */
138     } else {
139       XBT_DEBUG("There are no more processes to interleave.");
140
141       /* Trash the current state, no longer needed */
142       MC_SET_RAW_MEM;
143       xbt_fifo_shift(mc_stack_safety);
144       MC_state_delete(state);
145       MC_UNSET_RAW_MEM;
146
147       /* Check for deadlocks */
148       if(MC_deadlock_check()){
149         MC_show_deadlock(NULL);
150         return;
151       }
152
153       MC_SET_RAW_MEM;
154       /* Traverse the stack backwards until a state with a non empty interleave
155          set is found, deleting all the states that have it empty in the way.
156          For each deleted state, check if the request that has generated it 
157          (from it's predecesor state), depends on any other previous request 
158          executed before it. If it does then add it to the interleave set of the
159          state that executed that previous request. */
160       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
161         req = MC_state_get_internal_request(state);
162         xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
163           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
164             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
165               XBT_DEBUG("Dependent Transitions:");
166               prev_req = MC_state_get_executed_request(prev_state, &value);
167               req_str = MC_request_to_string(prev_req, value);
168               XBT_DEBUG("%s (state=%p)", req_str, prev_state);
169               xbt_free(req_str);
170               prev_req = MC_state_get_executed_request(state, &value);
171               req_str = MC_request_to_string(prev_req, value);
172               XBT_DEBUG("%s (state=%p)", req_str, state);
173               xbt_free(req_str);              
174             }
175
176             if(!MC_state_process_is_done(prev_state, req->issuer))
177               MC_state_interleave_process(prev_state, req->issuer);
178             else
179               XBT_DEBUG("Process %p is in done set", req->issuer);
180
181             break;
182           }
183         }
184         if (MC_state_interleave_size(state)) {
185           /* We found a back-tracking point, let's loop */
186           if(_surf_mc_checkpoint){
187             if(state->system_state != NULL){
188               MC_restore_snapshot(state->system_state);
189               xbt_fifo_unshift(mc_stack_safety, state);
190               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
191               MC_UNSET_RAW_MEM;
192             }else{
193               pos = xbt_fifo_size(mc_stack_safety);
194               item = xbt_fifo_get_first_item(mc_stack_safety);
195               while(pos>0){
196                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
197                 if(restore_state->system_state != NULL){
198                   break;
199                 }else{
200                   item = xbt_fifo_get_next_item(item);
201                   pos--;
202                 }
203               }
204               MC_restore_snapshot(restore_state->system_state);
205               xbt_fifo_unshift(mc_stack_safety, state);
206               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
207               MC_UNSET_RAW_MEM;
208               MC_replay(mc_stack_safety, pos);
209             }
210           }else{
211             xbt_fifo_unshift(mc_stack_safety, state);
212             XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
213             MC_UNSET_RAW_MEM;
214             MC_replay(mc_stack_safety, -1);
215           }
216           break;
217         } else {
218           MC_state_delete(state);
219         }
220       }
221       MC_UNSET_RAW_MEM;
222     }
223   }
224   MC_print_statistics(mc_stats);
225   MC_UNSET_RAW_MEM;
226
227   if(raw_mem_set)
228     MC_SET_RAW_MEM;
229   else
230     MC_UNSET_RAW_MEM;
231   
232
233   return;
234 }
235
236
237
238