wehub-resource-sync
61 lines
2.5 KiB
Plaintext
61 lines
2.5 KiB
Plaintext
---
|
|
# Authoritative formal design for realtime machine M1: connection lifecycle.
|
|
#
|
|
# Companion to:
|
|
# - docs/design/realtime-state-machines.md (the map + invariants)
|
|
# - core/http/endpoints/openai/conncoord (the Go implementation)
|
|
#
|
|
# The Go MBT adapter maps each action below onto conncoord.Coordinator.Apply and
|
|
# the StateGetter onto conncoord.Coordinator.State, so this spec is the source of
|
|
# truth the implementation is checked against.
|
|
#
|
|
# The legacy hazard (Part 2, failure mode 6 / invariants #8, #10): a single `done`
|
|
# channel reassigned on every VAD toggle and closed from two sites (toggle-off and
|
|
# teardown) guarded only by a vadServerStarted bool. Modeled here as `running`
|
|
# (the VAD goroutine's done channel is live) and `torn` (teardown happened).
|
|
#
|
|
# NOTE: FizzBee is pre-1.0. Validate the exact syntax/CLI against the version
|
|
# pinned in formal-verification/README.md before trusting the gate.
|
|
deadlock_detection: false
|
|
---
|
|
|
|
role Conn:
|
|
action Init:
|
|
self.running = 0 # VAD goroutine running (its done channel is live)
|
|
self.torn = 0 # teardown has happened
|
|
self.teardowns = 0 # how many times teardown ran -- MUST stay <= 1
|
|
|
|
# session.update toggled turn detection on. No-op after teardown (the legacy
|
|
# reassign-and-spawn must never resurrect a torn session).
|
|
atomic action VadOn:
|
|
if self.torn == 0:
|
|
self.running = 1
|
|
|
|
# session.update toggled turn detection off (close the running done channel).
|
|
atomic action VadOff:
|
|
if self.torn == 0:
|
|
self.running = 0
|
|
|
|
# Transport read loop ended / session closing. THE FIX: setting torn absorbs
|
|
# every later Close, so teardown's channel closes happen exactly once. To
|
|
# reproduce the legacy double-teardown hazard, delete `self.torn = 1` below:
|
|
# the checker then reports TeardownOnce violated (Close runs teardown again).
|
|
atomic action Close:
|
|
if self.torn == 0:
|
|
self.running = 0 # StopVAD if it was running (close-once)
|
|
self.teardowns += 1 # Teardown
|
|
self.torn = 1
|
|
|
|
action Init:
|
|
c = Conn()
|
|
|
|
# SAFETY: teardown runs at most once -- the done/decode/sound channels are closed
|
|
# exactly once, never double-closed (Part 4, invariant #10).
|
|
always assertion TeardownOnce:
|
|
return c.teardowns <= 1
|
|
|
|
# SAFETY: the VAD goroutine is never (re)started after teardown -- no
|
|
# send-after-close / no goroutine outliving the session (Part 4, invariant #8).
|
|
always assertion NoRunAfterTorn:
|
|
return not (c.torn == 1 and c.running == 1)
|