Model checkpoint staging ownership transfer

2026-07-17 15:01:15 +09:00 · 2026-07-17 15:01:15 +09:00 · 16cba3c317
commit 16cba3c317
parent ebf818d23c
13 changed files with 111 additions and 16 deletions
--- a/docs/protocol/Remora.cfg
+++ b/docs/protocol/Remora.cfg
@ -35,6 +35,7 @@ INVARIANTS
    CancellationSafety
    PermitSafety
    ResumeValidity
+    CheckpointStagingOwnership
    StagingOwnership
    CredentialLifecycleWellFormed
    NoOrphanSecrets
--- a/docs/protocol/Remora.tla
+++ b/docs/protocol/Remora.tla
@ -137,7 +137,7 @@ CredentialIntents ==
 VARIABLES
    \* DurableStore authority.
    phase, cancelRequested, currentToken, authority, dispatchNeeded,
-    committedAttempt, checkpoint,
+    committedAttempt, checkpoint, checkpointStageOwner,
    \* Abstracts the complete source-identity and destination-state proof.
    checkpointValid,

@ -157,7 +157,7 @@ VARIABLES

 durableVars ==
    <<phase, cancelRequested, currentToken, authority, dispatchNeeded,
-      committedAttempt, checkpoint, checkpointValid>>
+      committedAttempt, checkpoint, checkpointStageOwner, checkpointValid>>
 coordinationVars ==
    <<queued, reservation, reservationAge, leaseState, leaseAge, cancelNotice,
      liveProgress, liveProgressAttempt, coordLossCount>>
@ -226,6 +226,7 @@ Init ==
    /\ dispatchNeeded   = [j \in Jobs |-> TRUE]
    /\ committedAttempt = [j \in Jobs |-> NoAttempt]
    /\ checkpoint       = [j \in Jobs |-> 0]
+    /\ checkpointStageOwner = [j \in Jobs |-> NoAttempt]
    /\ checkpointValid  = [j \in Jobs |-> FALSE]
    /\ queued              = [j \in Jobs |-> FALSE]
    /\ reservation         = [j \in Jobs |-> NoWorker]
@ -291,6 +292,9 @@ AuthorizeAttempt(j, w) ==
       /\ CanReach(w, DurableSvc)
       /\ currentToken[j] < MaxAttempts
       /\ attemptState[a] = AttemptUnused
+       /\ IF checkpointValid[j]
+          THEN attemptState[checkpointStageOwner[j]] = AttemptStopped
+          ELSE TRUE
       /\ phase'          = [phase EXCEPT ![j] = Running]
       /\ currentToken'   = [currentToken EXCEPT ![j] = @ + 1]
       /\ authority'      = [authority EXCEPT ![j] = a]
@ -307,11 +311,15 @@ AuthorizeAttempt(j, w) ==
            [resumedFromCheckpoint EXCEPT
                ![a] = checkpointValid[j] /\ checkpoint[j] > 0]
       /\ stageState' =
-            [stageState EXCEPT
-                ![a] = IF ~checkpointValid[j] \/ checkpoint[j] = 0
-                        THEN StageNone
-                        ELSE IF checkpoint[j] = MaxProgress
-                             THEN StageComplete ELSE StagePartial]
+            IF checkpointValid[j]
+            THEN [stageState EXCEPT
+                    ![checkpointStageOwner[j]] = StageNone,
+                    ![a] = IF checkpoint[j] = MaxProgress
+                            THEN StageComplete ELSE StagePartial]
+            ELSE [stageState EXCEPT ![a] = StageNone]
+       /\ checkpointStageOwner' =
+            [checkpointStageOwner EXCEPT
+                ![j] = IF checkpointValid[j] THEN a ELSE NoAttempt]
       /\ UNCHANGED <<cancelRequested, committedAttempt, checkpoint,
                       checkpointValid>>
       /\ UNCHANGED coordinationVars
@ -512,7 +520,8 @@ ReapLostAttempt(a) ==
                ![a] = IF attemptState[a] = AttemptAuthorized
                        THEN AttemptStopped ELSE @]
       /\ UNCHANGED <<cancelRequested, currentToken, dispatchNeeded,
-                       committedAttempt, checkpoint, checkpointValid>>
+                       committedAttempt, checkpoint, checkpointStageOwner,
+                       checkpointValid>>
       /\ UNCHANGED coordinationVars
       /\ UNCHANGED workerVars
       /\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
