X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/e3531fcad45575830870605f5fd3a80b6b6f0ec7..8fc11b8e2c3f486babc8be5494ddd53ffcc659f4:/src/mc/mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index b3cc8baac2..668bea076b 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -33,6 +33,7 @@ int _sg_mc_timeout=0;
 int _sg_mc_max_depth=1000;
 int _sg_mc_visited=0;
 char *_sg_mc_dot_output_file = NULL;
+int _sg_mc_comms_determinism=0;
 
 int user_max_depth_reached = 0;
 
@@ -91,6 +92,13 @@ void _mc_cfg_cb_dot_output(const char *name, int pos) {
   _sg_mc_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name);
 }
 
+void _mc_cfg_cb_comms_determinism(const char *name, int pos) {
+  if (_sg_cfg_init_status && !_sg_do_model_check) {
+    xbt_die("You are specifying a value to enable/disable the detection of determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+  }
+  _sg_mc_comms_determinism= xbt_cfg_get_boolean(_sg_cfg_set, name);
+}
+
 /* MC global data structures */
 mc_state_t mc_current_state = NULL;
 char mc_replay_mode = FALSE;
@@ -164,7 +172,7 @@ void dw_variable_free(dw_variable_t v){
     xbt_free(v->name);
     xbt_free(v->type_origin);
     if(!v->global)
-      dw_location_free(v->address.location);
+      dw_location_free(v->location);
     xbt_free(v);
   }
 }
@@ -385,9 +393,9 @@ static int MC_dwarf_get_variable_index(xbt_dynar_t variables, char* var, void *a
       end = cursor - 1;
     }else{
       if(address){ /* global variable */
-        if(var_test->address.address == address)
+        if(var_test->address == address)
           return -1;
-        if(var_test->address.address > address)
+        if(var_test->address > address)
           end = cursor - 1;
         else
           start = cursor + 1;
@@ -398,7 +406,7 @@ static int MC_dwarf_get_variable_index(xbt_dynar_t variables, char* var, void *a
   }
 
   if(strcmp(var_test->name, var) == 0){
-    if(address && var_test->address.address < address)
+    if(address && var_test->address < address)
       return cursor+1;
     else
       return cursor;
@@ -410,7 +418,7 @@ static int MC_dwarf_get_variable_index(xbt_dynar_t variables, char* var, void *a
 }
 
 void MC_dwarf_register_global_variable(mc_object_info_t info, dw_variable_t variable) {
-  int index = MC_dwarf_get_variable_index(info->global_variables, variable->name, variable->address.address);
+  int index = MC_dwarf_get_variable_index(info->global_variables, variable->name, variable->address);
   if (index != -1)
     xbt_dynar_insert_at(info->global_variables, index, &variable);
   // TODO, else ?
@@ -1236,7 +1244,8 @@ void MC_replay(xbt_fifo_t stack, int start)
       xbt_free(key);
     }
   }
-  xbt_dynar_reset(communications_pattern);
+  if(_sg_mc_comms_determinism)
+    xbt_dynar_reset(communications_pattern);
   MC_UNSET_RAW_MEM;
   
 
@@ -1267,20 +1276,23 @@ void MC_replay(xbt_fifo_t stack, int start)
       }
     }
 
-    if(req->call == SIMCALL_COMM_ISEND)
-      comm_pattern = 1;
-    else if(req->call == SIMCALL_COMM_IRECV)
+    if(_sg_mc_comms_determinism){
+      if(req->call == SIMCALL_COMM_ISEND)
+        comm_pattern = 1;
+      else if(req->call == SIMCALL_COMM_IRECV)
       comm_pattern = 2;
-    
+    }
+
     SIMIX_simcall_pre(req, value);
 
-    MC_SET_RAW_MEM;
-    if(comm_pattern != 0){
-      get_comm_pattern(communications_pattern, req, comm_pattern);
+    if(_sg_mc_comms_determinism){
+      MC_SET_RAW_MEM;
+      if(comm_pattern != 0){
+        get_comm_pattern(communications_pattern, req, comm_pattern);
+      }
+      MC_UNSET_RAW_MEM;
+      comm_pattern = 0;
     }
-    MC_UNSET_RAW_MEM;
-
-    comm_pattern = 0;
     
     MC_wait_for_requests();
 
@@ -1562,9 +1574,9 @@ void MC_print_statistics(mc_stats_t stats)
     fprintf(dot_output, "}\n");
     fclose(dot_output);
   }
-  if(initial_state_safety != NULL){
-    // XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes");
-    // XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes");
+  if(initial_state_safety != NULL && _sg_mc_comms_determinism){
+    XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes");
+    XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes");
   }
   MC_UNSET_RAW_MEM;
 }