5 #include "../surf/surf_private.h"
6 #include "../simix/private.h"
11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
12 "Logging specific to MC (global)");
14 /* MC global data structures */
15 mc_snapshot_t initial_snapshot = NULL;
16 xbt_fifo_t mc_stack = NULL;
17 xbt_setset_t mc_setset = NULL;
18 mc_stats_t mc_stats = NULL;
19 mc_state_t mc_current_state = NULL;
20 char mc_replay_mode = FALSE;
23 * \brief Initialize the model-checker data structures
27 smx_process_t process;
29 /* Check if MC is already initialized */
33 /* Initialize the data structures that must be persistent across every
34 iteration of the model-checker (in RAW memory) */
37 /* Initialize statistics */
38 mc_stats = xbt_new0(s_mc_stats_t, 1);
39 mc_stats->state_size = 1;
41 /* Create exploration stack */
42 mc_stack = xbt_fifo_new();
44 /* Create the container for the sets */
45 mc_setset = xbt_setset_new(20);
47 /* Add the existing processes to mc's setset so they have an ID designated */
48 xbt_swag_foreach(process, simix_global->process_list){
49 xbt_setset_elm_add(mc_setset, process);
52 /* Initialize the control variable */
53 mc_exp_ctl = xbt_new0(e_mc_exp_ctl_t, 1);
54 *mc_exp_ctl = MC_EXPLORE;
60 /* Save the initial state */
62 initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
63 MC_take_snapshot(initial_snapshot);
67 void MC_modelcheck(void)
72 /* Compute initial state */
75 /* Fork an mc's slave exploration process and wait for it. */
76 /* The forked process will explore a trace until:
77 - a back-tracking point is found (it sets mc_expl_ctl to MC_explore)
78 - there are no more states to explore (it sets mc_expl_ctl to MC_STOP)
79 - a property is invalid (or dead-lock)
81 while(*mc_exp_ctl == MC_EXPLORE){
83 waitpid(pid, &status, 0);
84 mmalloc_detach(raw_heap);
85 raw_heap = mmalloc_attach(raw_heap_fd, (char*)(std_heap) + STD_HEAP_SIZE + getpagesize());
87 if (WIFSIGNALED(status)) {
88 INFO1("killed by signal %d\n", WTERMSIG(status));
90 }else if (WIFSTOPPED(status)) {
91 INFO1("stopped by signal %d\n", WSTOPSIG(status));
93 }else if (WIFCONTINUED(status)) {
98 if(*mc_exp_ctl == MC_DEADLOCK){
99 INFO0("**************************");
100 INFO0("*** DEAD-LOCK DETECTED ***");
101 INFO0("**************************");
102 MC_dump_stack(mc_stack);
103 MC_print_statistics(mc_stats);
108 /* if mc_stack is empty then create first state, otherwise replay */
109 if(xbt_fifo_size(mc_stack) == 0)
120 /* If we are the mc's master process then exit */
127 mmalloc_detach(raw_heap);
128 shm_unlink("raw_heap");
131 int MC_random(int min, int max)
133 /*FIXME: return mc_current_state->executed_transition->random.value;*/
138 * \brief Re-executes from the initial state all the transitions indicated by
139 * a given model-checker stack.
140 * \param stack The stack with the transitions to execute.
142 void MC_replay(xbt_fifo_t stack)
145 smx_req_t req = NULL, saved_req = NULL;
146 xbt_fifo_item_t item;
149 DEBUG0("**** Begin Replay ****");
151 /* Restore the initial state */
152 /*MC_restore_snapshot(initial_snapshot);*/
154 MC_wait_for_requests();
156 /* Traverse the stack from the initial state and re-execute the transitions */
157 for (item = xbt_fifo_get_last_item(stack);
158 item != xbt_fifo_get_first_item(stack);
159 item = xbt_fifo_get_prev_item(item)) {
161 state = (mc_state_t) xbt_fifo_get_item_content(item);
162 saved_req = MC_state_get_executed_request(state);
165 /* because we got a copy of the executed request, we have to fetch the
166 real one, pointed by the request field of the issuer process */
167 req = &saved_req->issuer->request;
169 /* Debug information */
170 if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
171 req_str = MC_request_to_string(req);
172 DEBUG1("Replay: %s", req_str);
177 SIMIX_request_pre(req);
178 MC_wait_for_requests();
180 /* Update statistics */
181 mc_stats->visited_states++;
182 mc_stats->executed_transitions++;
184 DEBUG0("**** End Replay ****");
188 * \brief Dumps the contents of a model-checker's stack and shows the actual
190 * \param stack The stack to dump
192 void MC_dump_stack(xbt_fifo_t stack)
196 MC_show_stack(stack);
199 while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
200 MC_state_delete(state);
204 void MC_show_stack(xbt_fifo_t stack)
207 xbt_fifo_item_t item;
209 char *req_str = NULL;
211 for (item = xbt_fifo_get_last_item(stack);
212 (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
213 : (NULL)); item = xbt_fifo_get_prev_item(item)) {
214 req = MC_state_get_executed_request(state);
216 req_str = MC_request_to_string(req);
217 INFO1("%s", req_str);
224 * \brief Schedules all the process that are ready to run
226 void MC_wait_for_requests(void)
228 char *req_str = NULL;
229 smx_req_t req = NULL;
232 SIMIX_context_runall(simix_global->process_to_run);
233 while((req = SIMIX_request_pop())){
234 if(!SIMIX_request_is_visible(req))
235 SIMIX_request_pre(req);
236 else if(req->call == REQ_COMM_WAITANY)
238 else if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
239 req_str = MC_request_to_string(req);
240 DEBUG1("Got: %s", req_str);
244 } while (xbt_swag_size(simix_global->process_to_run));
247 /****************************** Statistics ************************************/
248 void MC_print_statistics(mc_stats_t stats)
250 INFO1("State space size ~= %lu", stats->state_size);
251 INFO1("Expanded states = %lu", stats->expanded_states);
252 INFO1("Visited states = %lu", stats->visited_states);
253 INFO1("Executed transitions = %lu", stats->executed_transitions);
254 INFO1("Expanded / Visited = %lf",
255 (double) stats->visited_states / stats->expanded_states);
256 /*INFO1("Exploration coverage = %lf",
257 (double)stats->expanded_states / stats->state_size); */
260 /************************* Assertion Checking *********************************/
261 void MC_assert(int prop)
263 if (MC_IS_ENABLED && !prop) {
264 INFO0("**************************");
265 INFO0("*** PROPERTY NOT VALID ***");
266 INFO0("**************************");
267 INFO0("Counter-example execution trace:");
268 MC_dump_stack(mc_stack);
269 MC_print_statistics(mc_stats);
274 void MC_show_deadlock(smx_req_t req)
276 char *req_str = NULL;
277 INFO0("**************************");
278 INFO0("*** DEAD-LOCK DETECTED ***");
279 INFO0("**************************");
280 INFO0("Locked request:");
281 req_str = MC_request_to_string(req);
282 INFO1("%s", req_str);
284 INFO0("Counter-example execution trace:");
285 MC_dump_stack(mc_stack);