ZenWithTerms/tla/ZenWithTerms.tla (326 lines of code) (raw):
-------------------------------------------------------------------------------------
-------------------------------- MODULE ZenWithTerms --------------------------------
\* Imported modules used in this specification
EXTENDS Naturals, FiniteSets, Sequences, TLC
----
CONSTANTS Values
\* Set of node ids (all master-eligible nodes)
CONSTANTS Nodes
\* RPC message types
CONSTANTS
Join,
PublishRequest,
PublishResponse,
Commit
----
\* Set of requests and responses sent between nodes.
VARIABLE messages
\* Transitive closure of value updates as done by leaders
VARIABLE descendant
\* Values to bootstrap the cluster
VARIABLE initialConfiguration
VARIABLE initialValue
VARIABLE initialAcceptedVersion
\* node state (map from node id to state)
VARIABLE currentTerm
VARIABLE lastCommittedConfiguration
VARIABLE lastAcceptedTerm
VARIABLE lastAcceptedVersion
VARIABLE lastAcceptedValue
VARIABLE lastAcceptedConfiguration
VARIABLE joinVotes
VARIABLE startedJoinSinceLastReboot
VARIABLE electionWon
VARIABLE lastPublishedVersion
VARIABLE lastPublishedConfiguration
VARIABLE publishVotes
----
Terms == Nat
Versions == Nat
\* set of valid configurations (i.e. the set of all non-empty subsets of Nodes)
ValidConfigs == SUBSET(Nodes) \ {{}}
\* cluster-state versions that might have come from older systems
InitialVersions == Nat
\* quorums correspond to majority of votes in a config
IsQuorum(votes, config) == Cardinality(votes \cap config) * 2 > Cardinality(config)
IsElectionQuorum(n, votes) ==
/\ IsQuorum(votes, lastCommittedConfiguration[n])
/\ IsQuorum(votes, lastAcceptedConfiguration[n])
IsPublishQuorum(n, votes) ==
/\ IsQuorum(votes, lastCommittedConfiguration[n])
/\ IsQuorum(votes, lastPublishedConfiguration[n])
\* initial model state
Init == /\ messages = {}
/\ descendant = {}
/\ initialConfiguration \in ValidConfigs
/\ initialValue \in Values
/\ initialAcceptedVersion \in [Nodes -> InitialVersions]
/\ currentTerm = [n \in Nodes |-> 0]
/\ lastCommittedConfiguration = [n \in Nodes |-> {}] \* empty config
/\ lastAcceptedTerm = [n \in Nodes |-> 0]
/\ lastAcceptedVersion = initialAcceptedVersion
/\ lastAcceptedValue \in {[n \in Nodes |-> v] : v \in Values} \* all agree on initial value
/\ lastAcceptedConfiguration = [n \in Nodes |-> lastCommittedConfiguration[n]]
/\ joinVotes = [n \in Nodes |-> {}]
/\ startedJoinSinceLastReboot = [n \in Nodes |-> FALSE]
/\ electionWon = [n \in Nodes |-> FALSE]
/\ lastPublishedVersion = [n \in Nodes |-> 0]
/\ lastPublishedConfiguration = [n \in Nodes |-> lastCommittedConfiguration[n]]
/\ publishVotes = [n \in Nodes |-> {}]
\* Bootstrap node n with the initial state and config
SetInitialState(n) ==
/\ lastAcceptedConfiguration[n] = {} \* not already bootstrapped
/\ Assert(lastAcceptedTerm[n] = 0, "lastAcceptedTerm should be 0")
/\ Assert(lastCommittedConfiguration[n] = {}, "lastCommittedConfiguration should be empty")
/\ Assert(lastPublishedVersion[n] = 0, "lastPublishedVersion should be 0")
/\ Assert(lastPublishedConfiguration[n] = {}, "lastPublishedConfiguration should be empty")
/\ Assert(electionWon[n] = FALSE, "electionWon should be FALSE")
/\ Assert(joinVotes[n] = {}, "joinVotes should be empty")
/\ Assert(publishVotes[n] = {}, "publishVotes should be empty")
/\ lastAcceptedConfiguration' = [lastAcceptedConfiguration EXCEPT ![n] = initialConfiguration]
/\ lastAcceptedValue' = [lastAcceptedValue EXCEPT ![n] = initialValue]
/\ lastCommittedConfiguration' = [lastCommittedConfiguration EXCEPT ![n] = initialConfiguration]
/\ Assert(lastAcceptedTerm[n] = 0, "lastAcceptedTerm should be 0")
/\ Assert(lastAcceptedConfiguration'[n] /= {}, "lastAcceptedConfiguration should be non-empty")
/\ Assert(lastCommittedConfiguration'[n] /= {}, "lastCommittedConfiguration should be non-empty")
/\ UNCHANGED <<descendant, initialConfiguration, initialValue, messages, lastAcceptedTerm, lastAcceptedVersion,
lastPublishedVersion, lastPublishedConfiguration, electionWon, joinVotes, publishVotes,
startedJoinSinceLastReboot, currentTerm, initialAcceptedVersion>>
\* Send join request from node n to node nm for term t
HandleStartJoin(n, nm, t) ==
/\ t > currentTerm[n]
/\ LET
joinRequest == [method |-> Join,
source |-> n,
dest |-> nm,
term |-> t,
laTerm |-> lastAcceptedTerm[n],
laVersion |-> lastAcceptedVersion[n]]
IN
/\ currentTerm' = [currentTerm EXCEPT ![n] = t]
/\ lastPublishedVersion' = [lastPublishedVersion EXCEPT ![n] = 0]
/\ lastPublishedConfiguration' = [lastPublishedConfiguration EXCEPT ![n] = lastAcceptedConfiguration[n]]
/\ startedJoinSinceLastReboot' = [startedJoinSinceLastReboot EXCEPT ![n] = TRUE]
/\ electionWon' = [electionWon EXCEPT ![n] = FALSE]
/\ joinVotes' = [joinVotes EXCEPT ![n] = {}]
/\ publishVotes' = [publishVotes EXCEPT ![n] = {}]
/\ messages' = messages \cup { joinRequest }
/\ UNCHANGED <<lastCommittedConfiguration, lastAcceptedConfiguration, lastAcceptedVersion,
lastAcceptedValue, lastAcceptedTerm, descendant, initialConfiguration, initialValue, initialAcceptedVersion>>
\* node n handles a join request and checks if it has received enough joins (= votes)
\* for its term to be elected as master
HandleJoin(n, m) ==
/\ m.method = Join
/\ m.term = currentTerm[n]
/\ startedJoinSinceLastReboot[n]
/\ \/ m.laTerm < lastAcceptedTerm[n]
\/ /\ m.laTerm = lastAcceptedTerm[n]
/\ m.laVersion <= lastAcceptedVersion[n]
/\ lastAcceptedConfiguration[n] /= {} \* must be bootstrapped
/\ joinVotes' = [joinVotes EXCEPT ![n] = @ \cup { m.source }]
/\ electionWon' = [electionWon EXCEPT ![n] = IsElectionQuorum(n, joinVotes'[n])]
/\ IF electionWon[n] = FALSE /\ electionWon'[n]
THEN
\* initiating publish version with last accepted version to enable client requests
/\ lastPublishedVersion' = [lastPublishedVersion EXCEPT ![n] = lastAcceptedVersion[n]]
ELSE
UNCHANGED <<lastPublishedVersion>>
/\ UNCHANGED <<lastCommittedConfiguration, currentTerm, publishVotes, messages, descendant,
lastAcceptedVersion, lastAcceptedValue, lastAcceptedConfiguration,
lastAcceptedTerm, startedJoinSinceLastReboot, lastPublishedConfiguration,
initialConfiguration, initialValue, initialAcceptedVersion>>
\* client causes a cluster state change val with configuration cfg
HandleClientValue(n, t, v, val, cfg) ==
/\ electionWon[n]
/\ lastPublishedVersion[n] = lastAcceptedVersion[n] \* means we have the last published value / config (useful for CAS operations, where we need to read the previous value first)
/\ t = currentTerm[n]
/\ v > lastPublishedVersion[n]
/\ cfg /= lastAcceptedConfiguration[n] => lastCommittedConfiguration[n] = lastAcceptedConfiguration[n] \* only allow reconfiguration if there is not already a reconfiguration in progress
/\ IsQuorum(joinVotes[n], cfg) \* only allow reconfiguration if we have a quorum of (join) votes for the new config
/\ LET
publishRequests == { [method |-> PublishRequest,
source |-> n,
dest |-> ns,
term |-> t,
version |-> v,
value |-> val,
config |-> cfg,
commConf |-> lastCommittedConfiguration[n]] : ns \in Nodes }
newEntry == [prevT |-> lastAcceptedTerm[n],
prevV |-> lastAcceptedVersion[n],
nextT |-> t,
nextV |-> v]
matchingElems == { e \in descendant :
/\ e.nextT = newEntry.prevT
/\ e.nextV = newEntry.prevV }
newTransitiveElems == { [prevT |-> e.prevT,
prevV |-> e.prevV,
nextT |-> newEntry.nextT,
nextV |-> newEntry.nextV] : e \in matchingElems }
IN
/\ descendant' = descendant \cup {newEntry} \cup newTransitiveElems
/\ lastPublishedVersion' = [lastPublishedVersion EXCEPT ![n] = v]
/\ lastPublishedConfiguration' = [lastPublishedConfiguration EXCEPT ![n] = cfg]
/\ publishVotes' = [publishVotes EXCEPT ![n] = {}] \* publishVotes are only counted per publish version
/\ messages' = messages \cup publishRequests
/\ UNCHANGED <<startedJoinSinceLastReboot, lastCommittedConfiguration, currentTerm, electionWon,
lastAcceptedVersion, lastAcceptedValue, lastAcceptedTerm, lastAcceptedConfiguration,
joinVotes, initialConfiguration, initialValue, initialAcceptedVersion>>
\* handle publish request m on node n
HandlePublishRequest(n, m) ==
/\ m.method = PublishRequest
/\ m.term = currentTerm[n]
/\ (m.term = lastAcceptedTerm[n]) => (m.version > lastAcceptedVersion[n])
/\ lastAcceptedTerm' = [lastAcceptedTerm EXCEPT ![n] = m.term]
/\ lastAcceptedVersion' = [lastAcceptedVersion EXCEPT ![n] = m.version]
/\ lastAcceptedValue' = [lastAcceptedValue EXCEPT ![n] = m.value]
/\ lastAcceptedConfiguration' = [lastAcceptedConfiguration EXCEPT ![n] = m.config]
/\ lastCommittedConfiguration' = [lastCommittedConfiguration EXCEPT ![n] = m.commConf]
/\ LET
response == [method |-> PublishResponse,
source |-> n,
dest |-> m.source,
term |-> m.term,
version |-> m.version]
IN
/\ messages' = messages \cup {response}
/\ UNCHANGED <<startedJoinSinceLastReboot, currentTerm, descendant, lastPublishedConfiguration,
electionWon, lastPublishedVersion, joinVotes, publishVotes, initialConfiguration,
initialValue, initialAcceptedVersion>>
\* node n commits a change
HandlePublishResponse(n, m) ==
/\ m.method = PublishResponse
/\ electionWon[n]
/\ m.term = currentTerm[n]
/\ m.version = lastPublishedVersion[n]
/\ publishVotes' = [publishVotes EXCEPT ![n] = @ \cup {m.source}]
/\ IF
IsPublishQuorum(n, publishVotes'[n])
THEN
LET
commitRequests == { [method |-> Commit,
source |-> n,
dest |-> ns,
term |-> currentTerm[n],
version |-> lastPublishedVersion[n]] : ns \in Nodes }
IN
/\ messages' = messages \cup commitRequests
ELSE
UNCHANGED <<messages>>
/\ UNCHANGED <<startedJoinSinceLastReboot, lastCommittedConfiguration, currentTerm, electionWon, descendant,
lastAcceptedVersion, lastAcceptedValue, lastAcceptedTerm, lastAcceptedConfiguration,
lastPublishedVersion, lastPublishedConfiguration, joinVotes, initialConfiguration,
initialValue, initialAcceptedVersion>>
\* apply committed configuration to node n
HandleCommit(n, m) ==
/\ m.method = Commit
/\ m.term = currentTerm[n]
/\ m.term = lastAcceptedTerm[n]
/\ m.version = lastAcceptedVersion[n]
/\ (electionWon[n] => lastAcceptedVersion[n] = lastPublishedVersion[n])
/\ lastCommittedConfiguration' = [lastCommittedConfiguration EXCEPT ![n] = lastAcceptedConfiguration[n]]
/\ UNCHANGED <<currentTerm, joinVotes, messages, lastAcceptedTerm, lastAcceptedValue, startedJoinSinceLastReboot, descendant,
electionWon, lastAcceptedConfiguration, lastAcceptedVersion, lastPublishedVersion, publishVotes,
lastPublishedConfiguration, initialConfiguration, initialValue, initialAcceptedVersion>>
\* crash/restart node n (loses ephemeral state)
RestartNode(n) ==
/\ joinVotes' = [joinVotes EXCEPT ![n] = {}]
/\ startedJoinSinceLastReboot' = [startedJoinSinceLastReboot EXCEPT ![n] = FALSE]
/\ electionWon' = [electionWon EXCEPT ![n] = FALSE]
/\ lastPublishedVersion' = [lastPublishedVersion EXCEPT ![n] = 0]
/\ lastPublishedConfiguration' = [lastPublishedConfiguration EXCEPT ![n] = lastAcceptedConfiguration[n]]
/\ publishVotes' = [publishVotes EXCEPT ![n] = {}]
/\ UNCHANGED <<messages, lastAcceptedVersion, currentTerm, lastCommittedConfiguration, descendant,
lastAcceptedTerm, lastAcceptedValue, lastAcceptedConfiguration, initialConfiguration,
initialValue, initialAcceptedVersion>>
\* next-step relation
Next ==
\/ \E n \in Nodes : SetInitialState(n)
\/ \E n, nm \in Nodes : \E t \in Terms : HandleStartJoin(n, nm, t)
\/ \E m \in messages : HandleJoin(m.dest, m)
\/ \E n \in Nodes : \E t \in Terms : \E v \in Versions : \E val \in Values : \E vs \in ValidConfigs : HandleClientValue(n, t, v, val, vs)
\/ \E m \in messages : HandlePublishRequest(m.dest, m)
\/ \E m \in messages : HandlePublishResponse(m.dest, m)
\/ \E m \in messages : HandleCommit(m.dest, m)
\/ \E n \in Nodes : RestartNode(n)
----
\* Invariants
SingleNodeInvariant ==
\A n \in Nodes :
/\ lastAcceptedTerm[n] <= currentTerm[n]
/\ electionWon[n] = IsElectionQuorum(n, joinVotes[n]) \* cached value is consistent
/\ IF electionWon[n] THEN lastPublishedVersion[n] >= lastAcceptedVersion[n] ELSE lastPublishedVersion[n] = 0
/\ electionWon[n] => startedJoinSinceLastReboot[n]
/\ publishVotes[n] /= {} => electionWon[n]
OneMasterPerTerm ==
\A m1, m2 \in messages:
/\ m1.method = PublishRequest
/\ m2.method = PublishRequest
/\ m1.term = m2.term
=> m1.source = m2.source
LogMatching ==
\A m1, m2 \in messages:
/\ m1.method = PublishRequest
/\ m2.method = PublishRequest
/\ m1.term = m2.term
/\ m1.version = m2.version
=> m1.value = m2.value
CommittedPublishRequest(mp) ==
/\ mp.method = PublishRequest
/\ \E mc \in messages:
/\ mc.method = Commit
/\ mp.term = mc.term
/\ mp.version = mc.version
DescendantRelationIsStrictlyOrdered ==
\A d \in descendant:
/\ d.prevT <= d.nextT
/\ d.prevV < d.nextV
DescendantRelationIsTransitive ==
\A d1, d2 \in descendant:
d1.nextT = d2.prevT /\ d1.nextV = d2.prevV
=> [prevT |-> d1.prevT, prevV |-> d1.prevV, nextT |-> d2.nextT, nextV |-> d2.nextV] \in descendant
NewerOpsBasedOnOlderCommittedOps ==
\A m1, m2 \in messages :
/\ CommittedPublishRequest(m1)
/\ m2.method = PublishRequest
/\ m2.term >= m1.term
/\ m2.version > m1.version
=> [prevT |-> m1.term, prevV |-> m1.version, nextT |-> m2.term, nextV |-> m2.version] \in descendant
\* main invariant (follows from NewerOpsBasedOnOlderCommittedOps):
CommittedValuesDescendantsFromCommittedValues ==
\A m1, m2 \in messages :
/\ CommittedPublishRequest(m1)
/\ CommittedPublishRequest(m2)
/\ \/ m1.term /= m2.term
\/ m1.version /= m2.version
=>
\/ [prevT |-> m1.term, prevV |-> m1.version, nextT |-> m2.term, nextV |-> m2.version] \in descendant
\/ [prevT |-> m2.term, prevV |-> m2.version, nextT |-> m1.term, nextV |-> m1.version] \in descendant
CommittedValuesDescendantsFromInitialValue ==
\E v \in InitialVersions :
/\ \E n \in Nodes : v = initialAcceptedVersion[n]
/\ \E votes \in SUBSET(initialConfiguration) :
/\ IsQuorum(votes, initialConfiguration)
/\ \A n \in votes : initialAcceptedVersion[n] <= v
/\ \A m \in messages :
CommittedPublishRequest(m)
=>
[prevT |-> 0, prevV |-> v, nextT |-> m.term, nextV |-> m.version] \in descendant
CommitHasQuorumVsPreviousCommittedConfiguration ==
\A mc \in messages: mc.method = Commit
=> (\A mprq \in messages: (/\ mprq.method = PublishRequest
/\ mprq.term = mc.term
/\ mprq.version = mc.version)
=> IsQuorum({mprs.source: mprs \in {mprs \in messages: /\ mprs.method = PublishResponse
/\ mprs.term = mprq.term
/\ mprs.version = mprq.version
}}, mprq.commConf))
P2bInvariant ==
\A mc \in messages: mc.method = Commit
=> (\A mprq \in messages: mprq.method = PublishRequest
=> (mprq.term > mc.term => mprq.version > mc.version))
\* State-exploration limits
StateConstraint ==
/\ \A n \in Nodes: IF currentTerm[n] <= 1 THEN lastPublishedVersion[n] <= 2 ELSE lastPublishedVersion[n] <= 3
/\ Cardinality(messages) <= 15
====================================================================================================