Skip to content

✅ Prove Workspace effects survive a real host crash (#365 slice 7) - #419

Draft
taras wants to merge 2 commits into
agent/issue-365-6-atomic-workspacefrom
agent/issue-365-7-crash-boundary
Draft

✅ Prove Workspace effects survive a real host crash (#365 slice 7)#419
taras wants to merge 2 commits into
agent/issue-365-6-atomic-workspacefrom
agent/issue-365-7-crash-boundary

Conversation

@taras

@taras taras commented Aug 9, 2026

Copy link
Copy Markdown
Owner

Why

Issue #365 claims that one Workspace expansion produces one effect and one
caller-owned SQLite transaction, and that host interruption publishes none of
it. Every proof of that claim so far ends its transaction inside the test
process, where Effection tears the scope down — a cancellation, a failure or a
closed scope, never a crash. A crash runs no cleanup at all: it leaves an open
SQLite transaction with nobody to roll it back, and what the database holds
afterwards is SQLite's recovery rather than anything the adapter executes.

This is #365 slice 7, the final proof layer. It adds no product behavior.

What changes

Before:

  • Interruption was proven by cancellation, exception and scope teardown
    (WAC6, WAC13, WAC14). Restart was proven for the ordinary journal only
    (WJ25). Historical restoration was proven inside one process (WRR4).
  • The runtime boundary check read two files and searched them for eight names.

After:

  • WAC19–WAC21 prove the same boundary with real processes: a real SIGKILL
    during an uncommitted effect, a cold restart of a committed Workspace, and a
    cold reconstruction of an older event's root.
  • DLC13 sweeps the whole shared coordination surface, reads code rather than
    prose, and proves it can fail before it runs.

How it works

parent commits a baseline
  → crash child resumes it, writes, stops at the routed-append hook
  → parent reads the same database on a second connection
  → SIGKILL
  → inspector process reopens through the production provider

The crash timeline

Step Who State
1 parent Workspace mutation + root published, one filtered Yield appended, provider scope closed
2 crash child resumes the run; the baseline Yield replays (baselineExecutions: 0)
3 crash child BEGIN IMMEDIATE; mutation savepoint writes /crash.txt through DOFS
4 crash child root captured, current_root published, secret gate runs (gateCalls: 1)
5 crash child routed Yield inserted through transaction.journal
6 crash child kill pointafterRoutedJournalAppend reports and suspends; the transaction never reaches COMMIT
7 parent second raw read-only connection sees the baseline only
8 parent process.kill(pid, "SIGKILL"); join() reports signal: "SIGKILL", no exit code
9 inspector new process, new production provider: baseline filesystem, root, counts and journal

The child's readings at step 6 and the parent's at step 7 are of one database at
one moment, through the connection that made the writes and through a
connection that did not:

child (authoritative) parent (second connection)
/crash.txt present absent
retained roots 3 2
current_root the new root the baseline root
journal rows 2 1

Review guide

Start with: packages/workflow/tests/workspace-crash-recovery.test.ts

Then review:

  1. tests/support/workspace-crash-child.ts — the killed process and the inspector
  2. tests/support/workspace-restart-child.ts — commit, cold read, cold restoration
  3. tests/workspace-effect.test.ts DLC13 — the boundary sweep
  4. scripts/runtime-test-exclusions.ts, specs, architecture.md

Look carefully at:

  • The crash child assembles the adapter's own modules rather than calling
    useWorkflowRunStorage. The routed-append hook is installed when the
    connection registry is constructed, and the provider constructs its own; the
    child needs both that hook and the authoritative connection to read
    uncommitted rows from. The inspector and both restart processes use the
    provider itself.
  • The baseline is recorded as an unfinished run rather than as a completed
    durableRun. A journal holding a Close is a run with nothing left to
    execute, so the crash child's effect would never run at all.
  • The crash child holds an uncleared timer. Deno exits when its event loop
    empties, and a suspended Effection task is not on it.

What must stay true

  • One expansion, one effect, one caller-owned transaction — enforced by the
    slice-6 coordinator, checked across a process boundary by WAC19.
  • No second long-lived DOFS connection — the only other reader is a
    short-lived raw read-only DatabaseSync that distinguishes committed from
    uncommitted visibility.
  • No host type crosses into shared production APIs — enforced by module
    structure, checked by DLC13 over the globbed surface.

How to verify it

  • WAC19 proves a SIGKILL between the routed append and the commit
    publishes nothing, and fails if the transaction were committed before the
    parent looked. Verified by mutation: moving the child's announcement to after
    withWorkspaceEffects returns makes expect(during.outside).toEqual(before)
    fail with 5 blob refs against 2, 3 blobs against 2, and a changed current
    root.
  • WAC20 proves a cold process observes the committed filesystem, current
    root, ordered events, event identities and event-to-root associations, and
    fails if a recorded effect ran again — each effect appends its name to a
    marker file, and the first process's two lines must still be two.
  • WAC21 proves the older event's root reconstructs exactly. The negative
    lookup for /tree/file.txt happens before restoration and is answered from
    the live frontier, so the successful read afterwards is cache invalidation
    rather than a cache never consulted. The hardlink relationship is proven by
    identity rather than by inspection: resnapshotRoot === historical can only
    hold if the canonical manifest's hardlink group was reproduced. The manifests
    the historical root references and the later root does not are asserted
    non-empty, so restoration cannot have borrowed live content.
  • DLC13 proves the sweep can fail before it runs, on a crossing and on a
    comment that only looks like one, and names the modules it must have matched
    so a glob that matched nothing cannot report a clean boundary. It caught a
    real collision while being written (WorkflowRunTransaction contains
    RunTransaction).

deno task verify on this head: 12:42.91, all nine commands ok, tracked tree
unchanged
— vendor 6.6s, lint 5.4s, check 2.5s, test 762.2s, check:jsr 2.6s,
tsc 38.4s, test:node 436.3s, test:bun 627.8s, docs 35.9s. The new suite is
Deno-only and registered for Node and Bun in
scripts/runtime-test-exclusions.ts against this issue; both helpers still
typecheck under tsconfig.node.json.

This PR is stacked, so its CI does not run the jobs that target main. The
battery above is the local evidence for that gap.

Scope

Included

  • WAC19–WAC21 and their two subprocess helpers
  • The strengthened DLC13 boundary sweep
  • The Node/Bun runtime exclusion for the new Deno-only suite
  • Present-tense process-recovery statements in architecture.md,
    specs/workflow-spec.md §9.6 and specs/workflow-workspace-spec.md
    §10.1/§13, and the WAC19–WAC21 conformance rows

Intentionally unchanged

  • No production source changes at all
  • Public xmd workflow start/resume; API.Files and <File> integration
  • History, fork and root-selection commands or APIs
  • Worker Shell; Repository or Git effects; external effects
  • Schema, root format, transaction, journal and secret policy
  • Garbage collection; writable FUSE; native subprocess execution; workerd
  • WS0, WTX10, WRR4, WRR9, WRR10/10b, WJ25 and WAC1–WAC18 are untouched; this
    adds only the process-level composition they do not cover

New abstractions

  • tests/support/workspace-process.ts exists because the constants and the
    filesystem reader are shared by two child processes and the suite that
    launches them, and importing them from a child would run that child's
    main() inside the test.

Risks and limitations

  • The crash child assembles the adapter rather than installing the provider,
    for the reason above. If a future slice exposes the connection hooks through
    a provider-level seam, the child should use it.
  • code() in DLC13 does not model regular-expression literals. No module on
    the scanned surface contains one that could hide a forbidden name, and the
    scanner's own failure cases are asserted.

Scope confirmation

  • Every changed file supports the purpose described above.
  • Unrelated cleanup and formatting changes are excluded.
  • Generated or mechanical changes are clearly identified.
  • The description matches the final diff and test results.

Closes #365

Stacked on agent/issue-365-6-atomic-workspace (#415).

taras added 2 commits August 9, 2026 09:40
Every other atomic-Workspace proof ends its transaction inside the test
process, where Effection tears the scope down. A crash does none of that: it
leaves an open SQLite transaction with nobody to roll it back, and what the
database holds afterwards is SQLite's recovery rather than anything the adapter
runs.

So this is made of real processes. One resumes a committed run, performs a real
Workspace effect, and stops at the accepted construction-time routed-append
hook with the mutation, the immutable root, the current-root pointer and the
routed journal row all written and none of them committed. It says so on
standard output, a second connection is shown seeing only the baseline, and
then it is killed with SIGKILL. A different process, through a newly installed
production provider, finds the baseline filesystem, root, retained counts and
journal exactly.

Two more processes commit a Workspace history and reconstruct it cold: the
second observes the committed filesystem, current root, ordered events, event
identities and event-to-root associations without performing a recorded effect
again, then selects the older event's root through the adapter-private
materializer and rebuilds its topology, bytes, modes, hardlinks and symbolic
links from the DOFS content that root retains.

The crash child assembles the adapter's own modules rather than calling
`useWorkflowRunStorage`, because the routed-append hook is installed when the
connection registry is constructed and the provider constructs its own. The
inspector and both restart processes use the provider.

No production behavior changes.
The boundary check read two files and searched them for eight names, which
answered a smaller question than the one it was named after: whether any shared
module of the coordination surface names a host at all.

It now globs that surface — the workflow package outside its Deno adapter, and
the durable-stream coordination modules — and refuses storage and runtime
implementation types, the adapter's private connection, savepoint and
transaction-token identities, runtime detection, process globals, and imports
that reach an adapter, a vendored source or a host process.

Two things make the sweep answerable. It reads code rather than the file: these
modules explain in their own prose that they name no host, and a substring
search finds the explanation. And it proves it can fail before it runs, on a
crossing and on a comment that only looks like one, because a glob that matched
nothing would report the cleanest boundary of all.

The list of what it must have found is written down, so a module that stops
being matched fails instead of quietly leaving the surface.
@github-actions

github-actions Bot commented Aug 9, 2026

Copy link
Copy Markdown

PR #419: ✅ Prove Workspace effects survive a real host crash (#365 slice 7)

10 files, +1096 / -18

Scope

🔴 PR has 1114 lines changed. Split into focused PRs.

🟡 1114 lines changed. PRs under 400 receive more thorough review.

🟡 Changes span 6 directories.

Structural

🟡 1 console statements.

Slop

✅ Slop indicators look low.

Static Analysis

Oxlint: 2 diagnostics across 2 files (1 rule)
Density: 0.002 violations/added-line

no-floating-promises (2): packages/workflow/tests/support/workspace-crash-child.ts, packages/workflow/tests/support/workspace-restart-child.ts

Correctness

No extraneous code patterns detected.

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.

Commit Workspace mutations and journal results atomically

1 participant