Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'mc' into mc++
authorGabriel Corona <gabriel.corona@loria.fr>
Tue, 25 Feb 2014 12:09:35 +0000 (13:09 +0100)
committerGabriel Corona <gabriel.corona@loria.fr>
Tue, 25 Feb 2014 12:09:35 +0000 (13:09 +0100)
19 files changed:
examples/smpi/CMakeLists.txt
examples/smpi/mc/hostfile_non_deterministic [new file with mode: 0644]
examples/smpi/mc/hostfile_send_deterministic [new file with mode: 0644]
examples/smpi/mc/non_deterministic.c [new file with mode: 0644]
examples/smpi/mc/send_deterministic.c [new file with mode: 0644]
include/smpi/mpi.h
src/include/mc/mc.h
src/mc/mc_dpor.c
src/mc/mc_global.c
src/mc/mc_liveness.c
src/mc/mc_private.h
src/mc/mc_request.c
src/mc/mc_state.c
src/simgrid/sg_config.c
src/simix/smx_network.c
src/smpi/smpi_base.c
src/xbt/mmalloc/mm_diff.c
teshsuite/smpi/mpich3-test/coll/bcastzerotype.c
teshsuite/smpi/mpich3-test/datatype/unusual-noncontigs.c

index 154b3d5..9afad64 100644 (file)
@@ -23,10 +23,14 @@ if(enable_smpi)
     add_executable(mc/bugged1 mc/bugged1.c)
     add_executable(mc/bugged2 mc/bugged2.c)
     add_executable(mc/bugged1_liveness mc/bugged1_liveness.c)
+    add_executable(mc/send_deterministic mc/send_deterministic.c)
+    add_executable(mc/non_deterministic mc/non_deterministic.c)
   
     target_link_libraries(mc/bugged1 simgrid)
     target_link_libraries(mc/bugged2 simgrid)
     target_link_libraries(mc/bugged1_liveness simgrid)
+    target_link_libraries(mc/send_deterministic simgrid)
+    target_link_libraries(mc/non_deterministic simgrid)
   endif()
   
   target_link_libraries(bcbench simgrid)
