Skip to content

feat(tasks): #408 increment 2 — mailboxes (task_send/recv/try_recv/kill)#475

Merged
InauguralPhysicist merged 1 commit into
mainfrom
feat-408-tasks-inc2
Jul 7, 2026
Merged

feat(tasks): #408 increment 2 — mailboxes (task_send/recv/try_recv/kill)#475
InauguralPhysicist merged 1 commit into
mainfrom
feat-408-tasks-inc2

Conversation

@InauguralPhysicist

Copy link
Copy Markdown
Collaborator

Refs #408. Cooperative tasks can now communicate — unbounded FIFO mailboxes with share-nothing message passing, reusing increment 1's suspend/resume machinery for cooperative blocking.

API

  • task_send of [id, value] — deep-copy + append to id's mailbox, wake it if it waits in task_recv. Send-to-dead (finished/unknown target) is a silent drop returning 0, not an error — Akka dead-letters / Erlang cast, per the prior-art ruling (an error path here would be a nondeterminism magnet). Never blocks (unbounded v1).
  • task_recv of null — next message, or block cooperatively on an empty mailbox (suspends via the 1b path; delivered to the stack top on resume, same placeholder mechanism as join). Arena / nested-eval guard like the other suspending builtins.
  • task_try_recv of null — non-blocking; next message or null.
  • task_kill of id — deterministic teardown: drop mailbox + suspended slice, wake any joiner with an interrupt error, mark dead.

Two bugs found and fixed during share-nothing testing

  • task_apply_recv_result fired on any resume with a non-empty mailbox — wrongly draining a message when a task resumed from a plain task_yield. Now gated strictly on recv_blocked.
  • The recv wake cleared recv_blocked, so the resume delivery (which needs it set) stopped firing. Now task_deliver leaves it set and makes the wake-enqueue idempotent via mbox_count==1 (first message to a blocked-on-empty task) — a second send before resume can't double-enqueue the task.

Verification

  • Release 2614/2614; ASan+UBSan detect_leaks=1 2614/2614 tally 0; test_tasks (now 34 checks) valgrind-clean
  • New checks: producer/consumer FIFO delivery (total 100), task_try_recv non-blocking (null/msg/null), send-to-dead drop, deep-copy-message isolation (received value is a copy, not aliased to a post-send mutation), task_kill → joiner interrupt, determinism (byte-identical across runs)
  • New executable SPEC mailbox example (byte-exact doc gate); BUILTINS/CHANGELOG updated; doc-drift + freestanding + jit-smoke green

Not in this PR

Virtual time (task_sleep, discrete-event clock) and the pluggable seeded-strategy hook for the liferaft-DST consumer — the remaining #408 increments. Then the differential proof (liferaft's chaos scenario byte-equal on the task layer) and the full determinism-verification sweep.

🤖 Generated with Claude Code

Cooperative tasks can now communicate. Unbounded FIFO mailboxes with
messages deep-copied across the boundary (share-nothing, like channels),
reusing increment 1's suspend/resume machinery for cooperative blocking.

- task_send of [id, value]: deep-copy + append to id's mailbox, wake it if
  it waits in task_recv. Send-to-dead (finished/unknown target) is a SILENT
  DROP returning 0, not an error (Akka dead-letters / Erlang cast — an error
  path here would be a nondeterminism magnet). Never blocks (unbounded v1).
- task_recv of null: next message, or block cooperatively on an empty
  mailbox — suspends via the 1b path (recv_blocked), delivered to the stack
  top on resume (task_apply_recv_result), same placeholder mechanism as join.
  Arena/nested-eval guard like the other suspending builtins.
- task_try_recv of null: non-blocking; next message or null.
- task_kill of id: deterministic teardown — drop mailbox + suspended slice,
  wake any joiner with an interrupt error, mark dead.

Two bugs found and fixed during testing (share-nothing verification):
- task_apply_recv_result fired on any resume with a non-empty mailbox,
  wrongly draining a message when a task resumed from a plain task_yield.
  Now gated strictly on recv_blocked.
- The recv wake cleared recv_blocked, so the resume delivery (which needs it
  set) no longer fired. Now task_deliver leaves recv_blocked set and makes
  the wake-enqueue idempotent via mbox_count==1 (first message to a blocked-
  on-empty task), so a second send before resume can't double-enqueue.

Still deterministic by construction — byte-identical across runs.

Verification: release 2614/2614, ASan+UBSan detect_leaks=1 2614/2614 tally 0,
test_tasks (now 34 checks: producer/consumer FIFO, try_recv non-blocking,
send-to-dead drop, deep-copy-message isolation, task_kill→interrupt) valgrind-
clean. New executable SPEC mailbox example (doc gate). doc-drift, freestanding,
jit-smoke green. BUILTINS/CHANGELOG updated.

Refs #408

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@InauguralPhysicist InauguralPhysicist merged commit 93651c2 into main Jul 7, 2026
17 checks passed
@InauguralPhysicist InauguralPhysicist deleted the feat-408-tasks-inc2 branch July 7, 2026 23:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant