Controlled writer completion comparison v1

One-thread test harness · 5 September 2026 · not stalled-filesystem validation

Result and scope

Eleven shared Rust/model traces pass, alongside the existing 13 synchronous traces. The harness moves the actual ledger into one worker thread and withholds completion from the driver until a trace releases it. At every snapshot, it asserts exclusive ownership and verifies that a competing ledger open fails with ledger busy.

The schedules cover acknowledgement withholding, refusal of a second writer or premature reopen, success observed after timeout, uncertain completion and retry, restart with surviving or absent work, rollover fencing, and local-evidence in-flight deduplication and recovery. A timeout leaves the driver uncertain; later successful completion does not automatically acknowledge or clear that state.

Two different controlled outcomes

With start and persist:true (the default), the worker performs the actual ledger operation, including sync, before signaling the harness that it reached the gate. It then retains ledger ownership while completion delivery is paused. The driver continues to expose its last published accounting snapshot until completion is observed. Disk state can therefore be newer than that published snapshot.

With persist:false, the worker skips the ledger call and waits at the gate. Finishing as error_lost represents abandonment before execution. This is not a lost or rolled-back durable write, and this branch does not independently validate the skipped operation. Its test inputs are valid pending fixture operations.

finish with success exposes the returned result. error_survives suppresses the acknowledgement after the actual operation and marks the driver uncertain. It is a simulated uncertain notification, not an injected filesystem error. Actual sync error injection remains covered separately by docs/ADMISSION_FSYNC_V1.md. Mismatched gate/outcome combinations are rejected; the harness never erases a successful commit to manufacture an error_lost result.

A harness restart releases and joins its controlled worker, drops the ledger, and reopens the same journal. Work performed before the gate survives; skipped work is absent. The Python projection selects the corresponding allowed surviving/lost outcome before applying its restart transition. This is controlled cleanup, not a process crash or cancellation of a syscall.

Bounds and observation limits

There is at most one worker and one ledger owner, with one bounded release channel. A second write and recovery are blocked until ownership returns. Pending queues, response slots, fixture corpus, clock granularity, and snapshot-count comparisons retain the synchronous harness's limits. Local slot membership used during a wait comes from the last published, bounded fixed-corpus view.

The test thread uses real signatures, journal writes, and syncs when persistence is selected. A real sync that hangs before the gate would block the test; the conformance subprocess deadline can terminate that test process but is not proof of safe syscall cancellation. No actual stalled fsync, interrupted kernel call, transport framing, lost device write, or power cut is tested here.

The model comparison checks published state counts, credits, writer/uncertain state, and acknowledgement counts. It does not compare response bytes or establish full Rust refinement of the model's 128,000 generated events. These changes are in the example harness; no new worker is added to deployed node binaries.

Reproduce and next work

python3 model/driver_async_vectors.py
cargo build --locked --offline --features peer-recovery --example core_conformance
python3 conformance/run.py --suite conformance/driver-async-v1.json \
  --output docs/results/driver-async-v1.json \
  target/debug/examples/core_conformance

The driver_async_trace request adds start, finish (outcome: success, error_survives, or error_lost), and recover to the existing trace operations. It reports writer, poisoned, and the observed lock_busy condition. The JSON operation name does not imply an asynchronous storage backend.

Next: bounded loopback framing and explicit buffer/task measurements, preserving these acknowledgement and ownership rules. Production driver review and actual stalled-filesystem handling remain open. Public admission is disabled.