-
Notifications
You must be signed in to change notification settings - Fork 202
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Added missing Paxos (How to Win a Turing Award) models
Signed-off-by: Andrew Helwer <[email protected]>
- Loading branch information
Showing
23 changed files
with
2,550 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
91 changes: 91 additions & 0 deletions
91
specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/Consensus.tla
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,91 @@ | ||
| ----------------------------- 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 | ||
| ============================================================================= |
23 changes: 23 additions & 0 deletions
23
specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/FiniteSets.tla
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,23 @@ | ||
| ---------------------------- 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] | ||
| ============================================================================= |
17 changes: 17 additions & 0 deletions
17
specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/MC.cfg
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,17 @@ | ||
| \* MV CONSTANT declarations | ||
| CONSTANTS | ||
| a = a | ||
| b = b | ||
| c = c | ||
| \* MV CONSTANT definitions | ||
| CONSTANT | ||
| Value <- const_156017750645611000 | ||
| \* SPECIFICATION definition | ||
| SPECIFICATION | ||
| Spec | ||
| \* INVARIANT definition | ||
| INVARIANT | ||
| Inv | ||
| \* Generated on Mon Jun 10 07:38:26 PDT 2019 | ||
| CHECK_DEADLOCK FALSE | ||
|
|
16 changes: 16 additions & 0 deletions
16
specifications/PaxosHowToWinATuringAward/Consensus.toolbox/3Values/MC.tla
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,16 @@ | ||
| ---- MODULE MC ---- | ||
| EXTENDS Consensus, TLC | ||
|
|
||
| \* MV CONSTANT declarations@modelParameterConstants | ||
| CONSTANTS | ||
| a, b, c | ||
| ---- | ||
|
|
||
| \* MV CONSTANT definitions Value | ||
| const_156017750645611000 == | ||
| {a, b, c} | ||
| ---- | ||
|
|
||
| ============================================================================= | ||
| \* Modification History | ||
| \* Created Mon Jun 10 07:38:26 PDT 2019 by lamport |
Oops, something went wrong.