model-checker : new configuration flag for the detection of determinism in communicat...

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 0cf9f2d..28f184b 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -29,6 +29,7 @@ extern int _sg_mc_timeout;
 extern int _sg_mc_max_depth;
 extern int _sg_mc_visited;
 extern char* _sg_mc_dot_output_file;
+extern int _sg_mc_comms_determinism;
 
 extern xbt_dynar_t mc_heap_comparison_ignore;
 extern xbt_dynar_t stacks_areas;
@@ -43,6 +44,7 @@ void _mc_cfg_cb_timeout(const char *name, int pos);
 void _mc_cfg_cb_max_depth(const char *name, int pos);
 void _mc_cfg_cb_visited(const char *name, int pos);
 void _mc_cfg_cb_dot_output(const char *name, int pos);
+void _mc_cfg_cb_comms_determinism(const char *name, int pos);
 
 XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void);
 

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index f1e7de3..a45cc5f 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -423,15 +423,15 @@ void MC_dpor(void)
   char *req_str = NULL;
   int value;
   smx_simcall_t req = NULL, prev_req = NULL;
-  mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
+  mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restored_state=NULL;
   smx_process_t process = NULL;
   xbt_fifo_item_t item = NULL;
   mc_state_t state_test = NULL;
   int pos;
   int visited_state = -1;
   int enabled = 0;
-  int comm_pattern = 0;
   int interleave_size = 0;
+  int comm_pattern = 0;
 
   while (xbt_fifo_size(mc_stack_safety) > 0) {
 
@@ -474,25 +474,28 @@ void MC_dpor(void)
       xbt_dict_remove(first_enabled_state, key); 
       xbt_free(key);
       MC_UNSET_RAW_MEM;
-
-      if(req->call == SIMCALL_COMM_ISEND)
-        comm_pattern = 1;
-      else if(req->call == SIMCALL_COMM_IRECV)
-        comm_pattern = 2;
+      
+      if(_sg_mc_comms_determinism){
+        if(req->call == SIMCALL_COMM_ISEND)
+          comm_pattern = 1;
+        else if(req->call == SIMCALL_COMM_IRECV)
+          comm_pattern = 2;
+      }
 
       /* Answer the request */
       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 
-      MC_SET_RAW_MEM;
-      if(comm_pattern != 0){
-        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);
+      if(_sg_mc_comms_determinism){
+        MC_SET_RAW_MEM;
+        if(comm_pattern != 0){
+          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);
+        }
+        MC_UNSET_RAW_MEM; 
+        comm_pattern = 0;
       }
-      MC_UNSET_RAW_MEM;
-
-      comm_pattern = 0;
 
       /* Wait for requests (schedules processes) */
       MC_wait_for_requests();
@@ -586,22 +589,24 @@ void MC_dpor(void)
       }
 
       MC_SET_RAW_MEM;
-      if(!initial_state_safety->initial_communications_pattern_done){
-        //print_communications_pattern(initial_communications_pattern);
-      }else{
-        if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
-          //print_communications_pattern(communications_pattern);
-          deterministic_pattern(initial_communications_pattern, communications_pattern);
+
+      if(_sg_mc_comms_determinism){
+        if(!initial_state_safety->initial_communications_pattern_done){
+          //print_communications_pattern(initial_communications_pattern);
+        }else{
+          if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
+            //print_communications_pattern(communications_pattern);
+            deterministic_pattern(initial_communications_pattern, communications_pattern);
+          }
         }
+        initial_state_safety->initial_communications_pattern_done = 1;
       }
-      initial_state_safety->initial_communications_pattern_done = 1;
-      MC_UNSET_RAW_MEM;
 
       /* Trash the current state, no longer needed */
-      MC_SET_RAW_MEM;
       xbt_fifo_shift(mc_stack_safety);
       MC_state_delete(state);
       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
+
       MC_UNSET_RAW_MEM;        
       
       /* Check for deadlocks */
@@ -667,15 +672,15 @@ void MC_dpor(void)
               pos = xbt_fifo_size(mc_stack_safety);
               item = xbt_fifo_get_first_item(mc_stack_safety);
               while(pos>0){
-                restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
-                if(restore_state->system_state != NULL){
+                restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
+                if(restored_state->system_state != NULL){
                   break;
                 }else{
                   item = xbt_fifo_get_next_item(item);
                   pos--;
                 }
               }
-              MC_restore_snapshot(restore_state->system_state);
+              MC_restore_snapshot(restored_state->system_state);
               xbt_fifo_unshift(mc_stack_safety, state);
               MC_UNSET_RAW_MEM;
               MC_replay(mc_stack_safety, pos);
@@ -689,9 +694,11 @@ void MC_dpor(void)
           break;
         } else {
           req = MC_state_get_internal_request(state);
-          if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
-            if(!xbt_dynar_is_empty(communications_pattern))
-              xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
+          if(_sg_mc_comms_determinism){
+            if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
+              if(!xbt_dynar_is_empty(communications_pattern))
+                xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
+            }
           }
           XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1); 
           MC_state_delete(state);

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 930098f..a72abfe 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -35,6 +35,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 +94,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;
@@ -1262,7 +1270,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 +1302,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,7 +1600,7 @@ void MC_print_statistics(mc_stats_t stats)
     fprintf(dot_output, "}\n");
     fclose(dot_output);
   }
-  if(initial_state_safety != NULL){
+  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");
   }

diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c
index b812c87..0d904ae 100644 (file)
--- a/src/simgrid/sg_config.c
+++ b/src/simgrid/sg_config.c
@@ -574,6 +574,12 @@ void sg_config_init(int *argc, char **argv)
                      xbt_cfgelm_string, 0, 1, _mc_cfg_cb_property, NULL);
     xbt_cfg_setdefault_string(_sg_cfg_set, "model-check/property", "");
 
+    /* do determinism model-checking */
+        xbt_cfg_register(&_sg_cfg_set, "model-check/communications_determinism",
+                     "Enable/disable the detection of determinism in the communications schemes",
+                     xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_comms_determinism, NULL);
+    xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/communications_determinism", "no");
+
     /* Specify the kind of model-checking reduction */
     xbt_cfg_register(&_sg_cfg_set, "model-check/reduction",
                      "Specify the kind of exploration reduction (either none or DPOR)",