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 f17c79f..300dace 100644 (file)
--- a/examples/smpi/mc/non_deterministic.tesh
+++ b/examples/smpi/mc/non_deterministic.tesh
@@ -1,13 +1,12 @@
 #! ./tesh
 
 ! timeout 60
 #! ./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 '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'
 > [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 8531c03..8831df2 100644 (file)
--- a/examples/smpi/mc/send_deterministic.tesh
+++ b/examples/smpi/mc/send_deterministic.tesh
@@ -1,13 +1,12 @@
 #! ./tesh
 
 ! timeout 60
 #! ./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 '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'
 > [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 f9286fe..df76363 100644 (file)
--- 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;
 
 
   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)) {
     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);
 
     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);
       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++;
 
 
       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) {
         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);
             char *key = bprintf("%lu", process->pid);
             if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) {
               char *data = bprintf("%d", count);