Logo AND Algorithmique Numérique Distribuée

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