Route worker responses by correlation id

specs/.gitignore

@@ -0,0 +1,2 @@
+tla2tools.jar
+states/

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.

specs/WorkerBridge.cfg

@@ -0,0 +1,9 @@
+SPECIFICATION Spec
+
+CONSTANT MaxReq = 3
+
+INVARIANT TypeOK
+INVARIANT NoOrphan
+INVARIANT NoCrossTalk
+
+PROPERTY AllRequestsSettle

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 == <<nextId, kind, reqQueue, respQueue, handler, evalSeq, settled>>
+
+\* 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 <<respQueue, settled>>
+
+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 <<respQueue, evalSeq, settled>>
+
+(***************************************************************************)
+(* 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 <<nextId, kind, handler, evalSeq, settled>>
+
+(***************************************************************************)
+(* 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 <<nextId, kind, reqQueue, handler, evalSeq>>
+
+\* 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")
+
+=============================================================================

specs/WorkerBridgeFixed.cfg

@@ -0,0 +1,10 @@
+SPECIFICATION Spec
+
+CONSTANT MaxReq = 4
+
+INVARIANT TypeOK
+INVARIANT NoOrphan
+INVARIANT NoCrossTalk
+INVARIANT HandlerAgreesWithSettled
+
+PROPERTY AllRequestsSettle