@ -524,7 +533,8 @@ ScheduleRetry(j) ==
    /\ phase'          = [phase EXCEPT ![j] = Queued]
    /\ dispatchNeeded' = [dispatchNeeded EXCEPT ![j] = TRUE]
    /\ UNCHANGED <<cancelRequested, currentToken, authority,
-                    committedAttempt, checkpoint, checkpointValid>>
+                    committedAttempt, checkpoint, checkpointStageOwner,
+                    checkpointValid>>
    /\ UNCHANGED coordinationVars
    /\ UNCHANGED workerVars
    /\ UNCHANGED attemptVars
@ -539,7 +549,8 @@ RequestCancel(j) ==
        [authority EXCEPT
            ![j] = IF phase[j] = Running THEN @ ELSE NoAttempt]
    /\ dispatchNeeded' = [dispatchNeeded EXCEPT ![j] = FALSE]
-    /\ UNCHANGED <<currentToken, committedAttempt, checkpoint, checkpointValid>>
+    /\ UNCHANGED <<currentToken, committedAttempt, checkpoint,
+                    checkpointStageOwner, checkpointValid>>
    /\ UNCHANGED coordinationVars
    /\ UNCHANGED workerVars
    /\ UNCHANGED attemptVars
@ -556,7 +567,8 @@ FinalizeCancel(j) ==
            IF JobOf(a) = j /\ attemptState[a] = AttemptAuthorized
            THEN AttemptStopped ELSE attemptState[a]]
    /\ UNCHANGED <<cancelRequested, currentToken, dispatchNeeded,
-                    committedAttempt, checkpoint, checkpointValid>>
+                    committedAttempt, checkpoint, checkpointStageOwner,
+                    checkpointValid>>
    /\ UNCHANGED coordinationVars
    /\ UNCHANGED workerVars
    /\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
