model-checker : create mc directory in smpi examples and add new example for liveness...

diff --git a/examples/smpi/CMakeLists.txt b/examples/smpi/CMakeLists.txt
index 669d3e3..154b3d5 100644 (file)
--- a/examples/smpi/CMakeLists.txt
+++ b/examples/smpi/CMakeLists.txt
@@ -10,22 +10,29 @@ if(enable_smpi)
   set(EXECUTABLE_OUTPUT_PATH "${CMAKE_CURRENT_BINARY_DIR}")
 
   include_directories("${CMAKE_HOME_DIRECTORY}/include/smpi")
+  file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/mc/")
 
 
   add_executable(bcbench bcbench.c)
   add_executable(mvmul mvmul.c)
   add_executable(smpi_traced tracing/smpi_traced.c)
   add_executable(smpi_traced_simple tracing/smpi_traced_simple.c)
-  add_executable(mc_bugged1 mc_bugged1.c)
-  add_executable(mc_bugged2 mc_bugged2.c)
   add_executable(smpi_replay replay/replay.c)
-
+  
+  if(HAVE_MC)
+    add_executable(mc/bugged1 mc/bugged1.c)
+    add_executable(mc/bugged2 mc/bugged2.c)
+    add_executable(mc/bugged1_liveness mc/bugged1_liveness.c)
+  
+    target_link_libraries(mc/bugged1 simgrid)
+    target_link_libraries(mc/bugged2 simgrid)
+    target_link_libraries(mc/bugged1_liveness simgrid)
+  endif()
+  
   target_link_libraries(bcbench simgrid)
   target_link_libraries(mvmul simgrid)
   target_link_libraries(smpi_traced simgrid)
   target_link_libraries(smpi_traced_simple simgrid)
-  target_link_libraries(mc_bugged1 simgrid)
-  target_link_libraries(mc_bugged2 simgrid)
   target_link_libraries(smpi_replay simgrid)
 
 endif()
@@ -43,18 +50,23 @@ set(xml_files
   )
 set(examples_src
   ${examples_src}
-  ${CMAKE_CURRENT_SOURCE_DIR}/mc_bugged2.c
-  ${CMAKE_CURRENT_SOURCE_DIR}/mc_bugged1.c
   ${CMAKE_CURRENT_SOURCE_DIR}/mvmul.c
   ${CMAKE_CURRENT_SOURCE_DIR}/bcbench.c
   ${CMAKE_CURRENT_SOURCE_DIR}/replay/replay.c
   ${CMAKE_CURRENT_SOURCE_DIR}/tracing/smpi_traced.c
   ${CMAKE_CURRENT_SOURCE_DIR}/tracing/smpi_traced_simple.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged2.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged1.c
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/bugged1_liveness.c
   PARENT_SCOPE
   )
 set(bin_files
   ${bin_files}
   ${CMAKE_CURRENT_SOURCE_DIR}/hostfile
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/promela_bugged1_liveness
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged1_liveness
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged1
+  ${CMAKE_CURRENT_SOURCE_DIR}/mc/hostfile_bugged2
   PARENT_SCOPE
   )
 set(txt_files

diff --git a/examples/smpi/mc/bugged1 b/examples/smpi/mc/bugged1
new file mode 100755 (executable)
index 0000000..fa4c2ec
Binary files /dev/null and b/examples/smpi/mc/bugged1 differ

diff --git a/examples/smpi/mc_bugged1.c b/examples/smpi/mc/bugged1.c
similarity index 94%
rename from examples/smpi/mc_bugged1.c
rename to examples/smpi/mc/bugged1.c
index 699d293..68dd966 100644 (file)
--- a/examples/smpi/mc_bugged1.c
+++ b/examples/smpi/mc/bugged1.c
@@ -40,9 +40,9 @@ int main(int argc, char **argv)
     }
 
     printf("recv_buff = %d\n", recv_buff);
