add a test of MC detecting blocking send/send patterns

diff --git a/.gitignore b/.gitignore
index 8134b8e..c0c4ce0 100644 (file)
--- a/.gitignore
+++ b/.gitignore
@@ -213,6 +213,7 @@ examples/smpi/mc/smpi_bugged1
 examples/smpi/mc/smpi_bugged1_liveness
 examples/smpi/mc/smpi_bugged2
 examples/smpi/mc/smpi_mutual_exclusion
+examples/smpi/mc/smpi_sendsend
 examples/smpi/NAS/dt
 examples/smpi/NAS/ep
 examples/smpi/NAS/is

diff --git a/examples/smpi/CMakeLists.txt b/examples/smpi/CMakeLists.txt
index f528907..8109e2d 100644 (file)
--- a/examples/smpi/CMakeLists.txt
+++ b/examples/smpi/CMakeLists.txt
@@ -14,8 +14,8 @@ if(enable_smpi)
 
   set_target_properties(smpi_trace_call_location PROPERTIES COMPILE_FLAGS "-trace-call-location")
 
-  foreach(x bugged1 bugged2 bugged1_liveness only_send_deterministic mutual_exclusion non_termination1 
-            non_termination2 non_termination3 non_termination4)
+  foreach(x bugged1 bugged2 bugged1_liveness only_send_deterministic mutual_exclusion non_termination1
+            non_termination2 non_termination3 non_termination4 sendsend)
     if(SIMGRID_HAVE_MC)
       add_executable       (smpi_${x} EXCLUDE_FROM_ALL ${CMAKE_CURRENT_SOURCE_DIR}/mc/${x}.c)
       target_link_libraries(smpi_${x} simgrid)
@@ -72,6 +72,7 @@ set(txt_files     ${txt_files}     ${CMAKE_CURRENT_SOURCE_DIR}/replay/actions0.t
 if(enable_smpi)
   if(SIMGRID_HAVE_MC)
     ADD_TESH(smpi-mc-only-send-determinism --setenv srcdir=${CMAKE_HOME_DIRECTORY}/examples/smpi/mc --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --cd ${CMAKE_BINARY_DIR}/examples/smpi/mc ${CMAKE_HOME_DIRECTORY}/examples/smpi/mc/only_send_deterministic.tesh)
+    ADD_TESH(smpi-mc-sendsend --setenv srcdir=${CMAKE_HOME_DIRECTORY}/examples/smpi/mc --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --cd ${CMAKE_BINARY_DIR}/examples/smpi/mc ${CMAKE_HOME_DIRECTORY}/examples/smpi/mc/sendsend.tesh)
   endif()
 
   ADD_TESH(smpi-tracing        --setenv bindir=${CMAKE_BINARY_DIR}/examples/smpi/trace --setenv srcdir=${CMAKE_HOME_DIRECTORY}/examples/smpi/trace --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms --cd ${CMAKE_BINARY_DIR}/examples/smpi/trace ${CMAKE_HOME_DIRECTORY}/examples/smpi/trace/trace.tesh)

diff --git a/examples/smpi/mc/sendsend.c b/examples/smpi/mc/sendsend.c
new file mode 100644 (file)
index 0000000..cf83ee3
--- /dev/null
+++ b/examples/smpi/mc/sendsend.c
@@ -0,0 +1,48 @@
+/* A simple bugged MPI_Send and MPI_Recv test: it deadlocks when MPI_Send are blocking */
+
+/* Copyright (c) 2009-2019. 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 <mpi.h>
+#include <stdio.h>
+
+int main(int argc, char** argv)
+{
+  int size;
+  int rank;
+  MPI_Status status;
+
+  /* Initialize MPI */
+  int err = MPI_Init(&argc, &argv);
+  if (err != MPI_SUCCESS) {
+    printf("MPI initialization failed!\n");
+    exit(1);
+  }
+
+  MPI_Comm_size(MPI_COMM_WORLD, &size); /* Get nr of tasks */
+  MPI_Comm_rank(MPI_COMM_WORLD, &rank); /* Get id of this process */
+  if (size < 2) {
+    printf("run this program with exactly 2 processes (-np 2)\n");
+    MPI_Finalize();
+    exit(0);
+  }
+
+  int recv_buff;
+  if (rank == 0) {
+    MPI_Send(&rank, 1, MPI_INT, 1, 42, MPI_COMM_WORLD);
+    printf("Sent %d to rank 1\n", rank);
+    MPI_Recv(&recv_buff, 1, MPI_INT, 1, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
+    printf("rank 0 recv the data\n");
+  } 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("rank 1 recv the data\n");
+  }
+
+  MPI_Finalize();
+
+  return 0;
+}

