6 #include "../surf/surf_private.h"
7 #include "../simix/private.h"
12 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
13 "Logging specific to MC (global)");
15 /* MC global data structures */
17 mc_state_t mc_current_state = NULL;
18 char mc_replay_mode = FALSE;
19 double *mc_time = NULL;
20 mc_snapshot_t initial_snapshot = NULL;
24 xbt_fifo_t mc_stack_safety_stateful = NULL;
25 xbt_fifo_t mc_stack_safety_stateless = NULL;
26 mc_stats_t mc_stats = NULL;
30 xbt_fifo_t mc_stack_liveness_stateful = NULL;
31 mc_stats_pair_t mc_stats_pair = NULL;
32 xbt_fifo_t mc_stack_liveness_stateless = NULL;
33 mc_snapshot_t initial_snapshot_liveness = NULL;
35 xbt_automaton_t automaton;
39 * \brief Initialize the model-checker data structures
41 void MC_init_safety_stateless(void)
44 /* Check if MC is already initialized */
48 mc_time = xbt_new0(double, simix_process_maxpid);
50 /* Initialize the data structures that must be persistent across every
51 iteration of the model-checker (in RAW memory) */
54 /* Initialize statistics */
55 mc_stats = xbt_new0(s_mc_stats_t, 1);
56 mc_stats->state_size = 1;
58 /* Create exploration stack */
59 mc_stack_safety_stateless = xbt_fifo_new();
66 /* Save the initial state */
67 initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
68 MC_take_snapshot(initial_snapshot);
72 void MC_init_safety_stateful(void){
75 /* Check if MC is already initialized */
79 mc_time = xbt_new0(double, simix_process_maxpid);
81 /* Initialize the data structures that must be persistent across every
82 iteration of the model-checker (in RAW memory) */
85 /* Initialize statistics */
86 mc_stats = xbt_new0(s_mc_stats_t, 1);
87 mc_stats->state_size = 1;
89 /* Create exploration stack */
90 mc_stack_safety_stateful = xbt_fifo_new();
94 MC_dpor_stateful_init();
99 void MC_init_liveness_stateful(xbt_automaton_t a){
101 XBT_DEBUG("Start init mc");
103 mc_time = xbt_new0(double, simix_process_maxpid);
105 /* Initialize the data structures that must be persistent across every
106 iteration of the model-checker (in RAW memory) */
110 /* Initialize statistics */
111 mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
112 //mc_stats = xbt_new0(s_mc_stats_t, 1);
114 XBT_DEBUG("Creating snapshot_stack");
116 /* Create exploration stack */
117 mc_stack_liveness_stateful = xbt_fifo_new();
122 //MC_ddfs_stateful_init(a);
127 void MC_init_liveness_stateless(xbt_automaton_t a, char *prgm){
129 XBT_DEBUG("Start init mc");
131 mc_time = xbt_new0(double, simix_process_maxpid);
133 /* Initialize the data structures that must be persistent across every
134 iteration of the model-checker (in RAW memory) */
138 /* Initialize statistics */
139 mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
141 XBT_DEBUG("Creating stack");
143 /* Create exploration stack */
144 mc_stack_liveness_stateless = xbt_fifo_new();
149 prog_name = strdup(prgm);
151 MC_ddfs_stateless_init();
157 void MC_modelcheck(void)
159 MC_init_safety_stateless();
164 void MC_modelcheck_stateful(void)
166 MC_init_safety_stateful();
171 void MC_modelcheck_liveness_stateful(xbt_automaton_t a){
172 MC_init_liveness_stateful(a);
176 void MC_modelcheck_liveness_stateless(xbt_automaton_t a, char *prgm){
177 MC_init_liveness_stateless(a, prgm);
181 void MC_exit_liveness(void)
183 MC_print_statistics_pairs(mc_stats_pair);
192 MC_print_statistics(mc_stats);
198 int MC_random(int min, int max)
200 /*FIXME: return mc_current_state->executed_transition->random.value;*/
205 * \brief Schedules all the process that are ready to run
207 void MC_wait_for_requests(void)
209 smx_process_t process;
213 while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
214 SIMIX_process_runall();
215 xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
216 req = &process->request;
217 if (req->call != REQ_NO_REQ && !MC_request_is_visible(req))
218 SIMIX_request_pre(req, 0);
223 int MC_deadlock_check()
225 int deadlock = FALSE;
226 smx_process_t process;
227 if(xbt_swag_size(simix_global->process_list)){
229 xbt_swag_foreach(process, simix_global->process_list){
230 if(process->request.call != REQ_NO_REQ
231 && MC_request_is_enabled(&process->request)){
241 * \brief Re-executes from the initial state all the transitions indicated by
242 * a given model-checker stack.
243 * \param stack The stack with the transitions to execute.
245 void MC_replay(xbt_fifo_t stack)
249 smx_req_t req = NULL, saved_req = NULL;
250 xbt_fifo_item_t item;
253 XBT_DEBUG("**** Begin Replay ****");
255 /* Restore the initial state */
256 MC_restore_snapshot(initial_snapshot);
257 /* At the moment of taking the snapshot the raw heap was set, so restoring
258 * it will set it back again, we have to unset it to continue */
261 /* Traverse the stack from the initial state and re-execute the transitions */
262 for (item = xbt_fifo_get_last_item(stack);
263 item != xbt_fifo_get_first_item(stack);
264 item = xbt_fifo_get_prev_item(item)) {
266 state = (mc_state_t) xbt_fifo_get_item_content(item);
267 saved_req = MC_state_get_executed_request(state, &value);
270 /* because we got a copy of the executed request, we have to fetch the
271 real one, pointed by the request field of the issuer process */
272 req = &saved_req->issuer->request;
274 /* Debug information */
275 if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
276 req_str = MC_request_to_string(req, value);
277 XBT_DEBUG("Replay: %s (%p)", req_str, state);
282 SIMIX_request_pre(req, value);
283 MC_wait_for_requests();
285 /* Update statistics */
286 mc_stats->visited_states++;
287 mc_stats->executed_transitions++;
289 XBT_DEBUG("**** End Replay ****");
292 void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
296 smx_req_t req = NULL, saved_req = NULL;
297 xbt_fifo_item_t item;
299 mc_pair_stateless_t pair;
302 XBT_DEBUG("**** Begin Replay ****");
304 /* Restore the initial state */
305 MC_restore_snapshot(initial_snapshot_liveness);
306 /* At the moment of taking the snapshot the raw heap was set, so restoring
307 * it will set it back again, we have to unset it to continue */
312 item = xbt_fifo_get_last_item(stack);
314 while(depth <= xbt_fifo_size(stack)){
316 pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
317 state = (mc_state_t) pair->graph_state;
319 if(pair->requests > 0){
321 saved_req = MC_state_get_executed_request(state, &value);
322 //XBT_DEBUG("SavedReq->call %u", saved_req->call);
324 if(saved_req != NULL){
325 /* because we got a copy of the executed request, we have to fetch the
326 real one, pointed by the request field of the issuer process */
327 req = &saved_req->issuer->request;
328 //XBT_DEBUG("Req->call %u", req->call);
330 /* Debug information */
331 if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
332 req_str = MC_request_to_string(req, value);
333 XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
339 SIMIX_request_pre(req, value);
340 MC_wait_for_requests();
345 /* Update statistics */
346 mc_stats_pair->visited_pairs++;
348 item = xbt_fifo_get_prev_item(item);
353 /* Traverse the stack from the initial state and re-execute the transitions */
354 for (item = xbt_fifo_get_last_item(stack);
355 item != xbt_fifo_get_first_item(stack);
356 item = xbt_fifo_get_prev_item(item)) {
358 pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
359 state = (mc_state_t) pair->graph_state;
361 if(pair->requests > 0){
363 saved_req = MC_state_get_executed_request(state, &value);
364 //XBT_DEBUG("SavedReq->call %u", saved_req->call);
366 if(saved_req != NULL){
367 /* because we got a copy of the executed request, we have to fetch the
368 real one, pointed by the request field of the issuer process */
369 req = &saved_req->issuer->request;
370 //XBT_DEBUG("Req->call %u", req->call);
372 /* Debug information */
373 if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
374 req_str = MC_request_to_string(req, value);
375 XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
381 SIMIX_request_pre(req, value);
382 MC_wait_for_requests();
387 /* Update statistics */
388 mc_stats_pair->visited_pairs++;
392 XBT_DEBUG("**** End Replay ****");
397 * \brief Dumps the contents of a model-checker's stack and shows the actual
399 * \param stack The stack to dump
401 void MC_dump_stack_safety_stateless(xbt_fifo_t stack)
405 MC_show_stack_safety_stateless(stack);
408 while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
409 MC_state_delete(state);
414 void MC_show_stack_safety_stateless(xbt_fifo_t stack)
418 xbt_fifo_item_t item;
420 char *req_str = NULL;
422 for (item = xbt_fifo_get_last_item(stack);
423 (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
424 : (NULL)); item = xbt_fifo_get_prev_item(item)) {
425 req = MC_state_get_executed_request(state, &value);
427 req_str = MC_request_to_string(req, value);
428 XBT_INFO("%s", req_str);
434 void MC_show_deadlock(smx_req_t req)
436 /*char *req_str = NULL;*/
437 XBT_INFO("**************************");
438 XBT_INFO("*** DEAD-LOCK DETECTED ***");
439 XBT_INFO("**************************");
440 XBT_INFO("Locked request:");
441 /*req_str = MC_request_to_string(req);
442 XBT_INFO("%s", req_str);
444 XBT_INFO("Counter-example execution trace:");
445 MC_dump_stack_safety_stateless(mc_stack_safety_stateless);
448 void MC_show_deadlock_stateful(smx_req_t req)
450 /*char *req_str = NULL;*/
451 XBT_INFO("**************************");
452 XBT_INFO("*** DEAD-LOCK DETECTED ***");
453 XBT_INFO("**************************");
454 XBT_INFO("Locked request:");
455 /*req_str = MC_request_to_string(req);
456 XBT_INFO("%s", req_str);
458 XBT_INFO("Counter-example execution trace:");
459 MC_show_stack_safety_stateful(mc_stack_safety_stateful);
462 void MC_dump_stack_safety_stateful(xbt_fifo_t stack)
464 //mc_state_ws_t state;
466 MC_show_stack_safety_stateful(stack);
469 while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
470 MC_state_delete(state);
475 void MC_show_stack_safety_stateful(xbt_fifo_t stack)
479 xbt_fifo_item_t item;
481 char *req_str = NULL;
483 for (item = xbt_fifo_get_last_item(stack);
484 (item ? (state = (mc_state_ws_t) (xbt_fifo_get_item_content(item)))
485 : (NULL)); item = xbt_fifo_get_prev_item(item)) {
486 req = MC_state_get_executed_request(state->graph_state, &value);
488 req_str = MC_request_to_string(req, value);
489 XBT_INFO("%s", req_str);
495 void MC_show_stack_liveness_stateful(xbt_fifo_t stack){
498 xbt_fifo_item_t item;
500 char *req_str = NULL;
502 for (item = xbt_fifo_get_last_item(stack);
503 (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
504 : (NULL)); item = xbt_fifo_get_prev_item(item)) {
505 req = MC_state_get_executed_request(pair->graph_state, &value);
507 req_str = MC_request_to_string(req, value);
508 XBT_INFO("%s", req_str);
514 void MC_dump_stack_liveness_stateful(xbt_fifo_t stack){
518 while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
519 MC_pair_delete(pair);
523 void MC_show_stack_liveness_stateless(xbt_fifo_t stack){
525 mc_pair_stateless_t pair;
526 xbt_fifo_item_t item;
528 char *req_str = NULL;
530 for (item = xbt_fifo_get_last_item(stack);
531 (item ? (pair = (mc_pair_stateless_t) (xbt_fifo_get_item_content(item)))
532 : (NULL)); item = xbt_fifo_get_prev_item(item)) {
533 req = MC_state_get_executed_request(pair->graph_state, &value);
535 if(pair->requests>0){
536 req_str = MC_request_to_string(req, value);
537 XBT_INFO("%s", req_str);
540 XBT_INFO("End of system requests but evolution in Büchi automaton");
546 void MC_dump_stack_liveness_stateless(xbt_fifo_t stack){
547 mc_pair_stateless_t pair;
550 while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL)
551 MC_pair_stateless_delete(pair);
556 void MC_print_statistics(mc_stats_t stats)
558 XBT_INFO("State space size ~= %lu", stats->state_size);
559 XBT_INFO("Expanded states = %lu", stats->expanded_states);
560 XBT_INFO("Visited states = %lu", stats->visited_states);
561 XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
562 XBT_INFO("Expanded / Visited = %lf",
563 (double) stats->visited_states / stats->expanded_states);
564 /*XBT_INFO("Exploration coverage = %lf",
565 (double)stats->expanded_states / stats->state_size); */
568 void MC_print_statistics_pairs(mc_stats_pair_t stats)
570 XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
571 XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
572 //XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
573 XBT_INFO("Expanded / Visited = %lf",
574 (double) stats->visited_pairs / stats->expanded_pairs);
575 /*XBT_INFO("Exploration coverage = %lf",
576 (double)stats->expanded_states / stats->state_size); */
579 void MC_assert(int prop)
581 if (MC_IS_ENABLED && !prop) {
582 XBT_INFO("**************************");
583 XBT_INFO("*** PROPERTY NOT VALID ***");
584 XBT_INFO("**************************");
585 XBT_INFO("Counter-example execution trace:");
586 MC_dump_stack_safety_stateless(mc_stack_safety_stateless);
587 MC_print_statistics(mc_stats);
592 void MC_assert_stateful(int prop)
594 if (MC_IS_ENABLED && !prop) {
595 XBT_INFO("**************************");
596 XBT_INFO("*** PROPERTY NOT VALID ***");
597 XBT_INFO("**************************");
598 XBT_INFO("Counter-example execution trace:");
599 MC_dump_stack_safety_stateful(mc_stack_safety_stateful);
600 MC_print_statistics(mc_stats);
605 void MC_assert_pair_stateful(int prop){
606 if (MC_IS_ENABLED && !prop) {
607 XBT_INFO("**************************");
608 XBT_INFO("*** PROPERTY NOT VALID ***");
609 XBT_INFO("**************************");
610 //XBT_INFO("Counter-example execution trace:");
611 MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
612 //MC_dump_snapshot_stack(mc_snapshot_stack);
613 MC_print_statistics_pairs(mc_stats_pair);
618 void MC_assert_pair_stateless(int prop){
619 if (MC_IS_ENABLED && !prop) {
620 XBT_INFO("**************************");
621 XBT_INFO("*** PROPERTY NOT VALID ***");
622 XBT_INFO("**************************");
623 //XBT_INFO("Counter-example execution trace:");
624 MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
625 //MC_dump_snapshot_stack(mc_snapshot_stack);
626 MC_print_statistics_pairs(mc_stats_pair);
631 void MC_process_clock_add(smx_process_t process, double amount)
633 mc_time[process->pid] += amount;
636 double MC_process_clock_get(smx_process_t process)
639 return mc_time[process->pid];