-
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.
Merge pull request #76 from TypeDefinition/master
Add Simplified Fast Paxos
- Loading branch information
Showing
9 changed files
with
483 additions
and
3 deletions.
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
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,21 @@ | ||
| CONSTANTS | ||
| any = any | ||
| none = none | ||
| r1 = r1 | ||
| r2 = r2 | ||
| r3 = r3 | ||
| r4 = r4 | ||
| Replicas = {r1, r2, r3, r4} | ||
| v1 = v1 | ||
| v2 = v2 | ||
| v3 = v3 | ||
| Values = {v1, v2, v3} | ||
| Ballots = {0, 1, 2, 3, 4} | ||
| FastBallots = {1, 3} | ||
| Quorums = {{r1, r2, r3}, {r1, r2, r4}, {r1, r3, r4}, {r2, r3, r4}} | ||
| FastQuorums = {{r1, r2, r3}, {r1, r2, r4}, {r1, r3, r4}, {r2, r3, r4}} | ||
|
|
||
| SPECIFICATION FastSpec | ||
| INVARIANTS FastTypeOK FastNontriviality | ||
| PROPERTY PaxosConsistency | ||
| SYMMETRY PaxosSymmetry |
Binary file not shown.
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,158 @@ | ||
| --------------------------- MODULE FastPaxos ----------------------------- | ||
| (* | ||
| This is a simplified specification of Leslie Lamport's Fast Paxos protocol. | ||
| The following papers, Fast Paxos by Leslie Lamport and Fast Paxos Made Easy: Theory and Implementation by Zhao Wenbing | ||
| was referenced in writing this specification. | ||
| This simplified specification was written by Lim Ngian Xin Terry & Gaurav Gandhi. | ||
| The following assumptions are made in this simplified specification. | ||
| 1. There is a unique coordinator in the system. Therefore, Phase 1a and 1b can be omitted. | ||
| 2. All agents in the system can communicate with one another. | ||
| 3. Agents must have some stable storage that survives failure and restarts. | ||
| An agent restores its state from stable storage when it restarts, so the failure of an agent | ||
| is indistinguishable from its simply pausing. There is thus no need to model failures explicitly. | ||
| *) | ||
|
|
||
| EXTENDS Paxos | ||
|
|
||
| CONSTANTS FastQuorums, FastBallots | ||
|
|
||
| VARIABLES cValue \* Value chosen by coordinator. | ||
|
|
||
| ClassicBallots == Ballots \ FastBallots \* The set of ballots of classic rounds. | ||
|
|
||
| FastAssume == | ||
| /\ \A q \in FastQuorums : q \subseteq Replicas | ||
| /\ \A q, r \in FastQuorums : q \intersect r # {} | ||
| /\ \A q \in FastQuorums : (3 * Cardinality(Replicas)) \div 4 <= Cardinality(q) | ||
| /\ \A q \in Quorums : \A r, s \in FastQuorums : q \intersect r \intersect s # {} | ||
|
|
||
| ASSUME PaxosAssume /\ FastAssume | ||
|
|
||
| IsMajorityValue(M, v) == Cardinality(M) \div 2 < Cardinality({m \in M : m.value = v}) | ||
|
|
||
| (* | ||
| Phase 2a (Fast): | ||
| The coordinator starts a fast round by sending a P2a "Any" message, if no other values has been proposed before. | ||
| *) | ||
| FastAny == | ||
| /\ UNCHANGED<<decision, maxBallot, maxVBallot, maxValue, cValue>> | ||
| /\ \E f \in FastBallots : | ||
| /\ SendMessage([type |-> "P2a", | ||
| ballot |-> f, | ||
| value |-> any]) | ||
|
|
||
| (* | ||
| Phase 2b (Fast): | ||
| Acceptors can reply to a P2a "Any" message with a P2b message containing their proposed value. | ||
| *) | ||
| FastPropose == | ||
| /\ UNCHANGED<<decision, cValue>> | ||
| /\ \E a \in Replicas, m \in p2aMessages, v \in Values: | ||
| /\ m.value = any | ||
| /\ maxBallot[a] <= m.ballot | ||
| /\ maxValue[a] = none \/ maxValue[a] = v | ||
| /\ maxBallot' = [maxBallot EXCEPT ![a] = m.ballot] | ||
| /\ maxVBallot' = [maxVBallot EXCEPT ![a] = m.ballot] | ||
| /\ maxValue' = [maxValue EXCEPT ![a] = v] | ||
| /\ \A n \in p2bMessages : ~(n.ballot = m.ballot /\ n.acceptor = a) | ||
| /\ SendMessage([type |-> "P2b", | ||
| ballot |-> m.ballot, | ||
| acceptor |-> a, | ||
| value |-> v]) | ||
|
|
||
| (* | ||
| A value is chosen if a fast quorum of acceptors proposed that value in a fast round. | ||
| Because the quorum size of a fast round and classic round is different, we assume that the acceptor distinguishes | ||
| a fast round and classic round based on the P2a message it receives. If the P2a message contains the special value | ||
| "any", it is a fast round. Else it is a classic round. | ||
| *) | ||
| FastDecide == | ||
| /\ UNCHANGED<<messages, maxBallot, maxVBallot, maxValue, cValue>> | ||
| /\ \E b \in FastBallots, q \in FastQuorums : | ||
| LET M == {m \in p2bMessages : m.ballot = b /\ m.acceptor \in q} | ||
| V == {w \in Values : \E m \in M : w = m.value} | ||
| IN /\ \A a \in q : \E m \in M : m.acceptor = a | ||
| /\ 1 = Cardinality(V) | ||
| /\ \E m \in M : decision' = m.value | ||
|
|
||
| (* | ||
| Phase 2a (Classic) | ||
| If more than one value has been proposed, the collision is resolved using the following rules: | ||
| 1. If the proposals contain different values, a value must be selected if the majority of | ||
| acceptors in the fast quorum have casted a vote for that value. | ||
| 2. Otherwise, the coordinator is free to select any value. | ||
| *) | ||
| ClassicAccept == | ||
| /\ UNCHANGED<<decision, maxBallot, maxVBallot, maxValue>> | ||
| /\ \E b \in ClassicBallots, f \in FastBallots, q \in FastQuorums, v \in Values : | ||
| /\ f < b \* There was a fast round before this classic round. | ||
| /\ cValue = none \/ cValue = v | ||
| /\ cValue' = v | ||
| /\ \A m \in p2aMessages : m.ballot # b | ||
| /\ LET M == {m \in p2bMessages : m.ballot = f /\ m.acceptor \in q} | ||
| V == {w \in Values : \E m \in M : w = m.value} | ||
| IN /\ \A a \in q : \E m \in M : m.acceptor = a | ||
| /\ 1 < Cardinality(V) \* Collision occured. | ||
| /\ IF \E w \in V : IsMajorityValue(M, w) | ||
| THEN IsMajorityValue(M, v) \* Choose majority in quorum. | ||
| ELSE v \in V \* Choose any. | ||
| /\ SendMessage([type |-> "P2a", | ||
| ballot |-> b, | ||
| value |-> v]) | ||
|
|
||
| (* | ||
| Phase 2b (Classic) | ||
| Same as in Paxos. | ||
| *) | ||
| ClassicAccepted == | ||
| /\ UNCHANGED<<cValue>> | ||
| /\ PaxosAccepted | ||
|
|
||
| (* | ||
| Consensus is achieved when a majority of acceptors accept the same ballot number. | ||
| Functionally similar to PaxosDecide in Paxos.tla, but we also have to | ||
| ensure that it can only occur in classic rounds and not fast rounds. | ||
| *) | ||
| ClassicDecide == | ||
| /\ UNCHANGED<<messages, maxBallot, maxVBallot, maxValue, cValue>> | ||
| /\ \E b \in ClassicBallots, q \in Quorums : | ||
| LET M == {m \in p2bMessages : m.ballot = b /\ m.acceptor \in q} | ||
| IN /\ \A a \in q : \E m \in M : m.acceptor = a | ||
| /\ \E m \in M : decision' = m.value | ||
|
|
||
| FastTypeOK == /\ PaxosTypeOK | ||
| /\ cValue \in Values \union {none} | ||
|
|
||
| FastInit == /\ PaxosInit | ||
| /\ cValue = none | ||
|
|
||
| FastNext == \/ FastAny | ||
| \/ FastPropose | ||
| \/ FastDecide | ||
| \/ ClassicAccept | ||
| \/ ClassicAccepted | ||
| \/ ClassicDecide | ||
|
|
||
| FastSpec == /\ FastInit | ||
| /\ [][FastNext]_<<messages, decision, maxBallot, maxVBallot, maxValue, cValue>> | ||
| /\ SF_<<messages, decision, maxBallot, maxVBallot, maxValue, cValue>>(FastDecide) | ||
| /\ SF_<<messages, decision, maxBallot, maxVBallot, maxValue, cValue>>(ClassicDecide) | ||
|
|
||
| \* Non-triviality safety property: Only proposed values can be learnt. | ||
| FastNontriviality == \/ decision = none | ||
| \/ \E m \in p2bMessages : m.value = decision /\ m.ballot \in FastBallots | ||
|
|
||
| =============================================================== |
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,19 @@ | ||
| CONSTANTS | ||
| any = any | ||
| none = none | ||
| r1 = r1 | ||
| r2 = r2 | ||
| r3 = r3 | ||
| r4 = r4 | ||
| Replicas = {r1, r2, r3, r4} | ||
| v1 = v1 | ||
| v2 = v2 | ||
| v3 = v3 | ||
| Values = {v1, v2, v3} | ||
| Ballots = {0, 1, 2} | ||
| Quorums = {{r1, r2, r3}, {r1, r2, r4}, {r1, r3, r4}, {r2, r3, r4}} | ||
|
|
||
| SPECIFICATION PaxosSpec | ||
| INVARIANTS PaxosTypeOK PaxosNontriviality | ||
| PROPERTY PaxosConsistency | ||
| SYMMETRY PaxosSymmetry |
Binary file not shown.
Oops, something went wrong.