src/mc/mc_liveness.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 "mc_private.h"
   7 #include <unistd.h>
   8
   9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
  10                                 "Logging specific to algorithms for liveness properties verification");
  11
  12 xbt_dynar_t reached_pairs;
  13 xbt_dynar_t reached_pairs_hash;
  14 xbt_dynar_t visited_pairs;
  15 xbt_dynar_t visited_pairs_hash;
  16 xbt_dynar_t successors;
  17
  18 xbt_dynar_t hosts_table;
  19
  20
  21 /* fast implementation of djb2 algorithm */
  22 unsigned int hash_region(char *str, int str_len){
  23
  24   int c;
  25   register unsigned int hash = 5381;
  26
  27   while (str_len--) {
  28     c = *str++;
  29     hash = ((hash << 5) + hash) + c;    /* hash * 33 + c */
  30   }
  31
  32   return hash;
  33
  34 }
  35
  36 int reached(xbt_state_t st){
  37
  38   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  39
  40
  41   if(xbt_dynar_is_empty(reached_pairs)){
  42
  43     return 0;
  44
  45   }else{
  46
  47     MC_SET_RAW_MEM;
  48
  49     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
  50     MC_take_snapshot_liveness(sn);
  51
  52     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
  53     int res;
  54     int_f_void_t f;
  55
  56     /* Get values of propositional symbols */
  57     unsigned int cursor = 0;
  58     xbt_propositional_symbol_t ps = NULL;
  59     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
  60       f = (int_f_void_t)ps->function;
  61       res = (*f)();
  62       xbt_dynar_push_as(prop_ato, int, res);
  63     }
  64
  65     cursor = 0;
  66     mc_pair_reached_t pair_test = NULL;
  67
  68     //xbt_dict_t current_rdv_points = SIMIX_get_rdv_points();
  69
  70     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
  71       XBT_INFO("Pair reached #%d", pair_test->nb);
  72       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
  73         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
  74           //XBT_INFO("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points));
  75           //if(xbt_dict_length(pair_test->rdv_points) == xbt_dict_length(current_rdv_points)){
  76           //if(rdv_points_compare(pair_test->rdv_points, current_rdv_points) == 0){
  77           if(snapshot_compare(pair_test->system_state, sn) == 0){
  78
  79             MC_free_snapshot(sn);
  80             xbt_dynar_reset(prop_ato);
  81             xbt_free(prop_ato);
  82             MC_UNSET_RAW_MEM;
  83
  84             if(raw_mem_set)
  85               MC_SET_RAW_MEM;
  86             else
  87               MC_UNSET_RAW_MEM;
  88
  89             return 1;
  90           }
  91           /* }
  92              }else{
  93              XBT_INFO("Different size of rdv points (%d - %d)",xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points) );
  94              }*/
  95         }else{
  96           XBT_INFO("Different values of propositional symbols");
  97         }
  98       }else{
  99         XBT_INFO("Different automaton state");
 100       }
 101     }
 102
 103     MC_free_snapshot(sn);
 104     xbt_dynar_reset(prop_ato);
 105     xbt_free(prop_ato);
 106     MC_UNSET_RAW_MEM;
 107
 108     if(raw_mem_set)
 109       MC_SET_RAW_MEM;
 110     else
 111       MC_UNSET_RAW_MEM;
 112
 113     return 0;
 114
 115   }
 116 }
 117
 118 int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = current_pair */
 119
 120   xbt_dict_cursor_t cursor_dict = NULL;
 121   char *key;
 122   char *data;
 123   smx_rdv_t rdv1, rdv2;
 124   xbt_fifo_item_t item1, item2;
 125   smx_action_t action1, action2;
 126   xbt_fifo_item_t item_req1, item_req2;
 127   smx_simcall_t req1, req2;
 128   int i=0;
 129   int j=0;
 130
 131   xbt_dict_foreach(d1, cursor_dict, key, data){
 132     rdv1 = (smx_rdv_t)data;
 133     rdv2 = xbt_dict_get_or_null(d2, rdv1->name);
 134     if(rdv2 == NULL){
 135       XBT_INFO("Rdv point unknown");
 136       return 1;
 137     }else{
 138       if(xbt_fifo_size(rdv1->comm_fifo) != xbt_fifo_size(rdv2->comm_fifo)){
 139         XBT_INFO("Different total of actions in mailbox \"%s\" (%d - %d)", rdv1->name, xbt_fifo_size(rdv1->comm_fifo),xbt_fifo_size(rdv2->comm_fifo) );
 140         return 1;
 141       }else{
 142
 143         XBT_INFO("Total of actions in mailbox \"%s\" : %d", rdv1->name, xbt_fifo_size(rdv1->comm_fifo));
 144
 145         item1 = xbt_fifo_get_first_item(rdv1->comm_fifo);
 146         item2 = xbt_fifo_get_first_item(rdv2->comm_fifo);
 147
 148         while(i<xbt_fifo_size(rdv1->comm_fifo)){
 149           action1 = (smx_action_t) xbt_fifo_get_item_content(item1);
 150           action2 = (smx_action_t) xbt_fifo_get_item_content(item2);
 151
 152           if(action1->type != action2->type){
 153             XBT_INFO("Different type of action");
 154             return 1;
 155           }
 156
 157           if(action1->state != action2->state){
 158             XBT_INFO("Different state of action");
 159             return 1;
 160           }
 161
 162           if(xbt_fifo_size(action1->simcalls) != xbt_fifo_size(action2->simcalls)){
 163             XBT_INFO("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls));
 164             return 1;
 165           }else{
 166
 167             item_req1 = xbt_fifo_get_first_item(action1->simcalls);
 168             item_req2 = xbt_fifo_get_first_item(action2->simcalls);
 169
 170             while(j<xbt_fifo_size(action1->simcalls)){
 171
 172               req1 = (smx_simcall_t) xbt_fifo_get_item_content(item_req1);
 173               req2 = (smx_simcall_t) xbt_fifo_get_item_content(item_req2);
 174
 175               if(req1->call != req2->call){
 176                 XBT_INFO("Different simcall call in simcalls of action (%d - %d)", (int)req1->call, (int)req2->call);
 177                 return 1;
 178               }
 179               if(req1->issuer->pid != req2->issuer->pid){
 180                 XBT_INFO("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid);
 181                 return 1;
 182               }
 183
 184               item_req1 = xbt_fifo_get_next_item(item_req1);
 185               item_req2 = xbt_fifo_get_next_item(item_req2);
 186               j++;
 187
 188             }
 189           }
 190
 191           switch(action1->type){
 192           case 0: /* execution */
 193           case 1: /* parallel execution */
 194             if(strcmp(action1->execution.host->name, action2->execution.host->name) != 0)
 195               return 1;
 196             break;
 197           case 2: /* comm */
 198             if(action1->comm.type != action2->comm.type)
 199               return 1;
 200             //XBT_INFO("Type of comm : %d", action1->comm.type);
 201
 202             switch(action1->comm.type){
 203             case 0: /* SEND */
 204               if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
 205                 return 1;
 206               if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
 207                 return 1;
 208               break;
 209             case 1: /* RECEIVE */
 210               if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
 211                 return 1;
 212               if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
 213                 return 1;
 214               break;
 215             case 2: /* READY */
 216               if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
 217                 return 1;
 218               if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
 219                 return 1;
 220               if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
 221                 return 1;
 222               if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
 223                 return 1;
 224               break;
 225             case 3: /* DONE */
 226               if(action1->comm.src_proc->pid != action2->comm.src_proc->pid)
 227                 return 1;
 228               if(strcmp(action1->comm.src_proc->smx_host->name, action2->comm.src_proc->smx_host->name) != 0)
 229                 return 1;
 230               if(action1->comm.dst_proc->pid != action2->comm.dst_proc->pid)
 231                 return 1;
 232               if(strcmp(action1->comm.dst_proc->smx_host->name, action2->comm.dst_proc->smx_host->name) != 0)
 233                 return 1;
 234               break;
 235
 236             } /* end of switch on type of comm */
 237
 238             if(action1->comm.refcount != action2->comm.refcount)
 239               return 1;
 240             if(action1->comm.detached != action2->comm.detached)
 241               return 1;
 242             if(action1->comm.rate != action2->comm.rate)
 243               return 1;
 244             if(action1->comm.task_size != action2->comm.task_size)
 245               return 1;
 246             if(action1->comm.src_buff != action2->comm.src_buff)
 247               return 1;
 248             if(action1->comm.dst_buff != action2->comm.dst_buff)
 249               return 1;
 250             if(action1->comm.src_data != action2->comm.src_data)
 251               return 1;
 252             if(action1->comm.dst_data != action2->comm.dst_data)
 253               return 1;
 254
 255             break;
 256           case 3: /* sleep */
 257             if(strcmp(action1->sleep.host->name, action2->sleep.host->name) != 0)
 258               return 1;
 259             break;
 260           case 4: /* synchro */
 261
 262             break;
 263           default:
 264             break;
 265           }
 266
 267           item1 = xbt_fifo_get_next_item(item1);
 268           item2 = xbt_fifo_get_next_item(item2);
 269           i++;
 270         }
 271       }
 272     }
 273   }
 274
 275   return 0;
 276
 277 }
 278
 279 void set_pair_reached(xbt_state_t st){
 280
 281   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 282
 283   MC_SET_RAW_MEM;
 284
 285   mc_pair_reached_t pair = NULL;
 286   pair = xbt_new0(s_mc_pair_reached_t, 1);
 287   pair->nb = xbt_dynar_length(reached_pairs) + 1;
 288   pair->automaton_state = st;
 289   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 290   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
 291   //pair->rdv_points = xbt_dict_new();
 292   MC_take_snapshot_liveness(pair->system_state);
 293
 294   /* Get values of propositional symbols */
 295   unsigned int cursor = 0;
 296   xbt_propositional_symbol_t ps = NULL;
 297   int res;
 298   int_f_void_t f;
 299
 300   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 301     f = (int_f_void_t)ps->function;
 302     res = (*f)();
 303     xbt_dynar_push_as(pair->prop_ato, int, res);
 304   }
 305
 306   /*xbt_dict_t rdv_points = SIMIX_get_rdv_points();
 307
 308     xbt_dict_cursor_t cursor_dict = NULL;
 309     char *key;
 310     char *data;
 311     xbt_fifo_item_t item;
 312     smx_action_t action;
 313
 314     xbt_dict_foreach(rdv_points, cursor_dict, key, data){
 315     smx_rdv_t new_rdv = xbt_new0(s_smx_rvpoint_t, 1);
 316     new_rdv->name = strdup(((smx_rdv_t)data)->name);
 317     new_rdv->comm_fifo = xbt_fifo_new();
 318     xbt_fifo_foreach(((smx_rdv_t)data)->comm_fifo, item, action, smx_action_t) {
 319     smx_action_t a = xbt_new0(s_smx_action_t, 1);
 320     memcpy(a, action, sizeof(s_smx_action_t));
 321     xbt_fifo_push(new_rdv->comm_fifo, a);
 322     XBT_INFO("New action (type = %d, state = %d) in mailbox \"%s\"", action->type, action->state, key);
 323     if(action->type==2)
 324     XBT_INFO("Type of communication : %d, Ref count = %d", action->comm.type, action->comm.refcount);
 325     }
 326     //new_rdv->comm_fifo = xbt_fifo_copy(((smx_rdv_t)data)->comm_fifo);
 327     xbt_dict_set(pair->rdv_points, new_rdv->name, new_rdv, NULL);
 328     }*/
 329
 330   xbt_dynar_push(reached_pairs, &pair);
 331
 332   MC_UNSET_RAW_MEM;
 333
 334   if(raw_mem_set)
 335     MC_SET_RAW_MEM;
 336   else
 337     MC_UNSET_RAW_MEM;
 338
 339 }
 340
 341
 342 int reached_hash(xbt_state_t st){
 343
 344   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 345
 346   if(xbt_dynar_is_empty(reached_pairs_hash)){
 347
 348     return 0;
 349
 350   }else{
 351
 352     MC_SET_RAW_MEM;
 353
 354     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 355     MC_take_snapshot_liveness(sn);
 356
 357     int j;
 358     unsigned int hash_regions[sn->num_reg];
 359     for(j=0; j<sn->num_reg; j++){
 360       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
 361     }
 362
 363
 364     /* Get values of propositional symbols */
 365     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 366     unsigned int cursor = 0;
 367     xbt_propositional_symbol_t ps = NULL;
 368     int res;
 369     int_f_void_t f;
 370
 371     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 372       f = (int_f_void_t)ps->function;
 373       res = (*f)();
 374       xbt_dynar_push_as(prop_ato, int, res);
 375     }
 376
 377     mc_pair_reached_hash_t pair_test = NULL;
 378
 379     int region_diff = 0;
 380
 381     cursor = 0;
 382
 383     xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
 384
 385       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 386         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 387           for(j=0 ; j< sn->num_reg ; j++){
 388             if(hash_regions[j] != pair_test->hash_regions[j]){
 389               region_diff++;
 390             }
 391           }
 392           if(region_diff == 0){
 393             MC_free_snapshot(sn);
 394             xbt_dynar_reset(prop_ato);
 395             xbt_free(prop_ato);
 396             MC_UNSET_RAW_MEM;
 397
 398             if(raw_mem_set)
 399               MC_SET_RAW_MEM;
 400             else
 401               MC_UNSET_RAW_MEM;
 402
 403             return 1;
 404           }else{
 405             XBT_INFO("Different snapshot");
 406           }
 407         }else{
 408           XBT_INFO("Different values of propositional symbols");
 409         }
 410       }else{
 411         XBT_INFO("Different automaton state");
 412       }
 413
 414       region_diff = 0;
 415     }
 416
 417     MC_free_snapshot(sn);
 418     xbt_dynar_reset(prop_ato);
 419     xbt_free(prop_ato);
 420     MC_UNSET_RAW_MEM;
 421
 422     if(raw_mem_set)
 423       MC_SET_RAW_MEM;
 424     else
 425       MC_UNSET_RAW_MEM;
 426
 427     return 0;
 428
 429   }
 430 }
 431
 432 void set_pair_reached_hash(xbt_state_t st){
 433
 434   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 435
 436   MC_SET_RAW_MEM;
 437
 438   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 439   MC_take_snapshot_liveness(sn);
 440
 441   mc_pair_reached_hash_t pair = NULL;
 442   pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
 443   pair->automaton_state = st;
 444   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 445   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
 446
 447   int i;
 448
 449   for(i=0 ; i< sn->num_reg ; i++){
 450     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
 451   }
 452
 453   /* Get values of propositional symbols */
 454   unsigned int cursor = 0;
 455   xbt_propositional_symbol_t ps = NULL;
 456   int res;
 457   int_f_void_t f;
 458
 459   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 460     f = (int_f_void_t)ps->function;
 461     res = (*f)();
 462     xbt_dynar_push_as(pair->prop_ato, int, res);
 463   }
 464
 465   xbt_dynar_push(reached_pairs_hash, &pair);
 466
 467   MC_free_snapshot(sn);
 468
 469   MC_UNSET_RAW_MEM;
 470
 471   if(raw_mem_set)
 472     MC_SET_RAW_MEM;
 473   else
 474     MC_UNSET_RAW_MEM;
 475
 476 }
 477
 478
 479 int visited(xbt_state_t st, int sc){
 480
 481   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 482
 483   if(xbt_dynar_is_empty(visited_pairs)){
 484
 485     return 0;
 486
 487   }else{
 488
 489     MC_SET_RAW_MEM;
 490
 491     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 492     MC_take_snapshot_liveness(sn);
 493
 494     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 495
 496     /* Get values of propositional symbols */
 497     unsigned int cursor = 0;
 498     xbt_propositional_symbol_t ps = NULL;
 499     int res;
 500     int_f_void_t f;
 501
 502     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 503       f = (int_f_void_t)ps->function;
 504       res = (*f)();
 505       xbt_dynar_push_as(prop_ato, int, res);
 506     }
 507
 508     cursor = 0;
 509     mc_pair_visited_t pair_test = NULL;
 510
 511     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
 512       if(pair_test->search_cycle == sc) {
 513         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 514           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 515             if(snapshot_compare(pair_test->system_state, sn) == 0){
 516
 517               MC_free_snapshot(sn);
 518               xbt_dynar_reset(prop_ato);
 519               xbt_free(prop_ato);
 520               MC_UNSET_RAW_MEM;
 521
 522               if(raw_mem_set)
 523                 MC_SET_RAW_MEM;
 524               else
 525                 MC_UNSET_RAW_MEM;
 526
 527               return 1;
 528
 529             }else{
 530               XBT_INFO("Different snapshot");
 531             }
 532           }else{
 533             XBT_INFO("Different values of propositional symbols");
 534           }
 535         }else{
 536           XBT_INFO("Different automaton state");
 537         }
 538       }else{
 539         XBT_INFO("Different value of search_cycle");
 540       }
 541     }
 542
 543
 544     MC_free_snapshot(sn);
 545     xbt_dynar_reset(prop_ato);
 546     xbt_free(prop_ato);
 547     MC_UNSET_RAW_MEM;
 548
 549     if(raw_mem_set)
 550       MC_SET_RAW_MEM;
 551     else
 552       MC_UNSET_RAW_MEM;
 553
 554     return 0;
 555
 556   }
 557 }
 558
 559
 560 int visited_hash(xbt_state_t st, int sc){
 561
 562   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 563
 564   if(xbt_dynar_is_empty(visited_pairs_hash)){
 565
 566     return 0;
 567
 568   }else{
 569
 570     MC_SET_RAW_MEM;
 571
 572     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 573     MC_take_snapshot_liveness(sn);
 574
 575     int j;
 576     unsigned int hash_regions[sn->num_reg];
 577     for(j=0; j<sn->num_reg; j++){
 578       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
 579     }
 580
 581
 582     /* Get values of propositional symbols */
 583     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 584     unsigned int cursor = 0;
 585     xbt_propositional_symbol_t ps = NULL;
 586     int res;
 587     int_f_void_t f;
 588
 589     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 590       f = (int_f_void_t)ps->function;
 591       res = (*f)();
 592       xbt_dynar_push_as(prop_ato, int, res);
 593     }
 594
 595     mc_pair_visited_hash_t pair_test = NULL;
 596
 597     int region_diff = 0;
 598     cursor = 0;
 599
 600     xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
 601
 602       if(pair_test->search_cycle == sc) {
 603         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 604           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 605             for(j=0 ; j< sn->num_reg ; j++){
 606               if(hash_regions[j] != pair_test->hash_regions[j]){
 607                 region_diff++;
 608               }
 609             }
 610             if(region_diff == 0){
 611               MC_free_snapshot(sn);
 612               xbt_dynar_reset(prop_ato);
 613               xbt_free(prop_ato);
 614               MC_UNSET_RAW_MEM;
 615
 616               if(raw_mem_set)
 617                 MC_SET_RAW_MEM;
 618               else
 619                 MC_UNSET_RAW_MEM;
 620
 621               return 1;
 622             }else{
 623               //XBT_INFO("Different snapshot");
 624             }
 625           }else{
 626             //XBT_INFO("Different values of propositional symbols");
 627           }
 628         }else{
 629           //XBT_INFO("Different automaton state");
 630         }
 631       }else{
 632         //XBT_INFO("Different value of search_cycle");
 633       }
 634
 635       region_diff = 0;
 636     }
 637
 638     MC_free_snapshot(sn);
 639     xbt_dynar_reset(prop_ato);
 640     xbt_free(prop_ato);
 641     MC_UNSET_RAW_MEM;
 642
 643     if(raw_mem_set)
 644       MC_SET_RAW_MEM;
 645     else
 646       MC_UNSET_RAW_MEM;
 647
 648     return 0;
 649
 650   }
 651 }
 652
 653 void set_pair_visited_hash(xbt_state_t st, int sc){
 654
 655   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 656
 657   MC_SET_RAW_MEM;
 658
 659   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 660   MC_take_snapshot_liveness(sn);
 661
 662   mc_pair_visited_hash_t pair = NULL;
 663   pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
 664   pair->automaton_state = st;
 665   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 666   pair->search_cycle = sc;
 667   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
 668
 669   int i;
 670
 671   for(i=0 ; i< sn->num_reg ; i++){
 672     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
 673   }
 674
 675   /* Get values of propositional symbols */
 676   unsigned int cursor = 0;
 677   xbt_propositional_symbol_t ps = NULL;
 678   int res;
 679   int_f_void_t f;
 680
 681   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 682     f = (int_f_void_t)ps->function;
 683     res = (*f)();
 684     xbt_dynar_push_as(pair->prop_ato, int, res);
 685   }
 686
 687   xbt_dynar_push(visited_pairs_hash, &pair);
 688
 689   MC_free_snapshot(sn);
 690
 691   MC_UNSET_RAW_MEM;
 692
 693   if(raw_mem_set)
 694     MC_SET_RAW_MEM;
 695   else
 696     MC_UNSET_RAW_MEM;
 697
 698 }
 699
 700 void set_pair_visited(xbt_state_t st, int sc){
 701
 702   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 703
 704   MC_SET_RAW_MEM;
 705
 706   mc_pair_visited_t pair = NULL;
 707   pair = xbt_new0(s_mc_pair_visited_t, 1);
 708   pair->automaton_state = st;
 709   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 710   pair->search_cycle = sc;
 711   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
 712   MC_take_snapshot_liveness(pair->system_state);
 713
 714
 715   /* Get values of propositional symbols */
 716   unsigned int cursor = 0;
 717   xbt_propositional_symbol_t ps = NULL;
 718   int res;
 719   int_f_void_t f;
 720
 721   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 722     f = (int_f_void_t)ps->function;
 723     res = (*f)();
 724     xbt_dynar_push_as(pair->prop_ato, int, res);
 725   }
 726
 727   xbt_dynar_push(visited_pairs, &pair);
 728
 729   MC_UNSET_RAW_MEM;
 730
 731   if(raw_mem_set)
 732     MC_SET_RAW_MEM;
 733   else
 734     MC_UNSET_RAW_MEM;
 735
 736 }
 737
 738 void MC_pair_delete(mc_pair_t pair){
 739   xbt_free(pair->graph_state->proc_status);
 740   xbt_free(pair->graph_state);
 741   xbt_free(pair);
 742 }
 743
 744
 745
 746 int MC_automaton_evaluate_label(xbt_exp_label_t l){
 747
 748   switch(l->type){
 749   case 0 : {
 750     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 751     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 752     return (left_res || right_res);
 753   }
 754   case 1 : {
 755     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 756     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 757     return (left_res && right_res);
 758   }
 759   case 2 : {
 760     int res = MC_automaton_evaluate_label(l->u.exp_not);
 761     return (!res);
 762   }
 763   case 3 : {
 764     unsigned int cursor = 0;
 765     xbt_propositional_symbol_t p = NULL;
 766     int_f_void_t f;
 767     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
 768       if(strcmp(p->pred, l->u.predicat) == 0){
 769         f = (int_f_void_t)p->function;
 770         return (*f)();
 771       }
 772     }
 773     return -1;
 774   }
 775   case 4 : {
 776     return 2;
 777   }
 778   default :
 779     return -1;
 780   }
 781 }
 782
 783
 784 /********************* Double-DFS stateless *******************/
 785
 786 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
 787   xbt_free(pair->graph_state->proc_status);
 788   xbt_free(pair->graph_state);
 789   xbt_free(pair);
 790 }
 791
 792 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
 793   mc_pair_stateless_t p = NULL;
 794   p = xbt_new0(s_mc_pair_stateless_t, 1);
 795   p->automaton_state = st;
 796   p->graph_state = sg;
 797   p->requests = r;
 798   mc_stats_pair->expanded_pairs++;
 799   return p;
 800 }
 801
 802 void MC_ddfs_init(void){
 803
 804   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 805
 806   XBT_INFO("**************************************************");
 807   XBT_INFO("Double-DFS init");
 808   XBT_INFO("**************************************************");
 809
 810   mc_pair_stateless_t mc_initial_pair = NULL;
 811   mc_state_t initial_graph_state = NULL;
 812   smx_process_t process;
 813
 814
 815   MC_wait_for_requests();
 816
 817   MC_SET_RAW_MEM;
 818
 819   initial_graph_state = MC_state_pair_new();
 820   xbt_swag_foreach(process, simix_global->process_list){
 821     if(MC_process_is_enabled(process)){
 822       MC_state_interleave_process(initial_graph_state, process);
 823     }
 824   }
 825
 826   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
 827   //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
 828   //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
 829   //visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
 830   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 831
 832   /* Save the initial state */
 833   initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
 834   MC_take_snapshot_liveness(initial_snapshot_liveness);
 835
 836   MC_UNSET_RAW_MEM;
 837
 838   unsigned int cursor = 0;
 839   xbt_state_t state;
 840
 841   xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
 842     if(state->type == -1){
 843
 844       MC_SET_RAW_MEM;
 845       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 846       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 847       MC_UNSET_RAW_MEM;
 848
 849       if(cursor != 0){
 850         MC_restore_snapshot(initial_snapshot_liveness);
 851         MC_UNSET_RAW_MEM;
 852       }
 853
 854       MC_ddfs(0);
 855
 856     }else{
 857       if(state->type == 2){
 858
 859         MC_SET_RAW_MEM;
 860         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 861         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 862         MC_UNSET_RAW_MEM;
 863
 864         set_pair_reached(state);
 865         //set_pair_reached_hash(state);
 866
 867         if(cursor != 0){
 868           MC_restore_snapshot(initial_snapshot_liveness);
 869           MC_UNSET_RAW_MEM;
 870         }
 871
 872         MC_ddfs(1);
 873
 874       }
 875     }
 876   }
 877
 878   if(raw_mem_set)
 879     MC_SET_RAW_MEM;
 880   else
 881     MC_UNSET_RAW_MEM;
 882
 883
 884 }
 885
 886
 887 void MC_ddfs(int search_cycle){
 888
 889   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 890
 891   smx_process_t process;
 892   mc_pair_stateless_t current_pair = NULL;
 893
 894   if(xbt_fifo_size(mc_stack_liveness) == 0)
 895     return;
 896
 897
 898   /* Get current pair */
 899   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 900
 901   /* Update current state in buchi automaton */
 902   _mc_property_automaton->current_state = current_pair->automaton_state;
 903
 904
 905   XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
 906   XBT_INFO("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));
 907
 908   mc_stats_pair->visited_pairs++;
 909
 910   //sleep(1);
 911
 912   int value;
 913   mc_state_t next_graph_state = NULL;
 914   smx_simcall_t req = NULL;
 915   char *req_str;
 916
 917   xbt_transition_t transition_succ;
 918   unsigned int cursor = 0;
 919   int res;
 920
 921   mc_pair_stateless_t next_pair = NULL;
 922   mc_pair_stateless_t pair_succ;
 923
 924   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
 925
 926     //set_pair_visited(current_pair->automaton_state, search_cycle);
 927     //set_pair_visited_hash(current_pair->automaton_state, search_cycle);
 928
 929     //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
 930     //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
 931
 932     if(current_pair->requests > 0){
 933
 934       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 935
 936         /* Debug information */
 937
 938         req_str = MC_request_to_string(req, value);
 939         XBT_INFO("Execute: %s", req_str);
 940         xbt_free(req_str);
 941
 942         MC_state_set_executed_request(current_pair->graph_state, req, value);
 943
 944         /* Answer the request */
 945         SIMIX_simcall_pre(req, value);
 946
 947         /* Wait for requests (schedules processes) */
 948         MC_wait_for_requests();
 949
 950
 951         MC_SET_RAW_MEM;
 952
 953         /* Create the new expanded graph_state */
 954         next_graph_state = MC_state_pair_new();
 955
 956         /* Get enabled process and insert it in the interleave set of the next graph_state */
 957         xbt_swag_foreach(process, simix_global->process_list){
 958           if(MC_process_is_enabled(process)){
 959             MC_state_interleave_process(next_graph_state, process);
 960           }
 961         }
 962
 963         xbt_dynar_reset(successors);
 964
 965         MC_UNSET_RAW_MEM;
 966
 967
 968         cursor= 0;
 969         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 970
 971           res = MC_automaton_evaluate_label(transition_succ->label);
 972
 973           if(res == 1){ // enabled transition in automaton
 974             MC_SET_RAW_MEM;
 975             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 976             xbt_dynar_push(successors, &next_pair);
 977             MC_UNSET_RAW_MEM;
 978           }
 979
 980         }
 981
 982         cursor = 0;
 983
 984         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 985
 986           res = MC_automaton_evaluate_label(transition_succ->label);
 987
 988           if(res == 2){ // true transition in automaton
 989             MC_SET_RAW_MEM;
 990             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 991             xbt_dynar_push(successors, &next_pair);
 992             MC_UNSET_RAW_MEM;
 993           }
 994
 995         }
 996
 997         cursor = 0;
 998
 999         xbt_dynar_foreach(successors, cursor, pair_succ){
1000
1001           if(search_cycle == 1){
1002
1003             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
1004
1005               if(reached(pair_succ->automaton_state)){
1006                 //if(reached_hash(pair_succ->automaton_state)){
1007
1008                 XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
1009
1010                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1011                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
1012                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1013                 XBT_INFO("Counter-example that violates formula :");
1014                 MC_show_stack_liveness(mc_stack_liveness);
1015                 MC_dump_stack_liveness(mc_stack_liveness);
1016                 MC_print_statistics_pairs(mc_stats_pair);
1017                 exit(0);
1018
1019               }else{
1020
1021                 XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
1022
1023                 set_pair_reached(pair_succ->automaton_state);
1024                 //set_pair_reached_hash(pair_succ->automaton_state);
1025
1026                 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1027                 //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1028
1029                 MC_SET_RAW_MEM;
1030                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1031                 MC_UNSET_RAW_MEM;
1032
1033                 MC_ddfs(search_cycle);
1034
1035               }
1036
1037             }else{
1038
1039               //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1040                 //if(!visited(pair_succ->automaton_state, search_cycle)){
1041
1042                 MC_SET_RAW_MEM;
1043                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1044                 MC_UNSET_RAW_MEM;
1045
1046                 MC_ddfs(search_cycle);
1047
1048                 /*}else{
1049
1050                 XBT_INFO("Next pair already visited ! ");
1051
1052                 }*/
1053
1054             }
1055
1056           }else{
1057
1058             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1059
1060               XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
1061
1062               set_pair_reached(pair_succ->automaton_state);
1063               //set_pair_reached_hash(pair_succ->automaton_state);
1064
1065               search_cycle = 1;
1066
1067               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1068               //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1069
1070             }
1071
1072             //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1073               //if(!visited(pair_succ->automaton_state, search_cycle)){
1074
1075               MC_SET_RAW_MEM;
1076               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1077               MC_UNSET_RAW_MEM;
1078
1079               MC_ddfs(search_cycle);
1080
1081               /*}else{
1082
1083               XBT_INFO("Next pair already visited ! ");
1084
1085               }*/
1086
1087           }
1088
1089
1090           /* Restore system before checking others successors */
1091           if(cursor != (xbt_dynar_length(successors) - 1))
1092             MC_replay_liveness(mc_stack_liveness, 1);
1093
1094
1095         }
1096
1097         if(MC_state_interleave_size(current_pair->graph_state) > 0){
1098           XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
1099           MC_replay_liveness(mc_stack_liveness, 0);
1100         }
1101       }
1102
1103
1104     }else{  /*No request to execute, search evolution in Büchi automaton */
1105
1106       MC_SET_RAW_MEM;
1107
1108       /* Create the new expanded graph_state */
1109       next_graph_state = MC_state_pair_new();
1110
1111       xbt_dynar_reset(successors);
1112
1113       MC_UNSET_RAW_MEM;
1114
1115
1116       cursor= 0;
1117       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1118
1119         res = MC_automaton_evaluate_label(transition_succ->label);
1120
1121         if(res == 1){ // enabled transition in automaton
1122           MC_SET_RAW_MEM;
1123           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
1124           xbt_dynar_push(successors, &next_pair);
1125           MC_UNSET_RAW_MEM;
1126         }
1127
1128       }
1129
1130       cursor = 0;
1131
1132       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
1133
1134         res = MC_automaton_evaluate_label(transition_succ->label);
1135
1136         if(res == 2){ // true transition in automaton
1137           MC_SET_RAW_MEM;
1138           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
1139           xbt_dynar_push(successors, &next_pair);
1140           MC_UNSET_RAW_MEM;
1141         }
1142
1143       }
1144
1145       cursor = 0;
1146
1147       xbt_dynar_foreach(successors, cursor, pair_succ){
1148
1149         if(search_cycle == 1){
1150
1151           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
1152
1153             if(reached(pair_succ->automaton_state)){
1154               //if(reached_hash(pair_succ->automaton_state)){
1155
1156               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
1157
1158               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1159               XBT_INFO("|             ACCEPTANCE CYCLE            |");
1160               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1161               XBT_INFO("Counter-example that violates formula :");
1162               MC_show_stack_liveness(mc_stack_liveness);
1163               MC_dump_stack_liveness(mc_stack_liveness);
1164               MC_print_statistics_pairs(mc_stats_pair);
1165               exit(0);
1166
1167             }else{
1168
1169               XBT_INFO("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
1170
1171               set_pair_reached(pair_succ->automaton_state);
1172               //set_pair_reached_hash(pair_succ->automaton_state);
1173
1174               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1175               //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1176
1177               MC_SET_RAW_MEM;
1178               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1179               MC_UNSET_RAW_MEM;
1180
1181               MC_ddfs(search_cycle);
1182
1183             }
1184
1185           }else{
1186
1187             //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1188               //if(!visited(pair_succ->automaton_state, search_cycle)){
1189
1190               MC_SET_RAW_MEM;
1191               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1192               MC_UNSET_RAW_MEM;
1193
1194               MC_ddfs(search_cycle);
1195
1196               /*}else{
1197
1198               XBT_INFO("Next pair already visited ! ");
1199
1200               }*/
1201           }
1202
1203
1204         }else{
1205
1206           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1207
1208             set_pair_reached(pair_succ->automaton_state);
1209             //set_pair_reached_hash(pair_succ->automaton_state);
1210
1211             search_cycle = 1;
1212
1213             XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1214             //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1215
1216           }
1217
1218           //if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1219             //if(!visited(pair_succ->automaton_state, search_cycle)){
1220
1221             MC_SET_RAW_MEM;
1222             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1223             MC_UNSET_RAW_MEM;
1224
1225             MC_ddfs(search_cycle);
1226
1227             /*}else{
1228
1229             XBT_INFO("Next pair already visited ! ");
1230
1231             }*/
1232
1233         }
1234
1235         /* Restore system before checking others successors */
1236         if(cursor != xbt_dynar_length(successors) - 1)
1237           MC_replay_liveness(mc_stack_liveness, 1);
1238
1239
1240       }
1241
1242     }
1243
1244   }else{
1245
1246     XBT_INFO("Max depth reached");
1247
1248   }
1249
1250   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
1251     XBT_INFO("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
1252   }else{
1253     XBT_INFO("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
1254   }
1255
1256
1257   MC_SET_RAW_MEM;
1258   xbt_fifo_shift(mc_stack_liveness);
1259   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
1260     xbt_dynar_pop(reached_pairs, NULL);
1261     //xbt_dynar_pop(reached_pairs_hash, NULL);
1262   }
1263   MC_UNSET_RAW_MEM;
1264
1265   if(raw_mem_set)
1266     MC_SET_RAW_MEM;
1267   else
1268     MC_UNSET_RAW_MEM;
1269
1270 }