Zen with terms

.gitignore

@@ -4,6 +4,11 @@
 **/tla/*.toolbox/*.log
 **/tla/*.toolbox/*.pdf
 **/tla/*.toolbox/*.tex
+**/tla/*.toolbox/*___model_SnapShot*.launch
+**/tla/*.toolbox/**/*.tla
+**/tla/*.toolbox/**/*.out
+**/tla/*.toolbox/**/MC.cfg
 **/tla/*.pdf
+**/tla/*.old
 **/*~
 cluster/isabelle/output

ZenWithTerms/tla/ZenWithTerms.tla

@@ -0,0 +1,301 @@
+-------------------------------------------------------------------------------------
+
+-------------------------------- 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
+
+\* 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
+
+\* set of valid configurations (i.e. the set of all non-empty subsets of Nodes)
+ValidConfigs == SUBSET(Nodes) \ {{}}
+
+\* quorums correspond to majority of votes in a config
+IsQuorum(votes, config) == Cardinality(votes \cap config) * 2 > Cardinality(config)
+
+ElectionWon(n, votes) ==
+  /\ IsQuorum(votes, lastCommittedConfiguration[n])
+  /\ IsQuorum(votes, lastAcceptedConfiguration[n])
+
+\* initial model state
+Init == /\ messages = {}
+        /\ descendant = {}
+        /\ currentTerm = [n \in Nodes |-> 0]
+        /\ lastCommittedConfiguration \in {[n \in Nodes |-> vc] : vc \in ValidConfigs} \* all agree on initial config
+        /\ lastAcceptedTerm = [n \in Nodes |-> 0]
+        /\ lastAcceptedVersion = [n \in Nodes |-> 0]
+        /\ 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 |-> {}]
+
+\* 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>>
+
+\* node n handles a join request and checks if it has received enough joins (= votes)
+\* for its term to be elected as master
+HandleJoinRequest(n, m) ==
+  /\ m.method = Join
+  /\ m.term = currentTerm[n]
+  /\ startedJoinSinceLastReboot[n]
+  /\ \/ m.laTerm < lastAcceptedTerm[n]
+     \/ /\ m.laTerm = lastAcceptedTerm[n]
+        /\ m.laVersion <= lastAcceptedVersion[n]
+  /\ joinVotes' = [joinVotes EXCEPT ![n] = @ \cup { m.source }]
+  /\ electionWon' = [electionWon EXCEPT ![n] = ElectionWon(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>>
+
+\* client causes a cluster state change v with configuration vs
+ClientRequest(n, v, vs) ==
+  /\ 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)
+  /\ vs /= lastAcceptedConfiguration[n] => lastCommittedConfiguration[n] = lastAcceptedConfiguration[n] \* only allow reconfiguration if there is not already a reconfiguration in progress
+  /\ IsQuorum(joinVotes[n], vs) \* only allow reconfiguration if we have a quorum of (join) votes for the new config
+  /\ LET
+       newPublishVersion == lastPublishedVersion[n] + 1
+       publishRequests == { [method   |-> PublishRequest,
+                             source   |-> n,
+                             dest     |-> ns,
+                             term     |-> currentTerm[n],
+                             version  |-> newPublishVersion,
+                             value    |-> v,
+                             config   |-> vs,
+                             commConf |-> lastCommittedConfiguration[n]] : ns \in Nodes }
+        newEntry == [prevT |-> lastAcceptedTerm[n],
+                     prevV |-> lastAcceptedVersion[n],
+                     nextT |-> currentTerm[n],
+                     nextV |-> newPublishVersion]
+        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] = newPublishVersion]
+       /\ lastPublishedConfiguration' = [lastPublishedConfiguration EXCEPT ![n] = vs]
+       /\ 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>>
+
+\* 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>>
+
+\* node n commits a change
+HandlePublishResponse(n, m) ==
+  /\ m.method = PublishResponse
+  /\ m.term = currentTerm[n]
+  /\ m.version = lastPublishedVersion[n]
+  /\ publishVotes' = [publishVotes EXCEPT ![n] = @ \cup {m.source}]
+  /\ IF
+       /\ IsQuorum(publishVotes'[n], lastCommittedConfiguration[n])
+       /\ IsQuorum(publishVotes'[n], lastPublishedConfiguration[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>>
+
+\* apply committed configuration to node n
+HandleCommitRequest(n, m) ==
+  /\ m.method = Commit
+  /\ m.term = currentTerm[n]
+  /\ m.term = lastAcceptedTerm[n]
+  /\ m.version = lastAcceptedVersion[n]
+  /\ lastCommittedConfiguration' = [lastCommittedConfiguration EXCEPT ![n] = lastAcceptedConfiguration[n]]
+  /\ UNCHANGED <<currentTerm, joinVotes, messages, lastAcceptedTerm, lastAcceptedValue, startedJoinSinceLastReboot, descendant,
+                 electionWon, lastAcceptedConfiguration, lastAcceptedVersion, lastPublishedVersion, publishVotes,
+                 lastPublishedConfiguration>>
+
+\* crash/restart node n (loses ephemeral state)
+RestartNode(n) ==
+  /\ electionWon' = [electionWon EXCEPT ![n] = FALSE]
+  /\ startedJoinSinceLastReboot' = [startedJoinSinceLastReboot EXCEPT ![n] = FALSE]
+  /\ joinVotes' = [joinVotes EXCEPT ![n] = {}]
+  /\ lastPublishedVersion' = [lastPublishedVersion EXCEPT ![n] = 0]
+  /\ lastPublishedConfiguration' = [lastPublishedConfiguration EXCEPT ![n] = lastAcceptedConfiguration[n]]
+  /\ publishVotes' = [publishVotes EXCEPT ![n] = {}]
+  /\ UNCHANGED <<messages, lastAcceptedVersion, currentTerm, lastCommittedConfiguration, descendant,
+                 lastAcceptedTerm, lastAcceptedValue, lastAcceptedConfiguration>>
+
+\* next-step relation
+Next ==
+  \/ \E n, nm \in Nodes : \E t \in Terms : HandleStartJoin(n, nm, t)
+  \/ \E m \in messages : HandleJoinRequest(m.dest, m)
+  \/ \E n \in Nodes : \E v \in Values : \E vs \in ValidConfigs : ClientRequest(n, v, vs)
+  \/ \E m \in messages : HandlePublishRequest(m.dest, m)
+  \/ \E m \in messages : HandlePublishResponse(m.dest, m)
+  \/ \E m \in messages : HandleCommitRequest(m.dest, m)
+  \/ \E n \in Nodes : RestartNode(n)
+
+----
+
+\* Invariants
+
+SingleNodeInvariant ==
+  \A n \in Nodes :
+    /\ lastAcceptedTerm[n] <= currentTerm[n]
+    /\ electionWon[n] = ElectionWon(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
+  \* relation is transitive
+  /\ \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 ==
+  \A m \in messages : 
+      CommittedPublishRequest(m)
+    =>
+      [prevT |-> 0, prevV |-> 0, nextT |-> m.term, nextV |-> m.version] \in descendant
+
+\* State-exploration limits
+StateConstraint ==
+  /\ \A n \in Nodes: IF currentTerm[n] <= 1 THEN lastPublishedVersion[n] <= 2 ELSE lastPublishedVersion[n] <= 3
+  /\ Cardinality(messages) <= 15
+
+====================================================================================================

ZenWithTerms/tla/ZenWithTerms.toolbox/.project

@@ -0,0 +1,29 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>ZenWithTerms</name>
+	<comment></comment>
+	<projects>
+	</projects>
+	<buildSpec>
+		<buildCommand>
+			<name>toolbox.builder.TLAParserBuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+		<buildCommand>
+			<name>toolbox.builder.PCalAlgorithmSearchingBuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+	</buildSpec>
+	<natures>
+		<nature>toolbox.natures.TLANature</nature>
+	</natures>
+	<linkedResources>
+		<link>
+			<name>ZenWithTerms.tla</name>
+			<type>1</type>
+			<locationURI>PARENT-1-PROJECT_LOC/ZenWithTerms.tla</locationURI>
+		</link>
+	</linkedResources>
+</projectDescription>

ZenWithTerms/tla/ZenWithTerms.toolbox/.settings/org.lamport.tla.toolbox.prefs

@@ -0,0 +1,2 @@
+ProjectRootFile=PARENT-1-PROJECT_LOC/ZenWithTerms.tla
+eclipse.preferences.version=1