From: Marion Guthmuller <marion.guthmuller@inria.fr>
Date: Wed, 4 Jun 2014 08:35:10 +0000 (+0200)
Subject: model-checker : fix backtracking with comm determinism verification
X-Git-Tag: v3_12~956^2~11
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/5d58398955c920f5cb80a92e48f52a09b95bb7d6?hp=606fd6074429a2b25a185ba92dce29759ab41255

model-checker : fix backtracking with comm determinism verification
---

diff --git a/examples/smpi/mc/non_deterministic.tesh b/examples/smpi/mc/non_deterministic.tesh
index f17c79f5e2..300dace705 100644
--- a/examples/smpi/mc/non_deterministic.tesh
+++ b/examples/smpi/mc/non_deterministic.tesh
@@ -1,13 +1,12 @@
 #! ./tesh
 
 ! timeout 60
-$ ../../../smpi_script/bin/smpirun -hostfile ${srcdir:=.}/hostfile_non_deterministic  -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check:1 --cfg=model-check/reduction:none --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./non_deterministic
+$ ../../../smpi_script/bin/smpirun -hostfile ${srcdir:=.}/hostfile_non_deterministic  -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check:1 --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./non_deterministic
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'maxmin/precision' to '1e-3'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'surf/precision' to '1e-9'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'network/model' to 'SMPI'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'network/TCP_gamma' to '4194304'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check' to '1'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'none'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/communications_determinism' to '1'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/send_is_detached_thres' to '0'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/running_power' to '1e9'
diff --git a/examples/smpi/mc/send_deterministic.tesh b/examples/smpi/mc/send_deterministic.tesh
index 8531c03ab6..8831df27fb 100644
--- a/examples/smpi/mc/send_deterministic.tesh
+++ b/examples/smpi/mc/send_deterministic.tesh
@@ -1,13 +1,12 @@
 #! ./tesh
 
 ! timeout 60
-$ ../../../smpi_script/bin/smpirun -hostfile ${srcdir:=.}/hostfile_send_deterministic  -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check:1 --cfg=model-check/reduction:none --cfg=model-check/send_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./send_deterministic
+$ ../../../smpi_script/bin/smpirun -hostfile ${srcdir:=.}/hostfile_send_deterministic  -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check:1 --cfg=model-check/send_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./send_deterministic
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'maxmin/precision' to '1e-3'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'surf/precision' to '1e-9'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'network/model' to 'SMPI'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'network/TCP_gamma' to '4194304'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check' to '1'
-> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'none'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/send_determinism' to '1'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/send_is_detached_thres' to '0'
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/running_power' to '1e9'
diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index f9286fe511..df7636397e 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -508,7 +508,7 @@ void MC_replay(xbt_fifo_t stack, int start)
 
   MC_SET_MC_HEAP;
 
-  if (mc_reduce_kind == e_mc_reduce_dpor) {
+  if ((mc_reduce_kind == e_mc_reduce_dpor) && !_sg_mc_comms_determinism && !_sg_mc_send_determinism) {
     xbt_dict_reset(first_enabled_state);
     xbt_swag_foreach(process, simix_global->process_list) {
       if (MC_process_is_enabled(process)) {
@@ -536,7 +536,7 @@ void MC_replay(xbt_fifo_t stack, int start)
     state = (mc_state_t) xbt_fifo_get_item_content(item);
     saved_req = MC_state_get_executed_request(state, &value);
 
-    if (mc_reduce_kind == e_mc_reduce_dpor) {
+    if ((mc_reduce_kind == e_mc_reduce_dpor) && !_sg_mc_comms_determinism && !_sg_mc_send_determinism) {
       MC_SET_MC_HEAP;
       char *key = bprintf("%lu", saved_req->issuer->pid);
       xbt_dict_remove(first_enabled_state, key);
@@ -596,12 +596,11 @@ void MC_replay(xbt_fifo_t stack, int start)
 
       count++;
 
-      if (mc_reduce_kind == e_mc_reduce_dpor) {
+      if ((mc_reduce_kind == e_mc_reduce_dpor) && !_sg_mc_comms_determinism && !_sg_mc_send_determinism) {
         MC_SET_MC_HEAP;
         /* Insert in dict all enabled processes */
         xbt_swag_foreach(process, simix_global->process_list) {
-          if (MC_process_is_enabled(process)
-              /*&& !MC_state_process_is_done(state, process) */ ) {
+          if (MC_process_is_enabled(process) ) {
             char *key = bprintf("%lu", process->pid);
             if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) {
               char *data = bprintf("%d", count);