From 2392b01a24be1397c6d1b290707de4d315320e4f Mon Sep 17 00:00:00 2001 From: Maurice Scheffmacher Date: Mon, 17 Aug 2026 20:04:34 +0200 Subject: [PATCH 1/4] Bound RMS release proof concurrency --- .github/workflows/ci.yml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ffcd0d4..dad1f47 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -9,6 +9,10 @@ on: jobs: release-check: runs-on: ubuntu-latest + env: + # RMS tests create nested Cargo fixtures. Bound both layers so the hosted + # runner cannot lose its agent under concurrent compiler pressure. + CARGO_BUILD_JOBS: "2" steps: - uses: actions/checkout@v4 - uses: dtolnay/rust-toolchain@stable @@ -31,7 +35,7 @@ jobs: set -euo pipefail provider_test="tests::provider_pipeline_repairs_caches_refreshes_and_deduplicates" RUST_TEST_THREADS=1 cargo test -p rms --locked "$provider_test" -- --exact - cargo test -p rms --locked -- --skip "$provider_test" + RUST_TEST_THREADS=1 cargo test -p rms --locked -- --skip "$provider_test" cargo fmt --all --check cargo build -p rms --locked - name: RMS strict committed audit From a6986891e5cb5c519742a73602fa23e37a996c72 Mon Sep 17 00:00:00 2001 From: Maurice Scheffmacher Date: Mon, 17 Aug 2026 21:02:15 +0200 Subject: [PATCH 2/4] Isolate RMS release tests per process --- .github/workflows/ci.yml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index dad1f47..b642353 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -35,7 +35,17 @@ jobs: set -euo pipefail provider_test="tests::provider_pipeline_repairs_caches_refreshes_and_deduplicates" RUST_TEST_THREADS=1 cargo test -p rms --locked "$provider_test" -- --exact - RUST_TEST_THREADS=1 cargo test -p rms --locked -- --skip "$provider_test" + # Many RMS tests create nested toolchains and subprocess trees. Run + # every discovered test in a short-lived process so the hosted runner + # releases per-test resources instead of accumulating them for an hour. + cargo test -p rms --locked -- --list \ + | sed -n 's/: test$//p' \ + | while IFS= read -r rms_test; do + case "$rms_test" in + "$provider_test"|behavioral_contract::tests::cvc5_reference_solver_conformance) continue ;; + esac + cargo test -p rms --locked "$rms_test" -- --exact --nocapture + done cargo fmt --all --check cargo build -p rms --locked - name: RMS strict committed audit From a73589625a0f7d1a289652ce009ab6f65e084cfe Mon Sep 17 00:00:00 2001 From: Maurice Scheffmacher Date: Mon, 17 Aug 2026 21:13:53 +0200 Subject: [PATCH 3/4] Fix portable probe process-group termination --- tooling/rust/rms/src/main.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tooling/rust/rms/src/main.rs b/tooling/rust/rms/src/main.rs index 49a5886..40a3aa1 100644 --- a/tooling/rust/rms/src/main.rs +++ b/tooling/rust/rms/src/main.rs @@ -14706,7 +14706,10 @@ fn wait_child_with_timeout_observed( { let process_group = format!("-{}", child.id()); let _ = Command::new("kill") - .args(["-KILL", process_group.as_str()]) + // `--` is required by GNU kill. Without it, a negative + // process-group ID can be parsed as another option and + // descendants keep the captured pipes open after timeout. + .args(["-KILL", "--", process_group.as_str()]) .status(); } if let Err(error) = child.kill() { From 3f8c65054c360c63cd386dfbb36df20a313321cf Mon Sep 17 00:00:00 2001 From: Maurice Scheffmacher Date: Mon, 17 Aug 2026 22:07:51 +0200 Subject: [PATCH 4/4] Shard RMS native release proofs --- .github/workflows/ci.yml | 61 +++++++++++++++++++++++++++++----------- 1 file changed, 45 insertions(+), 16 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b642353..a8931be 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -7,45 +7,74 @@ on: branches: [main] jobs: - release-check: + native-release-proofs: + strategy: + fail-fast: false + matrix: + shard: [0, 1, 2, 3] runs-on: ubuntu-latest env: # RMS tests create nested Cargo fixtures. Bound both layers so the hosted # runner cannot lose its agent under concurrent compiler pressure. CARGO_BUILD_JOBS: "2" + RMS_TEST_SHARD_COUNT: "4" + RMS_TEST_SHARD: ${{ matrix.shard }} steps: - uses: actions/checkout@v4 - uses: dtolnay/rust-toolchain@stable - uses: actions/setup-python@v5 with: python-version: "3.11" - - name: Install cvc5 reference solver - env: - GH_TOKEN: ${{ github.token }} - run: | - archive="$RUNNER_TEMP/cvc5-Linux-x86_64-static.zip" - gh release download cvc5-1.3.2 --repo cvc5/cvc5 --pattern cvc5-Linux-x86_64-static.zip --dir "$RUNNER_TEMP" - test "$(sha256sum "$archive" | cut -d " " -f 1)" = "1060daaf507edef9d0a68e399cfc0e9038150bccb9e2d34d081d50a7687544d2" - unzip -q "$archive" -d "$RUNNER_TEMP/cvc5" - echo "$RUNNER_TEMP/cvc5/cvc5-Linux-x86_64-static/bin" >> "$GITHUB_PATH" - - name: cvc5 behavioral-contract conformance - run: cargo test -p rms --locked behavioral_contract::tests::cvc5_reference_solver_conformance -- --ignored --exact - - name: RMS native release proofs + - name: RMS native release proofs (shard ${{ matrix.shard }}) run: | set -euo pipefail provider_test="tests::provider_pipeline_repairs_caches_refreshes_and_deduplicates" - RUST_TEST_THREADS=1 cargo test -p rms --locked "$provider_test" -- --exact + if [ "$RMS_TEST_SHARD" = "0" ]; then + RUST_TEST_THREADS=1 cargo test -p rms --locked "$provider_test" -- --exact + fi # Many RMS tests create nested toolchains and subprocess trees. Run - # every discovered test in a short-lived process so the hosted runner - # releases per-test resources instead of accumulating them for an hour. + # each test in a short-lived process and split the ordered inventory + # across runners. This bounds both per-process resources and runner + # lifetime while preserving exact coverage of the discovered suite. + test_index=0 cargo test -p rms --locked -- --list \ | sed -n 's/: test$//p' \ | while IFS= read -r rms_test; do case "$rms_test" in "$provider_test"|behavioral_contract::tests::cvc5_reference_solver_conformance) continue ;; esac + selected_shard=$((test_index % RMS_TEST_SHARD_COUNT)) + test_index=$((test_index + 1)) + if [ "$selected_shard" -ne "$RMS_TEST_SHARD" ]; then + continue + fi cargo test -p rms --locked "$rms_test" -- --exact --nocapture done + + release-check: + needs: native-release-proofs + runs-on: ubuntu-latest + env: + CARGO_BUILD_JOBS: "2" + steps: + - uses: actions/checkout@v4 + - uses: dtolnay/rust-toolchain@stable + - uses: actions/setup-python@v5 + with: + python-version: "3.11" + - name: Install cvc5 reference solver + env: + GH_TOKEN: ${{ github.token }} + run: | + archive="$RUNNER_TEMP/cvc5-Linux-x86_64-static.zip" + gh release download cvc5-1.3.2 --repo cvc5/cvc5 --pattern cvc5-Linux-x86_64-static.zip --dir "$RUNNER_TEMP" + test "$(sha256sum "$archive" | cut -d " " -f 1)" = "1060daaf507edef9d0a68e399cfc0e9038150bccb9e2d34d081d50a7687544d2" + unzip -q "$archive" -d "$RUNNER_TEMP/cvc5" + echo "$RUNNER_TEMP/cvc5/cvc5-Linux-x86_64-static/bin" >> "$GITHUB_PATH" + - name: cvc5 behavioral-contract conformance + run: cargo test -p rms --locked behavioral_contract::tests::cvc5_reference_solver_conformance -- --ignored --exact + - name: Build release audit binary + run: | cargo fmt --all --check cargo build -p rms --locked - name: RMS strict committed audit