-
-
Save jrwest/bbc9d6ba73d56f96d14e to your computer and use it in GitHub Desktop.
A TLA+ Model of Plumtree (http://ieeexplore.ieee.org/xpl/articleDetails.jsp?reload=true&arnumber=4365705) showing it is not tolerant to a network which can drop messages
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
------------------------- MODULE ClusterMetaSimple ------------------------- | |
EXTENDS Integers, Sequences, TLC | |
(*************************************************************************** | |
Global States | |
***************************************************************************) | |
\* Set of nodes in the cluster | |
CONSTANT Nodes | |
\* The node that will be the only sender | |
CONSTANT Root | |
\* Broadasts to be performed | |
CONSTANT Broadcasts | |
\* Broadcasts performed | |
VARIABLE performedBroadcasts | |
\* Types of Messages in the System | |
CONSTANT BroadcastMessageType, PruneMessageType, | |
IHaveMessageType, GraftMessageType | |
\* Set of in-flight messages (messages sent by a node but not yet received) | |
\* TODO: this doesn't allow for duplicating messages (like Raft proof) since | |
\* it is a set | |
VARIABLE messages | |
(*************************************************************************** | |
per-node state | |
***************************************************************************) | |
\* Initial Eagers & Lazys for each node | |
CONSTANT InitEagers, InitLazys | |
\* Sets of Eager and Lazy peers | |
VARIABLE eagerPeers, lazyPeers | |
\* Received Broadcasts | |
VARIABLE received | |
(*************************************************************************** | |
Message Builders | |
***************************************************************************) | |
BroadcastMessage(s,d,id,round) == [type |-> BroadcastMessageType, | |
source |-> s, | |
dest |-> d, | |
bid |-> id, | |
round |-> round] | |
PruneMessage(broadcast)== [type |-> PruneMessageType, | |
\* responding to broadcast so switch sender/dest | |
source |-> broadcast.dest, | |
dest |-> broadcast.source] | |
\* An IHave looks the same as a Broadcast in this model because BroadcastMessage | |
\* does not include a payload. However, they are semantically different | |
IHaveMessage(s,d,id,round) == [type |-> IHaveMessageType, | |
source |-> s, | |
dest |-> d, | |
bid |-> id, | |
round |-> round] | |
GraftMessage(ihave) == [type |-> GraftMessageType, | |
\* responding to ihave so switch sender/dest | |
source |-> ihave.dest, | |
dest |-> ihave.source, | |
bid |-> ihave.bid, | |
round |-> ihave.round] | |
(*************************************************************************** | |
Helpers | |
***************************************************************************) | |
OutstandingBroadcasts == Broadcasts \ performedBroadcasts | |
SendAll(m) == messages' = UNION {messages,m} | |
WithSent(m) == UNION {messages, m} | |
Discard(m) == messages' = messages \ {m} | |
WithRemoved(m) == messages \ m | |
\* Builder for eager and lazy messages (broadcasts and ihaves) | |
PeerMessages(bid, receivedfrom, sender, round, peers, MessageBuilder(_, _, _, _)) == | |
LET dests == { d \in peers[sender] : ~(d = receivedfrom) } | |
IN { MessageBuilder(sender, d, bid, round) : d \in dests } | |
Received(bid, node) == received' = [received EXCEPT ![node] = UNION {@, {bid}}] | |
AddEager(node, eager) == /\ eagerPeers' = [eagerPeers EXCEPT ![node]=UNION {@, {eager}}] | |
/\ lazyPeers' = [lazyPeers EXCEPT ![node]= @ \ {eager}] | |
AddLazy(node, lazy) == /\ lazyPeers' = [lazyPeers EXCEPT ![node] = UNION {@, {lazy}}] | |
/\ eagerPeers' = [eagerPeers EXCEPT ![node] = @ \ {lazy}] | |
(*************************************************************************** | |
Message Handlers | |
***************************************************************************) | |
HandleBroadcastMessage(m) == \/ /\ m.bid \notin received[m.dest] | |
/\ Received(m.bid, m.dest) | |
\* use m.dest because we are sending this from the node | |
\* that received the message | |
/\ messages' = | |
UNION { messages, | |
PeerMessages(m.bid, m.source, m.dest, m.round+1, eagerPeers, BroadcastMessage), | |
PeerMessages(m.bid, m.source, m.dest, m.round+1, lazyPeers, IHaveMessage) | |
} \ {m} | |
\* add source to destinations eager set | |
/\ AddEager(m.dest, m.source) | |
\/ /\ m.bid \in received[m.dest] | |
\* add source to destinations lazy set and prune | |
/\ AddLazy(m.dest, m.source) | |
/\ messages' = UNION { messages, {PruneMessage(m)} } \ {m} | |
/\ UNCHANGED <<received>> | |
HandleIHaveMessage(m) == \/ /\ m.bid \notin received[m.dest] | |
\* send graft message for broadcast we haven't received | |
\* TODO: don't send graft message immediately, put ihave in missing set, use timer | |
/\ messages' = UNION { messages \ {m}, { GraftMessage(m) } } | |
\* add source to destinations eager set | |
/\ AddEager(m.dest, m.source) | |
\/ /\ m.bid \in received[m.dest] | |
/\ messages' = messages \ {m} | |
/\ UNCHANGED <<eagerPeers, lazyPeers>> | |
/\ UNCHANGED <<received>> | |
HandlePruneMessage(m) == /\ messages' = messages \ {m} | |
\* move source of message to dest's lazy set | |
/\ AddLazy(m.dest, m.source) | |
/\ UNCHANGED <<received>> | |
HandleGraftMessage(m) == /\ AddEager(m.dest, m.source) | |
\* send broadcast back to grafter | |
/\ messages' = UNION { messages \ {m}, | |
{ BroadcastMessage(m.dest,m.source,m.bid,m.round) } } | |
/\ UNCHANGED received | |
(*************************************************************************** | |
Initial State | |
***************************************************************************) | |
InitNodeState == /\ eagerPeers = [i \in Nodes |-> InitEagers[i]] | |
/\ lazyPeers = [i \in Nodes |-> InitLazys[i]] | |
/\ received = [i \in Nodes |-> {}] | |
Init == /\ performedBroadcasts = {} | |
/\ messages = {} | |
/\ InitNodeState | |
(*************************************************************************** | |
Transitions | |
***************************************************************************) | |
DropMessage == /\ \E m \in messages : messages' = messages \ {m} | |
/\ UNCHANGED <<received, eagerPeers, lazyPeers, performedBroadcasts>> | |
\* Begin a broadcast from the root of the tree | |
Broadcast(bid) == /\ performedBroadcasts' = UNION {performedBroadcasts, {bid}} | |
/\ Received(bid, Root) | |
/\ messages' = UNION {messages, | |
PeerMessages(bid, Root, Root, 0, eagerPeers, BroadcastMessage), | |
PeerMessages(bid, Root, Root, 0, lazyPeers, IHaveMessage)} | |
/\ UNCHANGED <<eagerPeers, lazyPeers>> | |
\* Receive a message | |
Receive == \E m \in messages : | |
\/ m.type = BroadcastMessageType /\ HandleBroadcastMessage(m) | |
\/ m.type = PruneMessageType /\ HandlePruneMessage(m) | |
\/ m.type = IHaveMessageType /\ HandleIHaveMessage(m) | |
\/ m.type = GraftMessageType /\ HandleGraftMessage(m) | |
/\ UNCHANGED <<performedBroadcasts>> | |
Next == \/ \E m \in OutstandingBroadcasts : Broadcast(m) | |
\/ Receive | |
\/ DropMessage | |
(*************************************************************************** | |
Invariants | |
***************************************************************************) | |
\* TODO: "type invariants" | |
ValidPeers == \A n \in Nodes : /\ \A e \in eagerPeers[n] : e \notin lazyPeers[n] | |
/\ n \notin eagerPeers[n] | |
/\ n \notin lazyPeers[n] | |
\* When there are no more messages in the network and no more broadcasts | |
\* the system should be consistent | |
EventuallyConsistent == messages = {} /\ performedBroadcasts = Broadcasts => | |
\A b \in Broadcasts : \A n \in Nodes : b \in received[n] | |
============================================================================= | |
\* Modification History | |
\* Last modified Mon Jul 08 22:17:01 PDT 2013 by jordan | |
\* Created Sun Jul 07 18:06:19 PDT 2013 by jordan |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment