feat(tasks): #408 increment 1c — adversarial hardening, determinism gate, SPEC#474
Merged
Conversation
…ate, SPEC Planted-fault verification of increment 1's two safety guards — proving each is load-bearing, not decoration (eigen-determinism-verification discipline: validate every checker with a planted fault) — plus the determinism gate and the SPEC executable Tasks section. Real bug found and fixed by the verification: - A task that ENDS (returns or dies) inside an active arena scope — e.g. the arena-suspend guard raises after arena_mark with no arena_reset — left the per-thread arena active. sched_finish then built the task's error dict via vm_take_error_value while g_arena.active, ARENA-allocating a value that crosses to the joiner (a later arena_reset would dangle it), and left the arena contaminating the next task's allocations. sched_finish now forces g_arena.active=0 before capturing result/error. Caught only under the EIGS_VALGRIND arena-interior poison gate (ASan can't see arena interiors). Planted-fault proofs (each verified by remove→detect→restore): - Save-buffer teardown decref (task_free): removing it leaks 99 bytes when a task is killed-outstanding while suspended with a heap value on its saved value stack (["str", task_yield] leaves the string on the stack at suspend). ASan-caught. Load-bearing. - Arena-suspend guard: removing it lets a task yield inside an arena scope; a sibling's arena_reset then reclaims its arena values, and the resumed read is an arena-interior use-after-reset. valgrind-caught (rc=99). Load-bearing. Regression coverage (test_tasks.eigs, now 23 checks): the heap-on-saved-stack kill-outstanding case (ASan gate) and the unjoined arena-dier + clean-arena- after case (valgrind gate) lock both fixes. New suite-level determinism check: task_pipeline.eigs prints byte-identically across two fresh processes. SPEC.md gains an executable Cooperative tasks section (byte-exact doc gate); CHANGELOG updated. Verification: release 2613/2613, ASan detect_leaks=1 2613/2613 tally 0, test_tasks valgrind-clean, doc-examples 64/64, doc-drift + freestanding + jit-smoke green. Refs #408 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.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.
Refs #408. Planted-fault verification of increment 1's two safety guards (proving each is load-bearing), the determinism suite gate, and the SPEC executable Tasks section. Completes increment 1.
A real bug the verification found
Adversarial valgrind testing surfaced a genuine correctness bug (not a test artifact): a task that ends inside an active arena scope — e.g. the arena-suspend guard raises after
arena_markwith noarena_reset— left the per-thread arena active.sched_finishthen built the task's error dict viavm_take_error_valuewhileg_arena.active, arena-allocating a value that crosses to the joiner (a laterarena_resetwould dangle it) and leaving the arena contaminating the next task's allocations. Fix:sched_finishforcesg_arena.active=0before capturing the result/error. Only theEIGS_VALGRINDarena-interior poison gate catches this — ASan can't see arena interiors.Planted-fault proofs (remove → detect → restore)
Both guards from increment 1 verified load-bearing, not decoration:
task_free): removing it leaks 99 bytes when a task is killed-outstanding while suspended with a heap value on its saved value stack (["str", task_yield]leaves the string on the stack at suspend). ASan-caught.arena_resetreclaims its arena values, and the resumed read is an arena-interior use-after-reset. valgrind-caught (rc=99).Regression coverage locks both fixes
test_tasks.eigs(now 23 checks) adds the heap-on-saved-stack kill-outstanding case (ASan gate) and the unjoined arena-dier + clean-arena-after case (valgrind gate). New suite-level determinism check:task_pipeline.eigsprints byte-identically across two fresh processes — the signature property, now guarded against future regressions.Docs
SPEC.md gains an executable Cooperative tasks section (byte-exact doc gate — interleaving order, join, deadlock). CHANGELOG updated.
Verification
Release 2613/2613; ASan
detect_leaks=12613/2613 tally 0;test_tasksvalgrind-clean; doc-examples 64/64; doc-drift + freestanding + jit-smoke green.Increment 1 complete
Remaining on #408: increment 2 — mailboxes (
task_send/task_recv), then virtual time and the pluggable seeded-strategy hook for the DST consumer. The full rigorous determinism sweep (seeded exhaustive injection, N-record accounting) is available to route to the determinism-verification engineer when increment 2 adds recorded state.🤖 Generated with Claude Code