@@ -58,6 +62,8 @@ set(examples_src
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged2.c
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged1.c
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged1_liveness.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/send_deterministic.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/non_deterministic.c
   PARENT_SCOPE
   )
 set(bin_files
@@ -67,6 +73,8 @@ set(bin_files
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged1_liveness
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged1
   ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged2
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_send_deterministic
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_non_deterministic
   PARENT_SCOPE
   )
 set(txt_files
diff --git a/examples/smpi/mc/hostfile_non_deterministic b/examples/smpi/mc/hostfile_non_deterministic
new file mode 100644 (file)
index 0000000..b6d1c07
--- /dev/null
@@ -0,0 +1,3 @@
+c-1.me
+c-2.me
+c-3.me
diff --git a/examples/smpi/mc/hostfile_send_deterministic b/examples/smpi/mc/hostfile_send_deterministic
new file mode 100644 (file)
index 0000000..b6d1c07
--- /dev/null
@@ -0,0 +1,3 @@
+c-1.me
+c-2.me
+c-3.me
diff --git a/examples/smpi/mc/non_deterministic.c b/examples/smpi/mc/non_deterministic.c
new file mode 100644 (file)
index 0000000..b73cbd2
--- /dev/null
@@ -0,0 +1,54 @@
+/* ../../../smpi_script/bin/smpirun -hostfile hostfile_send_deterministic -platform ../../platforms/cluster.xml -np 3 --cfg=model-check:1 --cfg=smpi/send_is_detached_thres:0 gdb\ --args\ ./send_deterministic */
+
+/* Copyright (c) 2009 - 2014. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include <stdio.h>
+#include <mpi.h>
+#include <simgrid/modelchecker.h>
+
+
+int main(int argc, char **argv)
+{
+  int recv_buff, err, size, rank, i;
+  MPI_Status status;
+
+  /* Initialize MPI */
+  err = MPI_Init(&argc, &argv);
+  if (err != MPI_SUCCESS) {
+    printf("MPI initialization failed!\n");
+    exit(1);
+  }
+
+  err = MPI_Comm_size(MPI_COMM_WORLD, &size);   /* Get nr of tasks */
+  err = MPI_Comm_rank(MPI_COMM_WORLD, &rank);   /* Get id of this process */
+  if (size < 2) {
+    printf("run this program with at least 2 processes \n");
+    MPI_Finalize();
+    exit(0);
+  }
+
+  if (rank == 0) {
+    printf("MPI_ISend / MPI_IRecv Test \n");
+
+    for(i=0; i < size - 1; i++){
+      MPI_Recv(&recv_buff, 1, MPI_INT, MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
+      printf("Message received from %d\n", recv_buff);
+      MPI_Send(&recv_buff, 1, MPI_INT, status.MPI_SOURCE, 42, MPI_COMM_WORLD);
+      // printf("Sent %d to rank %d\n", status.MPI_SOURCE);
+    }
+
+  }else{
+    MPI_Send(&rank, 1, MPI_INT, 0, 42, MPI_COMM_WORLD);
+    printf("Sent %d to rank 0\n", rank);
+    MPI_Recv(&recv_buff, 1, MPI_INT, 0, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
+    printf("Message received from %d\n", recv_buff);
+  }
+
+  MPI_Finalize();
+
+  return 0;
+}
diff --git a/examples/smpi/mc/send_deterministic.c b/examples/smpi/mc/send_deterministic.c
new file mode 100644 (file)
index 0000000..ecbcc49
--- /dev/null
@@ -0,0 +1,50 @@
+/* ../../../smpi_script/bin/smpirun -hostfile hostfile_send_deterministic -platform ../../platforms/cluster.xml -np 3 --cfg=model-check:1 --cfg=smpi/send_is_detached_thres:0 gdb\ --args\ ./send_deterministic */
+
+/* Copyright (c) 2009 - 2014. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include <stdio.h>
+#include <mpi.h>
+#include <simgrid/modelchecker.h>
+
+
+int main(int argc, char **argv)
+{
+  int recv_buff, err, size, rank, i;
+  MPI_Status status;
+
+  /* Initialize MPI */
+  err = MPI_Init(&argc, &argv);
+  if (err != MPI_SUCCESS) {
+    printf("MPI initialization failed!\n");
+    exit(1);
+  }
+
+  err = MPI_Comm_size(MPI_COMM_WORLD, &size);   /* Get nr of tasks */
+  err = MPI_Comm_rank(MPI_COMM_WORLD, &rank);   /* Get id of this process */
+  if (size < 2) {
+    printf("run this program with at least 2 processes \n");
+    MPI_Finalize();
+    exit(0);
+  }
+
+  if (rank == 0) {
+    printf("MPI_ISend / MPI_IRecv Test \n");
+
+    for(i=0; i < size - 1; i++){
+      MPI_Recv(&recv_buff, 1, MPI_INT, MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
+      printf("Message received from %d\n", recv_buff);
+    }
+
+  }else{
+    MPI_Send(&rank, 1, MPI_INT, 0, 42, MPI_COMM_WORLD);
+    printf("Sent %d to rank 0\n", rank);
+  }
+
+  MPI_Finalize();
+
+  return 0;
+}
index d840c9a..e8aa3ea 100644 (file)
 #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
index 298c779..bbcdc2f 100644 (file)
@@ -30,6 +30,8 @@ extern int _sg_mc_hash;
 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;
@@ -45,6 +47,8 @@ void _mc_cfg_cb_hash(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);
+void _mc_cfg_cb_send_determinism(const char *name, int pos);
 
 XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void);
 
index 4017885..7aaa065 100644 (file)
@@ -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){
@@ -102,7 +101,9 @@ static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){
     if(current_pattern->comm == pattern->comm){
       if(!current_pattern->completed){
         current_pattern->src_proc = pattern->comm->comm.src_proc->pid;
+        current_pattern->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host);
         current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
+        current_pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
         current_pattern->data_size = pattern->comm->comm.src_buff_size;
         current_pattern->data = xbt_malloc0(current_pattern->data_size);
         current_pattern->matched_comm = pattern->num;
@@ -123,13 +124,14 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
   if(call == 1){ // ISEND
     pattern->comm = simcall_comm_isend__get__result(request);
     pattern->type = SIMIX_COMM_SEND;
-    if(pattern->comm->comm.dst_proc != NULL){
+    if(pattern->comm->comm.dst_proc != NULL){ 
       pattern->matched_comm = complete_comm_pattern(list, pattern);
       pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
       pattern->completed = 1;
+      pattern->dst_host = simcall_host_get_name(pattern->comm->comm.dst_proc->smx_host);
     }
     pattern->src_proc = pattern->comm->comm.src_proc->pid;
+    pattern->src_host = simcall_host_get_name(request->issuer->smx_host);
     pattern->data_size = pattern->comm->comm.src_buff_size;
     pattern->data=xbt_malloc0(pattern->data_size);
     memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
@@ -139,12 +141,14 @@ void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
     if(pattern->comm->comm.src_proc != NULL){
       pattern->matched_comm = complete_comm_pattern(list, pattern);
       pattern->src_proc = pattern->comm->comm.src_proc->pid;
+      pattern->src_host = simcall_host_get_name(pattern->comm->comm.src_proc->smx_host);
       pattern->completed = 1;
       pattern->data_size = pattern->comm->comm.src_buff_size;
       pattern->data=xbt_malloc0(pattern->data_size);
       memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
     }
     pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
+    pattern->dst_host = simcall_host_get_name(request->issuer->smx_host);
   }
   if(pattern->comm->comm.rdv != NULL)
     pattern->rdv = strdup(pattern->comm->comm.rdv->name);
@@ -157,7 +161,10 @@ static void print_communications_pattern(xbt_dynar_t comms_pattern){
   unsigned int cursor = 0;
   mc_comm_pattern_t current_comm;
   xbt_dynar_foreach(comms_pattern, cursor, current_comm){
-    // fprintf(stderr, "%s (%d - comm %p, src : %lu, dst %lu, rdv name %s, data %p, matched with %d)\n", current_comm->type == SIMIX_COMM_SEND ? "iSend" : "iRecv", current_comm->num, current_comm->comm, current_comm->src_proc, current_comm->dst_proc, current_comm->rdv, current_comm->data, current_comm->matched_comm);
+    if(current_comm->type == SIMIX_COMM_SEND)
+      XBT_INFO("[(%lu) %s -> %s] %s ", current_comm->src_proc, current_comm->src_host, current_comm->dst_host, "iSend");
+    else
+      XBT_INFO("[(%lu) %s <- %s] %s ", current_comm->dst_proc, current_comm->dst_host, current_comm->src_host, "iRecv");
   }
 }
 
@@ -465,15 +472,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) {
 
@@ -516,25 +523,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 || _sg_mc_send_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 || _sg_mc_send_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();
@@ -628,24 +638,44 @@ 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 || _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;
-      }
-      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 */
@@ -711,15 +741,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);
@@ -733,10 +763,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);
index 987c6fc..1badcb3 100644 (file)
@@ -34,6 +34,8 @@ int _sg_mc_hash=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 _sg_mc_send_determinism=0;
 
 int user_max_depth_reached = 0;
 
@@ -99,6 +101,20 @@ 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);
+}
+
+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;
@@ -1216,7 +1232,8 @@ void MC_replay(xbt_fifo_t stack, int start)
       xbt_free(key);
     }
   }
