YoYo leader election algorithm (#124)

Signed-off-by: Stephan Merz <[email protected]>
tlaplus · Mar 4, 2024 · bbd3768 · bbd3768
1 parent b7d2d8c
commit bbd3768
Show file tree

Hide file tree

Showing 10 changed files with 925 additions and 0 deletions.
diff --git a/README.md b/README.md
@@ -87,6 +87,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           |          |             |         |           |          |
+| [Yo-Yo Leader Election](specifications/YoYo)                                                 | Ludovic Yvoz, Stephan Merz           |          |             |         |      ✔    |          |
 
 ## Examples Elsewhere
 Here is a list of specs stored in locations outside this repository, including submodules.

diff --git a/manifest.json b/manifest.json
@@ -5007,6 +5007,104 @@
           ]
         }
       ]
+    },
+    {
+      "path": "specifications/YoYo",
+      "title": "Yo-Yo Leader Election",
+      "description": "Algorithm due to Nicola Santoro for leader election in a connected undirected network",
+      "sources": ["https://research.nicola-santoro.com/DADA.html"],
+      "authors": [
+        "Ludovic Yvoz",
+        "Stephan Merz"
+      ],
+      "tags": [],
+      "modules": [
+        {
+          "path": "specifications/YoYo/YoYoNoPruning.tla",
+          "communityDependencies": [
+            "UndirectedGraphs"
+          ],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
+        {
+          "path": "specifications/YoYo/MCYoYoNoPruning.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/YoYo/MCYoYoNoPruning.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "liveness"
+              ],
+              "result": "success",
+              "distinctStates": 60,
+              "totalStates": 110,
+              "stateDepth": 19
+            }
+          ]
+        },
+        {
+          "path": "specifications/YoYo/YoYoPruning.tla",
+          "communityDependencies": [
+            "UndirectedGraphs"
+          ],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": []
+        },
+        {
+          "path": "specifications/YoYo/MCYoYoPruning.tla",
+          "communityDependencies": [],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/YoYo/MCYoYoPruning.cfg",
+              "runtime": "00:00:01",
+              "size": "small",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock",
+                "liveness"
+              ],
+              "result": "success",
+              "distinctStates": 102,
+              "totalStates": 157,
+              "stateDepth": 31
+            }
+          ]
+        },
+        {
+          "path": "specifications/YoYo/YoYoAllGraphs.tla",
+          "communityDependencies": [
+            "UndirectedGraphs"
+          ],
+          "tlaLanguageVersion": 2,
+          "features": [],
+          "models": [
+            {
+              "path": "specifications/YoYo/YoYoAllGraphs.cfg",
+              "runtime": "00:00:02",
+              "size": "medium",
+              "mode": "exhaustive search",
+              "features": [
+                "ignore deadlock",
+                "liveness"
+              ],
+              "result": "success",
+              "distinctStates": 26731,
+              "totalStates": 48535,
+              "stateDepth": 39
+            }
+          ]
+        }
+      ]
     }
   ]
 }
diff --git a/specifications/YoYo/MCYoYoNoPruning.cfg b/specifications/YoYo/MCYoYoNoPruning.cfg
@@ -0,0 +1,9 @@
+SPECIFICATION Spec
+
+INVARIANTS
+  TypeOK
+  NeighborInv
+
+PROPERTIES
+  NoNewSource
+  Liveness
diff --git a/specifications/YoYo/MCYoYoNoPruning.tla b/specifications/YoYo/MCYoYoNoPruning.tla
@@ -0,0 +1,18 @@
+--------------------------- MODULE MCYoYoNoPruning ---------------------------
+EXTENDS Integers
+
+Nodes == 1 .. 5
+Edges == {{1,2}, {1,5}, {3,4}, {3,5}, {4,5}}
+
+(*
+Nodes == {2,3,4,5,7,11,12,14,20,31,41}
+Edges == {{2,31}, {3,11}, {3,12}, {3,14}, {4,14}, {4,20}, 
+          {5,11}, {5,12}, {5,20}, {7,20}, {7,31}, 
+          {11,12}, {12,20}, {20,41}}
+*)
+
+VARIABLES phase, incoming, outgoing, mailbox
+
+INSTANCE YoYoNoPruning
+
+==============================================================================
diff --git a/specifications/YoYo/MCYoYoPruning.cfg b/specifications/YoYo/MCYoYoPruning.cfg
@@ -0,0 +1,12 @@
+SPECIFICATION Spec
+
+INVARIANTS
+  TypeOK
+  NeighborInv
+  FinishIffTerminated
+
+PROPERTIES
+\*  NoNewSource  -- fails for the small example graph
+  Liveness
+
+CHECK_DEADLOCK FALSE 
diff --git a/specifications/YoYo/MCYoYoPruning.tla b/specifications/YoYo/MCYoYoPruning.tla
@@ -0,0 +1,18 @@
+---------------------------- MODULE MCYoYoPruning ----------------------------
+EXTENDS Integers
+
+Nodes == 1 .. 5
+Edges == {{1,2}, {1,5}, {3,4}, {3,5}, {4,5}}
+
+(*
+Nodes == {2,3,4,5,7,11,12,14,20,31,41}
+Edges == {{2,31}, {3,11}, {3,12}, {3,14}, {4,14}, {4,20}, 
+          {5,11}, {5,12}, {5,20}, {7,20}, {7,31}, 
+          {11,12}, {12,20}, {20,41}}
+*)
+
+VARIABLES active, phase, incoming, outgoing, mailbox
+
+INSTANCE YoYoPruning
+
+==============================================================================
diff --git a/specifications/YoYo/YoYoAllGraphs.cfg b/specifications/YoYo/YoYoAllGraphs.cfg
@@ -0,0 +1,12 @@
+CONSTANT N = 5
+SPECIFICATION Spec
+
+INVARIANTS
+  TypeOK
+  NeighborInv
+  FinishIffTerminated
+
+PROPERTIES
+  Liveness
+
+CHECK_DEADLOCK FALSE