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