-  xbt_dynar_reset(communications_pattern);
+  if(_sg_mc_comms_determinism || _sg_mc_send_determinism)
+    xbt_dynar_reset(communications_pattern);
   MC_UNSET_RAW_MEM;
   
 
@@ -1247,20 +1264,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 || _sg_mc_send_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 || _sg_mc_send_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();
 
@@ -1543,8 +1563,10 @@ void MC_print_statistics(mc_stats_t stats)
     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(_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;
 }
index ebbb777..54f5143 100644 (file)
@@ -274,7 +274,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;
index 8997755..2b9ae41 100644 (file)
@@ -497,6 +497,8 @@ typedef struct s_mc_comm_pattern{
   int completed;
   unsigned long src_proc;
   unsigned long dst_proc;
+  const char *src_host;
+  const char *dst_host;
   char *rdv;
   size_t data_size;
   void *data;
index 5b7ce40..1a3d2aa 100644 (file)
@@ -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;
index f0c240d..7036c25 100644 (file)
@@ -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;
index ad88f30..dafa406 100644 (file)
@@ -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,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 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)",
index 428ef6a..1068eef 100644 (file)
@@ -443,7 +443,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);
index a6a3c57..2597663 100644 (file)
@@ -763,7 +763,7 @@ void smpi_mpi_wait(MPI_Request * request, MPI_Status * status)
   }
 
 #ifdef HAVE_MC
-  if(MC_is_active())
+  if(MC_is_active() && (*request)->action)
     (*request)->action->comm.dst_data = NULL; // dangling pointer : dst_data is freed with a wait, need to set it to NULL for system state comparison
 #endif
 
index 5717fa1..76865c9 100644 (file)
@@ -1037,7 +1037,7 @@ int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, mc_object_
         type = type->subtype;
       }
     }
-    if((type->byte_size == DW_TAG_pointer_type) || ((type->type == DW_TAG_base_type) && type->name!=NULL && (!strcmp(type->name, "char"))))
+    if((type->type == DW_TAG_pointer_type) || ((type->type == DW_TAG_base_type) && type->name!=NULL && (!strcmp(type->name, "char"))))
       type_size = -1;
     else
       type_size = type->byte_size;
index ece1e25..9ebf1f7 100644 (file)
@@ -20,7 +20,7 @@ int main(int argc, char *argv[])
     /* a random non-zero sized buffer */
 #define NELEM (10)
     buf = malloc(NELEM*sizeof(int));
-    assert(buf);
+    assert(buf!=NULL);
 
     for (i = 0; i < NELEM; i++) {
         buf[i] = wrank * NELEM + i;
index d6fd63c..5844207 100644 (file)
@@ -534,7 +534,7 @@ static int pack_and_check_expected(MPI_Datatype type, const char *name,
     err = MPI_Pack_size(type_size/sizeof(int), MPI_INT, MPI_COMM_SELF, &pack_size);
     check_err(MPI_Pack_size);
     pack_buf = malloc(pack_size);
-    assert(pack_buf);
+    assert(pack_buf!=NULL);
 
     pos = 0;
     err = MPI_Pack(&sendbuf[0], type_size/sizeof(int), MPI_INT, pack_buf, pack_size, &pos, MPI_COMM_SELF);