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) }); } };