Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : check current_heap before SET_RAW_MEM and restore it after UNSET_RAW_MEM
[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   initial_state->system_state = xbt_new0(s_mc_snapshot_t, 1);
43   MC_take_snapshot(initial_state->system_state);
44
45   xbt_fifo_unshift(mc_stack_safety, initial_state);
46
47   MC_UNSET_RAW_MEM;
48
49   if(raw_mem_set)
50     MC_SET_RAW_MEM;
51   else
52     MC_UNSET_RAW_MEM;
53   
54     
55   /* FIXME: Update Statistics 
56      mc_stats->state_size +=
57      xbt_setset_set_size(initial_state->enabled_transitions); */
58 }
59
60
61 /**
62  *   \brief Perform the model-checking operation using a depth-first search exploration
63  *         with Dynamic Partial Order Reductions
64  */
65 void MC_dpor(void)
66 {
67
68   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
69
70   char *req_str;
71   int value;
72   smx_simcall_t req = NULL, prev_req = NULL;
73   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
74   smx_process_t process = NULL;
75   xbt_fifo_item_t item = NULL;
76   int pos;
77
78   while (xbt_fifo_size(mc_stack_safety) > 0) {
79
80     /* Get current state */
81     state = (mc_state_t) 
82       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
83
84     XBT_DEBUG("**************************************************");
85     XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
86               xbt_fifo_size(mc_stack_safety), state,
87               MC_state_interleave_size(state));
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_safety) < MAX_DEPTH &&
95         (req = MC_state_get_request(state, &value))) {
96
97       /* Debug information */
98       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
99         req_str = MC_request_to_string(req, value);
100         XBT_DEBUG("Execute: %s", req_str);
101         xbt_free(req_str);
102       }
103
104       MC_state_set_executed_request(state, req, value);
105       mc_stats->executed_transitions++;
106
107       /* Answer the request */
108       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
109
110       /* Wait for requests (schedules processes) */
111       MC_wait_for_requests();
112
113       /* Create the new expanded state */
114       MC_SET_RAW_MEM;
115
116       next_state = MC_state_new();
117       
118       /* Get an enabled process and insert it in the interleave set of the next state */
119       xbt_swag_foreach(process, simix_global->process_list){
120         if(MC_process_is_enabled(process)){
121           MC_state_interleave_process(next_state, process);
122           break;
123         }
124       }
125
126       if(_surf_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_mc_checkpoint == 0)){
127         next_state->system_state = xbt_new0(s_mc_snapshot_t, 1);
128         MC_take_snapshot(next_state->system_state);
129       }
130
131       xbt_fifo_unshift(mc_stack_safety, next_state);
132       MC_UNSET_RAW_MEM;
133
134       /* FIXME: Update Statistics
135          mc_stats->state_size +=
136          xbt_setset_set_size(next_state->enabled_transitions);*/
137
138       /* Let's loop again */
139
140       /* The interleave set is empty or the maximum depth is reached, let's back-track */
141     } else {
142       XBT_DEBUG("There are no more processes to interleave.");
143
144       /* Trash the current state, no longer needed */
145       MC_SET_RAW_MEM;
146       xbt_fifo_shift(mc_stack_safety);
147       MC_state_delete(state);
148       MC_UNSET_RAW_MEM;
149
150       /* Check for deadlocks */
151       if(MC_deadlock_check()){
152         MC_show_deadlock(NULL);
153         return;
154       }
155
156       MC_SET_RAW_MEM;
157       /* Traverse the stack backwards until a state with a non empty interleave
158          set is found, deleting all the states that have it empty in the way.
159          For each deleted state, check if the request that has generated it 
160          (from it's predecesor state), depends on any other previous request 
161          executed before it. If it does then add it to the interleave set of the
162          state that executed that previous request. */
163       while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
164         req = MC_state_get_internal_request(state);
165         xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
166           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
167             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
168               XBT_DEBUG("Dependent Transitions:");
169               prev_req = MC_state_get_executed_request(prev_state, &value);
170               req_str = MC_request_to_string(prev_req, value);
171               XBT_DEBUG("%s (state=%p)", req_str, prev_state);
172               xbt_free(req_str);
173               prev_req = MC_state_get_executed_request(state, &value);
174               req_str = MC_request_to_string(prev_req, value);
175               XBT_DEBUG("%s (state=%p)", req_str, state);
176               xbt_free(req_str);              
177             }
178
179             if(!MC_state_process_is_done(prev_state, req->issuer))
180               MC_state_interleave_process(prev_state, req->issuer);
181             else
182               XBT_DEBUG("Process %p is in done set", req->issuer);
183
184             break;
185           }
186         }
187         if (MC_state_interleave_size(state)) {
188           /* We found a back-tracking point, let's loop */
189           if(_surf_mc_checkpoint){
190             if(state->system_state != NULL){
191               MC_restore_snapshot(state->system_state);
192               xbt_fifo_unshift(mc_stack_safety, state);
193               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
194               MC_UNSET_RAW_MEM;
195             }else{
196               pos = xbt_fifo_size(mc_stack_safety);
197               item = xbt_fifo_get_first_item(mc_stack_safety);
198               while(pos>0){
199                 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
200                 if(restore_state->system_state != NULL){
201                   break;
202                 }else{
203                   item = xbt_fifo_get_next_item(item);
204                   pos--;
205                 }
206               }
207               MC_restore_snapshot(restore_state->system_state);
208               xbt_fifo_unshift(mc_stack_safety, state);
209               XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
210               MC_UNSET_RAW_MEM;
211               MC_replay(mc_stack_safety, pos);
212             }
213           }else{
214             xbt_fifo_unshift(mc_stack_safety, state);
215             XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
216             MC_UNSET_RAW_MEM;
217             MC_replay(mc_stack_safety, -1);
218           }
219           break;
220         } else {
221           MC_state_delete(state);
222         }
223       }
224       MC_UNSET_RAW_MEM;
225     }
226   }
227   MC_print_statistics(mc_stats);
228   MC_UNSET_RAW_MEM;
229
230   if(raw_mem_set)
231     MC_SET_RAW_MEM;
232   else
233     MC_UNSET_RAW_MEM;
234   
235
236   return;
237 }
238
239
240
241