Repository navigation
feat(chapel): L2.3 cancel-token preemption - #154
Merged
Merged
Conversation
…s self-SIGKILL on CAS win Wave-2 follow-on to PR #146. Closes the explicitly-deferred "kill in-flight losers" gap from L2.2: once the CAS-winner is selected, every still-polling loser observes the shared `cancelToken.cancelled` flag on its next poll tick and SIGKILLs its own subprocess instead of running to its per-prover timeout. Loser wall is now bounded by `pollInterval ≈ 100 ms` rather than `max(losers)`. Changes: - `parallel_proof_search.chpl`: - New `class CancelToken { var cancelled: atomic bool }` — class (not record) so that all `coforall` tasks share the same instance by reference. - `tryProver` signature gains `cancelToken: borrowed CancelToken? = nil`. Existing callers (sequential, best-of) pass nil and behave identically. - tryProver's poll loop now checks `cancelToken!.cancelled.read()` each tick; on observing true, SIGKILLs the subprocess and returns a preempted `ProofResult` with `exitCode = -5` (distinct from -3 timeout / -4 subprocess error). - `parallelProofSearchSpeculative` creates `new owned CancelToken()` and pairs the successful `winnerIdx.compareAndSwap` with `cancelToken.cancelled.write(true)` so only the SAME prover that wins the CAS triggers the signal (no double-write). - `proofs/agda/ParallelSoundness.agda`: - Header docstring extended to spell out that the existing `cancellation-safety` theorem IS the L2.3 preemption claim: once a head witness is true, the verdict is true regardless of the tail. The L2.3 code change preserves this — preempted losers land in the result table with success=false but are never returned because winnerIdx is set before any cancellation could race the CAS. - No new Agda lemma — the existing theorem already covers L2.3. - `docs/decisions/2026-05-30-chapel-l23-cancel-token.md`: - ADR addendum to chapel-rehabilitation.md covering the decision rationale, the soundness argument, three race-condition counter-arguments, expected speedup, reproduction recipe, and Wave-3 follow-ups (real-corpus bench, preemption telemetry, reason-string on the token). - Cross-link from rehab ADR's Wave-2 plan to the new ADR. Verification: `chpl --library --static -o /tmp/lib_test parallel_proof_search.chpl chapel_ffi_exports.chpl -I ../zig_ffi` compiles cleanly. `just bench-chapel-mrr` still returns correct speculative winners; the trivial fixtures don't exercise the new code path enough to show a wall-clock improvement (the bench writeup predicted this — real corpus is Wave-3). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
enabled auto-merge (squash)
May 30, 2026 20:47
This was referenced May 30, 2026
hyperpolymath
added a commit
that referenced
this pull request
Sep 25, 2026
…396) ## Summary Review all 19 remaining issues without falsely closing roadmap or upstream-blocked work. - Repair eight duplicate Rust-toolchain `with:` mappings that GitHub rejects before creating jobs. - Fix workflow SPDX preamble validation for `actions-lock` managed files. - Add regression checks using the unchanged, pinned standards duplicate-key scanner. - Retire 33 obsolete ReScript exemptions after merged #362; add lossless Hypatia risk routing (runtime, FFI, proof, migration, conservative test-only review). - Link proof CI from five metadata siblings and record the currency gaps and disposition of every open issue in `docs/reports/2026-09-25-issue-maintenance.adoc`. Closes #216 (canonical owner header already on main). Closes #175 (completed informational audit following #166). Closes #196 (local cancel-token preemption already implemented by #154; benchmark and transport remain #161/#194). Closes #240 (legacy source removed by #362; obsolete exemptions removed here; real UI compilation remains #117/#266). Refs #239, #252, #314, #310. These remain open: classification is not expert review, re-arming is not a completed security burn-down, and this connection cannot rotate the owner-selected secret. ## Validation - `bash -n scripts/ci/*.sh` — pass - `bash scripts/ci/test-issue-regressions.sh` — pass, 34 workflows checked plus positive/negative fixtures - Checker rejects all eight original broken workflow files and accepts their repaired versions - Classifier preserves all original finding fields; tested routing, line preservation, unknown rules, mixed production/test paths, malformed input and empty reports - Archived 148-finding report classifies successfully (not represented as a fresh scan) - Vendored checker byte-for-byte compared to standards@2479cf769ed5f0481ccf64860a2ab954514c2b59 - `git diff --check` — pass - No `uses:` reference, Actions lock, proof, licence, secret, baseline severity, or gate strictness changed ## Known limits / pre-existing red checks Main run 36150127750 already fails baseline validation with 62 unfiltered findings at `info`. The baseline was NOT absent/skipped; it must not be broadened without evidence. The latest Security Scan has a pre-existing startup failure. Other main workflows also have failures; this PR does not claim to resolve all infrastructure. This sandbox cannot download Debian toolchain packages or GitHub release assets, so no fresh Hypatia scan or proof compilation is claimed. The integration returns 403 for Actions secrets/code-scanning alerts and cannot download Actions log blobs (job/annotation metadata is readable). Owner's #310 decision was rotate, not delete; no credential change made. ## Merge blocker discovered on this PR **All GitHub Actions runs are rejected by actor policy**, before creating any jobs: > Actor is not allowed to trigger Actions workflows. Workflow file: '.github/workflows/workflow-linter.yml'. Evidence: https://github.com/hyperpolymath/echidna/actions/runs/36185037867 (actor `arena-ai-coding-agent[bot]`). The main ruleset requires `scan / gitleaks`, `scan / rust-secrets`, and `scan / shell-secrets`. An authorized maintainer must permit this actor or trigger validation as an allowed actor. These checks are not being bypassed. Local test success must not be confused with CI success. ## Current disposition Auto-merge (squash) is enabled, but the PR is **not merged** while required Actions checks cannot run. Attempts to close the three already-resolved issues #216, #175, and #196 were also rejected with `Resource not accessible by integration` (confirmed via REST HTTP 403). **No issue was closed; all 19 remain open.** The closure keywords above are intended to close the four evidenced resolutions upon merge. Remaining roadmap, proof, credential and upstream work stays open intentionally. The GitHub connection needs Issues write permission to manage closures, and Actions policy must allow this actor (or validation must be run by an authorized maintainer). No administrative bypass was attempted. --------- Co-authored-by: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Wave-2 follow-on to PR #146. Closes the explicitly-deferred "kill
in-flight losers" gap from L2.2: once the CAS-winner is selected,
every still-polling loser observes the shared `cancelToken.cancelled`
flag on its next poll tick and SIGKILLs its own subprocess instead of
running to its per-prover timeout.
After this PR, loser wall is bounded by `pollInterval ≈ 100 ms`
rather than `max(losers)`.
What changed
`parallel_proof_search.chpl`
(not record) so all `coforall` tasks share by reference.
Sequential / best-of callers pass nil and behave identically.
each tick; on observing true, SIGKILL → preempted result with
`exitCode = -5` (distinct from -3 timeout / -4 subprocess error).
`winnerIdx.compareAndSwap` with `cancelToken.cancelled.write(true)`
so only the prover that wins the CAS triggers the signal.
`proofs/agda/ParallelSoundness.agda`
`cancellation-safety` theorem IS the L2.3 preemption claim.
No new lemma needed — `speculative (true ∷ bs) = true` for
arbitrary `bs` is exactly what preemption preserves.
ADR at `docs/decisions/2026-05-30-chapel-l23-cancel-token.md`
covering rationale, soundness, three race-condition counter-arguments,
expected speedup, reproduction recipe, Wave-3 follow-ups.
Cross-link from the rehab ADR's Wave-2 plan to the new ADR.
Test plan
🤖 Generated with Claude Code