ms2k/remora
SHA256
Watch
0
Code Releases Activity

Require executing authority for lease renewal.

Browse source 
RenewLease now demands current durable authority, AttemptExecuting, and a
non-terminal phase so a live lease cannot be extended after authority loss.
Align the mutable API renew prose with that precondition.
This commit is contained in:
ms2k 2026-07-15 16:59:35 +09:00
commit 0834f291d9
2 changed files with 11 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
docs/api/README.md
View file

@ -34,10 +34,12 @@ only when the corresponding `JobProtocol` action is enabled. Later eligibility
changes do not alter a stored response, while a fresh operation is evaluated changes do not alter a stored response, while a fresh operation is evaluated
against current eligibility. against current eligibility.
Renewal follows `RenewLease`: it may extend an existing live coordination lease Renewal follows `RenewLease`: it extends an existing live coordination lease only
after durable authority changes. It never creates or restores a claim. Progress while the attempt remains current durable authority, `AttemptExecuting`, and
and outcome operations require current fenced authority and return non-terminal. It never creates or restores a claim. After authority loss the
`precondition_failed` for stale or non-authoritative tuples. lease ages out or is released; it cannot be extended. Progress and outcome
operations require current fenced authority and return `precondition_failed`
for stale or non-authoritative tuples.
Activation returns the live lease expiry and a recommended renewal time. Renewal Activation returns the live lease expiry and a recommended renewal time. Renewal
returns the corresponding updated projection. These timestamps schedule worker returns the corresponding updated projection. These timestamps schedule worker

6
docs/protocol/Remora.tla
View file

@ -307,9 +307,13 @@ ActivateAttempt(a) ==
resumedFromCheckpoint, stageState, pendingOutcome>> resumedFromCheckpoint, stageState, pendingOutcome>>
RenewLease(a) == RenewLease(a) ==
LET w == attemptWorker[a] LET j == JobOf(a)
w == attemptWorker[a]
IN /\ leaseState[a] = LeaseLive IN /\ leaseState[a] = LeaseLive
/\ leaseAge[a] > 0 /\ leaseAge[a] > 0
/\ CurrentAuthority(a)
/\ attemptState[a] = AttemptExecuting
/\ phase[j] \notin TerminalPhases
/\ workerState[w] = WorkerUp /\ workerState[w] = WorkerUp
/\ CanReach(w, CoordSvc) /\ CanReach(w, CoordSvc)
/\ leaseAge' = [leaseAge EXCEPT ![a] = 0] /\ leaseAge' = [leaseAge EXCEPT ![a] = 0]