Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
508ef2803fcd6f54d0cc1f8698f1a4ec6b587b74
[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 mc_stats_t mc_stats = NULL;
18 mc_state_t mc_current_state = NULL;
19 char mc_replay_mode = FALSE;
20 double *mc_time = NULL;
21 xbt_fifo_t mc_snapshot_stack = NULL;
22
23 /**
24  *  \brief Initialize the model-checker data structures
25  */
26 void MC_init(void)
27 {
28   /* Check if MC is already initialized */
29   if (initial_snapshot)
30     return;
31
32   mc_time = xbt_new0(double, simix_process_maxpid);
33
34   /* Initialize the data structures that must be persistent across every
35      iteration of the model-checker (in RAW memory) */
36   MC_SET_RAW_MEM;
37
38   /* Initialize statistics */
39   mc_stats = xbt_new0(s_mc_stats_t, 1);
40   mc_stats->state_size = 1;
41
42   /* Create exploration stack */
43   mc_stack = xbt_fifo_new();
44
45   MC_UNSET_RAW_MEM;
46
47   MC_dpor_init();
48
49   MC_SET_RAW_MEM;
50   /* Save the initial state */
51   initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
52   MC_take_snapshot(initial_snapshot);
53   MC_UNSET_RAW_MEM;
54 }
55
56 void MC_init_with_automaton(xbt_automaton_t a){
57
58   XBT_DEBUG("Start init mc");
59   
60   mc_time = xbt_new0(double, simix_process_maxpid);
61
62   /* Initialize the data structures that must be persistent across every
63      iteration of the model-checker (in RAW memory) */
64
65   MC_SET_RAW_MEM;
66
67   /* Initialize statistics */
68   mc_stats = xbt_new0(s_mc_stats_t, 1);
69   mc_stats->state_size = 1;
70
71   XBT_DEBUG("Creating snapshot_stack");
72
73  /* Create exploration stack */
74   mc_snapshot_stack = xbt_fifo_new();
75
76   MC_UNSET_RAW_MEM;
77
78   MC_dfs_init(a);
79 }
80
81
82 void MC_modelcheck(void)
83 {
84   MC_init();
85   MC_dpor();
86   MC_exit();
87 }
88
89 void MC_modelcheck_with_automaton(xbt_automaton_t a){
90   MC_init_with_automaton(a);
91   MC_exit();
92 }
93
94 void MC_exit(void)
95 {
96   MC_print_statistics(mc_stats);
97   xbt_free(mc_time);
98   MC_memory_exit();
99 }
100
101 int MC_random(int min, int max)
102 {
103   /*FIXME: return mc_current_state->executed_transition->random.value;*/
104   return 0;
105 }
106
107 /**
108  * \brief Schedules all the process that are ready to run
109  */
110 void MC_wait_for_requests(void)
111 {
112   smx_process_t process;
113   smx_req_t req;
114   unsigned int iter;
115
116   while (xbt_dynar_length(simix_global->process_to_run)) {
117     SIMIX_process_runall();
118     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
119       req = &process->request;
120       if (req->call != REQ_NO_REQ && !MC_request_is_visible(req))
121           SIMIX_request_pre(req, 0);
122     }
123   }
124 }
125
126 int MC_deadlock_check()
127 {
128   int deadlock = FALSE;
129   smx_process_t process;
130   if(xbt_swag_size(simix_global->process_list)){
131     deadlock = TRUE;
132     xbt_swag_foreach(process, simix_global->process_list){
133       if(process->request.call != REQ_NO_REQ
134          && MC_request_is_enabled(&process->request)){
135         deadlock = FALSE;
136         break;
137       }
138     }
139   }
140   return deadlock;
141 }
142
143 /**
144  * \brief Re-executes from the initial state all the transitions indicated by
145  *        a given model-checker stack.
146  * \param stack The stack with the transitions to execute.
147 */
148 void MC_replay(xbt_fifo_t stack)
149 {
150   int value;
151   char *req_str;
152   smx_req_t req = NULL, saved_req = NULL;
153   xbt_fifo_item_t item;
154   mc_state_t state;
155
156   XBT_DEBUG("**** Begin Replay ****");
157
158   /* Restore the initial state */
159   MC_restore_snapshot(initial_snapshot);
160   /* At the moment of taking the snapshot the raw heap was set, so restoring
161    * it will set it back again, we have to unset it to continue  */
162   MC_UNSET_RAW_MEM;
163
164   /* Traverse the stack from the initial state and re-execute the transitions */
165   for (item = xbt_fifo_get_last_item(stack);
166        item != xbt_fifo_get_first_item(stack);
167        item = xbt_fifo_get_prev_item(item)) {
168
169     state = (mc_state_t) xbt_fifo_get_item_content(item);
170     saved_req = MC_state_get_executed_request(state, &value);
171    
172     if(saved_req){
173       /* because we got a copy of the executed request, we have to fetch the  
174          real one, pointed by the request field of the issuer process */
175       req = &saved_req->issuer->request;
176
177       /* Debug information */
178       if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
179         req_str = MC_request_to_string(req, value);
180         XBT_DEBUG("Replay: %s (%p)", req_str, state);
181         xbt_free(req_str);
182       }
183     }
184          
185     SIMIX_request_pre(req, value);
186     MC_wait_for_requests();
187          
188     /* Update statistics */
189     mc_stats->visited_states++;
190     mc_stats->executed_transitions++;
191   }
192   XBT_DEBUG("**** End Replay ****");
193 }
194
195 /**
196  * \brief Dumps the contents of a model-checker's stack and shows the actual
197  *        execution trace
198  * \param stack The stack to dump
199 */
200 void MC_dump_stack(xbt_fifo_t stack)
201 {
202   mc_state_t state;
203
204   MC_show_stack(stack);
205
206   MC_SET_RAW_MEM;
207   while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
208     MC_state_delete(state);
209   MC_UNSET_RAW_MEM;
210 }
211
212 void MC_show_stack(xbt_fifo_t stack)
213 {
214   int value;
215   mc_state_t state;
216   xbt_fifo_item_t item;
217   smx_req_t req;
218   char *req_str = NULL;
219   
220   for (item = xbt_fifo_get_last_item(stack);
221        (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
222         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
223     req = MC_state_get_executed_request(state, &value);
224     if(req){
225       req_str = MC_request_to_string(req, value);
226       XBT_INFO("%s", req_str);
227       xbt_free(req_str);
228     }
229   }
230 }
231
232 void MC_show_deadlock(smx_req_t req)
233 {
234   /*char *req_str = NULL;*/
235   XBT_INFO("**************************");
236   XBT_INFO("*** DEAD-LOCK DETECTED ***");
237   XBT_INFO("**************************");
238   XBT_INFO("Locked request:");
239   /*req_str = MC_request_to_string(req);
240   XBT_INFO("%s", req_str);
241   xbt_free(req_str);*/
242   XBT_INFO("Counter-example execution trace:");
243   MC_dump_stack(mc_stack);
244 }
245
246 void MC_print_statistics(mc_stats_t stats)
247 {
248   XBT_INFO("State space size ~= %lu", stats->state_size);
249   XBT_INFO("Expanded states = %lu", stats->expanded_states);
250   XBT_INFO("Visited states = %lu", stats->visited_states);
251   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
252   XBT_INFO("Expanded / Visited = %lf",
253         (double) stats->visited_states / stats->expanded_states);
254   /*XBT_INFO("Exploration coverage = %lf",
255      (double)stats->expanded_states / stats->state_size); */
256 }
257
258 void MC_assert(int prop)
259 {
260   if (MC_IS_ENABLED && !prop) {
261     XBT_INFO("**************************");
262     XBT_INFO("*** PROPERTY NOT VALID ***");
263     XBT_INFO("**************************");
264     XBT_INFO("Counter-example execution trace:");
265     MC_dump_stack(mc_stack);
266     MC_print_statistics(mc_stats);
267     xbt_abort();
268   }
269 }
270
271 void MC_assert_pair(int prop){
272   if (MC_IS_ENABLED && !prop) {
273     XBT_INFO("**************************");
274     XBT_INFO("*** PROPERTY NOT VALID ***");
275     XBT_INFO("**************************");
276     //XBT_INFO("Counter-example execution trace:");
277     //MC_show_snapshot_stack(mc_snapshot_stack);
278     //MC_dump_snapshot_stack(mc_snapshot_stack);
279     //MC_print_statistics(mc_stats);
280     xbt_abort();
281   }
282 }
283
284 void MC_process_clock_add(smx_process_t process, double amount)
285 {
286   mc_time[process->pid] += amount;
287 }
288
289 double MC_process_clock_get(smx_process_t process)
290 {
291   if(mc_time)
292     return mc_time[process->pid];
293   else
294     return 0;
295 }