model-checker : use separate configuration flags for comm determinism and send determ...

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 88bfb65..bbcdc2f 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -31,6 +31,7 @@ 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 int _sg_mc_send_determinism;
 
 extern xbt_dynar_t mc_heap_comparison_ignore;
 extern xbt_dynar_t stacks_areas;
@@ -47,6 +48,7 @@ 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);
+void _mc_cfg_cb_send_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 d0b158d..1fa1f26 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -92,7 +92,6 @@ static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t patte
     recv_index = 0;
     current_process++;
   }
-  // XBT_DEBUG("Communication-deterministic : %d, Send-deterministic : %d", initial_state_safety->comm_deterministic, initial_state_safety->send_deterministic);
 }
 
 static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){
@@ -517,7 +516,7 @@ void MC_dpor(void)
       xbt_free(key);
       MC_UNSET_RAW_MEM;
       
-      if(_sg_mc_comms_determinism){
+      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)
@@ -527,7 +526,7 @@ void MC_dpor(void)
       /* Answer the request */
       SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
 
-      if(_sg_mc_comms_determinism){
+      if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
         MC_SET_RAW_MEM;
         if(comm_pattern != 0){
           if(!initial_state_safety->initial_communications_pattern_done)
@@ -632,16 +631,36 @@ void MC_dpor(void)
 
       MC_SET_RAW_MEM;
 
-      if(_sg_mc_comms_determinism){
-        if(!initial_state_safety->initial_communications_pattern_done){
-          //print_communications_pattern(initial_communications_pattern);
-        }else{
+      if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
+        if(initial_state_safety->initial_communications_pattern_done){
           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(initial_state_safety->comm_deterministic == 0 && _sg_mc_comms_determinism){
+              XBT_INFO("****************************************************");
+              XBT_INFO("***** Non-deterministic communications pattern *****");
+              XBT_INFO("****************************************************");
+              XBT_INFO("Initial communications pattern:");
+              print_communications_pattern(initial_communications_pattern);
+              XBT_INFO("Communications pattern counter-example:");
+              print_communications_pattern(communications_pattern);
+              MC_print_statistics(mc_stats);
+              return;
+            }else if(initial_state_safety->send_deterministic == 0 && _sg_mc_send_determinism){
+              XBT_INFO("****************************************************");
+              XBT_INFO("***** Non-send-deterministic communications pattern *****");
+              XBT_INFO("****************************************************");
+              XBT_INFO("Initial communications pattern:");
+              print_communications_pattern(initial_communications_pattern);
+              XBT_INFO("Communications pattern counter-example:");
+              print_communications_pattern(communications_pattern);
+              MC_print_statistics(mc_stats);
+              return;
+            }
           }
+        }else{
+          initial_state_safety->initial_communications_pattern_done = 1;
         }
-        initial_state_safety->initial_communications_pattern_done = 1;
       }
 
       /* Trash the current state, no longer needed */

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index f92085f..7528e5b 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -35,6 +35,7 @@ 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 _sg_mc_send_determinism=0;
 
 int user_max_depth_reached = 0;
 
@@ -107,6 +108,13 @@ void _mc_cfg_cb_comms_determinism(const char *name, int pos) {
   _sg_mc_comms_determinism= xbt_cfg_get_boolean(_sg_cfg_set, name);
 }
 
+void _mc_cfg_cb_send_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 send-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_send_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;
@@ -1247,7 +1255,7 @@ void MC_replay(xbt_fifo_t stack, int start)
       xbt_free(key);
     }
   }
-  if(_sg_mc_comms_determinism)
+  if(_sg_mc_comms_determinism || _sg_mc_send_determinism)
     xbt_dynar_reset(communications_pattern);
   MC_UNSET_RAW_MEM;
   
@@ -1279,7 +1287,7 @@ void MC_replay(xbt_fifo_t stack, int start)
       }
     }
 
-    if(_sg_mc_comms_determinism){
+    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)
@@ -1288,7 +1296,7 @@ void MC_replay(xbt_fifo_t stack, int start)
 
     SIMIX_simcall_pre(req, value);
 
-    if(_sg_mc_comms_determinism){
+    if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
       MC_SET_RAW_MEM;
       if(comm_pattern != 0){
         get_comm_pattern(communications_pattern, req, comm_pattern);
@@ -1577,9 +1585,11 @@ void MC_print_statistics(mc_stats_t stats)
     fprintf(dot_output, "}\n");
     fclose(dot_output);
   }
-  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");
+  if(initial_state_safety != NULL){
+    if(_sg_mc_comms_determinism)
+      XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes");
+    if (_sg_mc_send_determinism)
+      XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes");
   }
   MC_UNSET_RAW_MEM;
 }

diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c
index 4886b39..dafa406 100644 (file)
--- a/src/simgrid/sg_config.c
+++ b/src/simgrid/sg_config.c
@@ -574,12 +574,18 @@ 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",
+    /* do communications 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");
 
+    /* do send determinism model-checking */
+    xbt_cfg_register(&_sg_cfg_set, "model-check/send_determinism",
+                     "Enable/disable the detection of send-determinism in the communications schemes",
+                     xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_send_determinism, NULL);
+    xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/send_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)",