diff --git a/manifest.json b/manifest.json index 332a4439..35f4ca75 100644 --- a/manifest.json +++ b/manifest.json @@ -1374,29 +1374,13 @@ "models": [] }, { - "path": "specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/Consensus.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [ - "proof" - ], - "models": [] - }, - { - "path": "specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/FiniteSets.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [], - "models": [] - }, - { - "path": "specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/MC.tla", + "path": "specifications/PaxosHowToWinATuringAward/MCConsensus.tla", "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], "models": [ { - "path": "specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/MC.cfg", + "path": "specifications/PaxosHowToWinATuringAward/MCConsensus.cfg", "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", @@ -1408,36 +1392,13 @@ ] }, { - "path": "specifications/PaxosHowToWinATuringAward/Paxos.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [], - "models": [] - }, - { - "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/Consensus.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [ - "proof" - ], - "models": [] - }, - { - "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/FiniteSets.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [], - "models": [] - }, - { - "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/MC.tla", + "path": "specifications/PaxosHowToWinATuringAward/MCPaxos.tla", "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], "models": [ { - "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/MC.cfg", + "path": "specifications/PaxosHowToWinATuringAward/MCPaxosSmall.cfg", "runtime": "00:01:00", "size": "medium", "mode": "exhaustive search", @@ -1445,49 +1406,9 @@ "liveness" ], "result": "success" - } - ] - }, - { - "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/Paxos.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [], - "models": [] - }, - { - "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/Voting.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [ - "proof" - ], - "models": [] - }, - { - "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/Consensus.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [ - "proof" - ], - "models": [] - }, - { - "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/FiniteSets.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [], - "models": [] - }, - { - "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/MC.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [], - "models": [ + }, { - "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/MC.cfg", + "path": "specifications/PaxosHowToWinATuringAward/MCPaxosTiny.cfg", "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", @@ -1499,54 +1420,13 @@ ] }, { - "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/Paxos.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [], - "models": [] - }, - { - "path": "specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/Voting.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [ - "proof" - ], - "models": [] - }, - { - "path": "specifications/PaxosHowToWinATuringAward/Voting.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [ - "proof" - ], - "models": [] - }, - { - "path": "specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/Consensus.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [ - "proof" - ], - "models": [] - }, - { - "path": "specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/FiniteSets.tla", - "communityDependencies": [], - "tlaLanguageVersion": 2, - "features": [], - "models": [] - }, - { - "path": "specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/MC.tla", + "path": "specifications/PaxosHowToWinATuringAward/MCVoting.tla", "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], "models": [ { - "path": "specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/MC.cfg", + "path": "specifications/PaxosHowToWinATuringAward/MCVoting.cfg", "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", @@ -1559,7 +1439,14 @@ ] }, { - "path": "specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/Voting.tla", + "path": "specifications/PaxosHowToWinATuringAward/Paxos.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/PaxosHowToWinATuringAward/Voting.tla", "communityDependencies": [], "tlaLanguageVersion": 2, "features": [ diff --git a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/.project b/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/.project deleted file mode 100644 index e7050887..00000000 --- a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/.project +++ /dev/null @@ -1,24 +0,0 @@ - - - Consensus - - - - - - toolbox.builder.TLAParserBuilder - - - - - - toolbox.natures.TLANature - - - - Consensus.tla - 1 - PARENT-1-PROJECT_LOC/Consensus.tla - - - diff --git a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/.settings/org.lamport.tla.toolbox.prefs b/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/.settings/org.lamport.tla.toolbox.prefs deleted file mode 100644 index 7c22c9dd..00000000 --- a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/.settings/org.lamport.tla.toolbox.prefs +++ /dev/null @@ -1,2 +0,0 @@ -ProjectRootFile=PARENT-1-PROJECT_LOC/Consensus.tla -eclipse.preferences.version=1 diff --git a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/Consensus.tla b/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/Consensus.tla deleted file mode 100644 index dc07c5bc..00000000 --- a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/Consensus.tla +++ /dev/null @@ -1,91 +0,0 @@ ------------------------------ MODULE Consensus ------------------------------ -(***************************************************************************) -(* This is an very abstract specification of the consensus problem, in *) -(* which a set of processes must choose a single value. We abstract away *) -(* even the processes. We specify the simple requirement that at most one *) -(* value is chosen by describing the set of all chosen values. The naive *) -(* requirement is that this set never contains more than one value, which *) -(* is an invariance property. But a little thought shows that this *) -(* requirement allows a value to be chosen then unchosen, and then another *) -(* value to be chosen. So we specify that the set of chosen values is *) -(* initially empty, it can be set to a single value, and then it can never *) -(* change. *) -(***************************************************************************) - -EXTENDS Naturals, FiniteSets - (*************************************************************************) - (* Imports standard modules that define operators of arithmetic on *) - (* natural numbers and the Cardinality operator, where Cardinality(S) is *) - (* the number of elements in the set S, if S is finite. *) - (*************************************************************************) -CONSTANT Value - (*************************************************************************) - (* The set of all values that can be chosen. *) - (*************************************************************************) -VARIABLE chosen - (*************************************************************************) - (* The set of all values that have been chosen. *) - (*************************************************************************) - -(***************************************************************************) -(* The type-correctness invariant asserting the "type" of the variable *) -(* 'chosen'. It isn't part of the spec itself--that is, the formula *) -(* describing the possible sequence of values that 'chosen' can have in a *) -(* behavior correct behavior of the system, but is an invariance property *) -(* that the spec should satisfy. *) -(***************************************************************************) -TypeOK == /\ chosen \subseteq Value - /\ IsFiniteSet(chosen) - -(***************************************************************************) -(* The initial predicate describing the possible initial state of *) -(* 'chosen'. *) -(***************************************************************************) -Init == chosen = {} - -(***************************************************************************) -(* The next-state relation describing how 'chosen' can change from one *) -(* step to the next. Note that is enabled (equals true for some next *) -(* value chosen' of choseen) if and only if chosen equals the empty set. *) -(***************************************************************************) -Next == /\ chosen = {} - /\ \E v \in Value : chosen' = {v} - -(***************************************************************************) -(* The TLA+ temporal formula that is the spec. *) -(***************************************************************************) -Spec == Init /\ [][Next]_chosen - ------------------------------------------------------------------------------ -(***************************************************************************) -(* The specification should imply the safety property that 'chosen' can *) -(* contain at most one value in any reachable state. This condition on *) -(* the state is expressed by Inv defined here. *) -(***************************************************************************) -Inv == /\ TypeOK - /\ Cardinality(chosen) \leq 1 - -(***************************************************************************) -(* You can now run the TLC model checker on the model named 3Values to *) -(* check that Inv is an invariant, meaning that it's true of every *) -(* reachable state. TLC's default setting to check for deadlock would *) -(* cause it to report a deadlock because no action is possible after a *) -(* value is chosen. We would say that the system terminated, but *) -(* termination is just deadlock that we want to happen, and we have to *) -(* tell TLC that we want deadlock by disabling its check for it. *) -(***************************************************************************) - - -(***************************************************************************) -(* The following theorem asserts the desired safety propert. Its proof *) -(* appears after the theorem. This proof is easily checked by the TLAPS *) -(* prover. *) -(***************************************************************************) -THEOREM Invariance == Spec => []Inv -<1>1. Init => Inv - -<1>2. Inv /\ [Next]_chosen => Inv' - -<1>3. QED - BY <1>1, <1>2 DEF Spec -============================================================================= diff --git a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/FiniteSets.tla b/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/FiniteSets.tla deleted file mode 100644 index 57ac4023..00000000 --- a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/FiniteSets.tla +++ /dev/null @@ -1,23 +0,0 @@ ----------------------------- MODULE FiniteSets ----------------------------- -LOCAL INSTANCE Naturals -LOCAL INSTANCE Sequences - (*************************************************************************) - (* Imports the definitions from Naturals and Sequences, but doesn't *) - (* export them. *) - (*************************************************************************) - -IsFiniteSet(S) == - (*************************************************************************) - (* A set S is finite iff there is a finite sequence containing all its *) - (* elements. *) - (*************************************************************************) - \E seq \in Seq(S) : \A s \in S : \E n \in 1..Len(seq) : seq[n] = s - -Cardinality(S) == - (*************************************************************************) - (* Cardinality is defined only for finite sets. *) - (*************************************************************************) - LET CS[T \in SUBSET S] == IF T = {} THEN 0 - ELSE 1 + CS[T \ {CHOOSE x : x \in T}] - IN CS[S] -============================================================================= diff --git a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/Consensus___3Values.launch b/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/Consensus___3Values.launch deleted file mode 100644 index 15d22ef7..00000000 --- a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/Consensus___3Values.launch +++ /dev/null @@ -1,29 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/MC.cfg b/specifications/PaxosHowToWinATuringAward/MCConsensus.cfg similarity index 100% rename from specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/MC.cfg rename to specifications/PaxosHowToWinATuringAward/MCConsensus.cfg diff --git a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/MC.tla b/specifications/PaxosHowToWinATuringAward/MCConsensus.tla similarity index 91% rename from specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/MC.tla rename to specifications/PaxosHowToWinATuringAward/MCConsensus.tla index 9cd62aba..3a343f8a 100644 --- a/specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/MC.tla +++ b/specifications/PaxosHowToWinATuringAward/MCConsensus.tla @@ -1,4 +1,4 @@ ----- MODULE MC ---- +---- MODULE MCConsensus ---- EXTENDS Consensus, TLC \* MV CONSTANT declarations@modelParameterConstants diff --git a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/MC.tla b/specifications/PaxosHowToWinATuringAward/MCPaxos.tla similarity index 92% rename from specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/MC.tla rename to specifications/PaxosHowToWinATuringAward/MCPaxos.tla index 39ec77f0..09e3d3c9 100644 --- a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/MC.tla +++ b/specifications/PaxosHowToWinATuringAward/MCPaxos.tla @@ -1,6 +1,8 @@ ----- MODULE MC ---- +---- MODULE MCPaxos ---- EXTENDS Paxos, TLC +CONSTANT MaxBallot + \* MV CONSTANT declarations@modelParameterConstants CONSTANTS a1, a2, a3 @@ -28,11 +30,11 @@ const_1560336937634607000 == \* CONSTANT definition @modelParameterDefinitions:1 def_ov_1560336937634609000 == -0..1 +0..MaxBallot ---- \* CONSTANT definition @modelParameterDefinitions:2 def_ov_1560336937634610000 == -0..1 +0..MaxBallot ---- \* PROPERTY definition @modelCorrectnessProperties:0 prop_1560336937635612000 == diff --git a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/MC.cfg b/specifications/PaxosHowToWinATuringAward/MCPaxosSmall.cfg similarity index 89% rename from specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/MC.cfg rename to specifications/PaxosHowToWinATuringAward/MCPaxosSmall.cfg index 59b9774c..53a0208c 100644 --- a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/MC.cfg +++ b/specifications/PaxosHowToWinATuringAward/MCPaxosSmall.cfg @@ -1,4 +1,6 @@ \* MV CONSTANT declarations +CONSTANT +MaxBallot = 2 CONSTANTS a1 = a1 a2 = a2 @@ -30,4 +32,4 @@ Inv \* PROPERTY definition PROPERTY prop_1560336937635612000 -\* Generated on Wed Jun 12 03:55:37 PDT 2019 \ No newline at end of file +\* Generated on Wed Jun 12 03:55:37 PDT 2019 diff --git a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/MC.cfg b/specifications/PaxosHowToWinATuringAward/MCPaxosTiny.cfg similarity index 57% rename from specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/MC.cfg rename to specifications/PaxosHowToWinATuringAward/MCPaxosTiny.cfg index 6cab228a..520e0d69 100644 --- a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/MC.cfg +++ b/specifications/PaxosHowToWinATuringAward/MCPaxosTiny.cfg @@ -1,4 +1,6 @@ \* MV CONSTANT declarations +CONSTANT +MaxBallot = 1 CONSTANTS a1 = a1 a2 = a2 @@ -9,18 +11,18 @@ v1 = v1 v2 = v2 \* MV CONSTANT definitions CONSTANT -Acceptor <- const_1560353114150701000 +Acceptor <- const_1560336937634605000 \* MV CONSTANT definitions CONSTANT -Value <- const_1560353114150702000 +Value <- const_1560336937634606000 \* CONSTANT definitions CONSTANT -Quorum <- const_1560353114150703000 +Quorum <- const_1560336937634607000 \* CONSTANT definition CONSTANT None = None -Ballot <- def_ov_1560353114150705000 -Ballot <- [Voting]def_ov_1560353114150706000 +Ballot <- def_ov_1560336937634609000 +Ballot <- [Voting]def_ov_1560336937634610000 \* SPECIFICATION definition SPECIFICATION Spec @@ -29,5 +31,5 @@ INVARIANT Inv \* PROPERTY definition PROPERTY -prop_1560353114151708000 -\* Generated on Wed Jun 12 08:25:14 PDT 2019 \ No newline at end of file +prop_1560336937635612000 +\* Generated on Wed Jun 12 03:55:37 PDT 2019 diff --git a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/MC.cfg b/specifications/PaxosHowToWinATuringAward/MCVoting.cfg similarity index 100% rename from specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/MC.cfg rename to specifications/PaxosHowToWinATuringAward/MCVoting.cfg diff --git a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/MC.tla b/specifications/PaxosHowToWinATuringAward/MCVoting.tla similarity index 96% rename from specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/MC.tla rename to specifications/PaxosHowToWinATuringAward/MCVoting.tla index b3fe72b7..1e61ffe9 100644 --- a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/MC.tla +++ b/specifications/PaxosHowToWinATuringAward/MCVoting.tla @@ -1,4 +1,4 @@ ----- MODULE MC ---- +---- MODULE MCVoting ---- EXTENDS Voting, TLC \* MV CONSTANT declarations@modelParameterConstants diff --git a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/.project b/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/.project deleted file mode 100644 index 131b40b4..00000000 --- a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/.project +++ /dev/null @@ -1,34 +0,0 @@ - - - Paxos - - - - - - toolbox.builder.TLAParserBuilder - - - - - - toolbox.natures.TLANature - - - - Consensus.tla - 1 - PARENT-1-PROJECT_LOC/Consensus.tla - - - Paxos.tla - 1 - PARENT-1-PROJECT_LOC/Paxos.tla - - - Voting.tla - 1 - PARENT-1-PROJECT_LOC/Voting.tla - - - diff --git a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/.settings/org.lamport.tla.toolbox.prefs b/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/.settings/org.lamport.tla.toolbox.prefs deleted file mode 100644 index 6119d2e6..00000000 --- a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/.settings/org.lamport.tla.toolbox.prefs +++ /dev/null @@ -1,2 +0,0 @@ -ProjectRootFile=PARENT-1-PROJECT_LOC/Paxos.tla -eclipse.preferences.version=1 diff --git a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/Paxos___SmallModel.launch b/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/Paxos___SmallModel.launch deleted file mode 100644 index b146baa8..00000000 --- a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/Paxos___SmallModel.launch +++ /dev/null @@ -1,43 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/Paxos___TinyModel.launch b/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/Paxos___TinyModel.launch deleted file mode 100644 index ef7f23b1..00000000 --- a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/Paxos___TinyModel.launch +++ /dev/null @@ -1,48 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/Consensus.tla b/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/Consensus.tla deleted file mode 100644 index c08e445b..00000000 --- a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/Consensus.tla +++ /dev/null @@ -1,112 +0,0 @@ ------------------------------ MODULE Consensus ------------------------------ -(***************************************************************************) -(* This is an very abstract specification of the consensus problem, in *) -(* which a set of processes must choose a single value. We abstract away *) -(* even the processes. We specify the simple requirement that at most one *) -(* value is chosen by describing the set of all chosen values. The naive *) -(* requirement is that this set never contains more than one value, which *) -(* is an invariance property. But a little thought shows that this *) -(* requirement allows a value to be chosen then unchosen, and then another *) -(* value to be chosen. So we specify that the set of chosen values is *) -(* initially empty, it can be set to a single value, and then it can never *) -(* change. *) -(* *) -(* We are ignoring liveness, so we do not any requirement that a value is *) -(* eventually chosen. *) -(***************************************************************************) - -EXTENDS Naturals, FiniteSets - (*************************************************************************) - (* Imports standard modules that define operators of arithmetic on *) - (* natural numbers and the Cardinality operator, where Cardinality(S) is *) - (* the number of elements in the set S, if S is finite. *) - (*************************************************************************) -CONSTANT Value - (*************************************************************************) - (* The set of all values that can be chosen. *) - (*************************************************************************) -VARIABLE chosen - (*************************************************************************) - (* The set of all values that have been chosen. *) - (*************************************************************************) - -(***************************************************************************) -(* The type-correctness invariant asserting the "type" of the variable *) -(* 'chosen'. It isn't part of the spec itself--that is, the formula *) -(* describing the possible sequence of values that 'chosen' can have in a *) -(* behavior correct behavior of the system, but is an invariance property *) -(* that the spec should satisfy. *) -(***************************************************************************) -TypeOK == /\ chosen \subseteq Value - /\ IsFiniteSet(chosen) - -(***************************************************************************) -(* The initial predicate describing the possible initial state of *) -(* 'chosen'. *) -(***************************************************************************) -Init == chosen = {} - -(***************************************************************************) -(* The next-state relation describing how 'chosen' can change from one *) -(* step to the next. Note that is enabled (equals true for some next *) -(* value chosen' of choseen) if and only if chosen equals the empty set. *) -(***************************************************************************) -Next == /\ chosen = {} - /\ \E v \in Value : chosen' = {v} - -(***************************************************************************) -(* The TLA+ temporal formula that is the spec. *) -(***************************************************************************) -Spec == Init /\ [][Next]_chosen - ------------------------------------------------------------------------------ -(***************************************************************************) -(* The specification should imply the safety property that 'chosen' can *) -(* contain at most one value in any reachable state. This condition on *) -(* the state is expressed by Inv defined here. *) -(***************************************************************************) -Inv == /\ TypeOK - /\ Cardinality(chosen) \leq 1 - -(***************************************************************************) -(* The following theorem asserts the desired safety propert. Its proof *) -(* appears after the theorem. This proof is easily checked by the TLAPS *) -(* prover. *) -(***************************************************************************) -THEOREM Invariance == Spec => []Inv -<1>1. Init => Inv - -<1>2. Inv /\ [Next]_chosen => Inv' - -<1>3. QED - BY <1>1, <1>2 DEF Spec - -(***************************************************************************) -(* If you are reading this specification in the Toolbox as you should be *) -(* (either the source file or its pretty-printed version), then you have *) -(* already opened the specification in the Toolbox. If not, you should do *) -(* that now. Download and run the Toolbox. Open a new specification with *) -(* this module file (Consensus.tla) as the root file. Along with the *) -(* module, this will install a TLC model named 3Values. Open that model. *) -(* You will see that the model specifies three things: *) -(* *) -(* - The specification is formula Spec. *) -(* *) -(* - Three unspecified constants a, b, and c (called model values) *) -(* are substituted for the declared constants Values. *) -(* *) -(* - TLC should check that formula Inv is an invariant (a *) -(* formula true on all reachable states of he specification. *) -(* *) -(* Run TLC on the model. For this tiny spec, this just takes perhaps a *) -(* millisecond plus the couple of seconds that TLC needs to start and stop *) -(* running any spec. *) -(* *) -(* TLC's default setting to check for deadlock would cause it to report a *) -(* deadlock because no action is possible after a value is chosen. We *) -(* would say that the system terminated, but termination is just deadlock *) -(* that we want to happen, and the model tells TLC that we want deadlock *) -(* by disabling its check for it. *) -(***************************************************************************) - -============================================================================= diff --git a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/FiniteSets.tla b/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/FiniteSets.tla deleted file mode 100644 index 57ac4023..00000000 --- a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/FiniteSets.tla +++ /dev/null @@ -1,23 +0,0 @@ ----------------------------- MODULE FiniteSets ----------------------------- -LOCAL INSTANCE Naturals -LOCAL INSTANCE Sequences - (*************************************************************************) - (* Imports the definitions from Naturals and Sequences, but doesn't *) - (* export them. *) - (*************************************************************************) - -IsFiniteSet(S) == - (*************************************************************************) - (* A set S is finite iff there is a finite sequence containing all its *) - (* elements. *) - (*************************************************************************) - \E seq \in Seq(S) : \A s \in S : \E n \in 1..Len(seq) : seq[n] = s - -Cardinality(S) == - (*************************************************************************) - (* Cardinality is defined only for finite sets. *) - (*************************************************************************) - LET CS[T \in SUBSET S] == IF T = {} THEN 0 - ELSE 1 + CS[T \ {CHOOSE x : x \in T}] - IN CS[S] -============================================================================= diff --git a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/MC.tla b/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/MC.tla deleted file mode 100644 index 5ffae426..00000000 --- a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/MC.tla +++ /dev/null @@ -1,43 +0,0 @@ ----- MODULE MC ---- -EXTENDS Paxos, TLC - -\* MV CONSTANT declarations@modelParameterConstants -CONSTANTS -a1, a2, a3 ----- - -\* MV CONSTANT declarations@modelParameterConstants -CONSTANTS -v1, v2 ----- - -\* MV CONSTANT definitions Acceptor -const_1560353114150701000 == -{a1, a2, a3} ----- - -\* MV CONSTANT definitions Value -const_1560353114150702000 == -{v1, v2} ----- - -\* CONSTANT definitions @modelParameterConstants:1Quorum -const_1560353114150703000 == -{{a1, a2}, {a1, a3}, {a2, a3}} ----- - -\* CONSTANT definition @modelParameterDefinitions:1 -def_ov_1560353114150705000 == -0..2 ----- -\* CONSTANT definition @modelParameterDefinitions:2 -def_ov_1560353114150706000 == -0..2 ----- -\* PROPERTY definition @modelCorrectnessProperties:0 -prop_1560353114151708000 == -V!Spec ----- -============================================================================= -\* Modification History -\* Created Wed Jun 12 08:25:14 PDT 2019 by lamport diff --git a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/Paxos.tla b/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/Paxos.tla deleted file mode 100644 index 9d8b9184..00000000 --- a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/Paxos.tla +++ /dev/null @@ -1,389 +0,0 @@ --------------------------------- MODULE Paxos ------------------------------- -(***************************************************************************) -(* This is a high-level specification of the Paxos consensus algorithm. *) -(* It refines the spec in module Voting, which you should read before *) -(* reading this module. In the Paxos consensus algorithm, acceptors *) -(* communicate by sending messages. There are additional processes called *) -(* leaders. The specification here essentially considers there to be a *) -(* separate leader for each ballot number. We can consider "leader" to be *) -(* a role, where in an implementation there will be a finite number of *) -(* leader processes each of which plays infinitely many of these leader *) -(* roles. *) -(* *) -(* Note: The algorithm described here is the Paxos consensus algorithm. *) -(* It is the crucial component of the Paxos algorithm, which implements a *) -(* fault-tolerant state machine using a sequence of instances of the *) -(* consensus algorithm. The Paxos algorithm is sometimes called *) -(* MultiPaxos, with the Paxos consensus algorithm being incorrectly called *) -(* the Paxos algorithm. I'm afraid I have contributed to this confusion *) -(* by being lazy and calling the module "Paxos" instead of *) -(* "PaxosConsensus". But incarnations of this module have already *) -(* appeared, so I'm reluctant to change its name now. *) -(***************************************************************************) - -EXTENDS Integers - -(***************************************************************************) -(* The constants and the assumptions about them are the same as for the *) -(* Voting algorithm. However, the second conjunct of the assumption, *) -(* which asserts that any two quorums have a non-empty intersection, is *) -(* not needed for the Paxos consensus algorithm to implement the Voting *) -(* algorithm. The Voting algorithm, and it, do not satisfy consensus *) -(* without that assumption. *) -(***************************************************************************) -CONSTANTS Value, Acceptor, Quorum - -ASSUME /\ \A Q \in Quorum : Q \subseteq Acceptor - /\ \A Q1, Q2 \in Quorum : Q1 \cap Q2 /= {} - -Ballot == Nat - -None == CHOOSE v : v \notin Ballot - (*************************************************************************) - (* This defines None to be an unspecified value that is not a ballot *) - (* number. *) - (*************************************************************************) - -(***************************************************************************) -(* We now define Message toe be the set of all possible messages that can *) -(* be sent in the algorithm. In TLA+, the expression *) -(* *) -(* (1) [type |-> "1a", bal |-> b] *) -(* *) -(* is a record r with two components, a `type'component, r.type, that *) -(* equals "1a" and whose bal component, r.bal, that equals b. The *) -(* expression *) -(* *) -(* (2) [type : {"1a"}, bal : Ballot] *) -(* *) -(* is the set of all records r with a components `type' and bal such that *) -(* r.type is an element of {"1a"} and r.bal is an element of Ballot. *) -(* Since "1a" is the only element of {"1a"}, formula (2) is the set of all *) -(* elements (1) such that b \in Ballot. *) -(* *) -(* The function of each type of message in the set Message is explained *) -(* below with the action that can send it. *) -(***************************************************************************) -Message == - [type : {"1a"}, bal : Ballot] - \cup [type : {"1b"}, acc : Acceptor, bal : Ballot, - mbal : Ballot \cup {-1}, mval : Value \cup {None}] - \cup [type : {"2a"}, bal : Ballot, val : Value] - \cup [type : {"2b"}, acc : Acceptor, bal : Ballot, val : Value] ------------------------------------------------------------------------------ -(***************************************************************************) -(* We now declare the following variables: *) -(* *) -(* maxBal - Is the same as the variable of that name in the Voting *) -(* algorithm. *) -(* *) -(* maxVBal *) -(* maxVal - As in the Voting algorithm, a vote is a <> *) -(* pair. The pair <> if a has not cast any vote. *) -(* *) -(* msgs - The set of all messages that have been sent. *) -(* *) -(* Messages are added to msgs when they are sent and are never removed. *) -(* An operation that is performed upon receipt of a message is represented *) -(* by an action that is enabled when the message is in msgs. This *) -(* simplifies the spec in the following ways: *) -(* *) -(* - A message can be broadcast to multiple recipients by just adding *) -(* (a single copy of) it to msgs. *) -(* *) -(* - Never removing the message automatically allows the possibility of *) -(* the same message being received twice. *) -(* *) -(* Since we are considering only safety, there is no need to explicitly *) -(* model message loss. The safety part of the spec says only what *) -(* messages may be received and does not assert that any message actually *) -(* is received. Thus, there is no difference between a lost message and *) -(* one that is never received. *) -(***************************************************************************) -VARIABLES maxBal, maxVBal, maxVal, msgs -vars == <> - (*************************************************************************) - (* It's convenient to name the tuple of all variables in a spec. *) - (*************************************************************************) - -(***************************************************************************) -(* The invariant that describes the "types" of the variables. *) -(***************************************************************************) -TypeOK == /\ maxBal \in [Acceptor -> Ballot \cup {-1}] - /\ maxVBal \in [Acceptor -> Ballot \cup {-1}] - /\ maxVal \in [Acceptor -> Value \cup {None}] - /\ msgs \subseteq Message - -(***************************************************************************) -(* The initial predicate should be obvious from the descriptions of the *) -(* variables given above. *) -(***************************************************************************) -Init == /\ maxBal = [a \in Acceptor |-> -1] - /\ maxVBal = [a \in Acceptor |-> -1] - /\ maxVal = [a \in Acceptor |-> None] - /\ msgs = {} ----------------------------------------------------------------------------- -(***************************************************************************) -(* We now define the subactions of the next-state actions. We begin by *) -(* defining an action that will be used in those subactions. The action *) -(* Send(m) asserts that message m is added to the set msgs. *) -(***************************************************************************) -Send(m) == msgs' = msgs \cup {m} - -(***************************************************************************) -(* The ballot b leader can perform actions Phase1a(b) and Phase2a(b). In *) -(* the Phase1a(b) action, it sends to all acceptors a phase 1a message (a *) -(* message m with m.type = "1a") that begins ballot b. Remember that the *) -(* same process can perform the role of leader for many different ballot *) -(* numbers b. In practice, it will stop playing the role of leader of *) -(* ballot b when it begins a higher-numbered ballot. (Remember the *) -(* definition of [type |-> "1a", bal |-> b] from the comment preceding the *) -(* definition of Message.) *) -(***************************************************************************) -Phase1a(b) == /\ Send([type |-> "1a", bal |-> b]) - /\ UNCHANGED <> - (************************************************************************) - (* Note that there is no enabling condition to prevent sending the *) - (* phase 1a message a second time. Since messages are never removed *) - (* from msg, performing the action a second time leaves msg and all the *) - (* other spec variables unchanged, so it's a stuttering step. Since *) - (* stuttering steps are always allowed, there's no reason to try to *) - (* prevent them. *) - (************************************************************************) - -(***************************************************************************) -(* Upon receipt of a ballot b phase 1a message, acceptor a can perform a *) -(* Phase1b(a) action only if b > maxBal[a]. The action sets maxBal[a] to *) -(* b and sends a phase 1b message to the leader containing the values of *) -(* maxVBal[a] and maxVal[a]. This action implements the *) -(* IncreaseMaxBal(a,b) action of the Voting algorithm for b = m.bal. *) -(***************************************************************************) -Phase1b(a) == - /\ \E m \in msgs : - /\ m.type = "1a" - /\ m.bal > maxBal[a] - /\ maxBal' = [maxBal EXCEPT ![a] = m.bal] - /\ Send([type |-> "1b", acc |-> a, bal |-> m.bal, - mbal |-> maxVBal[a], mval |-> maxVal[a]]) - /\ UNCHANGED <> - -(***************************************************************************) -(* In the Phase2a(b, v) action, the ballot b leader sends a type "2a" *) -(* message asking the acceptors to vote for v in ballot number b. The *) -(* enabling conditions of the action--its first two conjuncts--ensure that *) -(* three of the four enabling conditions of action VoteFor(a, b, v) in *) -(* module Voting will be true when acceptor a receives that message. *) -(* Those three enabling conditions are the second through fourth conjuncts *) -(* of that action. *) -(* *) -(* The first conjunct of Phase2a(b, v) asserts that at most one phase 2a *) -(* message is ever sent for ballot b. Since an acceptor will vote for a *) -(* value in ballot b only when it receives the appropriate phase 2a *) -(* message, the phase 2a message sent by this action this ensures that *) -(* these two enabling conjuncts of VoteFor(a,b,v) will be true forever: *) -(* *) -(* /\ \A vt \in votes[a] : vt[1] /= b *) -(* /\ \A c \in Acceptor \ {a} : *) -(* \A vt \in votes[c] : (vt[1] = b) => (vt[2] = v) *) -(* *) -(* The second conjunct of the Phase2a(b, v) action is the heart of the *) -(* Paxos consensus algorithm. It's a bit complicated, but I've tried a *) -(* number of times to write it in English, and it's much easier to *) -(* understand when written in mathematics. The LET/IN construct locally *) -(* defines Q1 to be the set of phase 1b messages sent in ballot number b *) -(* by acceptors in quorum Q; and it defines Q1bv to be the subset of those *) -(* messages indicating that the sender had voted in some ballot (which *) -(* must have been numbered less than b). You should study the IN clause *) -(* to convince yourself that it equals ShowsSafeAt(Q, b, v), defined in *) -(* module Voting, using the values of maxBal[a], maxVBal[a], and maxVal[a] *) -(* `a' sent in its phase 1b message to describe what votes it had cast *) -(* when it sent that message. Moreover, since `a' will no longer cast any *) -(* votes in ballots numbered less than b, the IN clause implies that *) -(* ShowsSafeAt(Q, b, v) is still true and will remain true forever. *) -(* Hence, this conjunct of Phase2a(b, v) checks the enabling condition *) -(* *) -(* /\ \E Q \in Quorum : ShowsSafeAt(Q, b, v) *) -(* *) -(* of module Voting's VoteFor(a, b, v) action. *) -(* *) -(* The type "2a" message sent by this action therefore tells every *) -(* acceptor `a' that, when it receives the message, all the enabling *) -(* conditions of VoteFor(a, b, v) but the first, maxBal[a] =< b, are *) -(* satisfied. *) -(***************************************************************************) -Phase2a(b, v) == - /\ ~ \E m \in msgs : m.type = "2a" /\ m.bal = b - /\ \E Q \in Quorum : - LET Q1b == {m \in msgs : /\ m.type = "1b" - /\ m.acc \in Q - /\ m.bal = b} - Q1bv == {m \in Q1b : m.mbal >= 0} - IN /\ \A a \in Q : \E m \in Q1b : m.acc = a - /\ \/ Q1bv = {} - \/ \E m \in Q1bv : - /\ m.mval = v - /\ \A mm \in Q1bv : m.mbal >= mm.mbal - /\ Send([type |-> "2a", bal |-> b, val |-> v]) - /\ UNCHANGED <> - - -(***************************************************************************) -(* The Phase2b(a) action describes what acceptor `a' does when it receives *) -(* a phase 2a message m, which is sent by the leader of ballot m.bal *) -(* asking acceptors to vote for m.val in that ballot. Acceptor `a' acts *) -(* on that request, voting for m.val in ballot number m.bal, iff m.bal >= *) -(* maxBal[a], which means that `a' has not participated in any ballot *) -(* numbered greater than m.bal. Thus, this enabling condition of the *) -(* Phase2b(a) action together with the receipt of the phase 2a message m *) -(* implies that the VoteFor(a, m.bal, m.val) action of module Voting is *) -(* enabled and can be executed. The Phase2b(a) message updates maxBal[a], *) -(* maxVBal[a], and maxVal[a] so their values mean what they were claimed *) -(* to mean in the comments preceding the variable declarations. *) -(***************************************************************************) -Phase2b(a) == - \E m \in msgs : - /\ m.type = "2a" - /\ m.bal >= maxBal[a] - /\ maxBal' = [maxBal EXCEPT ![a] = m.bal] - /\ maxVBal' = [maxVBal EXCEPT ![a] = m.bal] - /\ maxVal' = [maxVal EXCEPT ![a] = m.val] - /\ Send([type |-> "2b", acc |-> a, - bal |-> m.bal, val |-> m.val]) - -(***************************************************************************) -(* The definitions of Next and Spec are what we expect them to be. *) -(***************************************************************************) -Next == \/ \E b \in Ballot : \/ Phase1a(b) - \/ \E v \in Value : Phase2a(b, v) - \/ \E a \in Acceptor : Phase1b(a) \/ Phase2b(a) - -Spec == Init /\ [][Next]_vars ----------------------------------------------------------------------------- -(***************************************************************************) -(* We define `votes' to be the function such that votes[a] is the set of *) -(* pairs <> such that acceptor `a' has voted for v in ballot number *) -(* b by sending executing the Phase2b(a) action to send the appropriate *) -(* type "2b" message. The Paxos consensus algorithm implements the Voting *) -(* algorithm by implementing the variable `votes' of module Voting with *) -(* the expression `votes' of the current module, and implementing the *) -(* variable maxBal of module Voting with the variable of the same name of *) -(* the current module. *) -(***************************************************************************) -votes == - [a \in Acceptor |-> - {<> : m \in {mm \in msgs: /\ mm.type = "2b" - /\ mm.acc = a }}] -(***************************************************************************) -(* The following INSTANCE statement omits the redundant clause *) -(* *) -(* WITH votes <- votes, maxBal <- maxBal, *) -(* Value <- Value, Acceptor <- Acceptor, Quorum <- Quorum *) -(***************************************************************************) -V == INSTANCE Voting - -(***************************************************************************) -(* The inductive invariant Inv explains why the Paxos consensus algorithm *) -(* implements the Voting algorithm. It is defined after the INSTANCE *) -(* statement because it uses the operator V!ShowsSafeAt imported by that *) -(* statement. *) -(***************************************************************************) -Inv == - /\ TypeOK - /\ \A a \in Acceptor : maxBal[a] >= maxVBal[a] - /\ \A a \in Acceptor : IF maxVBal[a] = -1 - THEN maxVal[a] = None - ELSE <> \in votes[a] - /\ \A m \in msgs : - /\ (m.type = "1b") => /\ maxBal[m.acc] >= m.bal - /\ (m.mbal >= 0) => - <> \in votes[m.acc] - /\ (m.type = "2a") => /\ \E Q \in Quorum : - V!ShowsSafeAt(Q, m.bal, m.val) - /\ \A mm \in msgs : /\ mm.type ="2a" - /\ mm.bal = m.bal - => mm.val = m.val - /\ (m.type = "2b") => /\ maxVBal[m.acc] >= m.bal - /\ \E mm \in msgs : /\ mm.type = "2a" - /\ mm.bal = m.bal - /\ mm.val = m.val - -(***************************************************************************) -(* The following two theorems assert that Inv is an invariant of *) -(* the Paxos cconsensus algorithm and that this algorithm implements *) -(* the Voting algorithm with the declared variables and constants *) -(* of that algorithm implemented by the correspondingly-named expressions *) -(* in the current module. *) -(***************************************************************************) -THEOREM Invariance == Spec => []Inv - -THEOREM Implementation == Spec => V!Spec - -(***************************************************************************) -(* The ASSUME statement of this module trivial implies trivially implies *) -(* the instantiated version of the ASSUME statement of module Voting. *) -(* (Because the INSTANCE statement substitutes the constants of the *) -(* current module for the constants of the same name in module Voting, the *) -(* imported assumption is the same as the assumption of the current *) -(* module.) Hence, this theorem imported from module Voting is true in the *) -(* current module *) -(* *) -(* THEOREM V!Implementation == V!Spec => V!C!Spec *) -(* *) -(* Theorems Implementation and V!Implementation imply *) -(* *) -(* THEOREM Spec => V!C!Spec *) -(* *) -(* This theorem asserts that the Paxos consensus algorithm implements the *) -(* Consensus specification by substituting for the variable `chosen' of *) -(* the Consensus specification the value V!chosen of the current module. *) -(* The expression V!chosen is obtained by substituting the expression *) -(* `votes' of the current module for the variable `votes' of module Voting *) -(* in the expression `chosen' of module Voting. *) -(* *) -(* In other words, as we should expect, "implements" is a transitive *) -(* relation--under a suitable understanding of what transitivity means in *) -(* this situation. *) -(***************************************************************************) - -(**************************************************************************** -This current module is distributed with two models, TinyModel and -SmallModel. SmallModel is the same as the model by that name for the -Voting specification. TinyModel is the same except it defines Ballot -to contain only two elements. Run TLC on these models. You should -find that it takes a couple of seconds to run TinyModel and two or -three minutes to run SmallModel. - -Next, try the same thing you did with the Voting algorithm: Modify the -models so the assumption that any pair of quorums has an element in -common is no longer true. This time, running TLC will not find an -error. The correctness of theorems Invariance and Implementation does -not depend on that assumption. The Paxos consensus algorithm still -correctly implements the Voting algorithm; but the Voting algorithm is -incorrect if the assumption does not hold. - -Now go back to the original SmallModel, in which the quorum assumption -holds. - -When you have other things to do while TLC is running, try -increasing the size of the model a very little bit at a time and see -how the running time increases. You'll find that it increases -exponentially with the size of the model. - -Fortunately, exhaustively checking a small model is very effective at -finding errors. Since the Paxos consensus algorithm has been proved -correct, and that proof has been read by many people, I'm sure that the -basic algorithm is correct. Checking this spec on SmallModel makes me -quite confident that there are no "coding errors" in this TLA+ -specification of the algorithm. - -For checking safety properties, TLC can obtain close to linear speedup -using dozens of processors. After designing a new distributed -algorithm, you will have plenty of time to run TLC while the algorithm -is being implemented and the implementation tested. Use that time to -run it for as long as you can on the largest machine(s) that you can. -Testing the implementation is unlikely to find subtle errors in the -algorithm. -****************************************************************************) -============================================================================ diff --git a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/Voting.tla b/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/Voting.tla deleted file mode 100644 index 6a6892c8..00000000 --- a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/SmallModel/Voting.tla +++ /dev/null @@ -1,315 +0,0 @@ ------------------------------- MODULE Voting ------------------------------- -(***************************************************************************) -(* This is a high-level algorithm in which a set of processes *) -(* cooperatively choose a value. It is a high-level abstraction of the *) -(* Paxos consensus algorithm. Although I don't remember exactly what went *) -(* through my mind when I invented/discovered that algorithm, I'm pretty *) -(* sure that this spec formalizes the way I first thought of the *) -(* algorithm. It would have been very hard to find this algorithm had my *) -(* mind been distracted by the irrelevant details introduced by having the *) -(* processes communicate by messages. *) -(***************************************************************************) -EXTENDS Integers - -(***************************************************************************) -(* For historical reasons, the processes that choose a value are called *) -(* acceptors. We now declare the set Value of values, the set Acceptors *) -(* of acceptors, and another set Quorum that is a set of sets of acceptors *) -(* called quorums. *) -(***************************************************************************) -CONSTANTS Value, Acceptor, Quorum - -(***************************************************************************) -(* The following assumption asserts that Quorum is a set of subsets of the *) -(* set Acceptor, and that any two elements of Quorum have at least one *) -(* element (an acceptor) in common. Think of a quorum as a set consisting *) -(* of a majority (more than half) of the acceptors. *) -(***************************************************************************) -ASSUME /\ \A Q \in Quorum : Q \subseteq Acceptor - /\ \A Q1, Q2 \in Quorum : Q1 \cap Q2 /= {} - -(***************************************************************************) -(* Ballot is a set of "ballot numbers". For simplicity, we let it be the *) -(* set of natural numbers. However, we write Ballot for that set to *) -(* distinguish ballots from natural numbers used for other purposes. *) -(***************************************************************************) -Ballot == Nat ------------------------------------------------------------------------------ -(***************************************************************************) -(* The algorithm works by having acceptors cast votes in numbered ballots. *) -(* Each acceptor can cast one or more votes, where each vote cast by an *) -(* acceptor has the form <> indicating that the acceptor has voted *) -(* for value v in ballot number b. A value is chosen if a quorum of *) -(* acceptors have voted for it in the same ballot. *) -(* *) -(* We now declare the algorithm's variables 'votes' and 'maxBal'. For *) -(* each acceptor a, he value of votes[a] is the set of votes cast by `a'; *) -(* and maxBal[a] is an integer such that `a' will never cast any further *) -(* vote in a ballot numbered less than maxBal[a]. *) -(***************************************************************************) -VARIABLES votes, maxBal - -(***************************************************************************) -(* TypeOK asserts the "types" of the two variables. They are both *) -(* functions with domain Acceptor (arrays indexed by acceptors). For any *) -(* acceptor a, the value of votes[a] a set of <> pairs; and *) -(* the value of maxBal[a] is either a ballot number or -1. *) -(***************************************************************************) -TypeOK == - /\ votes \in [Acceptor -> SUBSET (Ballot \X Value)] - /\ maxBal \in [Acceptor -> Ballot \cup {-1}] - -(***************************************************************************) -(* Next comes a sequence of definitions of concepts used to explain the *) -(* algorithm. *) -(***************************************************************************) -VotedFor(a, b, v) == <> \in votes[a] - (************************************************************************) - (* True iff (if and only if) acceptor a has votted for value v in *) - (* ballot number b. *) - (************************************************************************) - -ChosenAt(b, v) == - \E Q \in Quorum : \A a \in Q : VotedFor(a, b, v) - (************************************************************************) - (* True iff a quorum of acceptors have all voted for value v in ballot *) - (* number b. *) - (************************************************************************) - -chosen == {v \in Value : \E b \in Ballot : ChosenAt(b, v)} - (************************************************************************) - (* Defines `chosen' to be the set of all values v for which ChosenAt(b, *) - (* v) is true for some ballot number b. This is the definition of what *) - (* it means for a value to be chosen under which the Voting algorithm *) - (* implements the Consensus specification. *) - (************************************************************************) - -DidNotVoteAt(a, b) == \A v \in Value : ~ VotedFor(a, b, v) - (************************************************************************) - (* True iff acceptor `a' has not voted in ballot number . *) - (************************************************************************) - -CannotVoteAt(a, b) == /\ maxBal[a] > b - /\ DidNotVoteAt(a, b) - (************************************************************************) - (* The algorithm will not allow acceptor `a' to vote in ballot number b *) - (* if maxBal[a] > b. Hence, CannotVoteAt(a, b) implies that `a' has *) - (* not and never will vote in ballot number b. *) - (************************************************************************) - -NoneOtherChoosableAt(b, v) == - \E Q \in Quorum : - \A a \in Q : VotedFor(a, b, v) \/ CannotVoteAt(a, b) - (************************************************************************) - (* This is true iff there is some quorum Q such that each acceptor `a' *) - (* in Q either has voted for v in ballot b or has not and never will *) - (* vote in ballot b. It implies that no value other than v has been or *) - (* ever can be chosen at ballot b. This is because for a value w to be *) - (* chosen at ballot b, all the acceptors in some quorum R must have *) - (* voted for w in ballot b. But any two ballots have an acceptor in *) - (* common, so some acceptor a in R that voted for w is in Q, and an *) - (* acceptor in Q can only have voted for v, so w must equal v. *) - (************************************************************************) - -SafeAt(b, v) == \A c \in 0..(b-1) : NoneOtherChoosableAt(c, v) - (************************************************************************) - (* True iff no value other than v has been or ever will be chosen in *) - (* any ballot numbered less than b. We read SafeAt(b, v) as "v is safe *) - (* at b". *) - (************************************************************************) - -(***************************************************************************) -(* This theorem asserts that every value is safe at ballot 0. *) -(***************************************************************************) -THEOREM AllSafeAtZero == \A v \in Value : SafeAt(0, v) - -(***************************************************************************) -(* The following theorem asserts that NoneOtherChoosableAt means what it's *) -(* name implies. The comments after its definition essentially contain a *) -(* proof of this theorem. *) -(***************************************************************************) -THEOREM ChoosableThm == - \A b \in Ballot, v \in Value : - ChosenAt(b, v) => NoneOtherChoosableAt(b, v) - -(***************************************************************************) -(* Now comes the definition of the inductive invariant Inv that *) -(* essentially explains why the algorithm is correct. *) -(***************************************************************************) -OneValuePerBallot == - \A a1, a2 \in Acceptor, b \in Ballot, v1, v2 \in Value : - VotedFor(a1, b, v1) /\ VotedFor(a2, b, v2) => (v1 = v2) - (************************************************************************) - (* This formula asserts that if any acceptors a1 and a2 have voted in a *) - (* ballot b, then they voted for the same value in ballot b. For *) - (* a1=a2, this implies that an acceptor can vote for at most one value *) - (* in any ballot. *) - (************************************************************************) - -VotesSafe == \A a \in Acceptor, b \in Ballot, v \in Value : - VotedFor(a, b, v) => SafeAt(b, v) - (************************************************************************) - (* This formula asserts that an acceptors can have voted in a ballot b *) - (* only if that value is safe at b. *) - (************************************************************************) - -(***************************************************************************) -(* The algorithm is essentially derived by ensuring that this formula Inv *) -(* is always true. *) -(***************************************************************************) -Inv == TypeOK /\ VotesSafe /\ OneValuePerBallot - -(***************************************************************************) -(* This definition is used in the defining the algorithm. You should *) -(* study it and make sure you understand what it says. *) -(***************************************************************************) -ShowsSafeAt(Q, b, v) == - /\ \A a \in Q : maxBal[a] >= b - /\ \E c \in -1..(b-1) : - /\ (c /= -1) => \E a \in Q : VotedFor(a, c, v) - /\ \A d \in (c+1)..(b-1), a \in Q : DidNotVoteAt(a, d) - -(***************************************************************************) -(* This is the theorem that's at the heart of the algorithm. It shows *) -(* that if the algorithm has maintained the invariance of Inv, then the *) -(* truth of ShowsSafeAt(Q, b, v) for some quorum Q ensures that v is safe *) -(* at b, so the algorithm can let an acceptor vote for v in ballot b *) -(* knowing VotesSafe will be preserved. *) -(***************************************************************************) -THEOREM ShowsSafety == - Inv => \A Q \in Quorum, b \in Ballot, v \in Value : - ShowsSafeAt(Q, b, v) => SafeAt(b, v) ------------------------------------------------------------------------------ -(***************************************************************************) -(* Finally, we get to the definition of the algorithm. The initial *) -(* predicate is obvious. *) -(***************************************************************************) -Init == /\ votes = [a \in Acceptor |-> {}] - /\ maxBal = [a \in Acceptor |-> -1] - -(***************************************************************************) -(* An acceptor `a' can increase maxBal[a] at any time. *) -(***************************************************************************) -IncreaseMaxBal(a, b) == - /\ b > maxBal[a] - /\ maxBal' = [maxBal EXCEPT ![a] = b] - /\ UNCHANGED votes - -(***************************************************************************) -(* The heart of the algorithm is the action in which an acceptor `a' votes *) -(* for a value v in ballot number b. The enabling condition contains the *) -(* following conjuncts, which ensure that the invariance of Inv is *) -(* maintained. *) -(* *) -(* - `a' cannot vote in a ballot numbered less than b *) -(* *) -(* - `a' cannot already have voted in ballot number b *) -(* *) -(* - No other acceptor can have voted for a value other than v *) -(* in ballot b. *) -(* *) -(* - Uses Theorem ShowsSafety to ensure that v is safe at b. *) -(* *) -(* In TLA+, a tuple t is a function (array) whose first element is t[1], *) -(* whose second element if t[2], and so on. Thus, a vote vt is the pair *) -(* <> *) -(***************************************************************************) -VoteFor(a, b, v) == - /\ maxBal[a] =< b - /\ \A vt \in votes[a] : vt[1] /= b - /\ \A c \in Acceptor \ {a} : - \A vt \in votes[c] : (vt[1] = b) => (vt[2] = v) - /\ \E Q \in Quorum : ShowsSafeAt(Q, b, v) - /\ votes' = [votes EXCEPT ![a] = votes[a] \cup {<>}] - /\ maxBal' = [maxBal EXCEPT ![a] = b] - -(***************************************************************************) -(* The rest of the spec is straightforward. *) -(***************************************************************************) -Next == \E a \in Acceptor, b \in Ballot : - \/ IncreaseMaxBal(a, b) - \/ \E v \in Value : VoteFor(a, b, v) - -Spec == Init /\ [][Next]_<> ------------------------------------------------------------------------------ -(***************************************************************************) -(* This theorem asserts that Inv is an invariant of the algorithm. The *) -(* high-level steps in its proof are given. *) -(***************************************************************************) -THEOREM Invariance == Spec => []Inv -<1>1. Init => Inv - -<1>2. Inv /\ [Next]_<> => Inv' - -<1>3. QED - BY <1>1, <1>2 DEF Spec ------------------------------------------------------------------------------ -(***************************************************************************) -(* This INSTANCE statement imports definitions from module Consensus into *) -(* the current module. All definition in module Consensus can be expanded *) -(* to definitions containing only TLA+ primitives and the declared names *) -(* Value and chosen. To import a definition from Consensus into the *) -(* current module, we have to say what expressions from the current module *) -(* are substituted for Value and chosen. The INSTANCE statement says that *) -(* expressions of the same name are substituted for them. (Because of *) -(* this, the WITH statement is redundant.) Note that in both modules, *) -(* Value is just a declared constant. However, in the current module, *) -(* `chosen' is an expression defined in terms of the variables votes and *) -(* maxBal while it is a variable in module consensus. The "C! ==" in the *) -(* statement means that defined identifiers are imported with "C!" *) -(* prepended to their names. Thus Spec of module Consensus is imported, *) -(* with these substitutions, as C!Spec. *) -(***************************************************************************) -C == INSTANCE Consensus - WITH Value <- Value, chosen <- chosen - -(***************************************************************************) -(* The following theorem asserts that the Voting algorithm implements the *) -(* Consensus specification, where the expression `chosen' of the current *) -(* module implements the variable `chosen' of Consensus. The high-level *) -(* steps of the the proof are also given. *) -(***************************************************************************) -THEOREM Implementation == Spec => C!Spec -<1>1. Init => C!Init - -<1>2. Inv /\ Inv' /\ [Next]_<> => [C!Next]_chosen - -<1>3. QED - BY <1>1, <1>2, Invariance DEF Spec, C!Spec - -(***************************************************************************) -(* This Voting specification comes with a TLC model named SmallModel. *) -(* That model tells TLC that Spec is the specification, that Acceptor and *) -(* Values should equal sets of model values with 3 acceptors and 2 values *) -(* and Quorums should equal the indicated set of values, and that it *) -(* should check theorems Invariance and Implementation. Observe that you *) -(* can't tell TLC simply to check those theorems; you have to tell TLC to *) -(* check the properties the theorems assert that Spec satisfies. (Instead *) -(* of telling TLC that Inv should be an invariant, you can tell it that *) -(* the spec should satisfy the temporal property []Inv.) *) -(* *) -(* Even though the constants are finite sets, the spec has infinitely many *) -(* reachable sets because a ballot number can be any element of the set *) -(* Nat of natural numbers. The model modifies the spec so it has a finite *) -(* set of reachable states by using a definition override (on the Spec *) -(* Options page) to redefine Ballot to equal 0..2. (Alternatively, we *) -(* could override the definition of Nat to equal 0..2.) *) -(* *) -(* Run TLC on the model. It should just take a couple of seconds. *) -(* *) -(* After doing that, show why the assumption that any pair of quorums has *) -(* an element in common is necessary by modifying the model so that *) -(* assumption doesn't hold. (It's best to clone SmallModel and modify the *) -(* clone.) Since TLC reports an error if an assumption isn't true, you *) -(* will have to comment out the second conjunct of the ASSUME statement, *) -(* which asserts that assumption. Comments can be written as follows: *) -(* *) -(* \* This is an end-of-line comment. *) -(* *) -(* (* This is another way to write a comment. *) -(* Note that comments can be nested. *) *) -(* *) -(* To help you see what the problem is, use the Trace Explorer on the *) -(* Error page to show the value of `chosen' in each state of the trace. *) -(***************************************************************************) -============================================================================= diff --git a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/Consensus.tla b/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/Consensus.tla deleted file mode 100644 index e5a95cfd..00000000 --- a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/Consensus.tla +++ /dev/null @@ -1,98 +0,0 @@ ------------------------------ MODULE Consensus ------------------------------ -(***************************************************************************) -(* This is an very abstract specification of the consensus problem, in *) -(* which a set of processes must choose a single value. We abstract away *) -(* even the processes. We specify the simple requirement that at most one *) -(* value is chosen by describing the set of all chosen values. The naive *) -(* requirement is that this set never contains more than one value, which *) -(* is an invariance property. But a little thought shows that this *) -(* requirement allows a value to be chosen then unchosen, and then another *) -(* value to be chosen. So we specify that the set of chosen values is *) -(* initially empty, it can be set to a single value, and then it can never *) -(* change. *) -(* *) -(* We are ignoring liveness, so we do not any requirement that a value is *) -(* eventually chosen. *) -(***************************************************************************) - -EXTENDS Naturals, FiniteSets - (*************************************************************************) - (* Imports standard modules that define operators of arithmetic on *) - (* natural numbers and the Cardinality operator, where Cardinality(S) is *) - (* the number of elements in the set S, if S is finite. *) - (*************************************************************************) -CONSTANT Value - (*************************************************************************) - (* The set of all values that can be chosen. *) - (*************************************************************************) -VARIABLE chosen - (*************************************************************************) - (* The set of all values that have been chosen. *) - (*************************************************************************) - -(***************************************************************************) -(* The type-correctness invariant asserting the "type" of the variable *) -(* 'chosen'. It isn't part of the spec itself--that is, the formula *) -(* describing the possible sequence of values that 'chosen' can have in a *) -(* behavior correct behavior of the system, but is an invariance property *) -(* that the spec should satisfy. *) -(***************************************************************************) -TypeOK == /\ chosen \subseteq Value - /\ IsFiniteSet(chosen) - -(***************************************************************************) -(* The initial predicate describing the possible initial state of *) -(* 'chosen'. *) -(***************************************************************************) -Init == chosen = {} - -(***************************************************************************) -(* The next-state relation describing how 'chosen' can change from one *) -(* step to the next. Note that is enabled (equals true for some next *) -(* value chosen' of choseen) if and only if chosen equals the empty set. *) -(***************************************************************************) -Next == /\ chosen = {} - /\ \E v \in Value : chosen' = {v} - -(***************************************************************************) -(* The TLA+ temporal formula that is the spec. *) -(***************************************************************************) -Spec == Init /\ [][Next]_chosen - ------------------------------------------------------------------------------ -(***************************************************************************) -(* The specification should imply the safety property that 'chosen' can *) -(* contain at most one value in any reachable state. This condition on *) -(* the state is expressed by Inv defined here. *) -(***************************************************************************) -Inv == /\ TypeOK - /\ Cardinality(chosen) \leq 1 - -(***************************************************************************) -(* You can now run the TLC model checker on the model named 3Values to *) -(* check that Inv is an invariant, meaning that it's true of every *) -(* reachable state. To specify a model, we have to specify a value for *) -(* the constant Value. Model 3Values specifies it to be a set of three *) -(* arbitrary constants. *) -(* *) -(* TLC's default setting to check for deadlock would cause it to report a *) -(* deadlock because no action is possible after a value is chosen. We *) -(* would say that the system terminated, but termination is just deadlock *) -(* that we want to happen, and the model tells TLC that we want deadlock *) -(* by disabling its check for it. *) -(***************************************************************************) - - -(***************************************************************************) -(* The following theorem asserts the desired safety propert. Its proof *) -(* appears after the theorem. This proof is easily checked by the TLAPS *) -(* prover. *) -(***************************************************************************) -THEOREM Invariance == Spec => []Inv -<1>1. Init => Inv - -<1>2. Inv /\ [Next]_chosen => Inv' - -<1>3. QED - BY <1>1, <1>2 DEF Spec -============================================================================= diff --git a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/FiniteSets.tla b/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/FiniteSets.tla deleted file mode 100644 index 57ac4023..00000000 --- a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/FiniteSets.tla +++ /dev/null @@ -1,23 +0,0 @@ ----------------------------- MODULE FiniteSets ----------------------------- -LOCAL INSTANCE Naturals -LOCAL INSTANCE Sequences - (*************************************************************************) - (* Imports the definitions from Naturals and Sequences, but doesn't *) - (* export them. *) - (*************************************************************************) - -IsFiniteSet(S) == - (*************************************************************************) - (* A set S is finite iff there is a finite sequence containing all its *) - (* elements. *) - (*************************************************************************) - \E seq \in Seq(S) : \A s \in S : \E n \in 1..Len(seq) : seq[n] = s - -Cardinality(S) == - (*************************************************************************) - (* Cardinality is defined only for finite sets. *) - (*************************************************************************) - LET CS[T \in SUBSET S] == IF T = {} THEN 0 - ELSE 1 + CS[T \ {CHOOSE x : x \in T}] - IN CS[S] -============================================================================= diff --git a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/Paxos.tla b/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/Paxos.tla deleted file mode 100644 index b17f7b54..00000000 --- a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/Paxos.tla +++ /dev/null @@ -1,289 +0,0 @@ --------------------------------- MODULE Paxos ------------------------------- -(***************************************************************************) -(* This is a high-level specification of the Paxos consensus algorithm. *) -(* It refines the spec in module Voting, which you should read before *) -(* reading this module. In the Paxos algorithm, acceptors communicate by *) -(* sending messages. There are additional processes called leaders. The *) -(* specification here essentially considers there to be a separate leader *) -(* for each ballot number. We can consider "leader" to be a role, where *) -(* in an implementation there will be a finite number of leader processes *) -(* each of which plays infinitely many of these leader roles. *) -(* *) -(* Note: The algorithm described here is the Paxos consensus algorithm. *) -(* It is the crucial component of the Paxos algorithm, which implements a *) -(* fault-tolerant state machine using a sequence of instances of the *) -(* consensus algorithm. The Paxos algorithm is sometimes called *) -(* MultiPaxos, with the Paxos consensus algorithm being incorrectly called *) -(* the Paxos algorithm. In this module, I am contributing to this *) -(* confusion by using "Paxos" as short for "Paxos consensus" simply *) -(* because always adding "consensus" would be a nuisance. But please be *) -(* aware that here, "Paxos" means "Paxos consensus". *) -(***************************************************************************) - -EXTENDS Integers - -(***************************************************************************) -(* The constants and the assumptions about them are the same as for the *) -(* Voting algorithm. However, the second conjunct of the assumption, *) -(* which asserts that any two quorums have a non-empty intersection, is *) -(* not needed for the Paxos algorithm to implement the Voting algorithm. *) -(* The Voting algorithm, and it, do not satisfy consensus without that *) -(* assumption. *) -(***************************************************************************) -CONSTANTS Value, Acceptor, Quorum - -ASSUME /\ \A Q \in Quorum : Q \subseteq Acceptor - /\ \A Q1, Q2 \in Quorum : Q1 \cap Q2 /= {} - -Ballot == Nat - -None == CHOOSE v : v \notin Ballot - (*************************************************************************) - (* This defines None to be an unspecified value that is not a ballot *) - (* number. *) - (*************************************************************************) - -(***************************************************************************) -(* We now define Message toe be the set of all possible messages that can *) -(* be sent in the algorithm. In TLA+, the expression *) -(* *) -(* (1) [type |-> "1a", bal |-> b] *) -(* *) -(* is a record r with two components, a `type'component, r.type, that *) -(* equals "1a" and whose bal component, r.bal, that equals b. The *) -(* expression *) -(* *) -(* (2) [type : {"1a"}, bal : Ballot] *) -(* *) -(* is the set of all records r with a components `type' and bal such that *) -(* r.type is an element of {"1a"} and r.bal is an element of Ballot. *) -(* Since "1a" is the only element of {"1a"}, formula (2) is the set of all *) -(* elements (1) such that b \in Ballot. *) -(* *) -(* The function of each type of message in the set Message is explained *) -(* below with the action that can send it. *) -(***************************************************************************) -Message == - [type : {"1a"}, bal : Ballot] - \cup [type : {"1b"}, acc : Acceptor, bal : Ballot, - mbal : Ballot \cup {-1}, mval : Value \cup {None}] - \cup [type : {"2a"}, bal : Ballot, val : Value] - \cup [type : {"2b"}, acc : Acceptor, bal : Ballot, val : Value] ------------------------------------------------------------------------------ -(***************************************************************************) -(* We now declare the following variables: *) -(* *) -(* maxBal - Is the same as the variable of that name in the Voting *) -(* algorithm. *) -(* *) -(* maxVBal *) -(* maxVal - As in the Voting algorithm, a vote is a <> *) -(* pair. The pair <> if a has not cast any vote. *) -(* *) -(* msgs - The set of all messages that have been sent. *) -(* *) -(* Messages are added to msgs when they are sent and are never removed. *) -(* An operation that is performed upon receipt of a message is represented *) -(* by an action that is enabled when the message is in msgs. This *) -(* simplifies the spec in the following ways: *) -(* *) -(* - A message can be broadcast to multiple recipients by just adding *) -(* (a single copy of) it to msgs. *) -(* *) -(* - Never removing the message automatically allows the possibility of *) -(* the same message being received twice. *) -(* *) -(* Since we are considering only safety, there is no need to explicitly *) -(* model message loss. The safety part of the spec says only what *) -(* messages may be received and does not assert that any message actually *) -(* is received. Thus, there is no difference between a lost message and *) -(* one that is never received. *) -(***************************************************************************) -VARIABLES maxBal, maxVBal, maxVal, msgs -vars == <> - (*************************************************************************) - (* It's convenient to name the tuple of all variables in a spec. *) - (*************************************************************************) - -(***************************************************************************) -(* The invariant that describes the "types" of the variables. *) -(***************************************************************************) -TypeOK == /\ maxBal \in [Acceptor -> Ballot \cup {-1}] - /\ maxVBal \in [Acceptor -> Ballot \cup {-1}] - /\ maxVal \in [Acceptor -> Value \cup {None}] - /\ msgs \subseteq Message - -(***************************************************************************) -(* The initial predicate should be obvious from the descriptions of the *) -(* variables given above. *) -(***************************************************************************) -Init == /\ maxBal = [a \in Acceptor |-> -1] - /\ maxVBal = [a \in Acceptor |-> -1] - /\ maxVal = [a \in Acceptor |-> None] - /\ msgs = {} ----------------------------------------------------------------------------- -(***************************************************************************) -(* We now define the subactions of the next-state actions. We begin by *) -(* defining an action that will be used in those subactions. The action *) -(* Send(m) asserts that message m is added to the set msgs. *) -(***************************************************************************) -Send(m) == msgs' = msgs \cup {m} - -(***************************************************************************) -(* The ballot b leader can perform actions Phase1a(b) and Phase2a(b). In *) -(* the Phase1a(b) action, it sends to all acceptors a phase 1a message (a *) -(* message m with m.type = "1a") that begins ballot b. Remember that the *) -(* same process can perform the role of leader for many different ballot *) -(* numbers b. In practice, it will stop playing the role of leader of *) -(* ballot b when it begins a higher-numbered ballot. (Remember the *) -(* definition of [type |-> "1a", bal |-> b] from the comment preceding the *) -(* definition of Message.) *) -(***************************************************************************) -Phase1a(b) == /\ Send([type |-> "1a", bal |-> b]) - /\ UNCHANGED <> - (************************************************************************) - (* Note that there is no enabling condition to prevent sending the *) - (* phase 1a message a second time. Since messages are never removed *) - (* from msg, performing the action a second time leaves msg and all the *) - (* other spec variables unchanged, so it's a stuttering step. Since *) - (* stuttering steps are always allowed, there's no reason to try to *) - (* prevent them. *) - (************************************************************************) - -(***************************************************************************) -(* Upon receipt of a ballot b phase 1a message, acceptor a can perform a *) -(* Phase1b(a) action only if b > maxBal[a]. The action sets maxBal[a] to *) -(* b and sends a phase 1b message to the leader containing the values of *) -(* maxVBal[a] and maxVal[a]. This action implements the *) -(* IncreaseMaxBal(a,b) action of the Voting algorithm for b = m.bal. *) -(***************************************************************************) -Phase1b(a) == - /\ \E m \in msgs : - /\ m.type = "1a" - /\ m.bal > maxBal[a] - /\ maxBal' = [maxBal EXCEPT ![a] = m.bal] - /\ Send([type |-> "1b", acc |-> a, bal |-> m.bal, - mbal |-> maxVBal[a], mval |-> maxVal[a]]) - /\ UNCHANGED <> - -(**************************************************************************** -In the Phase2a(b, v) action, the ballot b leader sends a type "2a" -message asking the acceptors to vote for v in ballot number b. The -enabling conditions of the action--its first two conjuncts--ensure that -three of the four enabling conditions of action VoteFor(a, b, v) in -module Voting will be true when acceptor a receives that message. -Those three enabling conditions are the second through fourth conjuncts -of that action. - -The first conjunct of Phase2a(b, v) asserts that at most one phase 2a -message is ever sent for ballot b. Since an acceptor will vote for a -value in ballot b only when it receives the appropriate phase 2a -message, the phase 2a message sent by this action this ensures that -these two enabling conjuncts of VoteFor(a,b,v) will be true forever: - - /\ \A vt \in votes[a] : vt[1] /= b - /\ \A c \in Acceptor \ {a} : - \A vt \in votes[c] : (vt[1] = b) => (vt[2] = v) - -The second conjunct of the Phase2a(b, v) action is the heart of the -Paxos consensus algorithm. It's a bit complicated, but I've tried a -number of times to write it in English, and it's much easier to -understand when written in mathematics. The LET/IN construct locally -defines Q1 to be the set of phase 1b messages sent in ballot number b -by acceptors in quorum Q; and it defines Q1bv to be the subset of those -messages indicating that the sender had voted in some ballot (which -must have been numbered less than b). You should study the IN clause -to convince yourself that it equals ShowsSafeAt(Q, b, v), defined in -module Voting, using the values of maxBal[a], maxVBal[a], and maxVal[a] -`a' sent in its phase 1b message to describe what votes it had cast -when it sent that message. Moreover, since `a' will no longer cast any -votes in ballots numbered less than b, the IN clause implies that -ShowsSafeAt(Q, b, v) is still true and will remain true forever. -Hence, this conjunct of Phase2a(b, v) checks the enabling condition - - /\ \E Q \in Quorum : ShowsSafeAt(Q, b, v) - -of module Voting's VoteFor(a, b, v) action. - -The type "2a" message sent by this action therefore tells every -acceptor `a' that, when it receives the message, all the enabling -conditions of VoteFor(a, b, v) but the first, maxBal[a] =< b, -are satisfied - - - -****************************************************************************) -Phase2a(b, v) == - /\ ~ \E m \in msgs : m.type = "2a" /\ m.bal = b - /\ \E Q \in Quorum : - LET Q1b == {m \in msgs : /\ m.type = "1b" - /\ m.acc \in Q - /\ m.bal = b} - Q1bv == {m \in Q1b : m.mbal >= 0} - IN /\ \A a \in Q : \E m \in Q1b : m.acc = a - /\ \/ Q1bv = {} - \/ \E m \in Q1bv : - /\ m.mval = v - /\ \A mm \in Q1bv : m.mbal >= mm.mbal - /\ Send([type |-> "2a", bal |-> b, val |-> v]) - /\ UNCHANGED <> - - -(*************************************************************************** -The Phase2b(a) action describes what acceptor `a' does when it -receives a phase 2a message m, which is sent by the leader of -ballot m.bal asking acceptors to vote for m.val in that ballot. -Acceptor `a' acts on that request, voting for m.val in ballot -number m.bal, iff m.bal >= maxBal[a], which means that `a' has -not participated in any ballot numbered greater than m.bal. - - ***************************************************************************) -Phase2b(a) == - \E m \in msgs : - /\ m.type = "2a" - /\ m.bal >= maxBal[a] - /\ maxBal' = [maxBal EXCEPT ![a] = m.bal] - /\ maxVBal' = [maxVBal EXCEPT ![a] = m.bal] - /\ maxVal' = [maxVal EXCEPT ![a] = m.val] - /\ Send([type |-> "2b", acc |-> a, - bal |-> m.bal, val |-> m.val]) - -Next == \/ \E b \in Ballot : \/ Phase1a(b) - \/ \E v \in Value : Phase2a(b, v) - \/ \E a \in Acceptor : Phase1b(a) \/ Phase2b(a) - -Spec == Init /\ [][Next]_vars ----------------------------------------------------------------------------- -votes == - [a \in Acceptor |-> - {<> : m \in {mm \in msgs: /\ mm.type = "2b" - /\ mm.acc = a }}] - -V == INSTANCE Voting - -Inv == - /\ TypeOK - /\ \A a \in Acceptor : maxBal[a] >= maxVBal[a] - /\ \A a \in Acceptor : IF maxVBal[a] = -1 - THEN maxVal[a] = None - ELSE <> \in votes[a] - /\ \A m \in msgs : - /\ (m.type = "1b") => /\ maxBal[m.acc] >= m.bal - /\ (m.mbal >= 0) => - <> \in votes[m.acc] - /\ (m.type = "2a") => /\ \E Q \in Quorum : - V!ShowsSafeAt(Q, m.bal, m.val) - /\ \A mm \in msgs : /\ mm.type ="2a" - /\ mm.bal = m.bal - => mm.val = m.val - /\ (m.type = "2b") => /\ maxVBal[m.acc] >= m.bal - /\ \E mm \in msgs : /\ mm.type = "2a" - /\ mm.bal = m.bal - /\ mm.val = m.val - -THEOREM Invariance == Spec => []Inv - -THEOREM Implementation == Spec => V!Spec -============================================================================ diff --git a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/Voting.tla b/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/Voting.tla deleted file mode 100644 index 0cfd268e..00000000 --- a/specifications/PaxosHowToWinATuringAward/Paxos.toolbox/TinyModel/Voting.tla +++ /dev/null @@ -1,300 +0,0 @@ ------------------------------- MODULE Voting ------------------------------- -(***************************************************************************) -(* This is a high-level algorithm in which a set of processes *) -(* cooperatively choose a value. It is a high-level abstraction of the *) -(* Paxos consensus algorithm. Although I don't remember exactly what went *) -(* through my mind when I invented/discovered that algorithm, I'm pretty *) -(* sure that this spec formalizes the way I first thought of the *) -(* algorithm. It would have been very hard to find this algorithm had my *) -(* mind been distracted by the irrelevant details introduced by having the *) -(* processes communicate by messages. *) -(***************************************************************************) -EXTENDS Integers - -(***************************************************************************) -(* For historical reasons, the processes that choose a value are called *) -(* acceptors. We now declare the set Value of values, the set Acceptors *) -(* of acceptors, and another set Quorum that is a set of sets of acceptors *) -(* called quorums. *) -(***************************************************************************) -CONSTANTS Value, Acceptor, Quorum - -(***************************************************************************) -(* The following assumption asserts that Quorum is a set of subsets of the *) -(* set Acceptor, and that any two elements of Quorum have at least one *) -(* element (an acceptor) in common. Think of a quorum as a set consisting *) -(* of a majority (more than half) of the acceptors. *) -(***************************************************************************) -ASSUME /\ \A Q \in Quorum : Q \subseteq Acceptor - /\ \A Q1, Q2 \in Quorum : Q1 \cap Q2 /= {} - -(***************************************************************************) -(* Ballot is a set of "ballot numbers". For simplicity, we let it be the *) -(* set of natural numbers. However, we write Ballot for that set to *) -(* distinguish ballots from natural numbers used for other purposes. *) -(***************************************************************************) -Ballot == Nat ------------------------------------------------------------------------------ -(***************************************************************************) -(* The algorithm works by having acceptors cast votes in numbered ballots. *) -(* Each acceptor can cast one or more votes, where each vote cast by an *) -(* acceptor has the form <> indicating that the acceptor has voted *) -(* for value v in ballot number b. A value is chosen if a quorum of *) -(* acceptors have voted for it in the same ballot. *) -(* *) -(* We now declare the algorithm's variables 'votes' and 'maxBal'. For *) -(* each acceptor a, he value of votes[a] is the set of votes cast by `a'; *) -(* and maxBal[a] is an integer such that `a' will never cast any further *) -(* vote in a ballot numbered less than maxBal[a]. *) -(***************************************************************************) -VARIABLES votes, maxBal - -(***************************************************************************) -(* TypeOK asserts the "types" of the two variables. They are both *) -(* functions with domain Acceptor (arrays indexed by acceptors). For any *) -(* acceptor a, the value of votes[a] a set of <> pairs; and *) -(* the value of maxBal[a] is either a ballot number or -1. *) -(***************************************************************************) -TypeOK == - /\ votes \in [Acceptor -> SUBSET (Ballot \X Value)] - /\ maxBal \in [Acceptor -> Ballot \cup {-1}] - -(***************************************************************************) -(* Next comes a sequence of definitions of concepts used to explain the *) -(* algorithm. *) -(***************************************************************************) -VotedFor(a, b, v) == <> \in votes[a] - (************************************************************************) - (* True iff (if and only if) acceptor a has votted for value v in *) - (* ballot number b. *) - (************************************************************************) - -ChosenAt(b, v) == - \E Q \in Quorum : \A a \in Q : VotedFor(a, b, v) - (************************************************************************) - (* True iff a quorum of acceptors have all voted for value v in ballot *) - (* number b. *) - (************************************************************************) - -chosen == {v \in Value : \E b \in Ballot : ChosenAt(b, v)} - (************************************************************************) - (* Defines `chosen' to be the set of all values v for which ChosenAt(b, *) - (* v) is true for some ballot number b. This is the definition of what *) - (* it means for a value to be chosen under which the Voting algorithm *) - (* implements the Consensus specification. *) - (************************************************************************) - -DidNotVoteAt(a, b) == \A v \in Value : ~ VotedFor(a, b, v) - (************************************************************************) - (* True iff acceptor `a' has not voted in ballot number . *) - (************************************************************************) - -CannotVoteAt(a, b) == /\ maxBal[a] > b - /\ DidNotVoteAt(a, b) - (************************************************************************) - (* The algorithm will not allow acceptor `a' to vote in ballot number b *) - (* if maxBal[a] > b. Hence, CannotVoteAt(a, b) implies that `a' has *) - (* not and never will vote in ballot number b. *) - (************************************************************************) - -NoneOtherChoosableAt(b, v) == - \E Q \in Quorum : - \A a \in Q : VotedFor(a, b, v) \/ CannotVoteAt(a, b) - (************************************************************************) - (* This is true iff there is some quorum Q such that each acceptor `a' *) - (* in Q either has voted for v in ballot b or has not and never will *) - (* vote in ballot b. It implies that no value other than v has been or *) - (* ever can be chosen at ballot b. This is because for a value w to be *) - (* chosen at ballot b, all the acceptors in some quorum R must have *) - (* voted for w in ballot b. But any two ballots have an acceptor in *) - (* common, so some acceptor a in R that voted for w is in Q, and an *) - (* acceptor in Q can only have voted for v, so w must equal v. *) - (************************************************************************) - -SafeAt(b, v) == \A c \in 0..(b-1) : NoneOtherChoosableAt(c, v) - (************************************************************************) - (* True iff no value other than v has been or ever will be chosen in *) - (* any ballot numbered less than b. We read SafeAt(b, v) as "v is safe *) - (* at b". *) - (************************************************************************) - -(***************************************************************************) -(* This theorem asserts that every value is safe at ballot 0. *) -(***************************************************************************) -THEOREM AllSafeAtZero == \A v \in Value : SafeAt(0, v) - -(***************************************************************************) -(* The following theorem asserts that NoneOtherChoosableAt means what it's *) -(* name implies. The comments after its definition essentially contain a *) -(* proof of this theorem. *) -(***************************************************************************) -THEOREM ChoosableThm == - \A b \in Ballot, v \in Value : - ChosenAt(b, v) => NoneOtherChoosableAt(b, v) - -(***************************************************************************) -(* Now comes the definition of the inductive invariant Inv that *) -(* essentially explains why the algorithm is correct. *) -(***************************************************************************) -OneValuePerBallot == - \A a1, a2 \in Acceptor, b \in Ballot, v1, v2 \in Value : - VotedFor(a1, b, v1) /\ VotedFor(a2, b, v2) => (v1 = v2) - (************************************************************************) - (* This formula asserts that if any acceptors a1 and a2 have voted in a *) - (* ballot b, then they voted for the same value in ballot b. For *) - (* a1=a2, this implies that an acceptor can vote for at most one value *) - (* in any ballot. *) - (************************************************************************) - -VotesSafe == \A a \in Acceptor, b \in Ballot, v \in Value : - VotedFor(a, b, v) => SafeAt(b, v) - (************************************************************************) - (* This formula asserts that an acceptors can have voted in a ballot b *) - (* only if that value is safe at b. *) - (************************************************************************) - -(***************************************************************************) -(* The algorithm is essentially derived by ensuring that this formula Inv *) -(* is always true. *) -(***************************************************************************) -Inv == TypeOK /\ VotesSafe /\ OneValuePerBallot - -(***************************************************************************) -(* This definition is used in the defining the algorithm. You should *) -(* study it and make sure you understand what it says. *) -(***************************************************************************) -ShowsSafeAt(Q, b, v) == - /\ \A a \in Q : maxBal[a] >= b - /\ \E c \in -1..(b-1) : - /\ (c /= -1) => \E a \in Q : VotedFor(a, c, v) - /\ \A d \in (c+1)..(b-1), a \in Q : DidNotVoteAt(a, d) - -(***************************************************************************) -(* This is the theorem that's at the heart of the algorithm. It shows *) -(* that if the algorithm has maintained the invariance of Inv, then the *) -(* truth of ShowsSafeAt(Q, b, v) for some quorum Q ensures that v is safe *) -(* at b, so the algorithm can let an acceptor vote for v in ballot b *) -(* knowing VotesSafe will be preserved. *) -(***************************************************************************) -THEOREM ShowsSafety == - Inv => \A Q \in Quorum, b \in Ballot, v \in Value : - ShowsSafeAt(Q, b, v) => SafeAt(b, v) ------------------------------------------------------------------------------ -(***************************************************************************) -(* Finally, we get to the definition of the algorithm. The initial *) -(* predicate is obvious. *) -(***************************************************************************) -Init == /\ votes = [a \in Acceptor |-> {}] - /\ maxBal = [a \in Acceptor |-> -1] - -(***************************************************************************) -(* An acceptor `a' can increase maxBal[a] at any time. *) -(***************************************************************************) -IncreaseMaxBal(a, b) == - /\ b > maxBal[a] - /\ maxBal' = [maxBal EXCEPT ![a] = b] - /\ UNCHANGED votes - -(***************************************************************************) -(* The heart of the algorithm is the action in which an acceptor `a' votes *) -(* for a value v in ballot number b. The enabling condition contains the *) -(* following conjuncts, which ensure that the invariance of Inv is *) -(* maintained. *) -(* *) -(* - `a' cannot vote in a ballot numbered less than b *) -(* *) -(* - `a' cannot already have voted in ballot number b *) -(* *) -(* - No other acceptor can have voted for a value other than v *) -(* in ballot b. *) -(* *) -(* - Uses Theorem ShowsSafety to ensure that v is safe at b. *) -(* *) -(* In TLA+, a tuple t is a function (array) whose first element is t[1], *) -(* whose second element if t[2], and so on. Thus, a vote vt is the pair *) -(* <> *) -(***************************************************************************) -VoteFor(a, b, v) == - /\ maxBal[a] =< b - /\ \A vt \in votes[a] : vt[1] /= b - /\ \A c \in Acceptor \ {a} : - \A vt \in votes[c] : (vt[1] = b) => (vt[2] = v) - /\ \E Q \in Quorum : ShowsSafeAt(Q, b, v) - /\ votes' = [votes EXCEPT ![a] = votes[a] \cup {<>}] - /\ maxBal' = [maxBal EXCEPT ![a] = b] - -(***************************************************************************) -(* The rest of the spec is straightforward. *) -(***************************************************************************) -Next == \E a \in Acceptor, b \in Ballot : - \/ IncreaseMaxBal(a, b) - \/ \E v \in Value : VoteFor(a, b, v) - -Spec == Init /\ [][Next]_<> ------------------------------------------------------------------------------ -(***************************************************************************) -(* This theorem asserts that Inv is an invariant of the algorithm. The *) -(* high-level steps in its proof are given. *) -(***************************************************************************) -THEOREM Invariance == Spec => []Inv -<1>1. Init => Inv - -<1>2. Inv /\ [Next]_<> => Inv' - -<1>3. QED - BY <1>1, <1>2 DEF Spec ------------------------------------------------------------------------------ -(***************************************************************************) -(* This INSTANCE statement imports definitions from module Consensus into *) -(* the current module. All definition in module Consensus can be expanded *) -(* to definitions containing only TLA+ primitives and the declared names *) -(* Value and chosen. To import a definition from Consensus into the *) -(* current module, we have to say what expressions from the current module *) -(* are substituted for Value and chosen. The INSTANCE statement says that *) -(* expressions of the same name are substituted for them. (Because of *) -(* this, the WITH statement is redundant.) Note that in both modules, *) -(* Value is just a declared constant. However, in the current module, *) -(* `chosen' is an expression defined in terms of the variables votes and *) -(* maxBal while it is a variable in module consensus. The "C! ==" in the *) -(* statement means that defined identifiers are imported with "C!" *) -(* prepended to their names. Thus Spec of module Consensus is imported, *) -(* with these substitutions, as C!Spec. *) -(***************************************************************************) -C == INSTANCE Consensus - WITH Value <- Value, chosen <- chosen - -(***************************************************************************) -(* The following theorem asserts that the Voting algorithm implements the *) -(* Consensus specification, where the expression `chosen' of the current *) -(* module implements the variable `chosen' of Consensus. The high-level *) -(* steps of the the proof are also given. *) -(***************************************************************************) -THEOREM Implementation == Spec => C!Spec -<1>1. Init => C!Init - -<1>2. Inv /\ Inv' /\ [Next]_<> => [C!Next]_chosen - -<1>3. QED - BY <1>1, <1>2, Invariance DEF Spec, C!Spec - -(***************************************************************************) -(* You can run TLC on model SmallModel in a few seconds. That model *) -(* instantiates Acceptor and Values as symmetric sets of model values with *) -(* 3 acceptors and 2 values, and uses a definition override (on the Spec *) -(* Options page) to redefine Ballot to equal 0..2. It checks theorems *) -(* Invariance and Implementation stated above. TLC executes it in a *) -(* couple of seconds. *) -(* *) -(* After doing that, show why the assumption that any pair of quorums has *) -(* an element in common by modifying the model so that assumption doesn't *) -(* hold. (It's best to clone SmallModel and modify the clone.) Since TLC *) -(* reports an error if an assumption isn't true You will have to comment *) -(* out the second conjunct of the ASSUME statement, which asserts that *) -(* assumption. Comments can be written as follows: *) -(* *) -(* \* This is an end of line comment. *) -(* *) -(* (* This is another way to write a comment. *) -(* Note that comments can be nested. *) *) -(***************************************************************************) -============================================================================= diff --git a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/.project b/specifications/PaxosHowToWinATuringAward/Voting.toolbox/.project deleted file mode 100644 index 9d851e42..00000000 --- a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/.project +++ /dev/null @@ -1,29 +0,0 @@ - - - Voting - - - - - - toolbox.builder.TLAParserBuilder - - - - - - toolbox.natures.TLANature - - - - Consensus.tla - 1 - PARENT-1-PROJECT_LOC/Consensus.tla - - - Voting.tla - 1 - PARENT-1-PROJECT_LOC/Voting.tla - - - diff --git a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/.settings/org.lamport.tla.toolbox.prefs b/specifications/PaxosHowToWinATuringAward/Voting.toolbox/.settings/org.lamport.tla.toolbox.prefs deleted file mode 100644 index 8a0e2766..00000000 --- a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/.settings/org.lamport.tla.toolbox.prefs +++ /dev/null @@ -1,2 +0,0 @@ -ProjectRootFile=PARENT-1-PROJECT_LOC/Voting.tla -eclipse.preferences.version=1 diff --git a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/Consensus.tla b/specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/Consensus.tla deleted file mode 100644 index 5fa47a70..00000000 --- a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/Consensus.tla +++ /dev/null @@ -1,113 +0,0 @@ ------------------------------ MODULE Consensus ------------------------------ -(***************************************************************************) -(* This is an very abstract specification of the consensus problem, in *) -(* which a set of processes must choose a single value. We abstract away *) -(* even the processes. We specify the simple requirement that at most one *) -(* value is chosen by describing the set of all chosen values. The naive *) -(* requirement is that this set never contains more than one value, which *) -(* is an invariance property. But a little thought shows that this *) -(* requirement allows a value to be chosen then unchosen, and then another *) -(* value to be chosen. So we specify that the set of chosen values is *) -(* initially empty, it can be set to a single value, and then it can never *) -(* change. *) -(* *) -(* We are ignoring liveness, so we do not any requirement that a value is *) -(* eventually chosen. *) -(***************************************************************************) - -EXTENDS Naturals, FiniteSets - (*************************************************************************) - (* Imports standard modules that define operators of arithmetic on *) - (* natural numbers and the Cardinality operator, where Cardinality(S) is *) - (* the number of elements in the set S, if S is finite. *) - (*************************************************************************) -CONSTANT Value - (*************************************************************************) - (* The set of all values that can be chosen. *) - (*************************************************************************) -VARIABLE chosen - (*************************************************************************) - (* The set of all values that have been chosen. *) - (*************************************************************************) - -(***************************************************************************) -(* The type-correctness invariant asserting the "type" of the variable *) -(* 'chosen'. It isn't part of the spec itself--that is, the formula *) -(* describing the possible sequence of values that 'chosen' can have in a *) -(* behavior correct behavior of the system, but is an invariance property *) -(* that the spec should satisfy. *) -(***************************************************************************) -TypeOK == /\ chosen \subseteq Value - /\ IsFiniteSet(chosen) - -(***************************************************************************) -(* The initial predicate describing the possible initial state of *) -(* 'chosen'. *) -(***************************************************************************) -Init == chosen = {} - -(***************************************************************************) -(* The next-state relation describing how 'chosen' can change from one *) -(* step to the next. Note that is enabled (equals true for some next *) -(* value chosen' of choseen) if and only if chosen equals the empty set. *) -(***************************************************************************) -Next == /\ chosen = {} - /\ \E v \in Value : chosen' = {v} - -(***************************************************************************) -(* The TLA+ temporal formula that is the spec. *) -(***************************************************************************) -Spec == Init /\ [][Next]_chosen - ------------------------------------------------------------------------------ -(***************************************************************************) -(* The specification should imply the safety property that 'chosen' can *) -(* contain at most one value in any reachable state. This condition on *) -(* the state is expressed by Inv defined here. *) -(***************************************************************************) -Inv == /\ TypeOK - /\ Cardinality(chosen) \leq 1 - -(***************************************************************************) -(* The following theorem asserts the desired safety propert. Its proof *) -(* appears after the theorem. This proof is easily checked by the TLAPS *) -(* prover. *) -(***************************************************************************) -THEOREM Invariance == Spec => []Inv -<1>1. Init => Inv - -<1>2. Inv /\ [Next]_chosen => Inv' - -<1>3. QED - BY <1>1, <1>2 DEF Spec - -(***************************************************************************) -(* If you are reading this specification in the Toolbox as you should be *) -(* (either the source file or its pretty-printed version), then you have *) -(* already opened the specification in the Toolbox. If not, you should do *) -(* that now. Download and run the Toolbox. Open a new specification with *) -(* this module file (Consensus.tla) as the root file, using the default *) -(* specification name, which is the name of the root file. Along with the *) -(* module, this will install a TLC model named 3Values. Open that model. *) -(* You will see that the model specifies three things: *) -(* *) -(* - The specification is formula Spec. *) -(* *) -(* - Three unspecified constants a, b, and c (called model values) *) -(* are substituted for the declared constants Values. *) -(* *) -(* - TLC should check that formula Inv is an invariant (a *) -(* formula true on all reachable states of he specification. *) -(* *) -(* Run TLC on the model. For this tiny spec, this just takes perhaps a *) -(* millisecond plus the couple of seconds that TLC needs to start and stop *) -(* running any spec. *) -(* *) -(* TLC's default setting to check for deadlock would cause it to report a *) -(* deadlock because no action is possible after a value is chosen. We *) -(* would say that the system terminated, but termination is just deadlock *) -(* that we want to happen, and the model tells TLC that we want deadlock *) -(* by disabling its check for it. *) -(***************************************************************************) - -============================================================================= diff --git a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/FiniteSets.tla b/specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/FiniteSets.tla deleted file mode 100644 index 57ac4023..00000000 --- a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/FiniteSets.tla +++ /dev/null @@ -1,23 +0,0 @@ ----------------------------- MODULE FiniteSets ----------------------------- -LOCAL INSTANCE Naturals -LOCAL INSTANCE Sequences - (*************************************************************************) - (* Imports the definitions from Naturals and Sequences, but doesn't *) - (* export them. *) - (*************************************************************************) - -IsFiniteSet(S) == - (*************************************************************************) - (* A set S is finite iff there is a finite sequence containing all its *) - (* elements. *) - (*************************************************************************) - \E seq \in Seq(S) : \A s \in S : \E n \in 1..Len(seq) : seq[n] = s - -Cardinality(S) == - (*************************************************************************) - (* Cardinality is defined only for finite sets. *) - (*************************************************************************) - LET CS[T \in SUBSET S] == IF T = {} THEN 0 - ELSE 1 + CS[T \ {CHOOSE x : x \in T}] - IN CS[S] -============================================================================= diff --git a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/Voting.tla b/specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/Voting.tla deleted file mode 100644 index 6a6892c8..00000000 --- a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/SmallModel/Voting.tla +++ /dev/null @@ -1,315 +0,0 @@ ------------------------------- MODULE Voting ------------------------------- -(***************************************************************************) -(* This is a high-level algorithm in which a set of processes *) -(* cooperatively choose a value. It is a high-level abstraction of the *) -(* Paxos consensus algorithm. Although I don't remember exactly what went *) -(* through my mind when I invented/discovered that algorithm, I'm pretty *) -(* sure that this spec formalizes the way I first thought of the *) -(* algorithm. It would have been very hard to find this algorithm had my *) -(* mind been distracted by the irrelevant details introduced by having the *) -(* processes communicate by messages. *) -(***************************************************************************) -EXTENDS Integers - -(***************************************************************************) -(* For historical reasons, the processes that choose a value are called *) -(* acceptors. We now declare the set Value of values, the set Acceptors *) -(* of acceptors, and another set Quorum that is a set of sets of acceptors *) -(* called quorums. *) -(***************************************************************************) -CONSTANTS Value, Acceptor, Quorum - -(***************************************************************************) -(* The following assumption asserts that Quorum is a set of subsets of the *) -(* set Acceptor, and that any two elements of Quorum have at least one *) -(* element (an acceptor) in common. Think of a quorum as a set consisting *) -(* of a majority (more than half) of the acceptors. *) -(***************************************************************************) -ASSUME /\ \A Q \in Quorum : Q \subseteq Acceptor - /\ \A Q1, Q2 \in Quorum : Q1 \cap Q2 /= {} - -(***************************************************************************) -(* Ballot is a set of "ballot numbers". For simplicity, we let it be the *) -(* set of natural numbers. However, we write Ballot for that set to *) -(* distinguish ballots from natural numbers used for other purposes. *) -(***************************************************************************) -Ballot == Nat ------------------------------------------------------------------------------ -(***************************************************************************) -(* The algorithm works by having acceptors cast votes in numbered ballots. *) -(* Each acceptor can cast one or more votes, where each vote cast by an *) -(* acceptor has the form <> indicating that the acceptor has voted *) -(* for value v in ballot number b. A value is chosen if a quorum of *) -(* acceptors have voted for it in the same ballot. *) -(* *) -(* We now declare the algorithm's variables 'votes' and 'maxBal'. For *) -(* each acceptor a, he value of votes[a] is the set of votes cast by `a'; *) -(* and maxBal[a] is an integer such that `a' will never cast any further *) -(* vote in a ballot numbered less than maxBal[a]. *) -(***************************************************************************) -VARIABLES votes, maxBal - -(***************************************************************************) -(* TypeOK asserts the "types" of the two variables. They are both *) -(* functions with domain Acceptor (arrays indexed by acceptors). For any *) -(* acceptor a, the value of votes[a] a set of <> pairs; and *) -(* the value of maxBal[a] is either a ballot number or -1. *) -(***************************************************************************) -TypeOK == - /\ votes \in [Acceptor -> SUBSET (Ballot \X Value)] - /\ maxBal \in [Acceptor -> Ballot \cup {-1}] - -(***************************************************************************) -(* Next comes a sequence of definitions of concepts used to explain the *) -(* algorithm. *) -(***************************************************************************) -VotedFor(a, b, v) == <> \in votes[a] - (************************************************************************) - (* True iff (if and only if) acceptor a has votted for value v in *) - (* ballot number b. *) - (************************************************************************) - -ChosenAt(b, v) == - \E Q \in Quorum : \A a \in Q : VotedFor(a, b, v) - (************************************************************************) - (* True iff a quorum of acceptors have all voted for value v in ballot *) - (* number b. *) - (************************************************************************) - -chosen == {v \in Value : \E b \in Ballot : ChosenAt(b, v)} - (************************************************************************) - (* Defines `chosen' to be the set of all values v for which ChosenAt(b, *) - (* v) is true for some ballot number b. This is the definition of what *) - (* it means for a value to be chosen under which the Voting algorithm *) - (* implements the Consensus specification. *) - (************************************************************************) - -DidNotVoteAt(a, b) == \A v \in Value : ~ VotedFor(a, b, v) - (************************************************************************) - (* True iff acceptor `a' has not voted in ballot number . *) - (************************************************************************) - -CannotVoteAt(a, b) == /\ maxBal[a] > b - /\ DidNotVoteAt(a, b) - (************************************************************************) - (* The algorithm will not allow acceptor `a' to vote in ballot number b *) - (* if maxBal[a] > b. Hence, CannotVoteAt(a, b) implies that `a' has *) - (* not and never will vote in ballot number b. *) - (************************************************************************) - -NoneOtherChoosableAt(b, v) == - \E Q \in Quorum : - \A a \in Q : VotedFor(a, b, v) \/ CannotVoteAt(a, b) - (************************************************************************) - (* This is true iff there is some quorum Q such that each acceptor `a' *) - (* in Q either has voted for v in ballot b or has not and never will *) - (* vote in ballot b. It implies that no value other than v has been or *) - (* ever can be chosen at ballot b. This is because for a value w to be *) - (* chosen at ballot b, all the acceptors in some quorum R must have *) - (* voted for w in ballot b. But any two ballots have an acceptor in *) - (* common, so some acceptor a in R that voted for w is in Q, and an *) - (* acceptor in Q can only have voted for v, so w must equal v. *) - (************************************************************************) - -SafeAt(b, v) == \A c \in 0..(b-1) : NoneOtherChoosableAt(c, v) - (************************************************************************) - (* True iff no value other than v has been or ever will be chosen in *) - (* any ballot numbered less than b. We read SafeAt(b, v) as "v is safe *) - (* at b". *) - (************************************************************************) - -(***************************************************************************) -(* This theorem asserts that every value is safe at ballot 0. *) -(***************************************************************************) -THEOREM AllSafeAtZero == \A v \in Value : SafeAt(0, v) - -(***************************************************************************) -(* The following theorem asserts that NoneOtherChoosableAt means what it's *) -(* name implies. The comments after its definition essentially contain a *) -(* proof of this theorem. *) -(***************************************************************************) -THEOREM ChoosableThm == - \A b \in Ballot, v \in Value : - ChosenAt(b, v) => NoneOtherChoosableAt(b, v) - -(***************************************************************************) -(* Now comes the definition of the inductive invariant Inv that *) -(* essentially explains why the algorithm is correct. *) -(***************************************************************************) -OneValuePerBallot == - \A a1, a2 \in Acceptor, b \in Ballot, v1, v2 \in Value : - VotedFor(a1, b, v1) /\ VotedFor(a2, b, v2) => (v1 = v2) - (************************************************************************) - (* This formula asserts that if any acceptors a1 and a2 have voted in a *) - (* ballot b, then they voted for the same value in ballot b. For *) - (* a1=a2, this implies that an acceptor can vote for at most one value *) - (* in any ballot. *) - (************************************************************************) - -VotesSafe == \A a \in Acceptor, b \in Ballot, v \in Value : - VotedFor(a, b, v) => SafeAt(b, v) - (************************************************************************) - (* This formula asserts that an acceptors can have voted in a ballot b *) - (* only if that value is safe at b. *) - (************************************************************************) - -(***************************************************************************) -(* The algorithm is essentially derived by ensuring that this formula Inv *) -(* is always true. *) -(***************************************************************************) -Inv == TypeOK /\ VotesSafe /\ OneValuePerBallot - -(***************************************************************************) -(* This definition is used in the defining the algorithm. You should *) -(* study it and make sure you understand what it says. *) -(***************************************************************************) -ShowsSafeAt(Q, b, v) == - /\ \A a \in Q : maxBal[a] >= b - /\ \E c \in -1..(b-1) : - /\ (c /= -1) => \E a \in Q : VotedFor(a, c, v) - /\ \A d \in (c+1)..(b-1), a \in Q : DidNotVoteAt(a, d) - -(***************************************************************************) -(* This is the theorem that's at the heart of the algorithm. It shows *) -(* that if the algorithm has maintained the invariance of Inv, then the *) -(* truth of ShowsSafeAt(Q, b, v) for some quorum Q ensures that v is safe *) -(* at b, so the algorithm can let an acceptor vote for v in ballot b *) -(* knowing VotesSafe will be preserved. *) -(***************************************************************************) -THEOREM ShowsSafety == - Inv => \A Q \in Quorum, b \in Ballot, v \in Value : - ShowsSafeAt(Q, b, v) => SafeAt(b, v) ------------------------------------------------------------------------------ -(***************************************************************************) -(* Finally, we get to the definition of the algorithm. The initial *) -(* predicate is obvious. *) -(***************************************************************************) -Init == /\ votes = [a \in Acceptor |-> {}] - /\ maxBal = [a \in Acceptor |-> -1] - -(***************************************************************************) -(* An acceptor `a' can increase maxBal[a] at any time. *) -(***************************************************************************) -IncreaseMaxBal(a, b) == - /\ b > maxBal[a] - /\ maxBal' = [maxBal EXCEPT ![a] = b] - /\ UNCHANGED votes - -(***************************************************************************) -(* The heart of the algorithm is the action in which an acceptor `a' votes *) -(* for a value v in ballot number b. The enabling condition contains the *) -(* following conjuncts, which ensure that the invariance of Inv is *) -(* maintained. *) -(* *) -(* - `a' cannot vote in a ballot numbered less than b *) -(* *) -(* - `a' cannot already have voted in ballot number b *) -(* *) -(* - No other acceptor can have voted for a value other than v *) -(* in ballot b. *) -(* *) -(* - Uses Theorem ShowsSafety to ensure that v is safe at b. *) -(* *) -(* In TLA+, a tuple t is a function (array) whose first element is t[1], *) -(* whose second element if t[2], and so on. Thus, a vote vt is the pair *) -(* <> *) -(***************************************************************************) -VoteFor(a, b, v) == - /\ maxBal[a] =< b - /\ \A vt \in votes[a] : vt[1] /= b - /\ \A c \in Acceptor \ {a} : - \A vt \in votes[c] : (vt[1] = b) => (vt[2] = v) - /\ \E Q \in Quorum : ShowsSafeAt(Q, b, v) - /\ votes' = [votes EXCEPT ![a] = votes[a] \cup {<>}] - /\ maxBal' = [maxBal EXCEPT ![a] = b] - -(***************************************************************************) -(* The rest of the spec is straightforward. *) -(***************************************************************************) -Next == \E a \in Acceptor, b \in Ballot : - \/ IncreaseMaxBal(a, b) - \/ \E v \in Value : VoteFor(a, b, v) - -Spec == Init /\ [][Next]_<> ------------------------------------------------------------------------------ -(***************************************************************************) -(* This theorem asserts that Inv is an invariant of the algorithm. The *) -(* high-level steps in its proof are given. *) -(***************************************************************************) -THEOREM Invariance == Spec => []Inv -<1>1. Init => Inv - -<1>2. Inv /\ [Next]_<> => Inv' - -<1>3. QED - BY <1>1, <1>2 DEF Spec ------------------------------------------------------------------------------ -(***************************************************************************) -(* This INSTANCE statement imports definitions from module Consensus into *) -(* the current module. All definition in module Consensus can be expanded *) -(* to definitions containing only TLA+ primitives and the declared names *) -(* Value and chosen. To import a definition from Consensus into the *) -(* current module, we have to say what expressions from the current module *) -(* are substituted for Value and chosen. The INSTANCE statement says that *) -(* expressions of the same name are substituted for them. (Because of *) -(* this, the WITH statement is redundant.) Note that in both modules, *) -(* Value is just a declared constant. However, in the current module, *) -(* `chosen' is an expression defined in terms of the variables votes and *) -(* maxBal while it is a variable in module consensus. The "C! ==" in the *) -(* statement means that defined identifiers are imported with "C!" *) -(* prepended to their names. Thus Spec of module Consensus is imported, *) -(* with these substitutions, as C!Spec. *) -(***************************************************************************) -C == INSTANCE Consensus - WITH Value <- Value, chosen <- chosen - -(***************************************************************************) -(* The following theorem asserts that the Voting algorithm implements the *) -(* Consensus specification, where the expression `chosen' of the current *) -(* module implements the variable `chosen' of Consensus. The high-level *) -(* steps of the the proof are also given. *) -(***************************************************************************) -THEOREM Implementation == Spec => C!Spec -<1>1. Init => C!Init - -<1>2. Inv /\ Inv' /\ [Next]_<> => [C!Next]_chosen - -<1>3. QED - BY <1>1, <1>2, Invariance DEF Spec, C!Spec - -(***************************************************************************) -(* This Voting specification comes with a TLC model named SmallModel. *) -(* That model tells TLC that Spec is the specification, that Acceptor and *) -(* Values should equal sets of model values with 3 acceptors and 2 values *) -(* and Quorums should equal the indicated set of values, and that it *) -(* should check theorems Invariance and Implementation. Observe that you *) -(* can't tell TLC simply to check those theorems; you have to tell TLC to *) -(* check the properties the theorems assert that Spec satisfies. (Instead *) -(* of telling TLC that Inv should be an invariant, you can tell it that *) -(* the spec should satisfy the temporal property []Inv.) *) -(* *) -(* Even though the constants are finite sets, the spec has infinitely many *) -(* reachable sets because a ballot number can be any element of the set *) -(* Nat of natural numbers. The model modifies the spec so it has a finite *) -(* set of reachable states by using a definition override (on the Spec *) -(* Options page) to redefine Ballot to equal 0..2. (Alternatively, we *) -(* could override the definition of Nat to equal 0..2.) *) -(* *) -(* Run TLC on the model. It should just take a couple of seconds. *) -(* *) -(* After doing that, show why the assumption that any pair of quorums has *) -(* an element in common is necessary by modifying the model so that *) -(* assumption doesn't hold. (It's best to clone SmallModel and modify the *) -(* clone.) Since TLC reports an error if an assumption isn't true, you *) -(* will have to comment out the second conjunct of the ASSUME statement, *) -(* which asserts that assumption. Comments can be written as follows: *) -(* *) -(* \* This is an end-of-line comment. *) -(* *) -(* (* This is another way to write a comment. *) -(* Note that comments can be nested. *) *) -(* *) -(* To help you see what the problem is, use the Trace Explorer on the *) -(* Error page to show the value of `chosen' in each state of the trace. *) -(***************************************************************************) -============================================================================= diff --git a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/Voting.pdf b/specifications/PaxosHowToWinATuringAward/Voting.toolbox/Voting.pdf deleted file mode 100644 index d3167c0f..00000000 Binary files a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/Voting.pdf and /dev/null differ diff --git a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/Voting___SmallModel.launch b/specifications/PaxosHowToWinATuringAward/Voting.toolbox/Voting___SmallModel.launch deleted file mode 100644 index f918b01f..00000000 --- a/specifications/PaxosHowToWinATuringAward/Voting.toolbox/Voting___SmallModel.launch +++ /dev/null @@ -1,57 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -