src/mc/mc_liveness.c

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