src/mc/mc_liveness.c

   1 #include "private.h"
   2 #include "unistd.h"
   3
   4 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
   5                                 "Logging specific to algorithms for liveness properties verification");
   6
   7 xbt_dynar_t initial_pairs = NULL;
   8 xbt_fifo_t reached_pairs;
   9 xbt_dynar_t successors = NULL;
  10 extern mc_snapshot_t initial_snapshot;
  11
  12 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
  13
  14   XBT_DEBUG("Compare snapshot");
  15
  16   if(s1->num_reg != s2->num_reg){
  17     XBT_DEBUG("Different num_reg");
  18     return 1;
  19   }
  20
  21   int i;
  22   int errors = 0;
  23
  24   for(i=0 ; i< s1->num_reg ; i++){
  25
  26     if(s1->regions[i]->size != s2->regions[i]->size){
  27       XBT_DEBUG("Different size of region");
  28       return 1;
  29     }
  30
  31     if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
  32       XBT_DEBUG("Different start addr of region");
  33       return 1;
  34     }
  35
  36     if(s1->regions[i]->type != s2->regions[i]->type){
  37       XBT_DEBUG("Different type of region");
  38       return 1;
  39     }
  40
  41
  42     if(s1->regions[i]->type == 0){
  43       if(mmalloc_compare_heap(s1->regions[i]->start_addr, s2->regions[i]->start_addr)){
  44         XBT_DEBUG("Different heap (mmalloc_compare)");
  45         errors++;
  46       }
  47     }else{
  48       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
  49         XBT_DEBUG("Different memcmp for data in libsimgrid or program");
  50         errors++;
  51       }
  52     }
  53
  54
  55   }
  56
  57   return (errors>0);
  58
  59 }
  60
  61 int reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s){
  62
  63
  64   if(xbt_fifo_size(reached_pairs) == 0){
  65
  66     return 0;
  67
  68   }else{
  69
  70     MC_SET_RAW_MEM;
  71
  72     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
  73
  74     /* Get values of propositional symbols */
  75     unsigned int cursor = 0;
  76     xbt_propositional_symbol_t ps = NULL;
  77     xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
  78       int (*f)() = ps->function;
  79       int res = (*f)();
  80       xbt_dynar_push_as(prop_ato, int, res);
  81     }
  82
  83
  84
  85     int i=0;
  86     xbt_fifo_item_t item = xbt_fifo_get_first_item(reached_pairs);
  87     mc_pair_reached_t pair_test = NULL;
  88
  89     while(i < xbt_fifo_size(reached_pairs)){
  90
  91       pair_test = (mc_pair_reached_t) xbt_fifo_get_item_content(item);
  92
  93       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
  94         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
  95           if(snapshot_compare(s, pair_test->system_state) == 0){
  96             MC_UNSET_RAW_MEM;
  97             return 1;
  98           }
  99         }
 100       }
 101
 102       item = xbt_fifo_get_next_item(item);
 103
 104       i++;
 105
 106     }
 107
 108     MC_UNSET_RAW_MEM;
 109     return 0;
 110
 111   }
 112 }
 113
 114 void set_pair_reached(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t sn){
 115
 116
 117   MC_SET_RAW_MEM;
 118
 119   mc_pair_reached_t pair = NULL;
 120   pair = xbt_new0(s_mc_pair_reached_t, 1);
 121   pair->automaton_state = st;
 122   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 123   pair->system_state = sn;
 124
 125   /* Get values of propositional symbols */
 126   unsigned int cursor = 0;
 127   xbt_propositional_symbol_t ps = NULL;
 128   xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
 129     int (*f)() = ps->function;
 130     int res = (*f)();
 131     xbt_dynar_push_as(pair->prop_ato, int, res);
 132   }
 133
 134   xbt_fifo_unshift(reached_pairs, pair);
 135
 136   MC_UNSET_RAW_MEM;
 137
 138
 139 }
 140
 141 void MC_pair_delete(mc_pair_t pair){
 142   xbt_free(pair->graph_state->proc_status);
 143   xbt_free(pair->graph_state);
 144   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 145   xbt_free(pair);
 146 }
 147
 148
 149
 150 int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
 151
 152   switch(l->type){
 153   case 0 : {
 154     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 155     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 156     return (left_res || right_res);
 157     break;
 158   }
 159   case 1 : {
 160     int left_res = MC_automaton_evaluate_label(a, l->u.or_and.left_exp);
 161     int right_res = MC_automaton_evaluate_label(a, l->u.or_and.right_exp);
 162     return (left_res && right_res);
 163     break;
 164   }
 165   case 2 : {
 166     int res = MC_automaton_evaluate_label(a, l->u.exp_not);
 167     return (!res);
 168     break;
 169   }
 170   case 3 : {
 171     unsigned int cursor = 0;
 172     xbt_propositional_symbol_t p = NULL;
 173     xbt_dynar_foreach(a->propositional_symbols, cursor, p){
 174       if(strcmp(p->pred, l->u.predicat) == 0){
 175         int (*f)() = p->function;
 176         return (*f)();
 177       }
 178     }
 179     return -1;
 180     break;
 181   }
 182   case 4 : {
 183     return 2;
 184     break;
 185   }
 186   default :
 187     return -1;
 188   }
 189 }
 190
 191
 192
 193
 194
 195 /********************* Double-DFS stateless *******************/
 196
 197 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
 198   xbt_free(pair->graph_state->proc_status);
 199   xbt_free(pair->graph_state);
 200   //xbt_free(pair->automaton_state); -> FIXME : à implémenter
 201   xbt_free(pair);
 202 }
 203
 204 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
 205   mc_pair_stateless_t p = NULL;
 206   p = xbt_new0(s_mc_pair_stateless_t, 1);
 207   p->automaton_state = st;
 208   p->graph_state = sg;
 209   p->requests = r;
 210   mc_stats_pair->expanded_pairs++;
 211   return p;
 212 }
 213
 214 void MC_ddfs_stateless_init(xbt_automaton_t a, char *prgm){
 215
 216   XBT_DEBUG("**************************************************");
 217   XBT_DEBUG("Double-DFS stateless init");
 218   XBT_DEBUG("**************************************************");
 219
 220   mc_pair_stateless_t mc_initial_pair = NULL;
 221   mc_state_t initial_graph_state = NULL;
 222   smx_process_t process;
 223
 224   MC_wait_for_requests();
 225
 226   MC_SET_RAW_MEM;
 227
 228   initial_graph_state = MC_state_pair_new();
 229   xbt_swag_foreach(process, simix_global->process_list){
 230     if(MC_process_is_enabled(process)){
 231       MC_state_interleave_process(initial_graph_state, process);
 232     }
 233   }
 234
 235   reached_pairs = xbt_fifo_new();
 236   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 237   //snapshot = xbt_new0(s_mc_snapshot_t, 1);
 238
 239   initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
 240   MC_take_snapshot_liveness(initial_snapshot, prgm);
 241
 242   MC_UNSET_RAW_MEM;
 243
 244   unsigned int cursor = 0;
 245   xbt_state_t state;
 246
 247   xbt_dynar_foreach(a->states, cursor, state){
 248     if(state->type == -1){
 249
 250       MC_SET_RAW_MEM;
 251       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 252       xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
 253       MC_UNSET_RAW_MEM;
 254
 255       if(cursor != 0){
 256         MC_restore_snapshot(initial_snapshot);
 257         MC_UNSET_RAW_MEM;
 258       }
 259
 260       MC_ddfs_stateless(a, 0, 0, prgm);
 261
 262     }else{
 263       if(state->type == 2){
 264
 265         MC_SET_RAW_MEM;
 266         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 267         xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
 268         MC_UNSET_RAW_MEM;
 269
 270         set_pair_reached(a, state, initial_snapshot);
 271
 272         if(cursor != 0){
 273           MC_restore_snapshot(initial_snapshot);
 274           MC_UNSET_RAW_MEM;
 275         }
 276
 277         MC_ddfs_stateless(a, 1, 0, prgm);
 278
 279       }
 280     }
 281   }
 282
 283 }
 284
 285
 286 void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay, char *prgm){
 287
 288   smx_process_t process;
 289   mc_pair_stateless_t current_pair = NULL;
 290   mc_snapshot_t snapshot = NULL;
 291
 292   if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
 293     return;
 294
 295   if(replay == 1){
 296     MC_replay_liveness(mc_stack_liveness_stateless, 0);
 297     current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
 298     xbt_swag_foreach(process, simix_global->process_list){
 299       if(MC_process_is_enabled(process)){
 300         MC_state_interleave_process(current_pair->graph_state, process);
 301       }
 302     }
 303   }
 304
 305   /* Get current pair */
 306   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
 307
 308   /* Update current state in buchi automaton */
 309   a->current_state = current_pair->automaton_state;
 310
 311
 312   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
 313   XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id, MC_state_interleave_size(current_pair->graph_state));
 314
 315   mc_stats_pair->visited_pairs++;
 316
 317   int value;
 318   mc_state_t next_graph_state = NULL;
 319   smx_req_t req = NULL;
 320   char *req_str;
 321
 322   xbt_transition_t transition_succ;
 323   unsigned int cursor = 0;
 324   int res;
 325
 326   mc_pair_stateless_t next_pair = NULL;
 327   mc_pair_stateless_t pair_succ;
 328
 329   if(xbt_fifo_size(mc_stack_liveness_stateless) < MAX_DEPTH_LIVENESS){
 330
 331     if(current_pair->requests > 0){
 332
 333       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 334
 335         /* Debug information */
 336         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 337           req_str = MC_request_to_string(req, value);
 338           XBT_DEBUG("Execute: %s", req_str);
 339           xbt_free(req_str);
 340         }
 341
 342         MC_state_set_executed_request(current_pair->graph_state, req, value);
 343
 344         /* Answer the request */
 345         SIMIX_request_pre(req, value);
 346
 347         /* Wait for requests (schedules processes) */
 348         MC_wait_for_requests();
 349
 350
 351         MC_SET_RAW_MEM;
 352
 353         /* Create the new expanded graph_state */
 354         next_graph_state = MC_state_pair_new();
 355
 356         /* Get enabled process and insert it in the interleave set of the next graph_state */
 357         xbt_swag_foreach(process, simix_global->process_list){
 358           if(MC_process_is_enabled(process)){
 359             MC_state_interleave_process(next_graph_state, process);
 360           }
 361         }
 362
 363         xbt_dynar_reset(successors);
 364
 365         MC_UNSET_RAW_MEM;
 366
 367
 368         cursor= 0;
 369         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 370
 371           res = MC_automaton_evaluate_label(a, transition_succ->label);
 372
 373           if(res == 1){ // enabled transition in automaton
 374             MC_SET_RAW_MEM;
 375             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 376             xbt_dynar_push(successors, &next_pair);
 377             MC_UNSET_RAW_MEM;
 378           }
 379
 380         }
 381
 382         cursor = 0;
 383
 384         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 385
 386           res = MC_automaton_evaluate_label(a, transition_succ->label);
 387
 388           if(res == 2){ // true transition in automaton
 389             MC_SET_RAW_MEM;
 390             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 391             xbt_dynar_push(successors, &next_pair);
 392             MC_UNSET_RAW_MEM;
 393           }
 394
 395         }
 396
 397
 398         if(xbt_dynar_length(successors) == 0){
 399           MC_SET_RAW_MEM;
 400           next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state, MC_state_interleave_size(next_graph_state));
 401           xbt_dynar_push(successors, &next_pair);
 402           MC_UNSET_RAW_MEM;
 403         }
 404
 405         cursor = 0;
 406
 407         xbt_dynar_foreach(successors, cursor, pair_succ){
 408
 409           if(search_cycle == 1){
 410
 411             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 412
 413               MC_SET_RAW_MEM;
 414               snapshot = xbt_new0(s_mc_snapshot_t, 1);
 415               MC_take_snapshot_liveness(snapshot, prgm);
 416               MC_UNSET_RAW_MEM;
 417
 418               if(reached(a, pair_succ->automaton_state, snapshot) == 1){
 419
 420                 XBT_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1, MC_state_interleave_size(pair_succ->graph_state));
 421
 422                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 423                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 424                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 425                 XBT_INFO("Counter-example that violates formula :");
 426                 MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
 427                 MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
 428                 MC_print_statistics_pairs(mc_stats_pair);
 429                 exit(0);
 430
 431               }else{
 432
 433                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 434
 435                 set_pair_reached(a, pair_succ->automaton_state, snapshot);
 436
 437               }
 438
 439             }
 440
 441           }else{
 442
 443             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 444
 445               XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 446
 447               MC_SET_RAW_MEM;
 448               snapshot = xbt_new0(s_mc_snapshot_t, 1);
 449               MC_take_snapshot_liveness(snapshot, prgm);
 450               MC_UNSET_RAW_MEM;
 451
 452               set_pair_reached(a, pair_succ->automaton_state, snapshot);
 453
 454               search_cycle = 1;
 455
 456             }
 457
 458           }
 459
 460           MC_SET_RAW_MEM;
 461           xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 462           MC_UNSET_RAW_MEM;
 463
 464           MC_ddfs_stateless(a, search_cycle, 0, prgm);
 465
 466           /* Restore system before checking others successors */
 467           if(cursor != (xbt_dynar_length(successors) - 1))
 468             MC_replay_liveness(mc_stack_liveness_stateless, 1);
 469
 470         }
 471
 472         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 473           XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
 474           MC_replay_liveness(mc_stack_liveness_stateless, 0);
 475         }
 476       }
 477
 478
 479     }else{  /*No request to execute, search evolution in Büchi automaton */
 480
 481       MC_SET_RAW_MEM;
 482
 483       /* Create the new expanded graph_state */
 484       next_graph_state = MC_state_pair_new();
 485
 486       xbt_dynar_reset(successors);
 487
 488       MC_UNSET_RAW_MEM;
 489
 490
 491       cursor= 0;
 492       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 493
 494         res = MC_automaton_evaluate_label(a, transition_succ->label);
 495
 496         if(res == 1){ // enabled transition in automaton
 497           MC_SET_RAW_MEM;
 498           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 499           xbt_dynar_push(successors, &next_pair);
 500           MC_UNSET_RAW_MEM;
 501         }
 502
 503       }
 504
 505       cursor = 0;
 506
 507       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 508
 509         res = MC_automaton_evaluate_label(a, transition_succ->label);
 510
 511         if(res == 2){ // true transition in automaton
 512           MC_SET_RAW_MEM;
 513           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 514           xbt_dynar_push(successors, &next_pair);
 515           MC_UNSET_RAW_MEM;
 516         }
 517
 518       }
 519
 520
 521       if(xbt_dynar_length(successors) == 0){
 522         MC_SET_RAW_MEM;
 523         next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state, MC_state_interleave_size(next_graph_state));
 524         xbt_dynar_push(successors, &next_pair);
 525         MC_UNSET_RAW_MEM;
 526       }
 527
 528       cursor = 0;
 529
 530       xbt_dynar_foreach(successors, cursor, pair_succ){
 531
 532         if(search_cycle == 1){
 533
 534           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 535
 536             MC_SET_RAW_MEM;
 537             snapshot = xbt_new0(s_mc_snapshot_t, 1);
 538             MC_take_snapshot_liveness(snapshot, prgm);
 539             MC_UNSET_RAW_MEM;
 540
 541             if(reached(a, pair_succ->automaton_state, snapshot) == 1){
 542
 543               XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness_stateless) + 1);
 544
 545               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 546               XBT_INFO("|             ACCEPTANCE CYCLE            |");
 547               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 548               XBT_INFO("Counter-example that violates formula :");
 549               MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
 550               MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
 551               MC_print_statistics_pairs(mc_stats_pair);
 552               exit(0);
 553
 554             }else{
 555
 556               XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness_stateless) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 557
 558               set_pair_reached(a, pair_succ->automaton_state, snapshot);
 559
 560             }
 561
 562           }
 563
 564         }else{
 565
 566           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)) && (xbt_fifo_size(mc_stack_liveness_stateless) < (MAX_DEPTH_LIVENESS - 1))){
 567
 568             MC_SET_RAW_MEM;
 569             snapshot = xbt_new0(s_mc_snapshot_t, 1);
 570             MC_take_snapshot_liveness(snapshot, prgm);
 571             MC_UNSET_RAW_MEM;
 572
 573             set_pair_reached(a, pair_succ->automaton_state, snapshot);
 574
 575             search_cycle = 1;
 576
 577           }
 578
 579         }
 580
 581         MC_SET_RAW_MEM;
 582         xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
 583         MC_UNSET_RAW_MEM;
 584
 585         MC_ddfs_stateless(a, search_cycle, 0, prgm);
 586
 587         /* Restore system before checking others successors */
 588         if(cursor != xbt_dynar_length(successors) - 1)
 589           MC_replay_liveness(mc_stack_liveness_stateless, 1);
 590
 591       }
 592
 593     }
 594   }
 595
 596   if(xbt_fifo_size(mc_stack_liveness_stateless) == MAX_DEPTH_LIVENESS ){
 597     XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle);
 598   }else{
 599     XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle);
 600   }
 601
 602
 603   MC_SET_RAW_MEM;
 604   xbt_fifo_shift(mc_stack_liveness_stateless);
 605   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 606     xbt_fifo_shift(reached_pairs);
 607   }
 608   if(snapshot != NULL)
 609     MC_free_snapshot(snapshot);
 610   MC_UNSET_RAW_MEM;
 611
 612   MC_pair_stateless_delete(current_pair);
 613
 614   /* FIXME : free memory (pair, snapshot)*/
 615
 616 }
 617