@ -664,6 +676,7 @@ PersistCheckpoint(a) ==
       /\ attemptProgress[a] > 0
       /\ (~checkpointValid[j] \/ checkpoint[j] # attemptProgress[a])
       /\ checkpoint' = [checkpoint EXCEPT ![j] = attemptProgress[a]]
+       /\ checkpointStageOwner' = [checkpointStageOwner EXCEPT ![j] = a]
       /\ checkpointValid' = [checkpointValid EXCEPT ![j] = TRUE]
       /\ UNCHANGED <<phase, cancelRequested, currentToken, authority,
                       dispatchNeeded, committedAttempt>>
@ -674,6 +687,8 @@ PersistCheckpoint(a) ==
 InvalidateCheckpoint(j) ==
    /\ ~Terminal(j)
    /\ checkpointValid[j]
+    /\ checkpointStageOwner' =
+        [checkpointStageOwner EXCEPT ![j] = NoAttempt]
    /\ checkpointValid' = [checkpointValid EXCEPT ![j] = FALSE]
    /\ UNCHANGED <<phase, cancelRequested, currentToken, authority,
                    dispatchNeeded, committedAttempt, checkpoint>>
@ -740,6 +755,7 @@ AcceptSuccess(a) ==
       /\ authority'        = [authority EXCEPT ![j] = NoAttempt]
       /\ committedAttempt' = [committedAttempt EXCEPT ![j] = a]
       /\ checkpoint'       = [checkpoint EXCEPT ![j] = MaxProgress]
+       /\ checkpointStageOwner' = [checkpointStageOwner EXCEPT ![j] = a]
       /\ checkpointValid'  = [checkpointValid EXCEPT ![j] = TRUE]
       /\ attemptState'     =
            [attemptState EXCEPT ![a] = AttemptCommitted]
@ -765,7 +781,8 @@ AcceptFailure(a, outcome) ==
            [attemptState EXCEPT ![a] = AttemptStopped]
       /\ pendingOutcome' = [pendingOutcome EXCEPT ![a] = NoOutcome]
       /\ UNCHANGED <<cancelRequested, currentToken, dispatchNeeded,
-                       committedAttempt, checkpoint, checkpointValid>>
+                       committedAttempt, checkpoint, checkpointStageOwner,
+                       checkpointValid>>
       /\ UNCHANGED coordinationVars
       /\ UNCHANGED workerVars
       /\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
@ -800,6 +817,9 @@ CleanupStage(a) ==
    IN /\ stageState[a] \in {StagePartial, StageComplete}
       /\ committedAttempt[j] # a
       /\ ~CurrentAuthority(a)
+       /\ (Terminal(j)
+            \/ ~checkpointValid[j]
+            \/ checkpointStageOwner[j] # a)
       /\ (attemptState[a] = AttemptStopped
            \/ workerState[attemptWorker[a]] = WorkerDown)
       /\ stageState' = [stageState EXCEPT ![a] = StageCleaned]
@ -1002,6 +1022,7 @@ TypeOK ==
    /\ dispatchNeeded   \in [Jobs -> BOOLEAN]
    /\ committedAttempt \in [Jobs -> AttemptIds \cup {NoAttempt}]
    /\ checkpoint       \in [Jobs -> 0..MaxProgress]
+    /\ checkpointStageOwner \in [Jobs -> AttemptIds \cup {NoAttempt}]
    /\ checkpointValid  \in [Jobs -> BOOLEAN]
    /\ queued              \in [Jobs -> BOOLEAN]
    /\ reservation         \in [Jobs -> Workers \cup {NoWorker}]
@ -1154,8 +1175,21 @@ ResumeValidity ==
        /\ (initialProgress[a] > 0 => resumedFromCheckpoint[a])
        /\ (resumedFromCheckpoint[a] => initialProgress[a] > 0)

-\* Uncommitted staging is only retained for live or stopped attempts, not cleaned
-\* while still authoritative (cleanup gated in CleanupStage).
+CheckpointStagingOwnership ==
+    \A j \in Jobs :
+        /\ (~checkpointValid[j] => checkpointStageOwner[j] = NoAttempt)
+        /\ (checkpointValid[j] =>
+                /\ checkpoint[j] > 0
+                /\ checkpointStageOwner[j] \in AttemptIds
+                /\ JobOf(checkpointStageOwner[j]) = j
+                /\ attemptState[checkpointStageOwner[j]] # AttemptUnused)
+        /\ (~Terminal(j) /\ checkpointValid[j] =>
+                stageState[checkpointStageOwner[j]]
+                    \in {StagePartial, StageComplete})
+        /\ (phase[j] = Running /\ checkpointValid[j] =>
+                checkpointStageOwner[j] = authority[j])
+
+\* Transfer removes the predecessor's cleanup eligibility before replacement I/O.
 StagingOwnership ==
    \A a \in AttemptIds :
        /\ (stageState[a] = StageCleaned =>
@ -1174,6 +1208,7 @@ TerminalStep ==
            /\ authority'[j] = authority[j]
            /\ committedAttempt'[j] = committedAttempt[j]
            /\ checkpoint'[j] = checkpoint[j]
+            /\ checkpointStageOwner'[j] = checkpointStageOwner[j]
            /\ checkpointValid'[j] = checkpointValid[j]
 FenceStep ==
    \A j \in Jobs : currentToken'[j] >= currentToken[j]
@ -1243,6 +1278,9 @@ CleanupEligible(a) ==
    /\ stageState[a] \in {StagePartial, StageComplete}
    /\ committedAttempt[JobOf(a)] # a
    /\ ~CurrentAuthority(a)
+    /\ (Terminal(JobOf(a))
+         \/ ~checkpointValid[JobOf(a)]
+         \/ checkpointStageOwner[JobOf(a)] # a)
    /\ (attemptState[a] = AttemptStopped
         \/ workerState[attemptWorker[a]] = WorkerDown)

--- a/docs/protocol/RemoraCombined.cfg
+++ b/docs/protocol/RemoraCombined.cfg
@ -35,6 +35,7 @@ INVARIANTS
    CancellationSafety
    PermitSafety
    ResumeValidity
+    CheckpointStagingOwnership
    StagingOwnership
    CredentialLifecycleWellFormed
    NoOrphanSecrets
--- a/docs/protocol/RemoraDisposition.cfg
+++ b/docs/protocol/RemoraDisposition.cfg
@ -32,6 +32,7 @@ INVARIANTS
    CancellationSafety
    PermitSafety
    ResumeValidity
+    CheckpointStagingOwnership
    StagingOwnership
    CredentialLifecycleWellFormed
    NoOrphanSecrets
--- a/docs/protocol/RemoraDurableFault.cfg
+++ b/docs/protocol/RemoraDurableFault.cfg
@ -34,6 +34,7 @@ INVARIANTS
    CancellationSafety
    PermitSafety
    ResumeValidity
+    CheckpointStagingOwnership
    StagingOwnership
    CredentialLifecycleWellFormed
    NoOrphanSecrets
--- a/docs/protocol/RemoraFencing.cfg
+++ b/docs/protocol/RemoraFencing.cfg
@ -34,6 +34,7 @@ INVARIANTS
    CancellationSafety
    PermitSafety
    ResumeValidity
+    CheckpointStagingOwnership
    StagingOwnership
    CredentialLifecycleWellFormed
    NoOrphanSecrets
--- a/docs/protocol/RemoraGlobal.cfg
+++ b/docs/protocol/RemoraGlobal.cfg
@ -33,6 +33,7 @@ INVARIANTS
    CancellationSafety
    PermitSafety
    ResumeValidity
+    CheckpointStagingOwnership
    StagingOwnership
    CredentialLifecycleWellFormed
    NoOrphanSecrets
--- a/docs/protocol/RemoraLocal.cfg
+++ b/docs/protocol/RemoraLocal.cfg
@ -33,6 +33,7 @@ INVARIANTS
    CancellationSafety
    PermitSafety
    ResumeValidity
+    CheckpointStagingOwnership
    StagingOwnership
    CredentialLifecycleWellFormed
    NoOrphanSecrets
--- a/docs/protocol/RemoraMultiShot.cfg
+++ b/docs/protocol/RemoraMultiShot.cfg
@ -33,6 +33,7 @@ INVARIANTS
    CancellationSafety
    PermitSafety
    ResumeValidity
+    CheckpointStagingOwnership
    StagingOwnership
    CredentialLifecycleWellFormed
    NoOrphanSecrets
--- a/docs/protocol/RemoraResume.cfg
+++ b/docs/protocol/RemoraResume.cfg
@ -0,0 +1,44 @@
+SPECIFICATION SafetySpec
+
+CHECK_DEADLOCK TRUE
+
+CONSTANTS
+    Jobs = {j1}
+    Workers = {w1}
+    InitialWorkers = {w1}
+    NoJob = NoJob
+    NoWorker = NoWorker
+    MaxAttempts = 2
+    MaxProgress = 2
+    LeaseLimit = 1
+    ReservationLimit = 1
+    LocalLimit = 1
+    GlobalLimit = 1
+    FaultsEnabled = FALSE
+    FaultServices = {}
+    MaxCoordLosses = 0
+    MaxPartitions = 0
+    MaxCredentialIntents = 0
+
+INVARIANTS
+    TypeOK
+    StateConsistency
+    AllocatedTokensUsed
+    LiveProgressWellFormed
+    LiveProgressCompatibleWithLiveLease
+    AtMostOneLiveLeasePerJob
+    AuthorityWellFormed
+    CommittedResultConsistent
+    CancellationSafety
+    PermitSafety
+    ResumeValidity
+    CheckpointStagingOwnership
+    StagingOwnership
+    CredentialLifecycleWellFormed
+    NoOrphanSecrets
+
+PROPERTIES
+    TerminalStateIsImmutable
+    FencingTokensMonotonic
+    CommitIsFencedCAS
+    FailureDispositionHonored
--- a/docs/protocol/RemoraStress.cfg
+++ b/docs/protocol/RemoraStress.cfg
@ -35,6 +35,7 @@ INVARIANTS
    CancellationSafety
    PermitSafety
    ResumeValidity
+    CheckpointStagingOwnership
    StagingOwnership
    CredentialLifecycleWellFormed
    NoOrphanSecrets
--- a/docs/protocol/RemoraTargetFault.cfg
+++ b/docs/protocol/RemoraTargetFault.cfg
@ -34,6 +34,7 @@ INVARIANTS
    CancellationSafety
    PermitSafety
    ResumeValidity
+    CheckpointStagingOwnership
    StagingOwnership
    CredentialLifecycleWellFormed
    NoOrphanSecrets
--- a/docs/spec/architecture.md
+++ b/docs/spec/architecture.md
@ -107,7 +107,7 @@ flowchart TD
 - Activation and inactive-attempt recovery serialize against the same durable authority. Recovery revalidates coordination after entering that boundary and reaps an attempt that remains authorized; compensation removes any pre-commit lease. Activation removes any lease that cannot be paired with the durable executing tuple.
 - Reservations have a bounded lifetime. Expiry makes unallocated work eligible for redispatch and makes a durably authorized attempt without its exact live lease eligible for reaping; it never reverses durable authority from coordination state alone.
 - A lost successful activation response replays success only while the exact live lease and complete durable executing tuple still agree. A changed attempt, fence, or worker incarnation is a precondition failure.
- The envelope projects the accepted non-secret source metadata and a sensitive-input reference, any durable `ResolvedSource`, the immutable execution grant and concrete target, the attempt-scoped staging identity, pinned credential-version references, and the validated checkpoint and destination-resume evidence available to that attempt.
+- The envelope projects the accepted non-secret source metadata and a sensitive-input reference, any durable `ResolvedSource`, the immutable execution grant and concrete target, the attempt's exact staging identity, pinned credential-version references, and the validated checkpoint and destination-resume evidence available to that attempt. A replacement may inherit the predecessor's physical staging identity only through the durable checkpoint-ownership transfer defined below.
 - A source identity or inventory that is initially unresolved is durably pinned once before concrete checkpoint validation or reuse relies on it. Pinning is a fenced durable mutation and a conflicting value is rejected.
 - Large source inventories, completed-part sets, and other unbounded collections are represented by durable streamable descriptors rather than materialized in the envelope.
 - Envelope transport is an implementation choice. It may accompany queue delivery or claim, or be read separately, but a worker never infers it from reconstructible coordination state.
@ -136,12 +136,15 @@ flowchart TD
 - Concrete work for `CleanupStage` is materialized from exact attempt ownership and pending cleanup data in `DurableStore`, independently of `CoordinationStore`.
 - Ambient cleanup processes are stateless and idempotent. Worker-local cleanup may reduce latency but is not the only cleanup path.
 - Cleanup addresses exact attempt object or multipart identities. Eligibility comes only from `CleanupStage`; missing coordination state, target-object age, and raw prefix membership are not substitutes.
+- Every reusable checkpoint has one durable logical staging owner. Its exact retained objects, multipart state, inventory rows, and pending cleanup identities are ineligible for cleanup while the job is nonterminal.
+- A replacement is authorized only after the checkpoint owner is durably stopped. Authorization atomically transfers logical ownership and all retained exact identities to the replacement before it can perform I/O. Physical keys may retain their original globally unique attempt namespace; key prefixes do not determine current logical ownership.
+- State beyond the checkpoint's validated boundary remains owned by the predecessor and becomes independently cleanup-eligible after transfer. A claimed or completed cleanup identity cannot be transferred or used as resume evidence.
 - Target lifecycle rules are storage hygiene only. They do not substitute for `JobProtocol` publication or cleanup eligibility and must not expire objects retained by a committed aggregate.
 - Independent writers and lifecycle mechanisms must be unable to replace or expire live or committed identities in Remora's reserved namespace. A deployment that cannot establish this property is unsupported.

 ## Source Identity and Resumption

- `checkpointValid` abstracts the concrete proof defined here. A reusable checkpoint binds an immutable `Source` identity, an exact completed boundary, and validated destination state; absent or changed proof makes the checkpoint unavailable to a replacement attempt.
+- `checkpointValid` abstracts the concrete proof defined here. A reusable checkpoint binds an immutable `Source` identity, an exact completed boundary, validated destination state, and its current durable staging owner; absent or changed proof makes the checkpoint unavailable to a replacement attempt.
 - HTTP identity includes the resolved final URL, a strong representation validator as defined by `RFC 9110`, representation length, and identity content encoding. Resume requires a conditional byte-range response whose validator, URL, encoding, and range exactly match the checkpoint. Weak validators, length, or modification time alone do not qualify.
 - Object-store identity includes endpoint, bucket, key, size, and an immutable version ID when available. Without a version ID, resume requires a matching conditional range read. Destination multipart reuse additionally requires the same endpoint, bucket, key, upload ID, and exact re-listed completed parts.
 - An HTTP or object-store single-object source supplies one explicit `result_path` validated under the manifest member-path rules. The adapter does not derive the result member path from a URL or object key.