Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'mc_without_ksm' into mc
authorGabriel Corona <gabriel.corona@loria.fr>
Fri, 16 May 2014 13:56:26 +0000 (15:56 +0200)
committerGabriel Corona <gabriel.corona@loria.fr>
Fri, 16 May 2014 13:56:26 +0000 (15:56 +0200)
Conflicts:
src/mc/mc_dpor.c
src/mc/mc_global.c
src/mc/mc_memory.c

1  2 
src/mc/mc_dpor.c
src/mc/mc_global.c
src/mc/mc_memory.c
src/mc/mc_private.h
src/xbt/mmalloc/mmprivate.h

@@@ -544,9 -545,10 +545,10 @@@ void MC_dpor(void
          char *key = bprintf("%lu", req->issuer->pid);
          xbt_dict_remove(first_enabled_state, key); 
          xbt_free(key);
 -        MC_UNSET_RAW_MEM;
 +        MC_SET_STD_HEAP;
        }
  
+       /* TODO : handle test and testany simcalls */
        if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
          if(req->call == SIMCALL_COMM_ISEND)
            comm_pattern = 1;
        SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
  
        if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
 -        MC_SET_RAW_MEM;
 +        MC_SET_MC_HEAP;
-         if(comm_pattern != 0){
+         if(comm_pattern == 1 || comm_pattern == 2){
            if(!initial_state_safety->initial_communications_pattern_done)
              get_comm_pattern(initial_communications_pattern, req, comm_pattern);
            else
              get_comm_pattern(communications_pattern, req, comm_pattern);
+         }else if(comm_pattern == 3){
+           current_comm = simcall_comm_wait__get__comm(req);
+           if(current_comm->comm.refcount == 1){ /* First wait only must be considered */
+             if(!initial_state_safety->initial_communications_pattern_done)
+               complete_comm_pattern(initial_communications_pattern, current_comm);
+             else
+               complete_comm_pattern(communications_pattern, current_comm);
+           }
+         }else if(comm_pattern == 4){
+           current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t);
+           if(current_comm->comm.refcount == 1){ /* First wait only must be considered */
+             if(!initial_state_safety->initial_communications_pattern_done)
+               complete_comm_pattern(initial_communications_pattern, current_comm);
+             else
+               complete_comm_pattern(communications_pattern, current_comm);
+           }
          }
 -        MC_UNSET_RAW_MEM; 
 +        MC_SET_STD_HEAP;
          comm_pattern = 0;
        }
  
@@@ -1163,44 -1164,60 +1164,60 @@@ void MC_replay(xbt_fifo_t stack, int st
          XBT_DEBUG("Replay: %s (%p)", req_str, state);
          xbt_free(req_str);
        }
-     }
  
-     if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
-       if(req->call == SIMCALL_COMM_ISEND)
-         comm_pattern = 1;
-       else if(req->call == SIMCALL_COMM_IRECV)
-         comm_pattern = 2;
-     }
+       /* TODO : handle test and testany simcalls */
+       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
+         if(req->call == SIMCALL_COMM_ISEND)
+           comm_pattern = 1;
+         else if(req->call == SIMCALL_COMM_IRECV)
+           comm_pattern = 2;
+         else if(req->call == SIMCALL_COMM_WAIT)
+           comm_pattern = 3;
+         else if(req->call == SIMCALL_COMM_WAITANY)
+           comm_pattern = 4;
+       }
  
-     SIMIX_simcall_pre(req, value);
+       SIMIX_simcall_pre(req, value);
  
-     if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
-       MC_SET_MC_HEAP;
-       if(comm_pattern != 0){
-         get_comm_pattern(communications_pattern, req, comm_pattern);
+       if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
 -        MC_SET_RAW_MEM;
++        MC_SET_MC_HEAP;
+         if(comm_pattern == 1 || comm_pattern == 2){
+           get_comm_pattern(communications_pattern, req, comm_pattern);
+         }else if (comm_pattern == 3/* || comm_pattern == 4*/){
+           current_comm = simcall_comm_wait__get__comm(req);
+           if(current_comm->comm.refcount == 1){ /* First wait only must be considered */
+             complete_comm_pattern(communications_pattern, current_comm);
+           }
+         }else if (comm_pattern == 4/* || comm_pattern == 4*/){
+           current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t);
+           if(current_comm->comm.refcount == 1){ /* First wait only must be considered */
+             complete_comm_pattern(communications_pattern, current_comm);
+           }
+         }
 -        MC_UNSET_RAW_MEM;
++        MC_SET_STD_HEAP;
+         comm_pattern = 0;
        }
-       MC_SET_STD_HEAP;
-       comm_pattern = 0;
-     }
      
-     MC_wait_for_requests();
-     count++;
-     if(mc_reduce_kind ==  e_mc_reduce_dpor){
-       MC_SET_MC_HEAP;
-       /* Insert in dict all enabled processes */
-       xbt_swag_foreach(process, simix_global->process_list){
-         if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
-           char *key = bprintf("%lu", process->pid);
-           if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
-             char *data = bprintf("%d", count);
-             xbt_dict_set(first_enabled_state, key, data, NULL);
+     
+       MC_wait_for_requests();
+       count++;
+       if(mc_reduce_kind ==  e_mc_reduce_dpor){
 -        MC_SET_RAW_MEM;
++        MC_SET_MC_HEAP;
+         /* Insert in dict all enabled processes */
+         xbt_swag_foreach(process, simix_global->process_list){
+           if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
+             char *key = bprintf("%lu", process->pid);
+             if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
+               char *data = bprintf("%d", count);
+               xbt_dict_set(first_enabled_state, key, data, NULL);
+             }
+             xbt_free(key);
            }
-           xbt_free(key);
          }
 -        MC_UNSET_RAW_MEM;
++        MC_SET_STD_HEAP;
        }
-       MC_SET_STD_HEAP;
      }
           
      /* Update statistics */
@@@ -27,11 -27,11 +27,11 @@@ void MC_memory_init(
  
  #if defined HAVE_GNU_LD && !defined MMALLOC_WANT_OVERRIDE_LEGACY 
    /* use the system malloc for the model-checker data */
 -  raw_heap = NULL;
 +  mc_heap = NULL;
  #else
    /* Create the second region a page after the first one ends + safety gap */
-   mc_heap = xbt_mheap_new(-1, (char*)(std_heap) + STD_HEAP_SIZE + xbt_pagesize);
 -  raw_heap = xbt_mheap_new_options(-1, (char*)(std_heap) + STD_HEAP_SIZE + xbt_pagesize, 0);
 -  xbt_assert(raw_heap != NULL);
++  mc_heap = xbt_mheap_new_options(-1, (char*)(std_heap) + STD_HEAP_SIZE + xbt_pagesize, 0);
 +  xbt_assert(mc_heap != NULL);
  #endif
  }
  
Simple merge
Simple merge