ms2k/remora
SHA256
Watch
0
Code Releases Activity

Document that SystemQuiescent and Done are TLC-only (IF-7).

Browse source 
Clarify the deadlock sink is not a product SLO: residual staging and coord
cleanup are best-effort GC, while safety remains CommittedResult and
StagingOwnership.
This commit is contained in:
ms2k 2026-07-10 14:23:57 +09:00
commit 6a0dfc9383
1 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
docs/protocol/Remora.tla
View file

@ -23,7 +23,8 @@ EXTENDS Naturals, FiniteSets, TLC
\* - Worker ids are incarnations: WorkerUnused -> WorkerUp is scale-up/restart;
\* WorkerDown is permanent for that id. CrashWorker will not crash the last
\* remaining Up/Unused incarnation so safety models stay free of total capacity loss.
\* - CHECK_DEADLOCK expects Done when the system is protocol-quiescent.
\* - CHECK_DEADLOCK uses Done at full SystemQuiescent (TLC sink only; not a
\* product SLO — residual staging/coord is best-effort GC, not safety).
CONSTANTS
Jobs, Workers, InitialWorkers, NoJob, NoWorker,
@ -165,7 +166,9 @@ CoordinationClean(j) ==
/\ liveProgress[j] = 0
/\ liveProgressAttempt[j] = NoAttempt
\* No in-flight protocol work and no uncommitted staging left to clean.
\* TLC full quiescence (terminal + coord clean + non-winner staging cleaned).
\* Product may retain orphans; do not assert this at runtime. Safety is
\* CommittedResult + StagingOwnership, not zero residual objects.
SystemQuiescent ==
/\ \A j \in Jobs : Terminal(j) /\ CoordinationClean(j)
/\ \A a \in AttemptIds :
@ -706,7 +709,7 @@ CleanupStage(a) ==
/\ UNCHANGED <<attemptState, attemptWorker, attemptProgress,
initialProgress, resumedFromCheckpoint, pendingOutcome>>
\* Terminal clean state: avoids TLC deadlock once protocol work is finished.
\* Stuttering sink for CHECK_DEADLOCK when SystemQuiescent; not a product API.
Done ==
/\ SystemQuiescent
/\ UNCHANGED vars