X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/57a4ce6a28d437d6f1b931b9732d9ed584e252cd..41a79ecaf5ce51f0513500e8cc7f9a0ed5435374:/teshsuite/smpi/isp/umpire/CMakeLists.txt

diff --git a/teshsuite/smpi/isp/umpire/CMakeLists.txt b/teshsuite/smpi/isp/umpire/CMakeLists.txt
index 3a7bd25c5a..1200f99eef 100644
--- a/teshsuite/smpi/isp/umpire/CMakeLists.txt
+++ b/teshsuite/smpi/isp/umpire/CMakeLists.txt
@@ -1,64 +1,115 @@
-set(umpire_src
+# See http://formalverification.cs.utah.edu/ISP_Tests/
+
+set(umpire_tests_passing
+  change-send-buffer
+  comm-dup-no-error
+  comm-dup-no-free
+  comm-dup-no-free2
+  comm-simple
+  comm-split-no-free
+  comm-translate-ranks
+  hello
+  no-error
+  no-error2
+  no-error3
+  no-error3-any_src
+  no-error-any_src
+  no-error-interleaved-isend
+  no-error-test
+  no-error-testall
+  no-error-testany
+  no-error-vector-isend
+  no-error-wait
+  no-error-waitany-any_src2
+  no-error-waitany-any_src3
+  no-error-waitany
+  no-error-wait-any_src
+  no-error-wait-any_src2
+  no-error-wait-any_src3
+  no-error-wait-any_src4
+  no-error-waitany-any_src
+  partial-recv
+  sendrecv-deadlock
+  send-recv-ok
+  irecv-isend-ok
+  irecv-isend-ok2
+  lost-request-waitall
+ ) # Passing (no deadlock) tests
+
+# These are supposed to deadlock but ISP does not find deadlock
+# and we don't either. What should be test here?
+set(umpire_tests_missed_deadlock
+  any_src-deadlock
+  any_src-can-deadlock
+  any_src-can-deadlock2
+  any_src-can-deadlock3
+  )
+
+set(umpire_tests_deadlock
+  any_src-can-deadlock10
+  any_src-can-deadlock10_mod
+  any_src-can-deadlock11
+  any_src-can-deadlock4
+  any_src-can-deadlock4_mod
+  any_src-can-deadlock5
+  any_src-can-deadlock5_mod
+  any_src-can-deadlock6
+  any_src-can-deadlock6_mod
+  any_src-can-deadlock7
+  any_src-can-deadlock8
+  any_src-can-deadlock9
+  any_src-waitall-deadlock
+  any_src-waitall-deadlock2
+  any_src-waitall-deadlock3
+  any_src-waitany-deadlock2
+  any_src-waitany-deadlock
+  any_src-wait-deadlock
+  any_src-wait-deadlock2
+  basic-deadlock
+  basic-deadlock-comm_create
+  basic-deadlock-comm_dup
+  basic-deadlock-comm_split
+  bcast-deadlock
+  collective-misorder
+  collective-misorder2
+  collective-misorder-allreduce
+  comm-bcast-deadlock
+  comm-deadlock
+  complex-deadlock
+  dropped-req
+  finalize-deadlock
+  irecv-deadlock
+  waitall-deadlock
+  waitany-deadlock
+  wait-deadlock
+ ) # failing (deadlocking) tests
+ 
+set(umpire_tests_problematic
+  deadlock-config # No deadlock detected by ISP unless MPI_Send blocking activated
+
+ ) # problematic tests
+ 
+ # These files are not listed on http://formalverification.cs.utah.edu/ISP_Tests/
+set(umpire_src_other
   abort1.c
   abort2.c
   abort3.c
   abort.c
-  any_src-can-deadlock10.c
-  any_src-can-deadlock10_mod.c
-  any_src-can-deadlock11.c
-  any_src-can-deadlock2.c
-  any_src-can-deadlock3.c
-  any_src-can-deadlock4.c
-  any_src-can-deadlock4_mod.c
-  any_src-can-deadlock5.c
-  any_src-can-deadlock5_mod.c
-  any_src-can-deadlock6.c
-  any_src-can-deadlock6_mod.c
-  any_src-can-deadlock7.c
-  any_src-can-deadlock8.c
-  any_src-can-deadlock9.c
-  any_src-can-deadlock.c
-  any_src-deadlock.c
-  any_src-waitall-deadlock2.c
-  any_src-waitall-deadlock3.c
-  any_src-waitall-deadlock.c
-  any_src-waitany-deadlock2.c
-  any_src-waitany-deadlock.c
-  any_src-wait-deadlock2.c
-  any_src-wait-deadlock.c
-  basic-deadlock.c
   basic-deadlock-cart_create.c
   basic-deadlock-cart_sub.c
-  basic-deadlock-comm_create.c
-  basic-deadlock-comm_dup.c
-  basic-deadlock-comm_split.c
   basic-deadlock-graph_create.c
   basic-deadlock-intercomm_create.c
   basic-deadlock-intercomm_merge.c
-  bcast-deadlock.c
-  change-send-buffer.c
   change-send-buffer-exhaustive.c
   change-send-buffer-type-exhaustive.c
   collective-exhaustive-byte-int-mismatch.c
   collective-exhaustive-no-error.c
-  collective-misorder2.c
-  collective-misorder-allreduce.c
   collective-misorder.c
-  comm-bcast-deadlock.c
-  comm-deadlock.c
-  comm-dup-no-error.c
-  comm-dup-no-free2.c
-  comm-dup-no-free.c
-  comm-simple.c
-  comm-split-no-free.c
-  comm-translate-ranks.c
-  complex-deadlock.c
+  collective-misorder2.c
+
   deadlock-config_blocking.c
-  deadlock-config.c
-  dropped-req.c
   errhandler-no-error.c
   errhandler-no-free.c
-  finalize-deadlock.c
   group-no-error2.c
   group-no-error3.c
   group-no-error.c
@@ -67,29 +118,19 @@ set(umpire_src
   group-no-free3.c
   group-no-free.c
   group-no-free-exhaustive.c
-  hello.c
   intercomm_create-deadlock2.c
   intercomm_create-deadlock3.c
   intercomm_create-deadlock4.c
   intercomm_create-deadlock.c
   intercomm_create-no-error.c
   intercomm_merge-deadlock.c
-  irecv-deadlock.c
-  irecv-isend-ok2.c
-  irecv-isend-ok.c
   lost-request2.c
   lost-request3.c
-  lost-request.c
-  lost-request-waitall.c
-  no-error2.c
-  no-error3-any_src.c
-  no-error3.c
+  lost-request.c  
   no-error4-any_src.c
   no-error4.c
-  no-error-any_src.c
-  no-error.c
   no-error-derived-comms.c
-  no-error-interleaved-isend.c
+    
   no-error-persistent-all-completions.c
   no-error-persistent.c
   no-error-persistent-test.c
@@ -98,28 +139,16 @@ set(umpire_src
   no-error-probe-any_src.c
   no-error-probe-any_tag.c
   no-error-probe.c
-  no-error-testall.c
-  no-error-testany.c
-  no-error-test.c
-  no-error-vector-isend.c
-  # no-error-wait2.c # Does not compile.
+  
+  no-error-wait2.c # Does not compile.
   no-error-waitall-any_src2.c
   no-error-waitall-any_src3.c
   no-error-waitall-any_src.c
   no-error-waitall.c
   no-error-waitany2.c
-  no-error-waitany-any_src2.c
-  no-error-waitany-any_src3.c
-  no-error-waitany-any_src.c
-  no-error-waitany.c
-  no-error-wait-any_src2.c
-  no-error-wait-any_src3.c
-  no-error-wait-any_src4.c
-  no-error-wait-any_src.c
-  no-error-wait.c
+  
   op-no-error.c
   op-no-free.c
-  partial-recv.c
   partial-recv-exhaustive.c
   partial-recv-persistent2.c
   partial-recv-persistent3.c
@@ -134,8 +163,6 @@ set(umpire_src
   probe-deadlock.c
   pt2pt-byte-int-mismatch.c
   remote_group-no-error.c
-  sendrecv-deadlock.c
-  send-recv-ok.c
   type-commit-twice.c
   type-no-error.c
   type-no-error-exhaustive.c
@@ -144,67 +171,65 @@ set(umpire_src
   type-no-free3.c
   type-no-free.c
   type-no-free-exhaustive.c
-  waitall-deadlock.c
-  waitany-deadlock.c
-  wait-deadlock.c
   )
 
-set(sources "")
-FOREACH(s ${umpire_src})
-  set(sources ${sources} ${CMAKE_CURRENT_SOURCE_DIR}/${s})
-ENDFOREACH()
-
-set(umpire_tesh "")
-foreach(tesh
-    any_src-can-deadlock10
-    any_src-can-deadlock4
-    any_src-can-deadlock5
-    any_src-can-deadlock6
-    any_src-waitall-deadlock2
-    any_src-waitall-deadlock3
-    any_src-waitany-deadlock2
-    any_src-waitany-deadlock
-    any_src-wait-deadlock
-    basic-deadlock-comm_create
-    basic-deadlock-comm_dup
-    basic-deadlock-comm_split
-    basic-deadlock
-    bcast-deadlock
-    collective-misorder-allreduce
-    collective-misorder
-    complex-deadlock
-    deadlock-config
-    finalize-deadlock
-    irecv-deadlock
-    no-error2
-    no-error3-any_src
-    no-error3
-    no-error
-    )
-  set(umpire_tesh ${umpire_tesh} teshsuite/smpi/isp/umpire/${tesh}.tesh)
-ENDFOREACH()
-
-set(examples_src ${examples_src} ${sources} PARENT_SCOPE)
-set(txt_files ${txt_files} ${CMAKE_CURRENT_SOURCE_DIR}/README PARENT_SCOPE)
-set(EXTRA_DIST ${EXTRA_DIST} ${CMAKE_CURRENT_SOURCE_DIR}/no-error-wait2.c PARENT_SCOPE)
-set(tesh_files ${tesh_files} ${umpire_tesh} PARENT_SCOPE)
-
-if(enable_smpi AND enable_smpi_ISP_testsuite)
-  if(WIN32)
-    set(CMAKE_C_FLAGS "-include ${CMAKE_HOME_DIRECTORY}/include/smpi/smpi_main.h")
-  else()
-    set(CMAKE_C_COMPILER "${CMAKE_BINARY_DIR}/smpi_script/bin/smpicc")
-    set(CMAKE_Fortran_COMPILER "${CMAKE_BINARY_DIR}/smpi_script/bin/smpiff")
-  endif()
+# Add these files to the archive
+#################
+
+set(sources "${CMAKE_CURRENT_SOURCE_DIR}/README")
+foreach(file ${umpire_src_other})
+  set(sources ${sources} ${CMAKE_CURRENT_SOURCE_DIR}/${file})
+endforeach()
+
+foreach(file ${umpire_tests_passing} ${umpire_tests_deadlock} ${umpire_tests_missed_deadlock} ${umpire_tests_problematic}  ) 
+  set(sources ${sources} ${CMAKE_CURRENT_SOURCE_DIR}/${file}.c)
+endforeach()
+set(txt_files ${txt_files} ${sources} PARENT_SCOPE)
+
+# Build the tests
+#################
+
+if(enable_smpi AND enable_model-checking AND enable_smpi_ISP_testsuite)
+  set(CMAKE_C_COMPILER "${CMAKE_BINARY_DIR}/smpi_script/bin/smpicc")
+  set(CMAKE_Fortran_COMPILER "${CMAKE_BINARY_DIR}/smpi_script/bin/smpiff")
 
   set(EXECUTABLE_OUTPUT_PATH "${CMAKE_CURRENT_BINARY_DIR}")
 
   include_directories(BEFORE "${CMAKE_HOME_DIRECTORY}/include/smpi")
 
-  FOREACH (s ${umpire_src})
-    STRING(REGEX REPLACE "\\.c$" "" exe ${s})
-    add_executable(${exe} ${s})
-    target_link_libraries(${exe} simgrid)
-    set_source_files_properties(${s} PROPERTIES COMPILE_FLAGS "-Wno-error")
-  ENDFOREACH(s)
+  foreach (test ${umpire_tests_passing} ${umpire_tests_deadlock} ${umpire_tests_problematic} )
+    add_executable(${test} ${test}.c)
+    target_link_libraries(${test} simgrid)
+    set_source_files_properties(${test}.c PROPERTIES COMPILE_FLAGS "-Wno-error")
+    set(umpire_tesh ${umpire_tesh} ${test})
+    set(files_to_clean ${files_to_clean} ${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh)
+  endforeach(test)
+  
+  # TODO, what should we do about ${umpire_tests_missed_deadlock}?
+
+  foreach (test ${umpire_tests_passing})
+    write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! timeout 30")
+    write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! output display" APPEND)
+    write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "\$ \${bindir:=.}/../../../../bin/smpirun -wrapper \"\${bindir:=.}/../../../../bin/simgrid-mc\" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich \${bindir:=.}/${test} --log=smpi_coll.thresh:error" APPEND)
+  endforeach()
+
+  foreach (test ${umpire_tests_deadlock} ${umpire_tests_problematic} )
+    write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! timeout 30"     )
+    write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! expect return 3" APPEND)
+    write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! output display"  APPEND)
+    write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "\$ \${bindir:=.}/../../../../bin/smpirun -wrapper \"\${bindir:=.}/../../../../bin/simgrid-mc\" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich \${bindir:=.}/${test} --log=smpi_coll.thresh:error" APPEND)
+  endforeach()
+endif()
+
+# Erase all tesh files on cleanup: they are generated anyway
+set_directory_properties ( PROPERTIES ADDITIONAL_MAKE_CLEAN_FILES "${files_to_clean}" )
+
+if(enable_smpi AND enable_model-checking AND enable_smpi_ISP_testsuite)
+  foreach (tesh ${umpire_tesh})
+    ADD_TESH(mc-umpire-${tesh}
+      --setenv srcdir=${CMAKE_CURRENT_SOURCE_DIR}
+      --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}
+      --cd ${CMAKE_CURRENT_SOURCE_DIR}
+      ${CMAKE_CURRENT_BINARY_DIR}/${tesh}.tesh)
+  endforeach()
 endif()