-
Notifications
You must be signed in to change notification settings - Fork 15
/
MessagePassing_v4_13.tla
125 lines (108 loc) · 5.74 KB
/
MessagePassing_v4_13.tla
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
--------------------------- MODULE MessagePassing_v4_13 ---------------------------
EXTENDS FiniteSets, FiniteSetsExt, Sequences, SequencesExt, Integers, TLC
CONSTANTS AddEntryRequestMessage,
AddEntryResponseMessage,
FenceRequestMessage,
FenceResponseMessage,
ReadRequestMessage,
ReadResponseMessage
VARIABLES messages
(***************************************************************************)
(* Message Passing *)
(* *)
(* Messages are represented by a funcion of MSG -> Delivery Count. *)
(* Each message sent is modelled as both delivered and lost via *)
(* existential quantification. When a message is processed, the delivery *)
(* count is decremented. *)
(* When a message is lost, the delivery count is set to -1 to *)
(* differentiate it from a processed message. Time outs are enabled by *)
(* detecting messages with a del count of -1. Once a time out has been *)
(* acted upon, the -1 count is cleared (set to 0) so the time out is not *)
(* triggered more than once. *)
(* Resending messages is not currently modelled but is supported by simply *)
(* incrementing the delivery count. *)
(* *)
(* NOTE: There are no ordering guarantees of message receipt for any given *)
(* actor. So a bookie may be delivered an AddEntryRequest from the *)
(* writer first, then a Read request from the 2nd client after that, *)
(* but the bookie process the read request first, and the add second.*)
(***************************************************************************)
ReadTimeoutForBookie(msgs, bookie) ==
\E msg \in DOMAIN msgs :
/\ msgs[msg] = -1
/\ msg.bookie = bookie
/\ msg.type \in {ReadRequestMessage, ReadResponseMessage}
WriteTimeoutForBookie(msgs, bookie, recovery) ==
\E msg \in DOMAIN msgs :
/\ msgs[msg] = -1
/\ msg.bookie = bookie
/\ msg.type \in {AddEntryRequestMessage, AddEntryResponseMessage}
/\ msg.recovery = recovery
ReadTimeoutCount(ensemble, recovery) ==
IF \E b \in ensemble : ReadTimeoutForBookie(messages, b)
THEN Cardinality({ b \in ensemble : ReadTimeoutForBookie(messages, b)})
ELSE 0
ClearWriteTimeout(bookie, recovery) ==
messages' = [m \in DOMAIN messages |-> IF /\ (m.type = AddEntryRequestMessage \/ m.type = AddEntryResponseMessage)
/\ m.bookie = bookie
/\ m.recovery = recovery
/\ messages[m] = -1
THEN 0
ELSE messages[m]]
ClearReadTimeouts(msg, ensemble) ==
messages' = [m \in DOMAIN messages |-> IF msg = m
THEN 0
ELSE IF /\ m.bookie \in ensemble
/\ (m.type = ReadRequestMessage \/ m.type = ReadResponseMessage)
/\ messages[m] = -1
THEN 0
ELSE messages[m]]
DelCountOf(msg, counts) ==
LET pair == CHOOSE c \in counts : c[1] = msg
IN pair[2]
\* Send a set of messages only if none have been previously sent
\* In any given step, a random subset of these messages are lost (including none)
\* The TLA+ is simply choosing a delivery count for each message that
\* TLC will explore exhaustively.
SendMessagesToEnsemble(msgs) ==
/\ \A msg \in msgs : msg \notin DOMAIN messages
/\ LET possible_del_counts == { s \in SUBSET (msgs \X {-1, 1}) :
/\ Cardinality(s) = Cardinality(msgs)
/\ \A msg \in msgs : \E s1 \in s : s1[1] = msg
}
IN
\E counts \in possible_del_counts :
LET msgs_to_send == [m \in msgs |-> DelCountOf(m, counts)]
IN messages' = messages @@ msgs_to_send
\* Send a message only if the message has not already been sent
SendMessage(msg) ==
/\ msg \notin DOMAIN messages
/\ \E delivered_count \in {-1,1} :
messages' = messages @@ (msg :> delivered_count)
\* Mark one message as processed and send a new message
ProcessedOneAndSendAnother(received_msg, send_msg) ==
/\ received_msg \in DOMAIN messages
/\ send_msg \notin DOMAIN messages
/\ messages[received_msg] >= 1
/\ \E delivered_count \in {-1, 1} :
/\ messages' = [messages EXCEPT ![received_msg] = @-1] @@ (send_msg :> delivered_count)
\* Mark one message as processed
MessageProcessed(msg) ==
/\ msg \in DOMAIN messages
/\ messages[msg] >= 1
/\ messages' = [messages EXCEPT ![msg] = @ - 1]
\* The message is of this type and has been delivered to the recipient
ReceivableMessageOfType(msgs, msg, message_type) ==
/\ msg.type = message_type
/\ msgs[msg] >= 1
IsEarliestMsg(msg) ==
~\E msg2 \in DOMAIN messages :
/\ ReceivableMessageOfType(messages, msg2, msg.type)
/\ msg2.recovery = msg.recovery
/\ msg2.entry.id < msg.entry.id
/\ msg2.bookie = msg.bookie
=============================================================================
\* Modification History
\* Last modified Mon Nov 22 10:23:17 CET 2021 by GUNMETAL
\* Last modified Mon Nov 23 09:37:09 CET 2020 by jvanlightly
\* Created Mon Nov 23 09:19:26 CET 2020 by jvanlightly