model-checker : conflit

diff --git a/include/smpi/mpi.h b/include/smpi/mpi.h
index d840c9a..e8aa3ea 100644 (file)
--- a/include/smpi/mpi.h
+++ b/include/smpi/mpi.h
@@ -16,5 +16,11 @@
 #include <xbt/sysdep.h>
 #include <xbt/log.h>
 #include <xbt/asserts.h>
+#include <simgrid/modelchecker.h>
+
+#ifdef HAVE_MC
+#undef assert
+#define assert(x) MC_assert(x)
+#endif
 
 #endif

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 507b6df..a3e2949 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,24 +589,24 @@ void MC_dpor(void)
       }
 
       MC_SET_RAW_MEM;
-      if(0) {
-      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 */
@@ -669,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);
@@ -691,10 +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){
-            // fprintf(stderr, "Remove state with isend or irecv\n");
-            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 e0a8bdd..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_comms_determinism=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);
 }
 
+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;
@@ -1236,7 +1244,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;
   
 
@@ -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;
-    
+    }
+
     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();
 
@@ -1562,9 +1574,9 @@ void MC_print_statistics(mc_stats_t stats)
     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;
 }

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index ea59370..2ff658d 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -264,7 +264,7 @@ static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_s
                 if(dot_output == NULL)
                   XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
                 else
-                  XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_pair->num, pair_test->num, pair->other_num);
+                  XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_pair->num, pair_test->num, new_pair->other_num);
                 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
                 xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
                 pair_test->visited_removed = 1;

diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index 5b7ce40..1a3d2aa 100644 (file)
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -17,7 +17,11 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) {
     return TRUE;
 
   if (r1->issuer == r2->issuer)
-      return FALSE;
+    return FALSE;
+
+  /* Wait with timeout transitions are not considered by the independance theorem, thus we consider them as dependant with all other transitions */
+  if((r1->call == SIMCALL_COMM_WAIT && simcall_comm_wait__get__timeout(r1) > 0) || (r2->call == SIMCALL_COMM_WAIT && simcall_comm_wait__get__timeout(r2) > 0))
+    return TRUE;
 
   if(r1->call == SIMCALL_COMM_ISEND && r2->call == SIMCALL_COMM_IRECV)
     return FALSE;
@@ -335,6 +339,8 @@ int MC_request_is_enabled(smx_simcall_t req)
       }
     }else{
       act = simcall_comm_wait__get__comm(req);
+      if(act->comm.detached && act->comm.src_proc == NULL && act->comm.type == SIMIX_COMM_READY)
+        return (act->comm.dst_proc != NULL);
       return (act->comm.src_proc && act->comm.dst_proc);
     }
     break;

diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index f0c240d..7036c25 100644 (file)
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -143,6 +143,7 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
   smx_process_t process = NULL;
   mc_procstate_t procstate = NULL;
   unsigned int start_count;
+  smx_action_t act = NULL;
 
   xbt_swag_foreach(process, simix_global->process_list){
     procstate = &state->proc_status[process->pid];
@@ -186,11 +187,14 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
             break;
 
           case SIMCALL_COMM_WAIT:
-            if(simcall_comm_wait__get__comm(&process->simcall)->comm.src_proc
-               && simcall_comm_wait__get__comm(&process->simcall)->comm.dst_proc){
+            act = simcall_comm_wait__get__comm(&process->simcall);
+            if(act->comm.src_proc && act->comm.dst_proc){
               *value = 0;
             }else{
-              *value = -1;
+              if(act->comm.src_proc == NULL && act->comm.type == SIMIX_COMM_READY && act->comm.detached == 1)
+                *value = 0;
+              else
+                *value = -1;
             }
             procstate->state = MC_DONE;
             return &process->simcall;

diff --git a/src/simgrid/sg_config.c b/src/simgrid/sg_config.c
index b812c87..7a1ceb4 100644 (file)
--- a/src/simgrid/sg_config.c
+++ b/src/simgrid/sg_config.c
@@ -564,7 +564,7 @@ void sg_config_init(int *argc, char **argv)
     /* do stateful model-checking */
     xbt_cfg_register(&_sg_cfg_set, "model-check/checkpoint",
                      "Specify the amount of steps between checkpoints during stateful model-checking (default: 0 => stateless verification). "
-                     "If value=on, one checkpoint is saved for each step => faster verification, but huge memory consumption; higher values are good compromises between speed and memory consumption.",
+                     "If value=1, one checkpoint is saved for each step => faster verification, but huge memory consumption; higher values are good compromises between speed and memory consumption.",
                      xbt_cfgelm_int, 0, 1, _mc_cfg_cb_checkpoint, NULL);
     xbt_cfg_setdefault_int(_sg_cfg_set, "model-check/checkpoint", 0);
 
@@ -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)",

diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c
index 7f9689a..1ca73e5 100644 (file)
--- a/src/simix/smx_network.c
+++ b/src/simix/smx_network.c
@@ -445,7 +445,7 @@ smx_action_t SIMIX_comm_isend(smx_process_t src_proc, smx_rdv_t rdv,
 
   if (MC_is_active()) {
     other_action->state = SIMIX_RUNNING;
-    return other_action;
+    return (detached ? NULL : other_action);
   }
 
   SIMIX_comm_start(other_action);