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 b3cc8ba..668bea0 100644 (file)
--- 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_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;
 
 
 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);
 }
 
   _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;
 /* 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)
     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);
   }
 }
     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 */
       end = cursor - 1;
     }else{
       if(address){ /* global variable */

-        if(var_test->address.address == address)
+        if(var_test->address == address)

           return -1;
           return -1;

-        if(var_test->address.address > address)
+        if(var_test->address > address)

           end = cursor - 1;
         else
           start = cursor + 1;
           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(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;
       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) {
 }
 
 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 ?
   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_free(key);
     }
   }

-  xbt_dynar_reset(communications_pattern);
+  if(_sg_mc_comms_determinism)
+    xbt_dynar_reset(communications_pattern);

   MC_UNSET_RAW_MEM;
   
 
   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;
       comm_pattern = 2;

-    
+    }
+

     SIMIX_simcall_pre(req, value);
 
     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();
 
     
     MC_wait_for_requests();
 


@@ -1562,9 +1574,9 @@ void MC_print_statistics(mc_stats_t stats)
     fprintf(dot_output, "}\n");
     fclose(dot_output);
   }
     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;
 }
   }
   MC_UNSET_RAW_MEM;
 }