feat(lib): lib/sync — cooperative-task locks (#488)#489
Merged
Conversation
Add a lib/sync.eigs stdlib module giving mutual exclusion ACROSS task_yield points for the #408 cooperative task layer: lock_new / lock_acquire / lock_release + with_lock of [lock, fn]. lock_acquire cooperatively yields until the lock is free then claims it — correct because there is no preemption between the acquire check passing and the claim, so the claim is atomic. with_lock runs the body under the lock and releases even if it raises, then re-raises. Surfaced by the eddy consumer (a concurrency-control DST on the task layer): only a NON-yielding region is implicitly atomic under cooperative scheduling, so a critical section that must span a yield needs an explicit lock. Filed as #488. test_sync.eigs (6 checks, wired into the suite): the hazard is real (unlocked non-atomic RMW loses updates, 50 of 100), the lock closes the race (exactly 100 with a yield inside the critical section), with_lock returns the body result + releases, and releases + re-raises on an aborting body. Full suite 2622/2622; lint + doc_drift clean; STDLIB.md entry + README table (51->52 modules). Still open under #488: a debug-mode assertion that a delimited region issued no scheduler yield (needs VM support) — the harder half; this delivers the lock. Refs #488. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This was referenced Jul 9, 2026
InauguralPhysicist
added a commit
that referenced
this pull request
Jul 9, 2026
The other half of #488 (the lib/sync locks landed in #489). A region under cooperative scheduling is atomic — mutual exclusion for free — ONLY while it issues no yield, but nothing marked such a region, so a task_yield (or a builtin that yields internally) introduced later broke atomicity SILENTLY: the program still ran and usually looked fine, failing only as a rare, seed-dependent anomaly. `must_not_yield of fn` runs `fn of null` as an atomic critical section and asserts it. A new g_no_yield_depth is incremented for the region; while nonzero, every task builtin that would actually SUSPEND raises `value` instead: - task_yield (when a scheduler is active), - blocking task_recv / blocking task_join (a live target), - task_sleep. Non-suspending ops stay legal in a region (task_try_recv, task_send, joining an already-finished task) — the guard sits on the actual-suspend path, so it never false-fires. The depth is only ever nonzero for the running task (a yield can't happen inside), so a plain counter is safe, and it is balanced even when the body raises (call_eigs_fn returns control either way). Nestable. Surfaced by the eddy consumer: its snapshot-isolation commit loop is correct only because it contains no yield. Regression (tests/test_tasks.eigs): a yield inside is caught (`value`) and the region depth is restored (a later yield works); a non-yielding region returns its body result; non-suspending ops are allowed; a blocking task_recv inside raises. Documented in docs/BUILTINS.md; discoverability gate satisfied. Full suite green release + ASan (leaks on) + jit-smoke, 2703/2703, no leak-tally increase. Closes #488 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
InauguralPhysicist
added a commit
that referenced
this pull request
Jul 9, 2026
… (#528) The other half of #488 (the lib/sync locks landed in #489). A region under cooperative scheduling is atomic — mutual exclusion for free — ONLY while it issues no yield, but nothing marked such a region, so a task_yield (or a builtin that yields internally) introduced later broke atomicity SILENTLY: the program still ran and usually looked fine, failing only as a rare, seed-dependent anomaly. `must_not_yield of fn` runs `fn of null` as an atomic critical section and asserts it. A new g_no_yield_depth is incremented for the region; while nonzero, every task builtin that would actually SUSPEND raises `value` instead: - task_yield (when a scheduler is active), - blocking task_recv / blocking task_join (a live target), - task_sleep. Non-suspending ops stay legal in a region (task_try_recv, task_send, joining an already-finished task) — the guard sits on the actual-suspend path, so it never false-fires. The depth is only ever nonzero for the running task (a yield can't happen inside), so a plain counter is safe, and it is balanced even when the body raises (call_eigs_fn returns control either way). Nestable. Surfaced by the eddy consumer: its snapshot-isolation commit loop is correct only because it contains no yield. Regression (tests/test_tasks.eigs): a yield inside is caught (`value`) and the region depth is restored (a later yield works); a non-yielding region returns its body result; non-suspending ops are allowed; a blocking task_recv inside raises. Documented in docs/BUILTINS.md; discoverability gate satisfied. Full suite green release + ASan (leaks on) + jit-smoke, 2703/2703, no leak-tally increase. Closes #488 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.
What
A
lib/sync.eigsstdlib module — cooperative-task synchronization for the #408 task layer:lock_new/lock_acquire/lock_releasewith_lock of [lock, fn]— runsfn of nullunder the lock, releasing even if the body raises, then re-raising.lock_acquirecooperatively yields until the lock is free, then claims it. It's correct because there is no preemption between the acquire check passing and the claim, so the claim is atomic — the same cooperative-scheduling property the arena-scope yield guard relies on, made available to user code.Why (surfaced by a real consumer)
The
eddyconsumer (a concurrency-control DST on the task layer) hit this directly: under cooperative scheduling, only a region that doesn't yield is implicitly atomic, so any critical section that must span atask_yieldneeds an explicit lock. Filed as #488; this delivers the lock half.Proof
test_sync.eigs(6 checks, wired into the suite):task_yieldinside the critical section;with_lockreturns the body result and releases; and on an aborting body it releases (not leaked) and re-raises.Gates
lib/sync.eigslints clean;doc_drift_checkclean.docs/STDLIB.mdentry + README module table (51 → 52).Still open under #488
A debug-mode assertion that a delimited region issued no scheduler yield (needs VM support) — the harder half, kept open. This PR is the lock.
Refs #488.
🤖 Generated with Claude Code