Skip to content

lib/sync: a way to mark a cooperative-task region as must-not-yield (atomic/critical) #488

Description

@InauguralPhysicist

Surfaced by

The eddy consumer (a deterministic concurrency-control tester on the #408
cooperative task layer), milestone 2. Filed per the forcing-function model —
surfacing the gap rather than working around it. Ledger: eddy FINDINGS.md
F-EDDY-03.

The observation

Under the #408 single-thread cooperative scheduler, any region of code that
does not call task_yield (or a yielding builtin like task_sleep/task_recv)
is atomic
— no other task can interleave. eddy's snapshot-isolation store
relies on exactly this: its transaction commit (apply buffered appends to the
shared store) is correct only because the commit loop contains no yield, so
under cooperative scheduling it is one indivisible step. This is a genuinely
nice property — mutual exclusion for free, no lock needed for conflict-free
critical sections.

The gap (a silent footgun)

Nothing in the language marks a region as must-not-yield. If a maintainer
later introduces a task_yield — or calls a builtin that yields internally —
inside such a region, atomicity breaks silently: the program still compiles
and usually runs fine, and the bug shows up only as a rare, seed-dependent
anomaly (in eddy's case, an isolation violation Elle catches at some seeds but
not others). The invariant "this must run without yielding" is load-bearing but
invisible and unchecked.

Proposed

A small lib/sync (pure EigenScript over the task layer) offering:

  • critical of fn / an atomic: block — documents and delimits a must-not-yield
    region; and
  • ideally a debug-mode assertion that the delimited region issued zero
    scheduler yields (raise value if it did), so an accidental yield fails loudly
    in tests instead of silently at some seed.

This is the cooperative-concurrency counterpart to the arena-scope yield guard
(cannot task_yield inside an arena scope) that already exists — the same
"you must not suspend here" idea, made available to user code.

Not urgent for eddy milestone 2 (append-only writes commute, so no blocking
lock is needed); it becomes load-bearing at the serializable rw-register phase
(milestone 3, SSI/2PL), where real lock acquisition across yield points and a
with_lock helper will also want to live in lib/sync. Filing now while the
motivation is concrete.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions