From 4cd5fce6993366946dc8452bfb5a6b9036c6c808 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 25 Jun 2026 09:08:23 +0000 Subject: [PATCH] Shard the long-running CORE runs of contracts-dfcc and jbmc-strings These two suites are the slowest non-sharded CORE ctest entries and, at a single 30-minute-capped test each, intermittently time out on the slower and highly variable macOS-14 runners (their per-run time there swings roughly 2-3x). Their timeouts (1800s) are already above the 1200s default, so the right remedy is sharding rather than a further timeout bump. Split each suite's CORE profile into 4 parallel shards via test.pl's --shard option. Add an add_sharded_test_pl_tests macro (next to add_test_pl_tests) that shards the CORE profile and registers THOROUGH/FUTURE/KNOWNBUG as single tests, so both suites share a single definition of the pattern rather than hand-expanding it; it builds on the existing add_sharded_test_pl_profile helper. The smaller pieces run in parallel as separate ctest entries instead of one indivisible test, so they no longer dominate the job wall-clock or approach the per-test timeout. Each shard keeps the suite's previous 30-minute cap, which is now ample headroom. The contracts-dfcc smt2_solver PATH environment is applied to each shard, and the THOROUGH/FUTURE/KNOWNBUG levels remain single tests. Co-authored-by: Kiro --- .gitignore | 2 +- jbmc/regression/jbmc-strings/CMakeLists.txt | 18 ++++++++++----- regression/CMakeLists.txt | 22 ++++++++++++++++++ regression/contracts-dfcc/CMakeLists.txt | 25 +++++++++++++-------- 4 files changed, 51 insertions(+), 16 deletions(-) diff --git a/.gitignore b/.gitignore index bbb0e3522c9..a1f228363a4 100644 --- a/.gitignore +++ b/.gitignore @@ -70,7 +70,7 @@ regression/solver-hardness/solver-hardness-simple/solver_hardness.json regression/goto-instrument-wmm-core/*/*.txt regression/goto-instrument-wmm-core/*/*.dot jbmc/regression/**/tests.log -jbmc/regression/**/tests-symex-driven-loading*.log +jbmc/regression/**/tests-*.log unit/memory-analyzer/input.inc unit/memory-analyzer/test.inc unit/gdb.txt diff --git a/jbmc/regression/jbmc-strings/CMakeLists.txt b/jbmc/regression/jbmc-strings/CMakeLists.txt index 70b1b81490c..724af86d85d 100644 --- a/jbmc/regression/jbmc-strings/CMakeLists.txt +++ b/jbmc/regression/jbmc-strings/CMakeLists.txt @@ -1,6 +1,13 @@ -add_test_pl_tests( - "$ --validate-goto-model --validate-ssa-equation" -) +set(jbmc_strings_cmdline + "$ --validate-goto-model --validate-ssa-equation") +set(jbmc_strings_shards 4) + +# The plain (non-symex-driven) CORE run of this suite is one of the slowest +# non-sharded CORE ctests; shard it (keeping its 30-minute per-shard timeout) +# so it runs as several parallel ctest entries on the macOS runners. See +# add_sharded_test_pl_tests. +add_sharded_test_pl_tests( + "${jbmc_strings_cmdline}" "core" ${jbmc_strings_shards} 1800) # The symex-driven-lazy-loading run of this suite is the single largest CORE # ctest on the macOS runners (~1-1.5h), and a single ctest test runs serially @@ -9,11 +16,10 @@ add_test_pl_tests( # dominating the job's wall-clock. add_sharded_test_pl_profile( "jbmc-strings-symex-driven-lazy-loading" - "$ --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" + "${jbmc_strings_cmdline} --symex-driven-lazy-loading" "-C;-X;symex-driven-lazy-loading-expected-failure" "CORE" "symex-driven-loading" - 4 + ${jbmc_strings_shards} 10800 ) -set_tests_properties("jbmc-strings-CORE" PROPERTIES TIMEOUT 1800) diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index 322954ea966..6d69f4e0349 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -53,6 +53,28 @@ macro(add_test_pl_tests cmdline) add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG ${ARGN}) endmacro(add_test_pl_tests) +# Like add_test_pl_tests, but split the CORE profile into +# parallel shards (see add_sharded_test_pl_profile) so a long-running CORE +# suite runs as several parallel ctest entries instead of one indivisible test +# -- e.g. to keep the slowest suites from dominating the macOS runners' +# wall-clock or approaching the per-test timeout. THOROUGH/FUTURE/KNOWNBUG +# remain single tests. names the per-shard CORE logs and each CORE +# shard is given . Any extra arguments (e.g. -X exclusions) are +# forwarded to every profile. +macro(add_sharded_test_pl_tests cmdline log_suffix shard_count timeout) + get_filename_component(TEST_DIR_NAME ${CMAKE_CURRENT_SOURCE_DIR} NAME) + message(STATUS "Adding sharded tests in directory: ${TEST_DIR_NAME}") + # Build the CORE flags as a list so an empty ARGN collapses to just -C (no + # spurious empty argument reaching test.pl). + set(_core_flags "-C" ${ARGN}) + add_sharded_test_pl_profile( + "${TEST_DIR_NAME}" "${cmdline}" "${_core_flags}" "CORE" + "${log_suffix}" ${shard_count} ${timeout}) + add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -T THOROUGH ${ARGN}) + add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -F FUTURE ${ARGN}) + add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG ${ARGN}) +endmacro(add_sharded_test_pl_tests) + # For the best possible utilisation of multiple cores when # running tests in parallel, it is important that these directories are # listed with decreasing runtimes (i.e. longest running at the top) diff --git a/regression/contracts-dfcc/CMakeLists.txt b/regression/contracts-dfcc/CMakeLists.txt index 5d641697bef..c16e0208dd4 100644 --- a/regression/contracts-dfcc/CMakeLists.txt +++ b/regression/contracts-dfcc/CMakeLists.txt @@ -13,9 +13,15 @@ else() endif() -add_test_pl_tests( - "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $ $ $ ${is_windows} true" ${gcc_only} -) +set(dfcc_cmd + "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $ $ $ ${is_windows} true") +set(dfcc_core_shards 4) + +# The CORE run of this suite is one of the slowest non-sharded CORE ctests; +# shard it (and keep its 30-minute per-shard timeout) so it runs as several +# parallel ctest entries on the macOS runners. See add_sharded_test_pl_tests. +add_sharded_test_pl_tests( + "${dfcc_cmd}" "dfcc-core" ${dfcc_core_shards} 1800 ${gcc_only}) add_test_pl_profile( "contracts-non-dfcc" @@ -42,15 +48,16 @@ add_test_pl_profile( # solver appears on the PATH in Windows already if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows") - set_property( - TEST "contracts-dfcc-CORE" - PROPERTY ENVIRONMENT - "PATH=$ENV{PATH}:$" - ) + foreach(shard RANGE 1 ${dfcc_core_shards}) + set_property( + TEST "contracts-dfcc-${shard}-CORE" + PROPERTY ENVIRONMENT + "PATH=$ENV{PATH}:$" + ) + endforeach() set_property( TEST "contracts-non-dfcc-CORE" PROPERTY ENVIRONMENT "PATH=$ENV{PATH}:$" ) endif() -set_tests_properties("contracts-dfcc-CORE" PROPERTIES TIMEOUT 1800)