diff --git a/examples/smpi/mc/sendsend.tesh b/examples/smpi/mc/sendsend.tesh
new file mode 100644 (file)
index 0000000..23874aa
--- /dev/null
+++ b/examples/smpi/mc/sendsend.tesh
@@ -0,0 +1,27 @@
+#! ./tesh
+
+p Testing the permissive model
+! timeout 60
+$ ../../../smpi_script/bin/smpirun -quiet -wrapper "${bindir:=.}/../../../bin/simgrid-mc" -np 2 -platform ${platfdir:=.}/cluster_backbone.xml --cfg=smpi/buffering:infty --log=xbt_cfg.thresh:warning ./smpi_sendsend
+> [0.000000] [mc_safety/INFO] Check a safety property. Reduction is: dpor.
+> [0.000000] [mc_safety/INFO] No property violation found.
+> [0.000000] [mc_safety/INFO] Expanded states = 7
+> [0.000000] [mc_safety/INFO] Visited states = 10
+> [0.000000] [mc_safety/INFO] Executed transitions = 8
+
+p Testing the paranoid model
+! timeout 60
+! expect return 3
+$ ../../../smpi_script/bin/smpirun -quiet -wrapper "${bindir:=.}/../../../bin/simgrid-mc" -np 2 -platform ${platfdir:=.}/cluster_backbone.xml --cfg=smpi/buffering:zero --log=xbt_cfg.thresh:warning ./smpi_sendsend
+> [0.000000] [mc_safety/INFO] Check a safety property. Reduction is: dpor.
+> [0.000000] [mc_global/INFO] **************************
+> [0.000000] [mc_global/INFO] *** DEAD-LOCK DETECTED ***
+> [0.000000] [mc_global/INFO] **************************
+> [0.000000] [mc_global/INFO] Counter-example execution trace:
+> [0.000000] [mc_global/INFO]   [(1)node-0.simgrid.org (0)] iSend(src=(1)node-0.simgrid.org (0), buff=(verbose only), size=(verbose only))
+> [0.000000] [mc_global/INFO]   [(2)node-1.simgrid.org (1)] iSend(src=(2)node-1.simgrid.org (1), buff=(verbose only), size=(verbose only))
+> [0.000000] [mc_record/INFO] Path = 1;2
+> [0.000000] [mc_safety/INFO] Expanded states = 3
+> [0.000000] [mc_safety/INFO] Visited states = 3
+> [0.000000] [mc_safety/INFO] Executed transitions = 2
+> Execution failed with code 3.

diff --git a/tools/cmake/Tests.cmake b/tools/cmake/Tests.cmake
index f380fde..461d420 100644 (file)
--- a/tools/cmake/Tests.cmake
+++ b/tools/cmake/Tests.cmake
@@ -92,6 +92,7 @@ IF(enable_java)
   ELSE()
     SET(TESH_CLASSPATH "${CMAKE_BINARY_DIR}/examples/deprecated/java/:${CMAKE_BINARY_DIR}/teshsuite/java/:${SIMGRID_JAR}")
   ENDIF()
+  ADD_TESH_FACTORIES(mc-sendsend                "ucontext;raw" --setenv bindir=${CMAKE_BINARY_DIR}/examples/smpi/mc --cd ${CMAKE_HOME_DIRECTORY}/examples/smpi/mc sendsend.tesh)
 ENDIF()
 
 # New tests should use the Catch Framework