1 # See http://formalverification.cs.utah.edu/ISP_Tests/
3 set(umpire_tests_passing
17 no-error-interleaved-isend
23 no-error-waitany-any_src2
24 no-error-waitany-any_src3
27 no-error-wait-any_src2
28 no-error-wait-any_src3
29 no-error-wait-any_src4
30 no-error-waitany-any_src
35 ) # Passing (no deadlock) tests
37 set(umpire_tests_passing_broken
42 # These are supposed to deadlock but ISP does not find deadlock
43 # and we don't either. What should be test here?
44 set(umpire_tests_missed_deadlock
51 set(umpire_tests_deadlock
52 any_src-can-deadlock10
56 any_src-waitall-deadlock
57 any_src-waitall-deadlock2
58 any_src-waitall-deadlock3
59 any_src-waitany-deadlock2
60 any_src-waitany-deadlock
62 any_src-wait-deadlock2
64 basic-deadlock-comm_create
65 basic-deadlock-comm_dup
66 basic-deadlock-comm_split
69 collective-misorder-allreduce
76 ) # failing (deadlocking) tests
78 # Compile but run those tests:
79 set(umpire_tests_deadlock_broken
80 any_src-can-deadlock10_mod
81 any_src-can-deadlock4_mod
82 any_src-can-deadlock5_mod
83 any_src-can-deadlock6_mod
87 any_src-can-deadlock11
94 set(umpire_tests_problematic
95 deadlock-config # No deadlock detected by ISP unless MPI_Send blocking activated
98 # These files are not listed on http://formalverification.cs.utah.edu/ISP_Tests/
104 basic-deadlock-cart_create.c
105 basic-deadlock-cart_sub.c
106 basic-deadlock-graph_create.c
107 basic-deadlock-intercomm_create.c
108 basic-deadlock-intercomm_merge.c
109 change-send-buffer-exhaustive.c
110 change-send-buffer-type-exhaustive.c
111 collective-exhaustive-byte-int-mismatch.c
112 collective-exhaustive-no-error.c
114 deadlock-config_blocking.c
115 errhandler-no-error.c
120 group-no-error-exhaustive.c
124 group-no-free-exhaustive.c
125 intercomm_create-deadlock2.c
126 intercomm_create-deadlock3.c
127 intercomm_create-deadlock4.c
128 intercomm_create-deadlock.c
129 intercomm_create-no-error.c
130 intercomm_merge-deadlock.c
136 no-error-derived-comms.c
138 no-error-persistent-all-completions.c
139 no-error-persistent.c
140 no-error-persistent-test.c
141 no-error-persistent-testpartial.c
142 no-error-persistent-waitpartial.c
143 no-error-probe-any_src.c
144 no-error-probe-any_tag.c
147 no-error-wait2.c # Does not compile.
148 no-error-waitall-any_src2.c
149 no-error-waitall-any_src3.c
150 no-error-waitall-any_src.c
156 partial-recv-exhaustive.c
157 partial-recv-persistent2.c
158 partial-recv-persistent3.c
159 partial-recv-persistent4.c
160 partial-recv-persistent.c
165 probe-any_src-types-can-mismatch.c
166 probe-any_tag-types-can-mismatch.c
168 pt2pt-byte-int-mismatch.c
169 remote_group-no-error.c
172 type-no-error-exhaustive.c
173 type-no-error-exhaustive-with-isends.c
177 type-no-free-exhaustive.c
180 # Add these files to the archive
183 set(sources "${CMAKE_CURRENT_SOURCE_DIR}/README")
184 foreach(file ${umpire_src_other})
185 set(sources ${sources} ${CMAKE_CURRENT_SOURCE_DIR}/${file})
189 ${umpire_tests_passing} ${umpire_tests_passing_broken}
190 ${umpire_tests_deadlock} ${umpire_tests_deadlock_broken} ${umpire_tests_missed_deadlock}
191 ${umpire_tests_problematic}
192 ${umpire_tests_ignored} )
193 set(sources ${sources} ${CMAKE_CURRENT_SOURCE_DIR}/${file}.c)
195 set(txt_files ${txt_files} ${sources} PARENT_SCOPE)
200 if(enable_smpi AND enable_model-checking AND enable_smpi_ISP_testsuite)
201 set(CMAKE_C_COMPILER "${CMAKE_BINARY_DIR}/smpi_script/bin/smpicc")
202 set(CMAKE_Fortran_COMPILER "${CMAKE_BINARY_DIR}/smpi_script/bin/smpiff")
204 include_directories(BEFORE "${CMAKE_HOME_DIRECTORY}/include/smpi")
206 foreach (test ${umpire_tests_passing} ${umpire_tests_deadlock} ${umpire_tests_problematic} )
207 add_executable(${test} EXCLUDE_FROM_ALL ${test}.c)
208 add_dependencies(tests ${test})
209 target_link_libraries(${test} simgrid)
210 set_source_files_properties(${test}.c PROPERTIES COMPILE_FLAGS "-Dlint -Wno-error -Wno-return-type")
211 set(umpire_tesh ${umpire_tesh} ${test})
212 set(files_to_clean ${files_to_clean} ${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh)
215 # TODO, what should we do about ${umpire_tests_missed_deadlock}?
217 foreach (test ${umpire_tests_passing})
218 write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! timeout 30")
219 write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! output display" APPEND)
220 write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "\$ \${bindir:=.}/../../../../smpi_script/bin/smpirun -wrapper \"\${bindir:=.}/../../../../bin/simgrid-mc\" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/host-speed:1Gf --cfg=smpi/coll-selector:ompi \${bindir:=.}/${test} --log=smpi_coll.thresh:error" APPEND)
223 foreach (test ${umpire_tests_deadlock} ${umpire_tests_problematic} )
224 write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! timeout 30" )
225 write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! expect return 3" APPEND)
226 write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "! output display" APPEND)
227 write_file(${CMAKE_CURRENT_BINARY_DIR}/${test}.tesh "\$ \${bindir:=.}/../../../../smpi_script/bin/smpirun -wrapper \"\${bindir:=.}/../../../../bin/simgrid-mc\" -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=smpi/buffering:zero --cfg=smpi/coll-selector:ompi \${bindir:=.}/${test} --log=smpi_coll.thresh:error" APPEND)
231 # Erase all tesh files on cleanup: they are generated anyway
232 set_directory_properties ( PROPERTIES ADDITIONAL_MAKE_CLEAN_FILES "${files_to_clean}" )
234 if(enable_smpi AND enable_model-checking AND enable_smpi_ISP_testsuite)
235 foreach (tesh ${umpire_tesh})
236 ADD_TESH(mc-umpire-${tesh}
237 --setenv srcdir=${CMAKE_CURRENT_SOURCE_DIR}
238 --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}
239 --cd ${CMAKE_CURRENT_SOURCE_DIR}
240 ${CMAKE_CURRENT_BINARY_DIR}/${tesh}.tesh)