model-checker : conflit

[simgrid.git] / src / mc / mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index db0a1a3..668bea0 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -19,8 +19,6 @@
 #include "xbt/automaton.h"
 #include "xbt/dict.h"
 
-static void MC_post_process_types(mc_object_info_t info);
-
 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
                                 "Logging specific to MC (global)");
@@ -35,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;
 
@@ -93,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;
@@ -166,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);
   }
 }
@@ -178,11 +184,7 @@ void dw_variable_free_voidp(void *t){
 // object_info
 
 mc_object_info_t MC_new_object_info(void) {
-  mc_object_info_t res = xbt_new(s_mc_object_info_t, 1);
-  res->file_name = NULL;
-  res->start_text = NULL;
-  res->start_data = NULL;
-  res->start_bss = NULL;
+  mc_object_info_t res = xbt_new0(s_mc_object_info_t, 1);
   res->local_variables = xbt_dict_new_homogeneous(NULL);
   res->global_variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
   res->types = xbt_dict_new_homogeneous(NULL);
@@ -391,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;
@@ -404,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;
@@ -416,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 ?
@@ -439,26 +441,6 @@ void MC_dwarf_register_variable(mc_object_info_t info, dw_frame_t frame, dw_vari
     MC_dwarf_register_non_global_variable(info, frame, variable);
 }
 
-static void MC_post_process_array_size(mc_object_info_t info, dw_type_t type) {
-  xbt_assert(type->dw_type_id, "No base type for array <%p>%s", type->id, type->name);
-  dw_type_t subtype = xbt_dict_get_or_null(info->types, type->dw_type_id);
-  xbt_assert(subtype, "Unkown base type <%s> for array <%p>%s", type->dw_type_id, type->id, type->name);
-  if(subtype->type==DW_TAG_array_type && type->byte_size==0) {
-         MC_post_process_array_size(info, subtype);
-  }
-  type->byte_size = type->element_count*subtype->byte_size;
-}
-
-static void MC_post_process_types(mc_object_info_t info) {
-  xbt_dict_cursor_t cursor;
-  char *origin;
-  dw_type_t type;
-  xbt_dict_foreach(info->types, cursor, origin, type){
-    if(type->type==DW_TAG_array_type && type->byte_size==0)
-      MC_post_process_array_size(info, type);
-  }
-}
-
 /*******************************  Ignore mechanism *******************************/
 /*********************************************************************************/
 
@@ -1262,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;
   
 
@@ -1293,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();
 
@@ -1588,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;
 }