From bbd37687d772c150a40bec484d4d5245384abc7a Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Mon, 4 Mar 2024 20:45:28 +0100 Subject: [PATCH] YoYo leader election algorithm (#124) Signed-off-by: Stephan Merz --- README.md | 1 + manifest.json | 98 +++++++++ specifications/YoYo/MCYoYoNoPruning.cfg | 9 + specifications/YoYo/MCYoYoNoPruning.tla | 18 ++ specifications/YoYo/MCYoYoPruning.cfg | 12 ++ specifications/YoYo/MCYoYoPruning.tla | 18 ++ specifications/YoYo/YoYoAllGraphs.cfg | 12 ++ specifications/YoYo/YoYoAllGraphs.tla | 240 +++++++++++++++++++++ specifications/YoYo/YoYoNoPruning.tla | 251 ++++++++++++++++++++++ specifications/YoYo/YoYoPruning.tla | 266 ++++++++++++++++++++++++ 10 files changed, 925 insertions(+) create mode 100644 specifications/YoYo/MCYoYoNoPruning.cfg create mode 100644 specifications/YoYo/MCYoYoNoPruning.tla create mode 100644 specifications/YoYo/MCYoYoPruning.cfg create mode 100644 specifications/YoYo/MCYoYoPruning.tla create mode 100644 specifications/YoYo/YoYoAllGraphs.cfg create mode 100644 specifications/YoYo/YoYoAllGraphs.tla create mode 100644 specifications/YoYo/YoYoNoPruning.tla create mode 100644 specifications/YoYo/YoYoPruning.tla diff --git a/README.md b/README.md index 48573b7b..267b5290 100644 --- 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 index 4645477e..5d0ee711 100644 --- 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 new file mode 100644 index 00000000..06ee7bf9 --- /dev/null +++ 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 new file mode 100644 index 00000000..6cf6d9db --- /dev/null +++ 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 + +============================================================================== \ No newline at end of file diff --git a/specifications/YoYo/MCYoYoPruning.cfg b/specifications/YoYo/MCYoYoPruning.cfg new file mode 100644 index 00000000..306c7590 --- /dev/null +++ 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 \ No newline at end of file diff --git a/specifications/YoYo/MCYoYoPruning.tla b/specifications/YoYo/MCYoYoPruning.tla new file mode 100644 index 00000000..dbcc4cc7 --- /dev/null +++ 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 + +============================================================================== \ No newline at end of file diff --git a/specifications/YoYo/YoYoAllGraphs.cfg b/specifications/YoYo/YoYoAllGraphs.cfg new file mode 100644 index 00000000..713a2555 --- /dev/null +++ b/specifications/YoYo/YoYoAllGraphs.cfg @@ -0,0 +1,12 @@ +CONSTANT N = 5 +SPECIFICATION Spec + +INVARIANTS + TypeOK + NeighborInv + FinishIffTerminated + +PROPERTIES + Liveness + +CHECK_DEADLOCK FALSE \ No newline at end of file diff --git a/specifications/YoYo/YoYoAllGraphs.tla b/specifications/YoYo/YoYoAllGraphs.tla new file mode 100644 index 00000000..f4a57404 --- /dev/null +++ b/specifications/YoYo/YoYoAllGraphs.tla @@ -0,0 +1,240 @@ +----------------------------- MODULE YoYoAllGraphs --------------------------- +(****************************************************************************) +(* This module describes the Yo-Yo algorithm with pruning. Unlike the basic *) +(* specification of that algorithm in module YoYoPruning, it allows the *) +(* algorithm to be verified for all undirected, loop-free, and connected *) +(* graphs over a fixed number of nodes. *) +(* *) +(* Authors: Ludovic Yvoz and Stephan Merz, 2024. *) +(****************************************************************************) + +EXTENDS TLC, Integers, FiniteSets, UndirectedGraphs + +CONSTANT N \* number of nodes + +ASSUME N \in Nat \ {0} + +Nodes == 1 .. N +(****************************************************************************) +(* Set of all (non-loop) edges over the set of nodes. The algorithm will *) +(* operate over a subset of edges that forms a connected graph. *) +(****************************************************************************) +Edges == {{e[1], e[2]} : e \in {e \in Nodes \X Nodes : e[1] # e[2]}} + +Min(S) == CHOOSE x \in S : \A y \in S : x <= y + +VARIABLES + (* the activation status of the node *) + active, + (* the phase (down or up) each node is currently executing *) + phase, + (* incoming and outgoing neighbors of each node *) + incoming, outgoing, + (* mailbox of each node *) + mailbox + +vars == <> + +(****************************************************************************) +(* Determine the kind of the node: leader, source, sink or internal. *) +(****************************************************************************) +kind(n) == + IF incoming[n] = {} /\ outgoing[n] = {} THEN "leader" + ELSE IF incoming[n] = {} THEN "source" + ELSE IF outgoing[n] = {} THEN "sink" + ELSE "internal" + +(****************************************************************************) +(* Messages sent during the algorithm. *) +(****************************************************************************) +Messages == + [phase : {"down"}, sndr : Nodes, val : Nodes] \cup + [phase : {"up"}, sndr : Nodes, reply : {"yes", "no"}, prune : BOOLEAN] +downMsg(s,v) == [phase |-> "down", sndr |-> s, val |-> v] +upMsg(s,r,p) == [phase |-> "up", sndr |-> s, reply |-> r, prune |-> p] + +(****************************************************************************) +(* Type correctness predicate. *) +(****************************************************************************) +TypeOK == + /\ active \in [Nodes -> BOOLEAN] + /\ phase \in [Nodes -> {"down", "up"}] + /\ incoming \in [Nodes -> SUBSET Nodes] + /\ outgoing \in [Nodes -> SUBSET Nodes] + /\ mailbox \in [Nodes -> SUBSET Messages] + /\ \A n \in Nodes : \A msg \in mailbox[n] : + /\ msg.phase = "down" => + /\ n \in outgoing[msg.sndr] + /\ \A mm \in mailbox[n] : \* at most one message per neighbor + mm.phase = "down" /\ mm.sndr = msg.sndr => mm = msg + /\ msg.phase = "up" => + /\ msg.sndr \in outgoing[n] + /\ \A mm \in mailbox[n] : \* at most one message per neighbor + mm.phase = "up" /\ mm.sndr = msg.sndr => mm = msg + +------------------------------------------------------------------------------ +(****************************************************************************) +(* Yo-Yo algorithm as a state machine. *) +(****************************************************************************) +Init == + /\ active = [n \in Nodes |-> TRUE] + /\ phase = [n \in Nodes |-> "down"] + /\ mailbox = [n \in Nodes |-> {}] + /\ \E Nbrs \in SUBSET Edges : + \* true by construction + \* /\ IsLoopFreeUndirectedGraph([node |-> Nodes, edge |-> Nbrs]) + /\ IsStronglyConnected([node |-> Nodes, edge |-> Nbrs]) + /\ incoming = [n \in Nodes |-> {m \in Nodes : {m,n} \in Nbrs /\ m < n}] + /\ outgoing = [n \in Nodes |-> {m \in Nodes : {m,n} \in Nbrs /\ m > n}] + +------------------------------------------------------------------------------ +(****************************************************************************) +(* Down phase: we distinguish sources and other nodes. *) +(* Note that a node retains "down" messages after executing the phase *) +(* because they are used during the up phase. *) +(****************************************************************************) +DownSource(n) == + /\ active[n] + /\ kind(n) = "source" + /\ phase[n] = "down" + /\ mailbox' = [m \in Nodes |-> + IF m \in outgoing[n] THEN mailbox[m] \cup {downMsg(n,n)} + ELSE mailbox[m]] + /\ phase' = [phase EXCEPT ![n] = "up"] + /\ UNCHANGED <> + +DownOther(n) == + /\ active[n] + /\ kind(n) \in {"internal", "sink"} + /\ phase[n] = "down" + /\ LET downMsgs == {msg \in mailbox[n] : msg.phase = "down"} + IN /\ {msg.sndr : msg \in downMsgs} = incoming[n] + /\ LET min == Min({msg.val : msg \in downMsgs}) + IN mailbox' = [m \in Nodes |-> + IF m \in outgoing[n] + THEN mailbox[m] \cup {downMsg(n,min)} + ELSE mailbox[m]] + /\ phase' = [phase EXCEPT ![n] = "up"] + /\ UNCHANGED <> + +Down(n) == DownSource(n) \/ DownOther(n) + +------------------------------------------------------------------------------ +(****************************************************************************) +(* Up phase, again distinguishing sources and other nodes. *) +(* *) +(* An internal or source node may already have received "down" messages *) +(* for the following round from neighbors that it still considers as *) +(* outgoing neighbors but for which the edge direction was reversed. *) +(* We therefore have to be careful to only consider "down" messages from *) +(* neighbors that the node considers as incoming, and also to preserve *) +(* "down" messages for the following round when cleaning the mailbox. *) +(****************************************************************************) +UpSource(n) == + /\ active[n] + /\ kind(n) = "source" + /\ phase[n] = "up" + /\ LET upMsgs == {msg \in mailbox[n] : msg.phase = "up"} + noSndrs == {msg.sndr : msg \in {mm \in upMsgs : mm.reply = "no"}} + pruned == {msg.sndr : msg \in {mm \in upMsgs : mm.prune}} + IN /\ {msg.sndr : msg \in upMsgs} = outgoing[n] + /\ mailbox' = [mailbox EXCEPT ![n] = mailbox[n] \ upMsgs] + /\ incoming' = [incoming EXCEPT ![n] = noSndrs \ pruned] + /\ outgoing' = [outgoing EXCEPT ![n] = @ \ (noSndrs \union pruned)] + /\ phase' = [phase EXCEPT ![n] = "down"] + /\ active' = active + +UpOther(n) == + /\ active[n] + /\ kind(n) \in {"internal", "sink"} + /\ phase[n] = "up" + /\ LET upMsgs == {msg \in mailbox[n] : msg.phase = "up"} + noSndrs == {msg.sndr : msg \in {mm \in upMsgs : mm.reply = "no"}} + pruned == {msg.sndr : msg \in {mm \in upMsgs : mm.prune}} + downMsgs == {msg \in mailbox[n] : msg.phase = "down" /\ msg.sndr \in incoming[n]} + valsRcvd == {msg.val : msg \in downMsgs} + senders(v) == {m \in incoming[n] : downMsg(m,v) \in downMsgs} + valSent(m) == (CHOOSE msg \in downMsgs : msg.sndr = m).val + isLoneSink == kind(n) = "sink" /\ Cardinality(incoming[n]) = 1 + IN /\ {msg.sndr : msg \in upMsgs} = outgoing[n] \* always true for sinks + /\ \* non-deterministically choose a sender for each value whose link + \* will not be pruned + \E keep \in {f \in [valsRcvd -> incoming[n]] : + \A v \in valsRcvd : f[v] \in senders(v)} : + /\ IF noSndrs = {} \* true in particular for sinks + THEN LET min == Min({msg.val : msg \in downMsgs}) + minSndrs == {msg.sndr : msg \in {mm \in downMsgs : mm.val = min}} + IN /\ mailbox' = [m \in Nodes |-> + IF m \in incoming[n] + THEN mailbox[m] \union + {upMsg(n, + IF m \in minSndrs THEN "yes" ELSE "no", + (m # keep[valSent(m)]) \/ isLoneSink)} + ELSE IF m = n THEN mailbox[m] \ (upMsgs \union downMsgs) + ELSE mailbox[m]] + /\ incoming' = [incoming EXCEPT ![n] = + IF isLoneSink THEN {} ELSE {keep[min]}] + /\ outgoing' = [outgoing EXCEPT ![n] = + (@ \ pruned) \union + {keep[v] : v \in valsRcvd \ {min}}] + ELSE /\ mailbox' = [m \in Nodes |-> + IF m \in incoming[n] + THEN mailbox[m] \union {upMsg(n, "no", m # keep[valSent(m)])} + ELSE IF m = n THEN mailbox[m] \ (upMsgs \union downMsgs) + ELSE mailbox[m]] + /\ incoming' = [incoming EXCEPT ![n] = noSndrs \ pruned] + /\ outgoing' = [outgoing EXCEPT ![n] = + (@ \ (noSndrs \union pruned)) \union + {keep[v] : v \in valsRcvd}] + /\ active' = [active EXCEPT ![n] = ~ isLoneSink] + /\ phase' = [phase EXCEPT ![n] = "down"] + +Up(n) == UpSource(n) \/ UpOther(n) + +------------------------------------------------------------------------------ + +Next == \E n \in Nodes : Down(n) \/ Up(n) + +Spec == Init /\ [][Next]_vars /\ WF_vars(Next) + +------------------------------------------------------------------------------ +(****************************************************************************) +(* Formulas used for verification. *) +(****************************************************************************) + +(****************************************************************************) +(* Predicate asserting that there will always be at least two source nodes. *) +(* Checking this as an invariant produces an execution that shows that all *) +(* sources except for the leader will be eliminated. *) +(****************************************************************************) +MoreThanOneSource == \E s1, s2 \in Nodes : + s1 # s2 /\ kind(s1) = "source" /\ kind(s2) = "source" + +(****************************************************************************) +(* Node m is an outgoing neighbor of node n iff n is an incoming neighbor *) +(* of m, except if the edge is being reversed, in which case there is a *) +(* "no" message in one of the mailboxes, or if the edge is being pruned, *) +(* in which case there is a corresponding message pending at node n. *) +(****************************************************************************) +NeighborInv == \A m,n \in Nodes : + m \in outgoing[n] <=> + \/ n \in incoming[m] + \/ /\ n \in outgoing[m] + /\ \/ upMsg(n, "no", FALSE) \in mailbox[m] + \/ upMsg(m, "no", FALSE) \in mailbox[n] + \/ /\ n \notin (incoming[m] \union outgoing[m]) + /\ \E r \in {"yes", "no"} : upMsg(m, r, TRUE) \in mailbox[n] + +(****************************************************************************) +(* Termination condition: the node with smallest identity is the leader, *) +(* all other nodes are inactive, all mailboxes are empty. *) +(* Check that the algorithm will reach such a state, and that this is the *) +(* only final (deadlock) state. *) +(****************************************************************************) +Termination == \A n \in Nodes : + /\ IF n = Min(Nodes) THEN kind(n) = "leader" ELSE ~ active[n] + /\ mailbox[n] = {} + +Liveness == <>Termination +FinishIffTerminated == ~(ENABLED Next) <=> Termination +============================================================================== \ No newline at end of file diff --git a/specifications/YoYo/YoYoNoPruning.tla b/specifications/YoYo/YoYoNoPruning.tla new file mode 100644 index 00000000..5f8f3f4d --- /dev/null +++ b/specifications/YoYo/YoYoNoPruning.tla @@ -0,0 +1,251 @@ +----------------------------- MODULE YoYoNoPruning --------------------------- +(****************************************************************************) +(* TLA+ specification of the Yo-Yo leader election algorithm in arbitrary *) +(* undirected graphs without self-loops. The algorithm was introduced by *) +(* Nicola Santoro, cf. "Design and Analysis of Distributed Algorithms", *) +(* section 3.8.3, see also https://en.wikipedia.org/wiki/Yo-yo_(algorithm). *) +(* The algorithm assumes that nodes are (identified by) integers, and the *) +(* node with the smallest identity will be elected leader. *) +(* *) +(* The algorithm orients the edges of the graph. Initially, all edges are *) +(* directed from smaller to larger node identities, so sources correspond *) +(* to local minima in their neighborhoods and sinks correspond to local *) +(* maxima. Sources are considered candidates for being leader, and as long *) +(* as their are at least two sources, each round will eliminate at least *) +(* one of them. *) +(* *) +(* Each round consists of two phases, traditionally called the "Yo-" and *) +(* "-Yo" phases, that will be called "down" and "up" phases below. *) +(* The down phase is initiated by the sources, which broadcast their *) +(* identity to all neighbors. Non-source nodes wait for values to have been *) +(* received from all incoming neighbors, then broadcast the minimum value *) +(* that has been received to all outgoing neighbors. (Sink nodes do not *) +(* send messages in the down phase.) *) +(* *) +(* The up phase is initiated by sink nodes when they have received values *) +(* from all neighbors in the down phase. They reply "yes" to all neighbors *) +(* that sent the minimum value and "no" to all other neighbors. The other *) +(* nodes wait until messages for the up phase have been received from all *) +(* outgoing neighbors. If one message is "no", they send "no" to all *) +(* incoming neighbors, otherwise they send "yes" to those incoming *) +(* neighbors who sent the smallest value during the down phase and "no" to *) +(* all other incoming neighbors. (Source nodes do not send messages in the *) +(* up phase.) *) +(* Moreover, edges along which a "no" message is sent during the up phase *) +(* change orientation. This may change the status of a node (source, *) +(* sink or internal). *) +(* *) +(* The algorithm stabilizes in a state where there is at most one source, *) +(* after which point only the identity of that source will be sent during *) +(* the down phase and only "yes" messages will be sent during the up phase. *) +(* However, no node detects termination. Ensuring termination of the *) +(* algorithm is achieved by pruning the graph, modeled in a variant of the *) +(* present specification. *) +(* *) +(* Authors: Ludovic Yvoz and Stephan Merz, 2024. *) +(****************************************************************************) + +EXTENDS TLC, Integers, FiniteSets, UndirectedGraphs + +CONSTANT Nodes, Edges \* the nodes and edges of the graph + +ASSUME + (* nodes are represented by their integer identities *) + /\ Nodes \subseteq Int + /\ Nodes # {} + /\ LET G == [node |-> Nodes, edge |-> Edges] + IN /\ IsUndirectedGraph(G) + /\ IsStronglyConnected(G) + +Neighbors(n) == {m \in Nodes : {m,n} \in Edges} + +Min(S) == CHOOSE x \in S : \A y \in S : x <= y + +VARIABLES + (* the phase (down or up) each node is currently executing *) + phase, + (* incoming and outgoing neighbors of each node *) + incoming, outgoing, + (* mailbox of each node *) + mailbox + +vars == <> + +(****************************************************************************) +(* Determine the kind of the node: source, sink or internal. *) +(****************************************************************************) +kind(n) == + IF incoming[n] = {} THEN "source" + ELSE IF outgoing[n] = {} THEN "sink" + ELSE "internal" + +(****************************************************************************) +(* Messages sent during the algorithm. *) +(****************************************************************************) +Messages == + [phase : {"down"}, sndr : Nodes, val : Nodes] \cup + [phase : {"up"}, sndr : Nodes, reply : {"yes", "no"}] +downMsg(s,v) == [phase |-> "down", sndr |-> s, val |-> v] +upMsg(s,r) == [phase |-> "up", sndr |-> s, reply |-> r] + +(****************************************************************************) +(* Type correctness predicate. *) +(****************************************************************************) +TypeOK == + /\ phase \in [Nodes -> {"down", "up"}] + /\ incoming \in [Nodes -> SUBSET Nodes] + /\ \A n \in Nodes : incoming[n] \subseteq Neighbors(n) + /\ outgoing \in [Nodes -> SUBSET Nodes] + /\ \A n \in Nodes : outgoing[n] \subseteq Neighbors(n) + /\ mailbox \in [Nodes -> SUBSET Messages] + /\ \A n \in Nodes : \A msg \in mailbox[n] : + /\ msg.phase = "down" => + /\ n \in outgoing[msg.sndr] + /\ \A mm \in mailbox[n] : \* at most one message per neighbor + mm.phase = "down" /\ mm.sndr = msg.sndr => mm = msg + /\ msg.phase = "up" => + /\ msg.sndr \in outgoing[n] + /\ \A mm \in mailbox[n] : \* at most one message per neighbor + mm.phase = "up" /\ mm.sndr = msg.sndr => mm = msg + +------------------------------------------------------------------------------ +(****************************************************************************) +(* Yo-Yo algorithm as a state machine. *) +(****************************************************************************) +Init == + /\ phase = [n \in Nodes |-> "down"] + /\ incoming = [n \in Nodes |-> { m \in Neighbors(n) : m < n}] + /\ outgoing = [n \in Nodes |-> { m \in Neighbors(n) : m > n}] + /\ mailbox = [n \in Nodes |-> {}] + +------------------------------------------------------------------------------ +(****************************************************************************) +(* Down phase: we distinguish sources and other nodes. *) +(* Note that a node retains "down" messages after executing the phase *) +(* because they are used during the up phase. *) +(****************************************************************************) +DownSource(n) == + /\ kind(n) = "source" + /\ phase[n] = "down" + /\ mailbox' = [m \in Nodes |-> + IF m \in outgoing[n] THEN mailbox[m] \cup {downMsg(n,n)} + ELSE mailbox[m]] + /\ phase' = [phase EXCEPT ![n] = "up"] + /\ UNCHANGED <> + +DownOther(n) == + /\ kind(n) \in {"internal", "sink"} + /\ phase[n] = "down" + /\ LET downMsgs == {msg \in mailbox[n] : msg.phase = "down"} + IN /\ {msg.sndr : msg \in downMsgs} = incoming[n] + /\ LET min == Min({msg.val : msg \in downMsgs}) + IN mailbox' = [m \in Nodes |-> + IF m \in outgoing[n] + THEN mailbox[m] \cup {downMsg(n,min)} + ELSE mailbox[m]] + /\ phase' = [phase EXCEPT ![n] = "up"] + /\ UNCHANGED <> + +Down(n) == DownSource(n) \/ DownOther(n) + +------------------------------------------------------------------------------ +(****************************************************************************) +(* Up phase, again distinguishing sources and other nodes. *) +(* *) +(* An internal or source node may already have received "down" messages *) +(* for the following round from neighbors that it still considers as *) +(* outgoing neighbors but for which the edge direction was reversed. *) +(* We therefore have to be careful to only consider "down" messages from *) +(* neighbors that the node considers as incoming, and also to preserve *) +(* "down" messages for the following round when cleaning the mailbox. *) +(****************************************************************************) +UpSource(n) == + /\ kind(n) = "source" + /\ phase[n] = "up" + /\ LET upMsgs == {msg \in mailbox[n] : msg.phase = "up"} + noSndrs == {msg.sndr : msg \in {mm \in upMsgs : mm.reply = "no"}} + IN /\ {msg.sndr : msg \in upMsgs} = outgoing[n] + /\ mailbox' = [mailbox EXCEPT ![n] = mailbox[n] \ upMsgs] + /\ incoming' = [incoming EXCEPT ![n] = noSndrs] + /\ outgoing' = [outgoing EXCEPT ![n] = @ \ noSndrs] + /\ phase' = [phase EXCEPT ![n] = "down"] + +UpOther(n) == + /\ kind(n) \in {"internal", "sink"} + /\ phase[n] = "up" + /\ LET upMsgs == {msg \in mailbox[n] : msg.phase = "up"} + noSndrs == {msg.sndr : msg \in {mm \in upMsgs : mm.reply = "no"}} + downMsgs == {msg \in mailbox[n] : msg.phase = "down" /\ msg.sndr \in incoming[n]} + IN /\ {msg.sndr : msg \in upMsgs} = outgoing[n] \* always true for sinks + /\ IF noSndrs = {} \* true in particular for sinks + THEN LET min == Min({msg.val : msg \in downMsgs}) + minSndrs == {msg.sndr : msg \in {mm \in downMsgs : mm.val = min}} + IN /\ mailbox' = [m \in Nodes |-> + IF m \in incoming[n] + THEN mailbox[m] \union + {upMsg(n, IF m \in minSndrs THEN "yes" ELSE "no")} + ELSE IF m = n THEN mailbox[m] \ (upMsgs \union downMsgs) + ELSE mailbox[m]] + /\ incoming' = [incoming EXCEPT ![n] = minSndrs] + /\ outgoing' = [outgoing EXCEPT ![n] = + @ \union (incoming[n] \ minSndrs)] + ELSE /\ mailbox' = [m \in Nodes |-> + IF m \in incoming[n] THEN mailbox[m] \union {upMsg(n, "no")} + ELSE IF m = n THEN mailbox[m] \ (upMsgs \union downMsgs) + ELSE mailbox[m]] + /\ incoming' = [incoming EXCEPT ![n] = noSndrs] + /\ outgoing' = [outgoing EXCEPT ![n] = + (@ \ noSndrs) \union incoming[n]] + /\ phase' = [phase EXCEPT ![n] = "down"] + +Up(n) == UpSource(n) \/ UpOther(n) + +------------------------------------------------------------------------------ + +Next == \E n \in Nodes : Down(n) \/ Up(n) + +Spec == Init /\ [][Next]_vars /\ WF_vars(Next) + +------------------------------------------------------------------------------ +(****************************************************************************) +(* Formulas used for verification. *) +(****************************************************************************) + +(****************************************************************************) +(* Predicate asserting that there will always be at least two source nodes. *) +(* Checking this as an invariant produces an execution that shows that all *) +(* sources except for the leader will be eliminated. *) +(****************************************************************************) +MoreThanOneSource == \E s1, s2 \in Nodes : + s1 # s2 /\ kind(s1) = "source" /\ kind(s2) = "source" + +(****************************************************************************) +(* Node m is an outgoing neighbor of node n iff n is an incoming neighbor *) +(* of m, except if the edge is being reversed, in which case there is a *) +(* "no" message in one of the mailboxes. *) +(****************************************************************************) +NeighborInv == \A m,n \in Nodes : + m \in outgoing[n] <=> + \/ n \in incoming[m] + \/ /\ n \in outgoing[m] + /\ upMsg(n, "no") \in mailbox[m] \/ upMsg(m, "no") \in mailbox[n] + +(****************************************************************************) +(* No new sources are generated during execution of the algorithm. *) +(****************************************************************************) +NoNewSource == + [][\A n \in Nodes : kind(n)' = "source" => kind(n) = "source"]_vars + +(****************************************************************************) +(* Stabilization condition: there is only one source node, all "down" *) +(* messages carry the identity of that node, all "up" messages say "yes". *) +(****************************************************************************) +Stabilization == + /\ kind(Min(Nodes)) = "source" + /\ \A n \in Nodes : kind(n) = "source" => n = Min(Nodes) + /\ \A n \in Nodes : \A msg \in mailbox[n] : + /\ msg.phase = "down" => msg.val = Min(Nodes) + /\ msg.phase = "up" => msg.reply = "yes" + +Liveness == <>[]Stabilization +============================================================================== \ No newline at end of file diff --git a/specifications/YoYo/YoYoPruning.tla b/specifications/YoYo/YoYoPruning.tla new file mode 100644 index 00000000..38277c32 --- /dev/null +++ b/specifications/YoYo/YoYoPruning.tla @@ -0,0 +1,266 @@ +------------------------------ MODULE YoYoPruning ---------------------------- +(****************************************************************************) +(* The version of the Yo-Yo algorithm without pruning stabilizes in a state *) +(* with a single source node. However, that algorithm does not terminate, *) +(* and no single node can detect that the algorithm has stabilized. In *) +(* order to ensure termination, the "up" ("-Yo") phase of the algorithm is *) +(* extended in order to prune the graph by applying the following rules. *) +(* *) +(* 1. A sink node with a single (incoming) neighbor receives only one value *) +(* during the "down" phase, and therefore replies "yes" in the "up" *) +(* phase of the algorithm. Since it does not contribute any useful *) +(* information, it will become inactive and be removed from the graph. *) +(* 2. A node (internal or sink) that receives the same value from several *) +(* neighbors non-deterministically chooses one of these neighbors and *) +(* prunes the links to all other neighbors that sent the same value. *) +(* The rationale is that these neighbors correspond to different paths *) +(* from the same source node, and maintaining one path is enough. *) +(* *) +(* Applying these two rules, nodes and links are eliminated until the only *) +(* remaining source becomes an isolated node, at which point it proclaims *) +(* itself to be the leader. All other nodes will have become inactive. *) +(* The pruning phase is implemented by adding a flag to "up" messages, *) +(* indicating to the receiver whether to prune the corresponding link. *) +(* *) +(* Authors: Ludovic Yvoz and Stephan Merz, 2024. *) +(****************************************************************************) + +EXTENDS TLC, Integers, FiniteSets, UndirectedGraphs + +CONSTANT Nodes, Edges \* the nodes and edges of the graph + +ASSUME + (* nodes are represented by their integer identities *) + /\ Nodes \subseteq Int + /\ Nodes # {} + /\ LET G == [node |-> Nodes, edge |-> Edges] + IN /\ IsUndirectedGraph(G) + /\ IsStronglyConnected(G) + +Neighbors(n) == {m \in Nodes : {m,n} \in Edges} + +Min(S) == CHOOSE x \in S : \A y \in S : x <= y + +VARIABLES + (* the activation status of the node *) + active, + (* the phase (down or up) each node is currently executing *) + phase, + (* incoming and outgoing neighbors of each node *) + incoming, outgoing, + (* mailbox of each node *) + mailbox + +vars == <> + +(****************************************************************************) +(* Determine the kind of the node: leader, source, sink or internal. *) +(****************************************************************************) +kind(n) == + IF incoming[n] = {} /\ outgoing[n] = {} THEN "leader" + ELSE IF incoming[n] = {} THEN "source" + ELSE IF outgoing[n] = {} THEN "sink" + ELSE "internal" + +(****************************************************************************) +(* Messages sent during the algorithm. *) +(****************************************************************************) +Messages == + [phase : {"down"}, sndr : Nodes, val : Nodes] \cup + [phase : {"up"}, sndr : Nodes, reply : {"yes", "no"}, prune : BOOLEAN] +downMsg(s,v) == [phase |-> "down", sndr |-> s, val |-> v] +upMsg(s,r,p) == [phase |-> "up", sndr |-> s, reply |-> r, prune |-> p] + +(****************************************************************************) +(* Type correctness predicate. *) +(****************************************************************************) +TypeOK == + /\ active \in [Nodes -> BOOLEAN] + /\ phase \in [Nodes -> {"down", "up"}] + /\ incoming \in [Nodes -> SUBSET Nodes] + /\ \A n \in Nodes : incoming[n] \subseteq Neighbors(n) + /\ outgoing \in [Nodes -> SUBSET Nodes] + /\ \A n \in Nodes : outgoing[n] \subseteq Neighbors(n) + /\ mailbox \in [Nodes -> SUBSET Messages] + /\ \A n \in Nodes : \A msg \in mailbox[n] : + /\ msg.phase = "down" => + /\ n \in outgoing[msg.sndr] + /\ \A mm \in mailbox[n] : \* at most one message per neighbor + mm.phase = "down" /\ mm.sndr = msg.sndr => mm = msg + /\ msg.phase = "up" => + /\ msg.sndr \in outgoing[n] + /\ \A mm \in mailbox[n] : \* at most one message per neighbor + mm.phase = "up" /\ mm.sndr = msg.sndr => mm = msg + +------------------------------------------------------------------------------ +(****************************************************************************) +(* Yo-Yo algorithm as a state machine. *) +(****************************************************************************) +Init == + /\ active = [n \in Nodes |-> TRUE] + /\ phase = [n \in Nodes |-> "down"] + /\ incoming = [n \in Nodes |-> { m \in Neighbors(n) : m < n}] + /\ outgoing = [n \in Nodes |-> { m \in Neighbors(n) : m > n}] + /\ mailbox = [n \in Nodes |-> {}] + +------------------------------------------------------------------------------ +(****************************************************************************) +(* Down phase: we distinguish sources and other nodes. *) +(* Note that a node retains "down" messages after executing the phase *) +(* because they are used during the up phase. *) +(****************************************************************************) +DownSource(n) == + /\ active[n] + /\ kind(n) = "source" + /\ phase[n] = "down" + /\ mailbox' = [m \in Nodes |-> + IF m \in outgoing[n] THEN mailbox[m] \cup {downMsg(n,n)} + ELSE mailbox[m]] + /\ phase' = [phase EXCEPT ![n] = "up"] + /\ UNCHANGED <> + +DownOther(n) == + /\ active[n] + /\ kind(n) \in {"internal", "sink"} + /\ phase[n] = "down" + /\ LET downMsgs == {msg \in mailbox[n] : msg.phase = "down"} + IN /\ {msg.sndr : msg \in downMsgs} = incoming[n] + /\ LET min == Min({msg.val : msg \in downMsgs}) + IN mailbox' = [m \in Nodes |-> + IF m \in outgoing[n] + THEN mailbox[m] \cup {downMsg(n,min)} + ELSE mailbox[m]] + /\ phase' = [phase EXCEPT ![n] = "up"] + /\ UNCHANGED <> + +Down(n) == DownSource(n) \/ DownOther(n) + +------------------------------------------------------------------------------ +(****************************************************************************) +(* Up phase, again distinguishing sources and other nodes. *) +(* *) +(* An internal or source node may already have received "down" messages *) +(* for the following round from neighbors that it still considers as *) +(* outgoing neighbors but for which the edge direction was reversed. *) +(* We therefore have to be careful to only consider "down" messages from *) +(* neighbors that the node considers as incoming, and also to preserve *) +(* "down" messages for the following round when cleaning the mailbox. *) +(****************************************************************************) +UpSource(n) == + /\ active[n] + /\ kind(n) = "source" + /\ phase[n] = "up" + /\ LET upMsgs == {msg \in mailbox[n] : msg.phase = "up"} + noSndrs == {msg.sndr : msg \in {mm \in upMsgs : mm.reply = "no"}} + pruned == {msg.sndr : msg \in {mm \in upMsgs : mm.prune}} + IN /\ {msg.sndr : msg \in upMsgs} = outgoing[n] + /\ mailbox' = [mailbox EXCEPT ![n] = mailbox[n] \ upMsgs] + /\ incoming' = [incoming EXCEPT ![n] = noSndrs \ pruned] + /\ outgoing' = [outgoing EXCEPT ![n] = @ \ (noSndrs \union pruned)] + /\ phase' = [phase EXCEPT ![n] = "down"] + /\ active' = active + +UpOther(n) == + /\ active[n] + /\ kind(n) \in {"internal", "sink"} + /\ phase[n] = "up" + /\ LET upMsgs == {msg \in mailbox[n] : msg.phase = "up"} + noSndrs == {msg.sndr : msg \in {mm \in upMsgs : mm.reply = "no"}} + pruned == {msg.sndr : msg \in {mm \in upMsgs : mm.prune}} + downMsgs == {msg \in mailbox[n] : msg.phase = "down" /\ msg.sndr \in incoming[n]} + valsRcvd == {msg.val : msg \in downMsgs} + senders(v) == {m \in incoming[n] : downMsg(m,v) \in downMsgs} + valSent(m) == (CHOOSE msg \in downMsgs : msg.sndr = m).val + isLoneSink == kind(n) = "sink" /\ Cardinality(incoming[n]) = 1 + IN /\ {msg.sndr : msg \in upMsgs} = outgoing[n] \* always true for sinks + /\ \* non-deterministically choose a sender for each value whose link + \* will not be pruned + \E keep \in {f \in [valsRcvd -> incoming[n]] : + \A v \in valsRcvd : f[v] \in senders(v)} : + /\ IF noSndrs = {} \* true in particular for sinks + THEN LET min == Min({msg.val : msg \in downMsgs}) + minSndrs == {msg.sndr : msg \in {mm \in downMsgs : mm.val = min}} + IN /\ mailbox' = [m \in Nodes |-> + IF m \in incoming[n] + THEN mailbox[m] \union + {upMsg(n, + IF m \in minSndrs THEN "yes" ELSE "no", + (m # keep[valSent(m)]) \/ isLoneSink)} + ELSE IF m = n THEN mailbox[m] \ (upMsgs \union downMsgs) + ELSE mailbox[m]] + /\ incoming' = [incoming EXCEPT ![n] = + IF isLoneSink THEN {} ELSE {keep[min]}] + /\ outgoing' = [outgoing EXCEPT ![n] = + (@ \ pruned) \union + {keep[v] : v \in valsRcvd \ {min}}] + ELSE /\ mailbox' = [m \in Nodes |-> + IF m \in incoming[n] + THEN mailbox[m] \union {upMsg(n, "no", m # keep[valSent(m)])} + ELSE IF m = n THEN mailbox[m] \ (upMsgs \union downMsgs) + ELSE mailbox[m]] + /\ incoming' = [incoming EXCEPT ![n] = noSndrs \ pruned] + /\ outgoing' = [outgoing EXCEPT ![n] = + (@ \ (noSndrs \union pruned)) \union + {keep[v] : v \in valsRcvd}] + /\ active' = [active EXCEPT ![n] = ~ isLoneSink] + /\ phase' = [phase EXCEPT ![n] = "down"] + +Up(n) == UpSource(n) \/ UpOther(n) + +------------------------------------------------------------------------------ + +Next == \E n \in Nodes : Down(n) \/ Up(n) + +Spec == Init /\ [][Next]_vars /\ WF_vars(Next) + +------------------------------------------------------------------------------ +(****************************************************************************) +(* Formulas used for verification. *) +(****************************************************************************) + +(****************************************************************************) +(* Predicate asserting that there will always be at least two source nodes. *) +(* Checking this as an invariant produces an execution that shows that all *) +(* sources except for the leader will be eliminated. *) +(****************************************************************************) +MoreThanOneSource == \E s1, s2 \in Nodes : + s1 # s2 /\ kind(s1) = "source" /\ kind(s2) = "source" + +(****************************************************************************) +(* Node m is an outgoing neighbor of node n iff n is an incoming neighbor *) +(* of m, except if the edge is being reversed, in which case there is a *) +(* "no" message in one of the mailboxes, or if the edge is being pruned, *) +(* in which case there is a corresponding message pending at node n. *) +(****************************************************************************) +NeighborInv == \A m,n \in Nodes : + m \in outgoing[n] <=> + \/ n \in incoming[m] + \/ /\ n \in outgoing[m] + /\ \/ upMsg(n, "no", FALSE) \in mailbox[m] + \/ upMsg(m, "no", FALSE) \in mailbox[n] + \/ /\ n \notin (incoming[m] \union outgoing[m]) + /\ \E r \in {"yes", "no"} : upMsg(m, r, TRUE) \in mailbox[n] + +(****************************************************************************) +(* The base algorithm without pruning ensures that no new sources are *) +(* generated during execution of the algorithm. Due to pruning, this *) +(* property may fail for the full algorithm, and TLC finds a counter- *) +(* example for the small example graph provided in the MC module (but the *) +(* property happens to be true for the larger graph). *) +(****************************************************************************) +NoNewSource == + [][\A n \in Nodes : kind(n)' = "source" => kind(n) = "source"]_vars + +(****************************************************************************) +(* Termination condition: the node with smallest identity is the leader, *) +(* all other nodes are inactive, all mailboxes are empty. *) +(* Check that the algorithm will reach such a state, and that this is the *) +(* only final (deadlock) state. *) +(****************************************************************************) +Termination == \A n \in Nodes : + /\ IF n = Min(Nodes) THEN kind(n) = "leader" ELSE ~ active[n] + /\ mailbox[n] = {} + +Liveness == <>Termination +FinishIffTerminated == ~(ENABLED Next) <=> Termination +============================================================================== \ No newline at end of file