146 lines
5.5 KiB
Text
146 lines
5.5 KiB
Text
---- MODULE Lease ----
|
|
EXTENDS Naturals
|
|
|
|
\* Equal clocks and urgent local steps project the bounded synthetic child fixture.
|
|
\* The invariant counts live processes; it makes no claim about kernel SA cleanup.
|
|
CONSTANTS LeaseSpan, ReplyMax
|
|
ASSUME LeaseSpan \in Nat \ {0} /\ ReplyMax \in 0..20
|
|
|
|
Retry == 5
|
|
Renew == 20
|
|
StopWait == 10
|
|
PollLow == 5
|
|
PollHigh == 11
|
|
Limit == LeaseSpan + 2 * PollHigh + ReplyMax + Retry + Renew + StopWait
|
|
|
|
VARIABLES now, version, seen, age, committed, leader, remaining,
|
|
signalled, oldAlive, standby, pollLeft, newAlive
|
|
vars == <<now, version, seen, age, committed, leader, remaining,
|
|
signalled, oldAlive, standby, pollLeft, newAlive>>
|
|
|
|
TypeOK ==
|
|
/\ now \in 0..Limit
|
|
/\ version \in 0..2 /\ seen \in 0..2 /\ age \in 0..LeaseSpan
|
|
/\ leader \in {"Pending", "Retry", "Renew", "Stopping", "Done"}
|
|
/\ standby \in {"Poll", "Check", "Acquired", "Callback", "Running"}
|
|
/\ remaining \in 0..Renew /\ pollLeft \in 0..PollHigh
|
|
/\ \A value \in {committed, signalled, oldAlive, newAlive} : value \in BOOLEAN
|
|
|
|
\* The incumbent is running; one final renewal commits before later requests fail.
|
|
Init ==
|
|
/\ now = 0 /\ version = 0 /\ seen = 0 /\ age = 0
|
|
/\ committed = FALSE /\ leader = "Pending" /\ remaining = 0
|
|
/\ signalled = FALSE /\ oldAlive = TRUE
|
|
/\ standby = "Poll" /\ pollLeft = 0 /\ newAlive = FALSE
|
|
|
|
Commit ==
|
|
/\ ~committed
|
|
/\ committed' = TRUE /\ version' = 1
|
|
/\ UNCHANGED <<now, seen, age, leader, remaining, signalled, oldAlive,
|
|
standby, pollLeft, newAlive>>
|
|
|
|
\* RenewDeadline bounds this successful response; the next retry starts afterward.
|
|
Reply ==
|
|
/\ committed /\ leader = "Pending" /\ now <= ReplyMax
|
|
/\ leader' = "Retry" /\ remaining' = Retry
|
|
/\ UNCHANGED <<now, version, seen, age, committed, signalled, oldAlive,
|
|
standby, pollLeft, newAlive>>
|
|
|
|
BeginRenew ==
|
|
/\ leader = "Retry" /\ remaining = 0
|
|
/\ leader' = "Renew" /\ remaining' = Renew
|
|
/\ UNCHANGED <<now, version, seen, age, committed, signalled, oldAlive,
|
|
standby, pollLeft, newAlive>>
|
|
|
|
Cancel ==
|
|
/\ leader = "Renew" /\ remaining = 0
|
|
/\ leader' = "Stopping" /\ remaining' = StopWait
|
|
/\ UNCHANGED <<now, version, seen, age, committed, signalled, oldAlive,
|
|
standby, pollLeft, newAlive>>
|
|
|
|
Signal ==
|
|
/\ leader = "Stopping" /\ ~signalled
|
|
/\ signalled' = TRUE
|
|
/\ UNCHANGED <<now, version, seen, age, committed, leader, remaining,
|
|
oldAlive, standby, pollLeft, newAlive>>
|
|
|
|
Reap ==
|
|
/\ leader = "Stopping" /\ signalled /\ oldAlive
|
|
/\ oldAlive' = FALSE
|
|
/\ UNCHANGED <<now, version, seen, age, committed, leader, remaining,
|
|
signalled, standby, pollLeft, newAlive>>
|
|
|
|
Return ==
|
|
/\ leader = "Stopping" /\ ~oldAlive
|
|
/\ leader' = "Done" /\ remaining' = 0
|
|
/\ UNCHANGED <<now, version, seen, age, committed, signalled, oldAlive,
|
|
standby, pollLeft, newAlive>>
|
|
|
|
\* An unchanged Lease does not reset the contender's local observation age.
|
|
Observe ==
|
|
/\ standby = "Poll" /\ pollLeft = 0
|
|
/\ age' = IF seen = version THEN age ELSE 0
|
|
/\ seen' = version /\ standby' = "Check"
|
|
/\ UNCHANGED <<now, version, committed, leader, remaining,
|
|
signalled, oldAlive, pollLeft, newAlive>>
|
|
|
|
Defer ==
|
|
/\ standby = "Check" /\ (age < LeaseSpan \/ seen /= version)
|
|
/\ standby' = "Poll" /\ pollLeft' \in PollLow..PollHigh
|
|
/\ UNCHANGED <<now, version, seen, age, committed, leader, remaining,
|
|
signalled, oldAlive, newAlive>>
|
|
|
|
Acquire ==
|
|
/\ standby = "Check" /\ age = LeaseSpan /\ seen = version
|
|
/\ version' = 2 /\ seen' = 2 /\ age' = 0
|
|
/\ standby' = "Acquired"
|
|
/\ UNCHANGED <<now, committed, leader, remaining,
|
|
signalled, oldAlive, pollLeft, newAlive>>
|
|
|
|
Start ==
|
|
/\ standby = "Acquired"
|
|
/\ standby' = "Callback"
|
|
/\ UNCHANGED <<now, version, seen, age, committed, leader, remaining,
|
|
signalled, oldAlive, pollLeft, newAlive>>
|
|
|
|
Spawn ==
|
|
/\ standby = "Callback"
|
|
/\ standby' = "Running" /\ newAlive' = TRUE
|
|
/\ UNCHANGED <<now, version, seen, age, committed, leader, remaining,
|
|
signalled, oldAlive, pollLeft>>
|
|
|
|
Done == leader = "Done" /\ standby = "Running"
|
|
|
|
\* Deadlines and local callbacks run before the next one-second clock step.
|
|
Urgent ==
|
|
\/ ~committed
|
|
\/ (leader = "Pending" /\ now = ReplyMax)
|
|
\/ (leader \in {"Retry", "Renew"} /\ remaining = 0)
|
|
\/ (leader = "Stopping" /\ (~signalled \/ ~oldAlive \/ remaining = 0))
|
|
\/ (standby = "Poll" /\ pollLeft = 0)
|
|
\/ standby \in {"Check", "Acquired", "Callback"}
|
|
|
|
Tick ==
|
|
/\ ~Done /\ ~Urgent
|
|
/\ now' = now + 1
|
|
/\ remaining' = IF leader \in {"Retry", "Renew", "Stopping"}
|
|
THEN remaining - 1 ELSE remaining
|
|
/\ age' = IF standby = "Poll" /\ age < LeaseSpan THEN age + 1 ELSE age
|
|
/\ pollLeft' = IF standby = "Poll" THEN pollLeft - 1 ELSE pollLeft
|
|
/\ UNCHANGED <<version, seen, committed, leader, signalled,
|
|
oldAlive, standby, newAlive>>
|
|
|
|
Next == Commit \/ Reply \/ BeginRenew \/ Cancel \/ Signal \/ Reap \/ Return
|
|
\/ Observe \/ Defer \/ Acquire \/ Start \/ Spawn \/ Tick
|
|
\/ (Done /\ UNCHANGED vars)
|
|
|
|
Spec ==
|
|
/\ Init /\ [][Next]_vars
|
|
/\ WF_vars(Commit) /\ WF_vars(Reply) /\ WF_vars(BeginRenew)
|
|
/\ WF_vars(Cancel) /\ WF_vars(Signal) /\ WF_vars(Reap) /\ WF_vars(Return)
|
|
/\ WF_vars(Observe) /\ WF_vars(Defer) /\ WF_vars(Acquire)
|
|
/\ WF_vars(Start) /\ WF_vars(Spawn) /\ WF_vars(Tick)
|
|
|
|
ProcessExclusion == ~(oldAlive /\ newAlive)
|
|
Handoff == <>Done
|
|
====
|