-#ifdef HAVE_MC
-    MC_assert(recv_buff == size - 1);
-#endif
+    //#ifdef HAVE_MC
+    //MC_assert(recv_buff == size - 1);
+    //#endif
 
   }else{
     MPI_Send(&rank, 1, MPI_INT, 0, 42, MPI_COMM_WORLD);

diff --git a/examples/smpi/mc/bugged1_liveness b/examples/smpi/mc/bugged1_liveness
new file mode 100755 (executable)
index 0000000..d643793
Binary files /dev/null and b/examples/smpi/mc/bugged1_liveness differ

diff --git a/examples/smpi/mc/bugged1_liveness.c b/examples/smpi/mc/bugged1_liveness.c
new file mode 100644 (file)
index 0000000..f0f5219
--- /dev/null
+++ b/examples/smpi/mc/bugged1_liveness.c
@@ -0,0 +1,89 @@
+#include <stdio.h>
+#include <mpi.h>
+#include <simgrid/modelchecker.h>
+
+#define GRANT_TAG 0
+#define REQUEST_TAG 1
+#define RELEASE_TAG 2
+
+int r, cs;
+
+static int predR(){
+  return r;
+}
+
+static int predCS(){
+  return cs;
+}
+
+
+int main(int argc, char **argv){
+
+  //int i;
+  int err, size, rank;
+  int recv_buff;
+  MPI_Status status;
+  int CS_used = 0;
+  
+  /* Initialize MPI */
+  err = MPI_Init(&argc, &argv);
+  if(err !=  MPI_SUCCESS){
+    printf("MPI initialization failed !\n");
+    exit(1);
+  }
+
+  MC_automaton_new_propositional_symbol("r", &predR);
+  MC_automaton_new_propositional_symbol("cs", &predCS);
+
+  MC_ignore(&(status.count), sizeof(status.count));
+
+  /* Get number of processes */
+  err = MPI_Comm_size(MPI_COMM_WORLD, &size);
+  /* Get id of this process */
+  err = MPI_Comm_rank(MPI_COMM_WORLD, &rank);
+
+  if(rank == 0){ /* Coordinator */
+    //for(i=0; i<size-1; i++) {
+    while(1){
+      MPI_Recv(&recv_buff, 1, MPI_INT, MPI_ANY_SOURCE, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
+      if(status.MPI_TAG == REQUEST_TAG){
+        if(CS_used){
+          printf("CS already used.\n");
+        }else{
+          if(recv_buff != 1){
+            printf("CS idle. Grant immediatly.\n");
+            MPI_Send(&rank, 1, MPI_INT, recv_buff, GRANT_TAG, MPI_COMM_WORLD);
+            CS_used = 1;
+          }
+        }
+      }else{
+        printf("CS release. Resource now idle.\n");
+        CS_used = 0;
+      }
+    }
+  }else{ /* Client */
+    while(1){
+      printf("%d asks the request.\n", rank);
+      MPI_Send(&rank, 1, MPI_INT, 0, REQUEST_TAG, MPI_COMM_WORLD);
+      if(rank == 1){
+        r = 1;
+        cs = 0;
+      }
+      MPI_Recv(&recv_buff, 1, MPI_INT, 0, MPI_ANY_TAG, MPI_COMM_WORLD, &status);
+      if(status.MPI_TAG == GRANT_TAG && rank == 1){
+        cs = 1;
+        r = 0;
+      }
+      printf("%d got the answer. Release it.\n", rank);
+      MPI_Send(&rank, 1, MPI_INT, 0, RELEASE_TAG, MPI_COMM_WORLD);
+      if(rank == 1){
+        r = 0;
+        cs = 0;
+      }
+    }
+  }
+
+  MPI_Finalize();
+
+  return 0;
+}

diff --git a/examples/smpi/mc/bugged2 b/examples/smpi/mc/bugged2
new file mode 100755 (executable)
index 0000000..d9bb0d2
Binary files /dev/null and b/examples/smpi/mc/bugged2 differ

diff --git a/examples/smpi/mc_bugged2.c b/examples/smpi/mc/bugged2.c
similarity index 100%
rename from examples/smpi/mc_bugged2.c
rename to examples/smpi/mc/bugged2.c

diff --git a/examples/smpi/mc/hostfile_bugged1 b/examples/smpi/mc/hostfile_bugged1
new file mode 100644 (file)
index 0000000..b6d1c07
--- /dev/null
+++ b/examples/smpi/mc/hostfile_bugged1
@@ -0,0 +1,3 @@
+c-1.me
+c-2.me
+c-3.me

diff --git a/examples/smpi/mc/hostfile_bugged1_liveness b/examples/smpi/mc/hostfile_bugged1_liveness
new file mode 100644 (file)
index 0000000..b6d1c07
--- /dev/null
+++ b/examples/smpi/mc/hostfile_bugged1_liveness
@@ -0,0 +1,3 @@
+c-1.me
+c-2.me
+c-3.me

diff --git a/examples/smpi/mc/hostfile_bugged2 b/examples/smpi/mc/hostfile_bugged2
new file mode 100644 (file)
index 0000000..7c988f8
--- /dev/null
+++ b/examples/smpi/mc/hostfile_bugged2
@@ -0,0 +1,36 @@
+c-1.me
+c-2.me
+c-3.me
+c-4.me
+c-5.me
+c-6.me
+c-7.me
+c-8.me
+c-9.me
+c-10.me
+c-11.me
+c-12.me
+c-13.me
+c-14.me
+c-15.me
+c-16.me
+c-17.me
+c-18.me
+c-19.me
+c-20.me
+c-21.me
+c-22.me
+c-23.me
+c-24.me
+c-25.me
+c-26.me
+c-27.me
+c-28.me
+c-29.me
+c-30.me
+c-31.me
+c-32.me
+c-33.me
+c-34.me
+c-35.me
+c-36.me

diff --git a/examples/smpi/mc/promela_bugged1_liveness b/examples/smpi/mc/promela_bugged1_liveness
new file mode 100644 (file)
index 0000000..96b491d
--- /dev/null
+++ b/examples/smpi/mc/promela_bugged1_liveness
@@ -0,0 +1,11 @@
+never { /* !G(r->Fcs) */
+T0_init :    /* init */
+       if
+       :: (1) -> goto T0_init
+       :: (!cs && r) -> goto accept_S2
+       fi;
+accept_S2 :    /* 1 */
+       if
+       :: (!cs) -> goto accept_S2
+       fi;
+}