Skip to content

Instantly share code, notes, and snippets.

@jrwest

jrwest/ClusterMetaSimple.tla Secret

Created Nov 21, 2013
Embed
What would you like to do?
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
------------------------- 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
You can’t perform that action at this time.