Add Practical SMR-system-style MultiPaxos Spec (#121)

Add SMR-style MultiPaxos spec Signed-off-by: Guanzhou Hu <me@josehu.com>
tlaplus · Feb 20, 2024 · cf8313d · cf8313d
1 parent 46bd732
commit cf8313d
Show file tree

Hide file tree

Showing 7 changed files with 787 additions and 0 deletions.
diff --git a/README.md b/README.md
@@ -86,6 +86,7 @@ Here is a list of specs included in this repository, with links to the relevant
 | [RFC 3506: Voucher Transaction System](specifications/byihive)                                      | Santhosh Raju, Cherry G. Mathew, Fransisca Andriani |          |             |         |     ✔     |          |
 | [TLA⁺ Level Checking](specifications/LevelChecking)                                                 | Leslie Lamport                                      |          |             |         |           |          |
 | [Condition-Based Consensus](specifications/cbc_max)                                                 | Thanh Hai Tran, Igor Konnov, Josef Widder           |          |             |         |           |          |
+| [MultiPaxos in SMR-Style](specifications/MultiPaxos-SMR)                                            | Guanzhou Hu                                         |          |             |    ✔    |     ✔     |          |
 
 ## Examples Elsewhere
 Here is a list of specs stored in locations outside this repository, including submodules.

diff --git a/manifest.json b/manifest.json
@@ -1234,6 +1234,59 @@
         }
       ]
     },
+    {
+      "path": "specifications/MultiPaxos-SMR",
+      "title": "MultiPaxos in SMR-Style",
+      "description": "MultiPaxos in practical state machine replication system style",
+      "sources": [
+        "https://www.josehu.com/technical/2024/02/19/practical-MultiPaxos-TLA-spec.html"
+      ],
+      "authors": [
+        "Guanzhou Hu"
+      ],
+      "tags": [
+        "intermediate"
+      ],
+      "modules": [
+        {
+          "path": "specifications/MultiPaxos-SMR/MultiPaxos.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [
+            "pluscal"
+          ],
+          "models": []
+        },
+        {
+          "path": "specifications/MultiPaxos-SMR/MultiPaxos_MC.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/MultiPaxos-SMR/MultiPaxos_MC_small.cfg",
+              "runtime": "00:00:10",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "symmetry"
+              ],
+              "result": "success"
+            },
+            {
+              "path": "specifications/MultiPaxos-SMR/MultiPaxos_MC.cfg",
+              "runtime": "00:07:53",
+              "size": "large",
+              "mode": "exhaustive search",
+              "features": [
+                "symmetry"
+              ],
+              "result": "success"
+            }
+          ]
+        }
+      ]
+    },
     {
       "path": "specifications/N-Queens",
       "title": "The N-Queens Puzzle",