Added models for byzpaxos

Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Jan 31, 2024 · cb9acd3 · cb9acd3
1 parent ca1dac7
commit cb9acd3
Show file tree

Hide file tree

Showing 10 changed files with 701 additions and 623 deletions.
diff --git a/README.md b/README.md
@@ -56,6 +56,7 @@ Here is a list of specs included in this repository, with links to the relevant
 | [SWMR Shared Memory Disk Paxos](specifications/diskpaxos)                                           | Leslie Lamport, Giuliano Losa              |          |             |         |     ✔     |          |
 | [Transaction Commit Models](specifications/transaction_commit)                                      | Leslie Lamport, Jim Gray, Murat Demirbas   |          |             |         |     ✔     |          |
 | [Span Tree Exercise](specifications/SpanningTree)                                                   | Leslie Lamport                             |          |             |         |     ✔     |          |
+| [Byzantine Paxos by Refinement](specifications/byzpaxos)                                            | Leslie Lamport                             |          |             |         |     ✔     |          |
 | [The Knuth-Yao Method](specifications/KnuthYao)                                                     | Ron Pressler, Markus Kuppe                 |          |             |         |     ✔     |          |
 | [Huang's Algorithm](specifications/Huang)                                                           | Markus Kuppe                               |          |             |         |     ✔     |          |
 | [EWD 426: Token Stabilization](specifications/ewd426)                                               | Murat Demirbas, Markus Kuppe               |          |             |         |     ✔     |          |
@@ -84,7 +85,6 @@ Here is a list of specs included in this repository, with links to the relevant
 | [PCR Testing for Snippets of DNA](specifications/glowingRaccoon)                                    | Martin Harrison                            |          |             |         |     ✔     |          |
 | [RFC 3506: Voucher Transaction System](specifications/byihive)                                      | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani |          |             |         |     ✔     |          |
 | [TLA⁺ Level Checking](specifications/LevelChecking)                                                 | Leslie Lamport                             |          |             |         |           |          |
-| [Byzantine Paxos by Refinement](specifications/byzpaxos)                                            | Leslie Lamport                             |          |             |         |           |          |
 | [Condition-Based Consensus](specifications/cbc_max)                                                 | Thanh Hai Tran, Igor Konnov, Josef Widder  |          |             |         |           |          |
 
 ## Examples Elsewhere
@@ -95,7 +95,6 @@ Ideally these will be moved into this repo over time.
 | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------ | :---------: | :-------: | :-----: | :------: |
 | IEEE 802.16 WiMAX Protocols (2006, [paper](https://users.cs.northwestern.edu/~ychen/Papers/npsec06.pdf), [specs](http://list.cs.northwestern.edu/802.16/))                                                                                                                    | Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, Hai Zhou     |              |            |          |           |
 | On the diversity of asynchronous communication (2016, [paper](https://dl.acm.org/doi/10.1007/s00165-016-0379-x), [specs](http://hurault.perso.enseeiht.fr/asynchronousCommunication/))                                                                                        | Florent Chevrou, Aurélie Hurault, Philippe Quéinnec                            |              |            |          |           |
-| [byzpaxos](specifications/byzpaxos)                                                                                               | Byzantizing Paxos by Refinement (Lamport, 2011)                                                                                           | Leslie Lamport                                                                 |              |     ✔      |          |           |
 | [Caesar](specifications/Caesar)                                                                                                   | Multi-leader generalized consensus protocol (Arun et al., 2017)                                                                           | Giuliano Losa                                                                  |              |     ✔      |    ✔     |           |
 | [CASPaxos](specifications/CASPaxos)                                                                                               | An extension of the single-decree Paxos algorithm to a compare-and-swap type register (Rystsov)                                           | Tobias Schottdorf                                                              |              |     ✔      |          |           |
 | [DataPort](specifications/DataPort)                                                                                               | Dataport protocal 505.89PT, only PDF files (Biggs & Noriaki, 2016)                                                                        | Geoffrey Biggs, Noriaki Ando                                                   |              |            |          |           |

diff --git a/manifest.json b/manifest.json
@@ -3295,7 +3295,16 @@
             "pluscal",
             "proof"
           ],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/byzpaxos/BPConProof.cfg",
+              "runtime": "unknown",
+              "size": "large",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "unknown"
+            }
+          ]
         },
         {
           "path": "specifications/byzpaxos/Consensus.tla",
@@ -3305,7 +3314,19 @@
             "pluscal",
             "proof"
           ],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/byzpaxos/Consensus.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock",
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
         },
         {
           "path": "specifications/byzpaxos/PConProof.tla",
@@ -3315,7 +3336,16 @@
             "pluscal",
             "proof"
           ],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/byzpaxos/PConProof.cfg",
+              "runtime": "00:06:00",
+              "size": "large",
+              "mode": "exhaustive search",
+              "features": [],
+              "result": "success"
+            }
+          ]
         },
         {
           "path": "specifications/byzpaxos/VoteProof.tla",
@@ -3325,7 +3355,19 @@
             "pluscal",
             "proof"
           ],
-          "models": []
+          "models": [
+            {
+              "path": "specifications/byzpaxos/VoteProof.cfg",
+              "runtime": "00:00:05",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock",
+                "liveness"
+              ],
+              "result": "success"
+            }
+          ]
         }
       ]
     },

diff --git a/specifications/byzpaxos/BPConProof.cfg b/specifications/byzpaxos/BPConProof.cfg
@@ -0,0 +1,11 @@
+CONSTANTS
+  Value = {v1, v2}
+  Acceptor = {a1, a2, a3}
+  FakeAcceptor = {fa1}
+  ByzQuorum = {{a1, a2, fa1}, {a1, a3, fa1}, {a2, a3, fa1}, {a1, a2, a3}}
+  WeakQuorum = {{a1, fa1}, {a2, fa1}, {a3, fa1}, {a1, a2}, {a1, a3}, {a2, a3}}
+  Ballot = {0, 1, 2}
+  None = None
+INVARIANT Inv
+SPECIFICATION Spec
+
diff --git a/specifications/byzpaxos/BPConProof.tla b/specifications/byzpaxos/BPConProof.tla
@@ -1617,6 +1617,7 @@ THEOREM Invariance == Spec => []Inv
 (* implements algorithm PCon under the refinement mapping                  *)
 (* defined by the INSTANCE statement above.                                *)
 (***************************************************************************)
+AbstractSpec == P!Spec
 THEOREM Spec => P!Spec
 <1>1. Init => P!Init
   <2>. HAVE Init

diff --git a/specifications/byzpaxos/Consensus.cfg b/specifications/byzpaxos/Consensus.cfg
@@ -0,0 +1,6 @@
+CONSTANT Value = {v1, v2, v3}
+INVARIANTS TypeOK Inv
+PROPERTY Success
+SPECIFICATION LiveSpec
+CHECK_DEADLOCK FALSE
+
diff --git a/specifications/byzpaxos/PConProof.cfg b/specifications/byzpaxos/PConProof.cfg
@@ -0,0 +1,9 @@
+CONSTANTS
+  Value = {v1, v2}
+  Acceptor = {a1, a2, a3}
+  Quorum = {{a1, a2}, {a1, a3}, {a2, a3}, {a1, a2, a3}}
+  Ballot = {0, 1, 2}
+  None = None
+INVARIANTS TypeOK PAccInv P1bInv P1cInv P2aInv
+SPECIFICATION Spec
+