From 17a29d52a3c9d950c0e9cf9ab46f5413a1b97604 Mon Sep 17 00:00:00 2001 From: InauguralPhysicist Date: Wed, 8 Jul 2026 22:05:07 -0500 Subject: [PATCH] =?UTF-8?q?feat(lib):=20lib/sync=20=E2=80=94=20cooperative?= =?UTF-8?q?-task=20locks=20(#488)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- CHANGELOG.md | 13 +++++++++ README.md | 3 ++- docs/STDLIB.md | 10 +++++++ lib/sync.eigs | 59 +++++++++++++++++++++++++++++++++++++++++ tests/run_all_tests.sh | 5 ++++ tests/test_sync.eigs | 60 ++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 149 insertions(+), 1 deletion(-) create mode 100644 lib/sync.eigs create mode 100644 tests/test_sync.eigs diff --git a/CHANGELOG.md b/CHANGELOG.md index dd33af2..e87e5d2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,19 @@ All notable changes to EigenScript are documented here. ## [Unreleased] +### Added +- **`lib/sync` — cooperative-task locks (#488).** A `lib/sync.eigs` stdlib + module giving mutual exclusion **across** `task_yield` points for the #408 + task layer: `lock_new` / `lock_acquire` / `lock_release`, plus + `with_lock of [lock, fn]` (runs `fn of null` under the lock, releasing even + if the body raises, then re-raising). `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. Surfaced by the + `eddy` consumer (concurrency-control DST): a critical section that spans a + yield needs an explicit lock, since only a non-yielding region is implicitly + atomic. Still open under #488: a debug-mode *assertion* that a delimited + region issued no scheduler yield (needs VM support). + ## [0.28.0] - 2026-07-08 ### Added diff --git a/README.md b/README.md index c260d36..f63e546 100644 --- a/README.md +++ b/README.md @@ -17,7 +17,7 @@ A complete, standalone programming language with native observer semantics, real concurrency, a 44-widget GUI toolkit, embedded database, tensor math, -and a 51-module standard library (14 STEM) — all in a single zero-dependency C binary. +and a 52-module standard library (14 STEM) — all in a single zero-dependency C binary. ## Try it in your browser @@ -246,6 +246,7 @@ Pure EigenScript libraries under `lib/`: | `lib/data.eigs` | `df_from_csv`, `df_select`, `df_where`, `df_sort_by`, `df_join`, `df_group_by` | | `lib/stats.eigs` | `mean`, `median`, `std_dev`, `variance`, `histogram`, `correlation`, `describe` | | `lib/concurrent.eigs` | `future`, `await_all`, `parallel_map`, `parallel_each`, `worker_pool` | +| `lib/sync.eigs` | `lock_new`, `lock_acquire`, `lock_release`, `with_lock` | | `lib/store.eigs` | `open`, `put`, `get`, `find`, `upsert`, `bulk_put`, `to_dataframe` | | `lib/ui.eigs` | 44-widget GUI toolkit (buttons, sliders, tables, charts, trees, etc.) | | `lib/physics.eigs` | Kinematics, forces, waves, thermodynamics, EM, optics, relativity, quantum | diff --git a/docs/STDLIB.md b/docs/STDLIB.md index 97c84fd..4d1425a 100644 --- a/docs/STDLIB.md +++ b/docs/STDLIB.md @@ -742,6 +742,16 @@ Statistical functions: `mean`, `median`, `std_dev`, `variance`, `quantile`, High-level concurrency: `future`, `await_all`, `parallel_map`, `parallel_each`, `worker_pool`. +### lib/sync.eigs +Cooperative-task synchronization for the #408 task layer. A lock gives +mutual exclusion **across** `task_yield` points — while one task holds it, +another that tries to acquire cooperatively yields until it is released +(correct because there is no preemption between the acquire check passing +and the claim). `lock_new`, `lock_acquire`, `lock_release`, and +`with_lock of [lock, fn]` (runs `fn of null` under the lock, releasing even +if the body raises). Acquire only from within tasks — it spins with +`task_yield`, so it needs the scheduler active. + ### lib/store.eigs EigenStore high-level layer: `find`, `find_one`, `upsert`, `bulk_put`, `to_dataframe`. diff --git a/lib/sync.eigs b/lib/sync.eigs new file mode 100644 index 0000000..31d7620 --- /dev/null +++ b/lib/sync.eigs @@ -0,0 +1,59 @@ +# ============================================================ +# Sync Library — cooperative-task synchronization (#408 task layer) +# ============================================================ +# +# Coordination primitives for cooperative tasks (task_spawn / task_yield). A +# lock gives mutual exclusion ACROSS yield points: while one task holds it, any +# other task that tries to acquire cooperatively yields until it is released. +# Correct by the cooperative model — there is no preemption between the acquire +# check passing and the claim, so claiming the lock is itself atomic. +# +# How to use: +# load_file of "lib/sync.eigs" +# lk is lock_new of null +# lock_acquire of lk # yields cooperatively until free, then claims it +# # ... critical section: may span task_yield; the lock is held across yields +# lock_release of lk +# +# # exception-safe form (releases even if the body raises): +# with_lock of [lk, body_fn] # acquire, run body_fn of null, release +# +# NOTE: acquire spins with task_yield, so it is only meaningful while the #408 +# scheduler is active (>= 1 task_spawn). With no tasks there is nothing to yield +# to and a contended acquire would loop forever — acquire only from within tasks. + +# lock_new() — a fresh, unheld lock. +define lock_new() as: + return {"held": 0} + +# lock_acquire(lk) — claim the lock, cooperatively yielding until it is free. +define lock_acquire(lk) as: + loop while lk.held == 1: + task_yield of null + lk.held is 1 + return null + +# lock_release(lk) — release the lock. +define lock_release(lk) as: + lk.held is 0 + return null + +# with_lock([lk, fn]) — run `fn of null` while holding `lk`, releasing it even +# if the body raises (the lock is never leaked on an aborted critical section), +# then re-raise. Returns the body's result. +define with_lock(n) as: + lk is n[0] + body is n[1] + lock_acquire of lk + failed is 0 + err is null + result is null + try: + result is body of null + catch e: + failed is 1 + err is e + lock_release of lk + if failed == 1: + throw of err + return result diff --git a/tests/run_all_tests.sh b/tests/run_all_tests.sh index fa92a84..4f55b1f 100755 --- a/tests/run_all_tests.sh +++ b/tests/run_all_tests.sh @@ -2144,6 +2144,11 @@ check_eigs_suite "worker arena return deep-copied before detach" test_spawn_aren # teardown of suspended/killed tasks (incl. heap-on-saved-stack + arena-dier). check_eigs_suite "cooperative tasks: yield/join/deadlock/teardown (#408)" test_tasks.eigs "All tests passed" 1 +# lib/sync — cooperative-task lock gives mutual exclusion across yield points +# (#488): unlocked non-atomic RMW loses updates, the lock closes the race, +# with_lock releases + re-raises on abort. +check_eigs_suite "lib/sync cooperative locks (#488)" test_sync.eigs "All tests passed" 1 + # #408 determinism-by-construction: a task program with cooperative yields must # print byte-identically on two fresh processes (the signature property — the # interleaving is a pure function of program order, no tape). diff --git a/tests/test_sync.eigs b/tests/test_sync.eigs new file mode 100644 index 0000000..52742ac --- /dev/null +++ b/tests/test_sync.eigs @@ -0,0 +1,60 @@ +# lib/sync.eigs — cooperative-task locks give mutual exclusion ACROSS yield +# points; with_lock runs a body under the lock and releases even on abort. +load_file of "lib/test.eigs" +load_file of "lib/sync.eigs" + +# --- the hazard is real: a non-atomic read-yield-write increment loses updates +# WITHOUT a lock (both tasks interleave inside the critical section) --- +counter is 0 +define bump_nolock() as: + i is 0 + loop while i < 50: + c is counter + task_yield of null + counter is c + 1 + i is i + 1 + return null +a is task_spawn of bump_nolock +b is task_spawn of bump_nolock +task_join of a +task_join of b +assert_true of [counter < 100, "unlocked non-atomic RMW loses updates (the hazard is real)"] + +# --- the lock closes the race: exactly 100, even with a yield in the section --- +counter is 0 +lk is lock_new of null +define bump_locked() as: + i is 0 + loop while i < 50: + lock_acquire of lk + c is counter + task_yield of null # yield INSIDE the critical section + counter is c + 1 + lock_release of lk + i is i + 1 + return null +a2 is task_spawn of bump_locked +b2 is task_spawn of bump_locked +task_join of a2 +task_join of b2 +assert_eq of [counter, 100, "lock gives mutual exclusion across yield points (no lost updates)"] + +# --- with_lock returns the body result and releases the lock --- +lk2 is lock_new of null +define give7() as: + return 7 +assert_eq of [with_lock of [lk2, give7], 7, "with_lock returns the body result"] +assert_eq of [lk2.held, 0, "with_lock releases the lock after the body"] + +# --- with_lock releases + re-raises when the body aborts (lock not leaked) --- +wthrew is 0 +define boom() as: + throw of "boom" +try: + with_lock of [lk2, boom] +catch e: + wthrew is 1 +assert_eq of [wthrew, 1, "with_lock re-raises a body error"] +assert_eq of [lk2.held, 0, "with_lock releases the lock even when the body raises"] + +test_summary of null