From 9d7a12b27fdd54159b7b58643e70bfd1295b39d4 Mon Sep 17 00:00:00 2001 From: Kevin Blackburn-Matzen Date: Sat, 18 Jul 2026 11:47:17 -0700 Subject: [PATCH] Route worker responses by correlation id MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The WorkerBridge held a single responseHandler slot and dispatched worker responses by message *type* alone, so concurrent requests displaced and settled each other. TLA+ models of the old and new protocols are in specs/; TLC produced two counterexamples against the old design, both replayed as tests in workerBridge.test.ts: - Two evaluates in flight: the first's `sdf` response reached the second's handler, passed its `seq === evalSeq` check (it *was* the newest), and resolved the second promise with the first's geometry. The staleness guard checked whether the handler was current, never whether the response matched it. - An export displaced by an edit: `useEvaluator` fires on any store change and overwrote the export's handler, so the `exportResult` matched neither branch of the evaluate handler and was discarded. Toolbar's await never returned. Every request now carries an rid that the worker echoes on all responses including progress and errors, and the handler slot becomes a map keyed by rid. Superseded evaluates resolve(null) instead of returning unsettled — useEvaluator already has its own evalSeq guard. worker.onerror now rejects everything outstanding rather than only logging. Co-Authored-By: Claude Opus 4.8 --- specs/.gitignore | 2 + specs/README.md | 104 ++++++++++++++++++++ specs/WorkerBridge.cfg | 9 ++ specs/WorkerBridge.tla | 168 ++++++++++++++++++++++++++++++++ specs/WorkerBridgeFixed.cfg | 10 ++ specs/WorkerBridgeFixed.tla | 141 +++++++++++++++++++++++++++ specs/WorkerBridge_orphan.cfg | 8 ++ specs/check.sh | 38 ++++++++ src/engine/workerBridge.test.ts | 162 ++++++++++++++++++++++++++++++ src/engine/workerBridge.ts | 141 +++++++++++++++++++-------- src/types/geometry.ts | 20 ++-- src/worker/sdfWorker.ts | 21 ++-- 12 files changed, 766 insertions(+), 58 deletions(-) create mode 100644 specs/.gitignore create mode 100644 specs/README.md create mode 100644 specs/WorkerBridge.cfg create mode 100644 specs/WorkerBridge.tla create mode 100644 specs/WorkerBridgeFixed.cfg create mode 100644 specs/WorkerBridgeFixed.tla create mode 100644 specs/WorkerBridge_orphan.cfg create mode 100755 specs/check.sh create mode 100644 src/engine/workerBridge.test.ts diff --git a/specs/.gitignore b/specs/.gitignore new file mode 100644 index 0000000..fd09fae --- /dev/null +++ b/specs/.gitignore @@ -0,0 +1,2 @@ +tla2tools.jar +states/ diff --git a/specs/README.md b/specs/README.md new file mode 100644 index 0000000..f44f566 --- /dev/null +++ b/specs/README.md @@ -0,0 +1,104 @@ +# TLA+ specifications + +Formal models of Sinter's concurrent protocols, checked with TLC. + +## Running + +Requires a JVM. `./check.sh` downloads `tla2tools.jar` into this directory on +first run (it is gitignored — do not commit the 2MB jar). + +```sh +./check.sh # run every spec +./check.sh WorkerBridgeFixed # run one +``` + +## WorkerBridge — `src/engine/workerBridge.ts` + +Models the singleton bridge that multiplexes `evaluate`, `exportSTL`, and +`export3MF` over one Web Worker. + +Two safety properties are specified: + +- **`NoOrphan`** — when nothing is in flight, no issued request is still + pending. Equivalently: every promise returned by the bridge eventually + settles. +- **`NoCrossTalk`** — a request is settled by its own response, never by + another request's. + +### `WorkerBridge.tla` — current design. **Both properties fail.** + +The bridge holds a *single* `responseHandler` slot (`workerBridge.ts:12`) and +dispatches responses by message *type* alone — there are no correlation ids. +Every call overwrites the slot (`:35`, `:55`, `:67`). + +`NoCrossTalk` fails in 5 states: + +| # | action | effect | +|---|--------|--------| +| 2 | `evaluate` #1 | `evalSeq = 1`, handler ← #1 | +| 3 | `evaluate` #2 | `evalSeq = 2`, handler ← #2 (**#1's handler is gone**) | +| 4 | worker answers #1 | `sdf` response for request #1 queued | +| 5 | bridge delivers it | handler is #2's; `seq === evalSeq` passes, so **#2's promise resolves with #1's geometry** | + +`NoOrphan` fails on the same prefix: #1 never settles, and when #2's own +response arrives its `resolve` is a no-op because #2 is already settled. + +The other instance of `NoOrphan` — the one most likely to be seen in +practice — is an **export orphaned by an edit**. `exportSTL` installs its +handler; `useEvaluator` fires on the next store change (`useEvaluator.ts:40`) +and overwrites it; the worker's `exportResult` then reaches an *evaluate* +handler, matches neither the `msg.type === 'sdf'` nor the +`msg.type === 'error'` branch, and is silently discarded. The `await` in +`Toolbar.tsx:68` never returns. + +A third path, visible in the model as the `handler.seq # evalSeq` branch: a +superseded evaluate returns at `:37` *without* settling. If the newest +evaluate is itself orphaned, `evaluating` is never cleared and the viewport +spinner (`Viewport.tsx:36`) spins forever. + +Note that none of these require the worker to misbehave. The worker is +correct and FIFO throughout; the defect is entirely in the bridge's +dispatch. + +### `WorkerBridgeFixed.tla` — corrected design. **All properties hold.** + +Checked exhaustively at `MaxReq = 4` (2,535 distinct states, depth 13), +including the liveness property `AllRequestsSettle` under weak fairness. + +Three changes: + +1. Requests carry a correlation id; the worker echoes it on every response, + errors included. +2. The single handler slot becomes a **map** from correlation id to handler. + Issuing registers; delivering settles and deregisters exactly one entry. + Nothing is displaced. +3. A superseded `evaluate` still settles (`resolve(null)`) rather than + returning without settling. Staleness becomes a caller-side concern — + `useEvaluator` already has its own `evalSeqRef` guard + (`useEvaluator.ts:28,33`). + +The protocol is implemented in `src/engine/workerBridge.ts`, with the +correlation id (`rid`) threaded through `src/types/geometry.ts` and echoed by +`src/worker/sdfWorker.ts`. Both counterexamples above are replayed as +executable regression tests in `src/engine/workerBridge.test.ts` — they fail +against the old design and pass against the new one. + +`HandlerAgreesWithSettled` is the invariant that makes the other two hold, +and the one an implementation must preserve: an id is registered **iff** its +promise has not settled. Deleting a map entry without settling it, or +settling without deleting, breaks it. + +### Not modelled + +- **Cancellation.** The worker processes its queue synchronously to + completion (`sdfWorker.ts:165`); there is no way to drop queued work. The + fixed spec makes every request settle, but a 256³ export still blocks + every evaluate behind it. Real cancellation needs either a `cancel` + message checked inside `evaluateCPUWithProgress`'s recursion + (`sdfWorker.ts:93`) or worker termination and respawn. Worth a follow-up + spec once the design is chosen. +- **`progressHandler`**, which has the same single-slot problem + (`workerBridge.ts:13`, `:54`, `:66`) and is cleared by whichever export + finishes first. The correlation-id fix applies unchanged. +- **`worker.onerror`** (`:28`), which only logs. Under the fixed protocol it + should reject every registered handler and clear the map. diff --git a/specs/WorkerBridge.cfg b/specs/WorkerBridge.cfg new file mode 100644 index 0000000..e2e1079 --- /dev/null +++ b/specs/WorkerBridge.cfg @@ -0,0 +1,9 @@ +SPECIFICATION Spec + +CONSTANT MaxReq = 3 + +INVARIANT TypeOK +INVARIANT NoOrphan +INVARIANT NoCrossTalk + +PROPERTY AllRequestsSettle diff --git a/specs/WorkerBridge.tla b/specs/WorkerBridge.tla new file mode 100644 index 0000000..1d62247 --- /dev/null +++ b/specs/WorkerBridge.tla @@ -0,0 +1,168 @@ +--------------------------- MODULE WorkerBridge --------------------------- +(***************************************************************************) +(* Model of the CURRENT design of src/engine/workerBridge.ts. *) +(* *) +(* The bridge is a singleton multiplexing three request kinds (evaluate, *) +(* exportSTL, export3MF -- the two exports behave identically here, so *) +(* they are collapsed into one "export" kind) over a single Worker, using *) +(* ONE `responseHandler` slot and NO correlation identifiers. Responses *) +(* are dispatched purely by message *type*. *) +(* *) +(* This spec is expected to FAIL. Both NoOrphan and NoCrossTalk have *) +(* counterexamples at MaxReq = 2. See WorkerBridgeFixed.tla for the *) +(* corrected protocol. *) +(***************************************************************************) +EXTENDS Naturals, Sequences + +CONSTANT MaxReq \* how many requests the client may issue + +Ids == 1..MaxReq + +\* The empty handler slot: `responseHandler = null` (workerBridge.ts:12). +NoHandler == [kind |-> "none", id |-> 0, seq |-> 0] + +\* A request that has neither resolved nor rejected. +Pending == [state |-> "pending", by |-> 0] + +VARIABLES + nextId, \* next request id to allocate + kind, \* id -> "evaluate" | "export" + reqQueue, \* postMessage queue, main thread -> worker + respQueue, \* postMessage queue, worker -> main thread + handler, \* THE single responseHandler slot + evalSeq, \* this.evalSeq (workerBridge.ts:14) + settled \* id -> [state, by]; `by` records WHICH request's response settled it + +vars == <> + +\* The ids actually handed out so far. +Issued == 1..(nextId - 1) + +Init == + /\ nextId = 1 + /\ kind = [i \in Ids |-> "evaluate"] + /\ reqQueue = <<>> + /\ respQueue = <<>> + /\ handler = NoHandler + /\ evalSeq = 0 + /\ settled = [i \in Ids |-> Pending] + +(***************************************************************************) +(* Client actions. *) +(* *) +(* Note that BOTH issue actions overwrite `handler` unconditionally -- *) +(* this is workerBridge.ts:35, :55 and :67. The previous handler is *) +(* dropped on the floor, along with the promise it was going to settle. *) +(***************************************************************************) + +IssueEvaluate == \* workerBridge.ts:31-49 + /\ nextId <= MaxReq + /\ kind' = [kind EXCEPT ![nextId] = "evaluate"] + /\ evalSeq' = evalSeq + 1 \* const seq = ++this.evalSeq + /\ handler' = [kind |-> "evaluate", id |-> nextId, seq |-> evalSeq + 1] + /\ reqQueue' = Append(reqQueue, nextId) + /\ nextId' = nextId + 1 + /\ UNCHANGED <> + +IssueExport == \* workerBridge.ts:51-73 + /\ nextId <= MaxReq + /\ kind' = [kind EXCEPT ![nextId] = "export"] + /\ handler' = [kind |-> "export", id |-> nextId, seq |-> 0] + /\ reqQueue' = Append(reqQueue, nextId) + /\ nextId' = nextId + 1 + /\ UNCHANGED <> + +(***************************************************************************) +(* The worker. Single-threaded, strictly FIFO, no cancellation: once a *) +(* request is queued it WILL be processed to completion (sdfWorker.ts:165).*) +(* It answers with the response type for that request's kind, or errors. *) +(***************************************************************************) + +RespTypeOf(k) == IF k = "evaluate" THEN "sdf" ELSE "exportResult" + +WorkerProcess == + /\ reqQueue # <<>> + /\ \E t \in {RespTypeOf(kind[Head(reqQueue)]), "error"} : + respQueue' = Append(respQueue, [id |-> Head(reqQueue), type |-> t]) + /\ reqQueue' = Tail(reqQueue) + /\ UNCHANGED <> + +(***************************************************************************) +(* Bridge onmessage (workerBridge.ts:21-26) plus the installed handler. *) +(* *) +(* Settling is idempotent: calling resolve()/reject() on an already- *) +(* settled promise is a no-op in JS, so a second attempt changes nothing. *) +(***************************************************************************) + +Settle(i, st, src) == + IF settled[i].state = "pending" + THEN settled' = [settled EXCEPT ![i] = [state |-> st, by |-> src]] + ELSE UNCHANGED settled + +Deliver(msg) == + IF handler = NoHandler + THEN UNCHANGED settled \* `if (this.responseHandler)` fails + ELSE IF handler.kind = "evaluate" + THEN IF handler.seq # evalSeq + THEN UNCHANGED settled \* :37 stale -- returns WITHOUT settling + ELSE IF msg.type = "sdf" + THEN Settle(handler.id, "resolved", msg.id) + ELSE IF msg.type = "error" + THEN Settle(handler.id, "rejected", msg.id) + ELSE UNCHANGED settled \* exportResult hits neither branch + ELSE IF msg.type = "exportResult" + THEN Settle(handler.id, "resolved", msg.id) + ELSE IF msg.type = "error" + THEN Settle(handler.id, "rejected", msg.id) + ELSE UNCHANGED settled \* sdf hits neither branch + +BridgeDeliver == + /\ respQueue # <<>> + /\ Deliver(Head(respQueue)) + /\ respQueue' = Tail(respQueue) + /\ UNCHANGED <> + +\* Allow stuttering once all work is issued and drained, so TLC does not +\* report a spurious deadlock. +Terminating == + /\ nextId > MaxReq + /\ reqQueue = <<>> + /\ respQueue = <<>> + /\ UNCHANGED vars + +Next == IssueEvaluate \/ IssueExport \/ WorkerProcess \/ BridgeDeliver \/ Terminating + +Spec == Init /\ [][Next]_vars /\ WF_vars(WorkerProcess) /\ WF_vars(BridgeDeliver) + +(***************************************************************************) +(* Properties. *) +(***************************************************************************) + +TypeOK == + /\ nextId \in 1..(MaxReq + 1) + /\ kind \in [Ids -> {"evaluate", "export"}] + /\ evalSeq \in 0..MaxReq + /\ \A i \in Ids : settled[i].state \in {"pending", "resolved", "rejected"} + +\* Nothing is in flight: every request has been processed and every response +\* has been delivered to the bridge. +Quiescent == reqQueue = <<>> /\ respQueue = <<>> + +\* SAFETY 1. When the system is at rest, no issued request is still pending. +\* Equivalently: every promise returned by evaluate/exportSTL/export3MF +\* eventually settles. VIOLATED -- an export in flight when an evaluate is +\* issued has its handler overwritten, and its exportResult then falls +\* through the evaluate handler's if/else-if chain and is discarded. +NoOrphan == Quiescent => \A i \in Issued : settled[i].state # "pending" + +\* SAFETY 2. A request is settled by its OWN response, never another's. +\* VIOLATED -- two evaluates in flight: the first's `sdf` response is +\* delivered to the second's handler, which passes the `seq === evalSeq` +\* check (it IS the newest) and resolves the second promise with the first +\* request's geometry. +NoCrossTalk == \A i \in Issued : settled[i].state # "pending" => settled[i].by = i + +\* LIVENESS. The same claim as NoOrphan, stated temporally. +AllRequestsSettle == <>[](\A i \in Issued : settled[i].state # "pending") + +============================================================================= diff --git a/specs/WorkerBridgeFixed.cfg b/specs/WorkerBridgeFixed.cfg new file mode 100644 index 0000000..8d90910 --- /dev/null +++ b/specs/WorkerBridgeFixed.cfg @@ -0,0 +1,10 @@ +SPECIFICATION Spec + +CONSTANT MaxReq = 4 + +INVARIANT TypeOK +INVARIANT NoOrphan +INVARIANT NoCrossTalk +INVARIANT HandlerAgreesWithSettled + +PROPERTY AllRequestsSettle diff --git a/specs/WorkerBridgeFixed.tla b/specs/WorkerBridgeFixed.tla new file mode 100644 index 0000000..7e4a048 --- /dev/null +++ b/specs/WorkerBridgeFixed.tla @@ -0,0 +1,141 @@ +------------------------ MODULE WorkerBridgeFixed ------------------------- +(***************************************************************************) +(* Corrected WorkerBridge protocol. *) +(* *) +(* Three changes relative to WorkerBridge.tla: *) +(* *) +(* 1. Every request carries a correlation id. The worker echoes it back *) +(* on every response (including errors). *) +(* 2. The single `responseHandler` slot becomes a MAP from correlation *) +(* id to handler. Issuing a request registers an entry; delivering a *) +(* response settles and removes exactly that entry. Nothing is ever *) +(* overwritten. *) +(* 3. A superseded evaluate still SETTLES (resolve(null)) instead of *) +(* returning without settling. Staleness becomes a caller-side *) +(* concern -- useEvaluator.ts already has its own evalSeqRef guard at *) +(* src/engine/useEvaluator.ts:28,33 -- rather than a reason to strand *) +(* a promise. *) +(* *) +(* Both safety properties and the liveness property hold. *) +(***************************************************************************) +EXTENDS Naturals, Sequences + +CONSTANT MaxReq + +Ids == 1..MaxReq + +Pending == [state |-> "pending", by |-> 0] + +VARIABLES + nextId, + kind, + reqQueue, + respQueue, + inflight, \* SET of correlation ids with a registered handler + evalSeq, + settled + +vars == <> + +Issued == 1..(nextId - 1) + +Init == + /\ nextId = 1 + /\ kind = [i \in Ids |-> "evaluate"] + /\ reqQueue = <<>> + /\ respQueue = <<>> + /\ inflight = {} + /\ evalSeq = 0 + /\ settled = [i \in Ids |-> Pending] + +(***************************************************************************) +(* Client actions. Registration is additive -- no handler is displaced. *) +(***************************************************************************) + +IssueEvaluate == + /\ nextId <= MaxReq + /\ kind' = [kind EXCEPT ![nextId] = "evaluate"] + /\ evalSeq' = evalSeq + 1 + /\ inflight' = inflight \cup {nextId} + /\ reqQueue' = Append(reqQueue, nextId) + /\ nextId' = nextId + 1 + /\ UNCHANGED <> + +IssueExport == + /\ nextId <= MaxReq + /\ kind' = [kind EXCEPT ![nextId] = "export"] + /\ inflight' = inflight \cup {nextId} + /\ reqQueue' = Append(reqQueue, nextId) + /\ nextId' = nextId + 1 + /\ UNCHANGED <> + +(***************************************************************************) +(* Worker. Unchanged, except that the correlation id is echoed back -- *) +(* which the model already did, since responses were tagged with `id`. *) +(***************************************************************************) + +RespTypeOf(k) == IF k = "evaluate" THEN "sdf" ELSE "exportResult" + +WorkerProcess == + /\ reqQueue # <<>> + /\ \E t \in {RespTypeOf(kind[Head(reqQueue)]), "error"} : + respQueue' = Append(respQueue, [id |-> Head(reqQueue), type |-> t]) + /\ reqQueue' = Tail(reqQueue) + /\ UNCHANGED <> + +(***************************************************************************) +(* Bridge dispatch, keyed by correlation id. Note there is no longer any *) +(* dependence on the message *type* for routing, and no fall-through case: *) +(* a registered request is always settled by its own response. *) +(***************************************************************************) + +Deliver(msg) == + IF msg.id \in inflight + THEN /\ settled' = [settled EXCEPT ![msg.id] = + [state |-> IF msg.type = "error" THEN "rejected" + ELSE "resolved", + by |-> msg.id]] + /\ inflight' = inflight \ {msg.id} + ELSE UNCHANGED <> + +BridgeDeliver == + /\ respQueue # <<>> + /\ Deliver(Head(respQueue)) + /\ respQueue' = Tail(respQueue) + /\ UNCHANGED <> + +Terminating == + /\ nextId > MaxReq + /\ reqQueue = <<>> + /\ respQueue = <<>> + /\ UNCHANGED vars + +Next == IssueEvaluate \/ IssueExport \/ WorkerProcess \/ BridgeDeliver \/ Terminating + +Spec == Init /\ [][Next]_vars /\ WF_vars(WorkerProcess) /\ WF_vars(BridgeDeliver) + +(***************************************************************************) +(* Properties -- identical statements to WorkerBridge.tla. *) +(***************************************************************************) + +TypeOK == + /\ nextId \in 1..(MaxReq + 1) + /\ kind \in [Ids -> {"evaluate", "export"}] + /\ inflight \subseteq Ids + /\ evalSeq \in 0..MaxReq + /\ \A i \in Ids : settled[i].state \in {"pending", "resolved", "rejected"} + +Quiescent == reqQueue = <<>> /\ respQueue = <<>> + +NoOrphan == Quiescent => \A i \in Issued : settled[i].state # "pending" +NoCrossTalk == \A i \in Issued : settled[i].state # "pending" => settled[i].by = i + +\* An id is registered iff its promise has not settled. This is the +\* invariant that makes the other two hold, and the one an implementation +\* must not break (e.g. by deleting a map entry without settling). +HandlerAgreesWithSettled == + \A i \in Issued : (i \in inflight) <=> (settled[i].state = "pending") + +AllRequestsSettle == <>[](\A i \in Issued : settled[i].state # "pending") + +============================================================================= diff --git a/specs/WorkerBridge_orphan.cfg b/specs/WorkerBridge_orphan.cfg new file mode 100644 index 0000000..5048b19 --- /dev/null +++ b/specs/WorkerBridge_orphan.cfg @@ -0,0 +1,8 @@ +\* Checks only the "every promise settles" property, so TLC reports the +\* orphaned-export counterexample rather than stopping at the cross-talk one. +SPECIFICATION Spec + +CONSTANT MaxReq = 3 + +INVARIANT TypeOK +INVARIANT NoOrphan diff --git a/specs/check.sh b/specs/check.sh new file mode 100755 index 0000000..c08bedb --- /dev/null +++ b/specs/check.sh @@ -0,0 +1,38 @@ +#!/usr/bin/env bash +# Run the TLA+ specs through TLC. Usage: ./check.sh [SpecName ...] +set -uo pipefail +cd "$(dirname "$0")" + +JAR=tla2tools.jar +if [ ! -f "$JAR" ]; then + echo "Downloading $JAR..." + curl -fsSL -o "$JAR" \ + https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar +fi + +# WorkerBridge models the current, known-broken design: its counterexamples +# are the point, so a TLC failure there is the expected outcome. +declare -a SPECS +if [ $# -gt 0 ]; then SPECS=("$@"); else SPECS=(WorkerBridge WorkerBridgeFixed); fi + +status=0 +for spec in "${SPECS[@]}"; do + echo "=== $spec ===" + java -XX:+UseParallelGC -cp "$JAR" tlc2.TLC -nowarning \ + -config "$spec.cfg" "$spec.tla" + rc=$? + case "$spec" in + WorkerBridge) + if [ $rc -eq 0 ]; then + echo "!! $spec was expected to produce a counterexample but passed." + status=1 + else + echo "(counterexample expected -- see README.md)" + fi + ;; + *) + [ $rc -ne 0 ] && status=1 + ;; + esac +done +exit $status diff --git a/src/engine/workerBridge.test.ts b/src/engine/workerBridge.test.ts new file mode 100644 index 0000000..2b1594b --- /dev/null +++ b/src/engine/workerBridge.test.ts @@ -0,0 +1,162 @@ +import { describe, it, expect, beforeEach, vi } from 'vitest'; +import type { WorkerRequest } from '../types/geometry'; + +/** + * Regression tests for the WorkerBridge correlation-id protocol. + * + * The first two cases are the counterexamples TLC produced against the old + * single-handler design (specs/WorkerBridge.tla), replayed against the real + * bridge. Both fail on that design and pass on the current one. + */ + +class FakeWorker { + static latest: FakeWorker; + onmessage: ((e: MessageEvent) => void) | null = null; + onerror: ((e: any) => void) | null = null; + sent: WorkerRequest[] = []; + + constructor() { FakeWorker.latest = this; } + postMessage(msg: WorkerRequest) { this.sent.push(msg); } + terminate() {} + + emit(msg: any) { this.onmessage?.({ data: msg } as MessageEvent); } + fail(message: string) { this.onerror?.({ message }); } +} + +/** Let queued microtasks and timers run. */ +const flush = () => new Promise((r) => setTimeout(r, 0)); + +/** Observe a promise's outcome without awaiting it. */ +function track(p: Promise) { + const state = { settled: false, value: undefined as T | undefined, error: undefined as any }; + p.then( + (v) => { state.settled = true; state.value = v; }, + (e) => { state.settled = true; state.error = e; }, + ); + return state; +} + +function sdfResponse(rid: number, glsl: string) { + return { + type: 'sdf', rid, glsl, + paramCount: 0, paramValues: [], + bbMin: [0, 0, 0], bbMax: [1, 1, 1], + }; +} + +let bridge: typeof import('./workerBridge').workerBridge; +let worker: FakeWorker; + +beforeEach(async () => { + vi.resetModules(); + vi.stubGlobal('Worker', FakeWorker); + bridge = (await import('./workerBridge')).workerBridge; + worker = FakeWorker.latest; + worker.emit({ type: 'ready' }); + await flush(); +}); + +describe('WorkerBridge correlation ids', () => { + it('does not settle one evaluate with another evaluate\'s response', async () => { + // TLC counterexample for NoCrossTalk (specs/WorkerBridge.tla). + const first = track(bridge.evaluate(null)); + const second = track(bridge.evaluate(null)); + await flush(); + expect(worker.sent).toHaveLength(2); + + // The worker answers the FIRST request while the second is still in flight. + worker.emit(sdfResponse(worker.sent[0].rid, 'FIRST')); + worker.emit(sdfResponse(worker.sent[1].rid, 'SECOND')); + await flush(); + + // The old design resolved `second` with FIRST's geometry here. + expect(second.value?.glsl).toBe('SECOND'); + // The superseded evaluate still settles, with null rather than stale data. + expect(first.settled).toBe(true); + expect(first.value).toBeNull(); + }); + + it('settles an export whose handler would have been displaced by an evaluate', async () => { + // TLC counterexample for NoOrphan: the export's handler is overwritten by + // the evaluate, and its exportResult then matches neither branch of the + // evaluate handler. + const data = new ArrayBuffer(8); + const exported = track(bridge.exportSTL(null)); + await flush(); + const exportRid = worker.sent[0].rid; + + const evaluated = track(bridge.evaluate(null)); + await flush(); + + worker.emit({ type: 'exportResult', rid: exportRid, format: 'stl', data }); + await flush(); + + // The old design left this pending forever — Toolbar's await never returned. + expect(exported.settled).toBe(true); + expect(exported.value).toBeInstanceOf(Blob); + + worker.emit(sdfResponse(worker.sent[1].rid, 'GLSL')); + await flush(); + expect(evaluated.settled).toBe(true); + }); + + it('routes progress to the originating export only', async () => { + const stl: string[] = []; + const mf: string[] = []; + void bridge.exportSTL(null, (stage) => stl.push(stage)); + await flush(); + void bridge.export3MF(null, (stage) => mf.push(stage)); + await flush(); + + worker.emit({ type: 'progress', rid: worker.sent[0].rid, stage: 'stl-stage', percent: 10 }); + worker.emit({ type: 'progress', rid: worker.sent[1].rid, stage: '3mf-stage', percent: 20 }); + await flush(); + + expect(stl).toEqual(['stl-stage']); + expect(mf).toEqual(['3mf-stage']); + }); + + it('rejects only the request that errored', async () => { + const exported = track(bridge.exportSTL(null)); + await flush(); + const evaluated = track(bridge.evaluate(null)); + await flush(); + + worker.emit({ type: 'error', rid: worker.sent[0].rid, message: 'No geometry to export' }); + await flush(); + + expect(exported.error?.message).toBe('No geometry to export'); + expect(evaluated.settled).toBe(false); + + worker.emit(sdfResponse(worker.sent[1].rid, 'GLSL')); + await flush(); + expect(evaluated.value?.glsl).toBe('GLSL'); + }); + + it('rejects every outstanding request when the worker itself fails', async () => { + const exported = track(bridge.exportSTL(null)); + const evaluated = track(bridge.evaluate(null)); + await flush(); + + worker.fail('boom'); + await flush(); + + expect(exported.error?.message).toBe('boom'); + expect(evaluated.error?.message).toBe('boom'); + }); + + it('ignores a duplicate response for an already-settled request', async () => { + const evaluated = track(bridge.evaluate(null)); + await flush(); + const rid = worker.sent[0].rid; + + worker.emit(sdfResponse(rid, 'GLSL')); + await flush(); + expect(evaluated.value?.glsl).toBe('GLSL'); + + // Must not throw, and must not disturb any later request's entry. + expect(() => worker.emit(sdfResponse(rid, 'AGAIN'))).not.toThrow(); + await flush(); + expect(evaluated.value?.glsl).toBe('GLSL'); + }); +}); diff --git a/src/engine/workerBridge.ts b/src/engine/workerBridge.ts index 1d67f30..7b1ffb7 100644 --- a/src/engine/workerBridge.ts +++ b/src/engine/workerBridge.ts @@ -2,15 +2,34 @@ import type { WorkerRequest, WorkerResponse, ClipPlane } from '../types/geometry import type { SDFNodeUI } from '../types/operations'; import type { SDFDisplayData } from '../store/modelerStore'; -type ResponseHandler = (response: WorkerResponse) => void; type ProgressHandler = (stage: string, percent: number) => void; +/** + * One in-flight request. Registered under its correlation id when the request + * is posted, removed when — and only when — its promise settles. + * + * Invariant (HandlerAgreesWithSettled in specs/WorkerBridgeFixed.tla): + * an id is present in `pending` iff its promise has not settled. Every path + * that deletes an entry must settle it, and vice versa. + */ +interface PendingRequest { + kind: 'evaluate' | 'export'; + /** For evaluates: the evalSeq at issue time, used to detect supersession. */ + seq: number; + /** Blob MIME type for exports. */ + mime: string; + resolve: (value: any) => void; + reject: (error: Error) => void; + onProgress?: ProgressHandler; +} + class WorkerBridge { private worker: Worker; private readyPromise: Promise; private resolveReady!: () => void; - private responseHandler: ResponseHandler | null = null; - private progressHandler: ProgressHandler | null = null; + /** Correlation id -> in-flight request. Replaces the old single handler slot. */ + private pending = new Map(); + private nextRid = 1; private evalSeq = 0; constructor() { @@ -21,55 +40,97 @@ class WorkerBridge { this.worker.onmessage = (event: MessageEvent) => { const msg = event.data; if (msg.type === 'ready') { this.resolveReady(); return; } - if (msg.type === 'progress') { if (this.progressHandler) this.progressHandler(msg.stage, msg.percent); return; } - if (this.responseHandler) this.responseHandler(msg); + + // Route by correlation id alone — never by message type. A response for + // an unknown id is one we have already settled; drop it. + const req = this.pending.get(msg.rid); + if (!req) return; + + if (msg.type === 'progress') { + req.onProgress?.(msg.stage, msg.percent); + return; + } + + this.pending.delete(msg.rid); + + if (msg.type === 'error') { + req.reject(new Error(msg.message)); + return; + } + + if (req.kind === 'evaluate') { + if (msg.type !== 'sdf') { + req.reject(new Error(`Unexpected '${msg.type}' response for evaluate request`)); + return; + } + // A superseded evaluate still settles. Staleness is the caller's + // concern — useEvaluator has its own evalSeq guard — but the promise + // must never be stranded. + if (req.seq !== this.evalSeq) { req.resolve(null); return; } + if (!msg.glsl) { req.resolve(null); return; } + req.resolve({ + glsl: msg.glsl, + paramCount: msg.paramCount, + paramValues: msg.paramValues, + textures: msg.textures || [], + bbMin: msg.bbMin, + bbMax: msg.bbMax, + hasWarn: !!msg.hasWarn, + }); + return; + } + + if (msg.type !== 'exportResult') { + req.reject(new Error(`Unexpected '${msg.type}' response for export request`)); + return; + } + req.resolve(new Blob([msg.data], { type: req.mime })); }; - this.worker.onerror = (err) => console.error('Worker error:', err); + // A worker-level failure settles everything outstanding; otherwise every + // pending promise hangs forever. + this.worker.onerror = (err) => { + console.error('Worker error:', err); + const outstanding = [...this.pending.values()]; + this.pending.clear(); + for (const req of outstanding) { + req.reject(new Error(err.message || 'Worker error')); + } + }; } - async evaluate(tree: SDFNodeUI | null, _resolution?: number, clip?: ClipPlane): Promise { + private async issue( + build: (rid: number) => WorkerRequest, + entry: Omit, + ): Promise { await this.readyPromise; - const seq = ++this.evalSeq; - return new Promise((resolve, reject) => { - this.responseHandler = (msg) => { - // Ignore responses for stale evaluate calls - if (seq !== this.evalSeq) return; - if (msg.type === 'sdf') { - if (!msg.glsl) { - resolve(null); - } else { - resolve({ glsl: msg.glsl, paramCount: msg.paramCount, paramValues: msg.paramValues, textures: msg.textures || [], bbMin: msg.bbMin, bbMax: msg.bbMax, hasWarn: !!msg.hasWarn }); - } - } else if (msg.type === 'error') reject(new Error(msg.message)); - }; - const req: WorkerRequest = { type: 'evaluate', tree, clip }; - this.worker.postMessage(req); + const rid = this.nextRid++; + return new Promise((resolve, reject) => { + this.pending.set(rid, { ...entry, resolve, reject }); + this.worker.postMessage(build(rid)); }); } + async evaluate(tree: SDFNodeUI | null, _resolution?: number, clip?: ClipPlane): Promise { + const seq = ++this.evalSeq; + return this.issue( + (rid) => ({ type: 'evaluate', rid, tree, clip }), + { kind: 'evaluate', seq, mime: '' }, + ); + } + async exportSTL(tree: SDFNodeUI | null, onProgress?: ProgressHandler): Promise { - await this.readyPromise; - return new Promise((resolve, reject) => { - this.progressHandler = onProgress || null; - this.responseHandler = (msg) => { - if (msg.type === 'exportResult') { this.progressHandler = null; resolve(new Blob([msg.data], { type: 'application/octet-stream' })); } - else if (msg.type === 'error') { this.progressHandler = null; reject(new Error(msg.message)); } - }; - this.worker.postMessage({ type: 'exportSTL', tree } as WorkerRequest); - }); + return this.issue( + (rid) => ({ type: 'exportSTL', rid, tree }), + { kind: 'export', seq: 0, mime: 'application/octet-stream', onProgress }, + ); } async export3MF(tree: SDFNodeUI | null, onProgress?: ProgressHandler): Promise { - await this.readyPromise; - return new Promise((resolve, reject) => { - this.progressHandler = onProgress || null; - this.responseHandler = (msg) => { - if (msg.type === 'exportResult') { this.progressHandler = null; resolve(new Blob([msg.data], { type: 'application/vnd.ms-package.3dmanufacturing-3dmodel+xml' })); } - else if (msg.type === 'error') { this.progressHandler = null; reject(new Error(msg.message)); } - }; - this.worker.postMessage({ type: 'export3MF', tree } as WorkerRequest); - }); + return this.issue( + (rid) => ({ type: 'export3MF', rid, tree }), + { kind: 'export', seq: 0, mime: 'application/vnd.ms-package.3dmanufacturing-3dmodel+xml', onProgress }, + ); } } diff --git a/src/types/geometry.ts b/src/types/geometry.ts index 70bcd12..a0fed32 100644 --- a/src/types/geometry.ts +++ b/src/types/geometry.ts @@ -12,15 +12,19 @@ export interface ClipPlane { position: number; } +// Every request carries a correlation id `rid`, echoed back on every response +// it produces. The bridge routes responses by rid alone — never by message +// type — so concurrent requests cannot displace or settle each other. See +// specs/WorkerBridgeFixed.tla. export type WorkerRequest = - | { type: 'evaluate'; tree: SDFNodeUI | null; resolution?: number; clip?: ClipPlane } - | { type: 'exportSTL'; tree: SDFNodeUI | null } - | { type: 'export3MF'; tree: SDFNodeUI | null }; + | { type: 'evaluate'; rid: number; tree: SDFNodeUI | null; resolution?: number; clip?: ClipPlane } + | { type: 'exportSTL'; rid: number; tree: SDFNodeUI | null } + | { type: 'export3MF'; rid: number; tree: SDFNodeUI | null }; export type WorkerResponse = - | { type: 'mesh'; positions: ArrayBuffer; normals: ArrayBuffer; indices: ArrayBuffer; thickness?: ArrayBuffer } - | { type: 'sdf'; glsl: string; paramCount: number; paramValues: number[]; textures?: { name: string; width: number; height: number; data: number[] }[]; bbMin: [number, number, number]; bbMax: [number, number, number]; hasWarn?: boolean } - | { type: 'exportResult'; format: 'stl' | '3mf'; data: ArrayBuffer } - | { type: 'progress'; stage: string; percent: number } - | { type: 'error'; message: string } + | { type: 'mesh'; rid: number; positions: ArrayBuffer; normals: ArrayBuffer; indices: ArrayBuffer; thickness?: ArrayBuffer } + | { type: 'sdf'; rid: number; glsl: string; paramCount: number; paramValues: number[]; textures?: { name: string; width: number; height: number; data: number[] }[]; bbMin: [number, number, number]; bbMax: [number, number, number]; hasWarn?: boolean } + | { type: 'exportResult'; rid: number; format: 'stl' | '3mf'; data: ArrayBuffer } + | { type: 'progress'; rid: number; stage: string; percent: number } + | { type: 'error'; rid: number; message: string } | { type: 'ready' }; diff --git a/src/worker/sdfWorker.ts b/src/worker/sdfWorker.ts index e570826..ad5b2cd 100644 --- a/src/worker/sdfWorker.ts +++ b/src/worker/sdfWorker.ts @@ -164,60 +164,61 @@ function evaluateCPUWithProgress(root: SDFNode, bbox: BBox, res: number, onProgr self.onmessage = (event: MessageEvent) => { const req = event.data; + const rid = req.rid; try { switch (req.type) { case 'evaluate': { if (!req.tree) { - self.postMessage({ type: 'sdf', glsl: '', paramCount: 0, paramValues: [], bbMin: [0,0,0], bbMax: [0,0,0] }); + self.postMessage({ type: 'sdf', rid, glsl: '', paramCount: 0, paramValues: [], bbMin: [0,0,0], bbMax: [0,0,0] }); return; } const root = toSDFNode(req.tree); if (!root) { - self.postMessage({ type: 'sdf', glsl: '', paramCount: 0, paramValues: [], bbMin: [0,0,0], bbMax: [0,0,0] }); + self.postMessage({ type: 'sdf', rid, glsl: '', paramCount: 0, paramValues: [], bbMin: [0,0,0], bbMax: [0,0,0] }); return; } const bbox = prepareBBox(root); const bbMin: [number, number, number] = [...bbox.min]; const bbMax: [number, number, number] = [...bbox.max]; const compiled = generateSDFFunction(root); - self.postMessage({ type: 'sdf', glsl: compiled.glsl, paramCount: compiled.paramCount, paramValues: compiled.paramValues, textures: compiled.textures, bbMin, bbMax, hasWarn: compiled.hasWarn }); + self.postMessage({ type: 'sdf', rid, glsl: compiled.glsl, paramCount: compiled.paramCount, paramValues: compiled.paramValues, textures: compiled.textures, bbMin, bbMax, hasWarn: compiled.hasWarn }); break; } case 'exportSTL': { const progress: ProgressFn = (stage, percent) => { - self.postMessage({ type: 'progress', stage, percent: Math.round(percent) }); + self.postMessage({ type: 'progress', rid, stage, percent: Math.round(percent) }); }; const mesh = evaluateAndMeshWithProgress(req.tree, 256, progress); - if (!mesh) { self.postMessage({ type: 'error', message: 'No geometry to export' }); return; } + if (!mesh) { self.postMessage({ type: 'error', rid, message: 'No geometry to export' }); return; } progress('Simplifying mesh', 80); const simplified = simplifyMesh(mesh, 0.5, (pct) => { progress('Simplifying mesh', 80 + pct * 0.15); }); progress('Encoding STL', 95); const data = exportBinarySTL(simplified); - self.postMessage({ type: 'exportResult', format: 'stl' as const, data }, [data]); + self.postMessage({ type: 'exportResult', rid, format: 'stl' as const, data }, [data]); break; } case 'export3MF': { const progress: ProgressFn = (stage, percent) => { - self.postMessage({ type: 'progress', stage, percent: Math.round(percent) }); + self.postMessage({ type: 'progress', rid, stage, percent: Math.round(percent) }); }; const mesh = evaluateAndMeshWithProgress(req.tree, 256, progress); - if (!mesh) { self.postMessage({ type: 'error', message: 'No geometry to export' }); return; } + if (!mesh) { self.postMessage({ type: 'error', rid, message: 'No geometry to export' }); return; } progress('Simplifying mesh', 80); const simplified = simplifyMesh(mesh, 0.5, (pct) => { progress('Simplifying mesh', 80 + pct * 0.15); }); progress('Encoding 3MF', 95); const data = export3MF(simplified); - self.postMessage({ type: 'exportResult', format: '3mf' as const, data }, [data]); + self.postMessage({ type: 'exportResult', rid, format: '3mf' as const, data }, [data]); break; } } } catch (err: any) { - self.postMessage({ type: 'error', message: err.message || String(err) }); + self.postMessage({ type: 'error', rid, message: err.message || String(err) }); } };