src/mc/mc_global.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 <unistd.h>
   7 #include <sys/types.h>
   8 #include <sys/wait.h>
   9 #include <sys/time.h>
  10
  11 #include "../surf/surf_private.h"
  12 #include "../simix/smx_private.h"
  13 #include "xbt/fifo.h"
  14 #include "mc_private.h"
  15
  16
  17 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
  18                                 "Logging specific to MC (global)");
  19
  20 /* MC global data structures */
  21
  22 mc_state_t mc_current_state = NULL;
  23 char mc_replay_mode = FALSE;
  24 double *mc_time = NULL;
  25 mc_snapshot_t initial_snapshot = NULL;
  26
  27 /* Safety */
  28
  29 xbt_fifo_t mc_stack_safety_stateful = NULL;
  30 xbt_fifo_t mc_stack_safety_stateless = NULL;
  31 mc_stats_t mc_stats = NULL;
  32
  33 /* Liveness */
  34
  35 mc_stats_pair_t mc_stats_pair = NULL;
  36 xbt_fifo_t mc_stack_liveness = NULL;
  37 mc_snapshot_t initial_snapshot_liveness = NULL;
  38
  39 xbt_automaton_t automaton;
  40 char *prog_name;
  41
  42 static void MC_init_liveness(xbt_automaton_t a, char *prgm);
  43 static void MC_assert_pair(int prop);
  44
  45
  46 /**
  47  *  \brief Initialize the model-checker data structures
  48  */
  49 void MC_init_safety_stateless(void)
  50 {
  51
  52   /* Check if MC is already initialized */
  53   if (initial_snapshot)
  54     return;
  55
  56   mc_time = xbt_new0(double, simix_process_maxpid);
  57
  58   /* Initialize the data structures that must be persistent across every
  59      iteration of the model-checker (in RAW memory) */
  60   MC_SET_RAW_MEM;
  61
  62   /* Initialize statistics */
  63   mc_stats = xbt_new0(s_mc_stats_t, 1);
  64   mc_stats->state_size = 1;
  65
  66   /* Create exploration stack */
  67   mc_stack_safety_stateless = xbt_fifo_new();
  68
  69   MC_UNSET_RAW_MEM;
  70
  71   MC_dpor_init();
  72
  73   MC_SET_RAW_MEM;
  74   /* Save the initial state */
  75   initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
  76   MC_take_snapshot(initial_snapshot);
  77   MC_UNSET_RAW_MEM;
  78 }
  79
  80 void MC_init_safety_stateful(void){
  81
  82
  83    /* Check if MC is already initialized */
  84   if (initial_snapshot)
  85     return;
  86
  87   mc_time = xbt_new0(double, simix_process_maxpid);
  88
  89   /* Initialize the data structures that must be persistent across every
  90      iteration of the model-checker (in RAW memory) */
  91   MC_SET_RAW_MEM;
  92
  93   /* Initialize statistics */
  94   mc_stats = xbt_new0(s_mc_stats_t, 1);
  95   mc_stats->state_size = 1;
  96
  97   /* Create exploration stack */
  98   mc_stack_safety_stateful = xbt_fifo_new();
  99
 100   MC_UNSET_RAW_MEM;
 101
 102   MC_dpor_stateful_init();
 103
 104
 105 }
 106
 107 static void MC_init_liveness(xbt_automaton_t a, char *prgm){
 108
 109   XBT_DEBUG("Start init mc");
 110
 111   mc_time = xbt_new0(double, simix_process_maxpid);
 112
 113   /* Initialize the data structures that must be persistent across every
 114      iteration of the model-checker (in RAW memory) */
 115
 116   MC_SET_RAW_MEM;
 117
 118   /* Initialize statistics */
 119   mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
 120
 121   XBT_DEBUG("Creating stack");
 122
 123  /* Create exploration stack */
 124   mc_stack_liveness = xbt_fifo_new();
 125
 126   MC_UNSET_RAW_MEM;
 127
 128   automaton = a;
 129   prog_name = strdup(prgm);
 130
 131   MC_ddfs_init();
 132
 133
 134 }
 135
 136
 137 void MC_modelcheck(void)
 138 {
 139   MC_init_safety_stateless();
 140   MC_dpor();
 141   MC_exit();
 142 }
 143
 144 void MC_modelcheck_stateful(void)
 145 {
 146   MC_init_safety_stateful();
 147   MC_dpor_stateful();
 148   MC_exit();
 149 }
 150
 151
 152 void MC_modelcheck_liveness(xbt_automaton_t a, char *prgm){
 153   MC_init_liveness(a, prgm);
 154   MC_exit_liveness();
 155 }
 156
 157 void MC_exit_liveness(void)
 158 {
 159   MC_print_statistics_pairs(mc_stats_pair);
 160   //xbt_free(mc_time);
 161   //MC_memory_exit();
 162   exit(0);
 163 }
 164
 165
 166 void MC_exit(void)
 167 {
 168   MC_print_statistics(mc_stats);
 169   xbt_free(mc_time);
 170   MC_memory_exit();
 171 }
 172
 173
 174 int MC_random(int min, int max)
 175 {
 176   /*FIXME: return mc_current_state->executed_transition->random.value;*/
 177   return 0;
 178 }
 179
 180 /**
 181  * \brief Schedules all the process that are ready to run
 182  */
 183 void MC_wait_for_requests(void)
 184 {
 185   smx_process_t process;
 186   smx_simcall_t req;
 187   unsigned int iter;
 188
 189   while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
 190     SIMIX_process_runall();
 191     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
 192       req = &process->simcall;
 193       if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
 194           SIMIX_simcall_pre(req, 0);
 195     }
 196   }
 197 }
 198
 199 int MC_deadlock_check()
 200 {
 201   int deadlock = FALSE;
 202   smx_process_t process;
 203   if(xbt_swag_size(simix_global->process_list)){
 204     deadlock = TRUE;
 205     xbt_swag_foreach(process, simix_global->process_list){
 206       if(process->simcall.call != SIMCALL_NONE
 207          && MC_request_is_enabled(&process->simcall)){
 208         deadlock = FALSE;
 209         break;
 210       }
 211     }
 212   }
 213   return deadlock;
 214 }
 215
 216 /**
 217  * \brief Re-executes from the initial state all the transitions indicated by
 218  *        a given model-checker stack.
 219  * \param stack The stack with the transitions to execute.
 220 */
 221 void MC_replay(xbt_fifo_t stack)
 222 {
 223   int value;
 224   char *req_str;
 225   smx_simcall_t req = NULL, saved_req = NULL;
 226   xbt_fifo_item_t item;
 227   mc_state_t state;
 228
 229   XBT_DEBUG("**** Begin Replay ****");
 230
 231   /* Restore the initial state */
 232   MC_restore_snapshot(initial_snapshot);
 233   /* At the moment of taking the snapshot the raw heap was set, so restoring
 234    * it will set it back again, we have to unset it to continue  */
 235   MC_UNSET_RAW_MEM;
 236
 237   /* Traverse the stack from the initial state and re-execute the transitions */
 238   for (item = xbt_fifo_get_last_item(stack);
 239        item != xbt_fifo_get_first_item(stack);
 240        item = xbt_fifo_get_prev_item(item)) {
 241
 242     state = (mc_state_t) xbt_fifo_get_item_content(item);
 243     saved_req = MC_state_get_executed_request(state, &value);
 244
 245     if(saved_req){
 246       /* because we got a copy of the executed request, we have to fetch the
 247          real one, pointed by the request field of the issuer process */
 248       req = &saved_req->issuer->simcall;
 249
 250       /* Debug information */
 251       if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
 252         req_str = MC_request_to_string(req, value);
 253         XBT_DEBUG("Replay: %s (%p)", req_str, state);
 254         xbt_free(req_str);
 255       }
 256     }
 257
 258     SIMIX_simcall_pre(req, value);
 259     MC_wait_for_requests();
 260
 261     /* Update statistics */
 262     mc_stats->visited_states++;
 263     mc_stats->executed_transitions++;
 264   }
 265   XBT_DEBUG("**** End Replay ****");
 266 }
 267
 268 void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
 269 {
 270   int value;
 271   char *req_str;
 272   smx_simcall_t req = NULL, saved_req = NULL;
 273   xbt_fifo_item_t item;
 274   mc_state_t state;
 275   mc_pair_stateless_t pair;
 276   int depth = 1;
 277
 278   XBT_DEBUG("**** Begin Replay ****");
 279
 280   /* Restore the initial state */
 281   MC_restore_snapshot(initial_snapshot_liveness);
 282   /* At the moment of taking the snapshot the raw heap was set, so restoring
 283    * it will set it back again, we have to unset it to continue  */
 284   MC_UNSET_RAW_MEM;
 285
 286   if(all_stack){
 287
 288     item = xbt_fifo_get_last_item(stack);
 289
 290     while(depth <= xbt_fifo_size(stack)){
 291
 292       pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
 293       state = (mc_state_t) pair->graph_state;
 294
 295       if(pair->requests > 0){
 296
 297         saved_req = MC_state_get_executed_request(state, &value);
 298         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
 299
 300         if(saved_req != NULL){
 301           /* because we got a copy of the executed request, we have to fetch the
 302              real one, pointed by the request field of the issuer process */
 303           req = &saved_req->issuer->simcall;
 304           //XBT_DEBUG("Req->call %u", req->call);
 305
 306           /* Debug information */
 307           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
 308             req_str = MC_request_to_string(req, value);
 309             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
 310             xbt_free(req_str);
 311           }
 312
 313         }
 314
 315         SIMIX_simcall_pre(req, value);
 316         MC_wait_for_requests();
 317       }
 318
 319       depth++;
 320
 321       /* Update statistics */
 322       mc_stats_pair->visited_pairs++;
 323
 324       item = xbt_fifo_get_prev_item(item);
 325     }
 326
 327   }else{
 328
 329     /* Traverse the stack from the initial state and re-execute the transitions */
 330     for (item = xbt_fifo_get_last_item(stack);
 331          item != xbt_fifo_get_first_item(stack);
 332          item = xbt_fifo_get_prev_item(item)) {
 333
 334       pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
 335       state = (mc_state_t) pair->graph_state;
 336
 337       if(pair->requests > 0){
 338
 339         saved_req = MC_state_get_executed_request(state, &value);
 340         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
 341
 342         if(saved_req != NULL){
 343           /* because we got a copy of the executed request, we have to fetch the
 344              real one, pointed by the request field of the issuer process */
 345           req = &saved_req->issuer->simcall;
 346           //XBT_DEBUG("Req->call %u", req->call);
 347
 348           /* Debug information */
 349           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
 350             req_str = MC_request_to_string(req, value);
 351             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
 352             xbt_free(req_str);
 353           }
 354
 355         }
 356
 357         SIMIX_simcall_pre(req, value);
 358         MC_wait_for_requests();
 359       }
 360
 361       depth++;
 362
 363       /* Update statistics */
 364       mc_stats_pair->visited_pairs++;
 365     }
 366   }
 367
 368   XBT_DEBUG("**** End Replay ****");
 369 }
 370
 371
 372 /**
 373  * \brief Dumps the contents of a model-checker's stack and shows the actual
 374  *        execution trace
 375  * \param stack The stack to dump
 376 */
 377 void MC_dump_stack_safety_stateless(xbt_fifo_t stack)
 378 {
 379   mc_state_t state;
 380
 381   MC_show_stack_safety_stateless(stack);
 382
 383   MC_SET_RAW_MEM;
 384   while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
 385     MC_state_delete(state);
 386   MC_UNSET_RAW_MEM;
 387 }
 388
 389
 390 void MC_show_stack_safety_stateless(xbt_fifo_t stack)
 391 {
 392   int value;
 393   mc_state_t state;
 394   xbt_fifo_item_t item;
 395   smx_simcall_t req;
 396   char *req_str = NULL;
 397
 398   for (item = xbt_fifo_get_last_item(stack);
 399        (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
 400         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 401     req = MC_state_get_executed_request(state, &value);
 402     if(req){
 403       req_str = MC_request_to_string(req, value);
 404       XBT_INFO("%s", req_str);
 405       xbt_free(req_str);
 406     }
 407   }
 408 }
 409
 410 void MC_show_deadlock(smx_simcall_t req)
 411 {
 412   /*char *req_str = NULL;*/
 413   XBT_INFO("**************************");
 414   XBT_INFO("*** DEAD-LOCK DETECTED ***");
 415   XBT_INFO("**************************");
 416   XBT_INFO("Locked request:");
 417   /*req_str = MC_request_to_string(req);
 418   XBT_INFO("%s", req_str);
 419   xbt_free(req_str);*/
 420   XBT_INFO("Counter-example execution trace:");
 421   MC_dump_stack_safety_stateless(mc_stack_safety_stateless);
 422 }
 423
 424 void MC_show_deadlock_stateful(smx_simcall_t req)
 425 {
 426   /*char *req_str = NULL;*/
 427   XBT_INFO("**************************");
 428   XBT_INFO("*** DEAD-LOCK DETECTED ***");
 429   XBT_INFO("**************************");
 430   XBT_INFO("Locked request:");
 431   /*req_str = MC_request_to_string(req);
 432   XBT_INFO("%s", req_str);
 433   xbt_free(req_str);*/
 434   XBT_INFO("Counter-example execution trace:");
 435   MC_show_stack_safety_stateful(mc_stack_safety_stateful);
 436 }
 437
 438 void MC_dump_stack_safety_stateful(xbt_fifo_t stack)
 439 {
 440   //mc_state_ws_t state;
 441
 442   MC_show_stack_safety_stateful(stack);
 443
 444   /*MC_SET_RAW_MEM;
 445   while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
 446     MC_state_delete(state);
 447     MC_UNSET_RAW_MEM;*/
 448 }
 449
 450
 451 void MC_show_stack_safety_stateful(xbt_fifo_t stack)
 452 {
 453   int value;
 454   mc_state_ws_t state;
 455   xbt_fifo_item_t item;
 456   smx_simcall_t req;
 457   char *req_str = NULL;
 458
 459   for (item = xbt_fifo_get_last_item(stack);
 460        (item ? (state = (mc_state_ws_t) (xbt_fifo_get_item_content(item)))
 461         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 462     req = MC_state_get_executed_request(state->graph_state, &value);
 463     if(req){
 464       req_str = MC_request_to_string(req, value);
 465       XBT_INFO("%s", req_str);
 466       xbt_free(req_str);
 467     }
 468   }
 469 }
 470
 471
 472 void MC_show_stack_liveness(xbt_fifo_t stack){
 473   int value;
 474   mc_pair_stateless_t pair;
 475   xbt_fifo_item_t item;
 476   smx_simcall_t req;
 477   char *req_str = NULL;
 478
 479   for (item = xbt_fifo_get_last_item(stack);
 480        (item ? (pair = (mc_pair_stateless_t) (xbt_fifo_get_item_content(item)))
 481         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 482     req = MC_state_get_executed_request(pair->graph_state, &value);
 483     if(req){
 484       if(pair->requests>0){
 485         req_str = MC_request_to_string(req, value);
 486         XBT_INFO("%s", req_str);
 487         xbt_free(req_str);
 488       }else{
 489         XBT_INFO("End of system requests but evolution in Büchi automaton");
 490       }
 491     }
 492   }
 493 }
 494
 495 void MC_dump_stack_liveness(xbt_fifo_t stack){
 496   mc_pair_stateless_t pair;
 497
 498   MC_SET_RAW_MEM;
 499   while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL)
 500     MC_pair_stateless_delete(pair);
 501   MC_UNSET_RAW_MEM;
 502 }
 503
 504
 505 void MC_print_statistics(mc_stats_t stats)
 506 {
 507   XBT_INFO("State space size ~= %lu", stats->state_size);
 508   XBT_INFO("Expanded states = %lu", stats->expanded_states);
 509   XBT_INFO("Visited states = %lu", stats->visited_states);
 510   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
 511   XBT_INFO("Expanded / Visited = %lf",
 512         (double) stats->visited_states / stats->expanded_states);
 513   /*XBT_INFO("Exploration coverage = %lf",
 514      (double)stats->expanded_states / stats->state_size); */
 515 }
 516
 517 void MC_print_statistics_pairs(mc_stats_pair_t stats)
 518 {
 519   XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
 520   XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
 521   //XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
 522   XBT_INFO("Expanded / Visited = %lf",
 523         (double) stats->visited_pairs / stats->expanded_pairs);
 524   /*XBT_INFO("Exploration coverage = %lf",
 525      (double)stats->expanded_states / stats->state_size); */
 526 }
 527
 528 void MC_assert(int prop)
 529 {
 530   if (MC_IS_ENABLED && !prop) {
 531     XBT_INFO("**************************");
 532     XBT_INFO("*** PROPERTY NOT VALID ***");
 533     XBT_INFO("**************************");
 534     XBT_INFO("Counter-example execution trace:");
 535     MC_dump_stack_safety_stateless(mc_stack_safety_stateless);
 536     MC_print_statistics(mc_stats);
 537     xbt_abort();
 538   }
 539 }
 540
 541 void MC_assert_stateful(int prop)
 542 {
 543   if (MC_IS_ENABLED && !prop) {
 544     XBT_INFO("**************************");
 545     XBT_INFO("*** PROPERTY NOT VALID ***");
 546     XBT_INFO("**************************");
 547     XBT_INFO("Counter-example execution trace:");
 548     MC_dump_stack_safety_stateful(mc_stack_safety_stateful);
 549     MC_print_statistics(mc_stats);
 550     xbt_abort();
 551   }
 552 }
 553
 554
 555 static void MC_assert_pair(int prop){
 556   if (MC_IS_ENABLED && !prop) {
 557     XBT_INFO("**************************");
 558     XBT_INFO("*** PROPERTY NOT VALID ***");
 559     XBT_INFO("**************************");
 560     //XBT_INFO("Counter-example execution trace:");
 561     MC_show_stack_liveness(mc_stack_liveness);
 562     //MC_dump_snapshot_stack(mc_snapshot_stack);
 563     MC_print_statistics_pairs(mc_stats_pair);
 564     xbt_abort();
 565   }
 566 }
 567
 568 void MC_process_clock_add(smx_process_t process, double amount)
 569 {
 570   mc_time[process->pid] += amount;
 571 }
 572
 573 double MC_process_clock_get(smx_process_t process)
 574 {
 575   if(mc_time)
 576     return mc_time[process->pid];
 577   else
 578     return 0;
 579 }
 580
 581 void MC_diff(void){
 582
 583   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 584   MC_take_snapshot_liveness(sn);
 585
 586   int i;
 587
 588   XBT_INFO("Number of regions : %d", sn->num_reg);
 589
 590   for(i=0; i<sn->num_reg; i++){
 591
 592     switch(sn->regions[i]->type){
 593     case 0: /* heap */
 594       XBT_INFO("Size of heap : %zu", sn->regions[i]->size);
 595       mmalloc_display_info_heap(sn->regions[i]->data);
 596       break;
 597     case 1 : /* libsimgrid */
 598       XBT_INFO("Size of libsimgrid : %zu", sn->regions[i]->size);
 599       break;
 600     case 2 : /* data program */
 601       XBT_INFO("Size of data program : %zu", sn->regions[i]->size);
 602       break;
 603     case 3 : /* stack */
 604       XBT_INFO("Size of stack : %zu", sn->regions[i]->size);
 605       XBT_INFO("Start addr of stack : %p", sn->regions[i]->start_addr);
 606       break;
 607     }
 608
 609   }
 610
 611 }