-
Notifications
You must be signed in to change notification settings - Fork 3
/
OpAWSet.tla
89 lines (82 loc) · 4.36 KB
/
OpAWSet.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
------------------------------ MODULE OpAWSet ------------------------------
EXTENDS AWSet, FiniteSets
CONSTANTS Read(_), InitMsg
-----------------------------------------------------------------------------
VARIABLES
aset, \* aset[r]: the set of active elements maintained by r \in Replica
abuf, \* abuf[r]: the buffer for elements added by r \in Replica since the last broadcast
rbuf, \* rbuf[r]: the buffer for elements removed by r \in Replica since the last broadcast
(* variables for network: *)
incoming, \* incoming[r]: incoming channel at replica r \in Replica
lmsg, \* lmsg[r]: the last message delivered at r \in Replica to the upper-layer protocol
vc, \* vc[r][s] denotes the latest message from s \in Replica observed by r \in Replica
(* variables for correctness: *)
doset, \* doset[r]: the set of updates generated by replica r \in Replica
delset, \* uset[r]: the set of updates delivered by replica r \in Replica
uincoming, \* uincoming[r]: incoming channel for broadcasting/delivering updates at r \in Replica
buset \* buset[r]: the buffer of local updates made by r \in Replica since the last broadcast
nVars == <<incoming, lmsg, vc>>
cVars == <<doset, delset, uincoming, buset>>
vars == <<aset, abuf, rbuf, seq, nVars, cVars>>
-----------------------------------------------------------------------------
Msg == [aid : Aid, abuf : SUBSET Element, rbuf: SUBSET Element]
Network == INSTANCE ReliableCausalNetwork \* WITH incoming <- incoming, lmsg <- lmsg, vc <- vc
ReadOpAWSet(r) == {ele.d: ele \in aset[r]} \* read the state of r\in Replica
Correctness == INSTANCE OpCorrectness
\* WITH doset <- doset, delset <- delset, uincoming <- uincoming, buset <- buset
-----------------------------------------------------------------------------
TypeOK ==
/\aset \in [Replica -> SUBSET Element]
/\abuf \in [Replica -> SUBSET Element]
/\rbuf \in [Replica -> SUBSET Element]
/\IntTypeOK
/\Correctness!CTypeOK
-----------------------------------------------------------------------------
Init ==
/\ aset = [r \in Replica |-> {}]
/\ abuf = [r \in Replica |-> {}]
/\ rbuf = [r \in Replica |-> {}]
/\ IntInit
/\ Network!RCNInit
/\ Correctness!OpCInit
-----------------------------------------------------------------------------
Add(d, r) == \* r\in Replica adds d \in Data
/\ LET e == [aid |-> [r |-> r, seq |-> seq[r]], d |-> d]
IN /\ aset' = [aset EXCEPT ![r] = @ \union {e}]
/\ abuf' = [abuf EXCEPT ![r] = @ \union {e}]
/\ IntDo(r)
/\ Correctness!OpCDo(r)
/\ UNCHANGED <<rbuf, nVars>>
Remove(d, r) == \* r\in Replica removes d \in Data
/\ LET E == {ele \in aset[r] : ele.d = d} \* E may be empty
IN /\ aset' = [aset EXCEPT ![r] = @ \ E]
/\ rbuf' = [rbuf EXCEPT ![r] = @ \cup E]
/\ IntDo(r)
/\ Correctness!OpCDo(r)
/\ UNCHANGED <<abuf, nVars>>
Do(r) == \* We ignore ReadOpAWSet(r) since it does not modify states.
\E d \in Data : Add(d, r) \/ Remove(d, r)
-----------------------------------------------------------------------------
Send(r) == \* r\in Replica sends a message
/\ buset[r] # {}
/\ abuf' = [abuf EXCEPT ![r] = {}]
/\ rbuf' = [rbuf EXCEPT ![r] = {}]
/\ Network!RCNBroadcast(r, [aid |-> [r |-> r, seq |-> seq[r]],
abuf|-> abuf[r], rbuf|-> rbuf[r]])
/\ IntSend(r)
/\ Correctness!OpCSend(r)
/\ UNCHANGED <<aset>>
Deliver(r) == \* r\in Replica delivers a message (lmsg'[r])
/\IntDeliver(r)
/\Network!RCNDeliver(r)
/\Correctness!OpCDeliver(r, lmsg'[r].aid)
/\aset' = [aset EXCEPT ![r] = (@ \cup lmsg'[r].abuf) \ lmsg'[r].rbuf]
/\UNCHANGED <<abuf, rbuf>>
-----------------------------------------------------------------------------
Next == \E r \in Replica: Do(r) \/ Send(r) \/ Deliver(r)
Fairness == \A r \in Replica: WF_vars(Send(r)) /\ WF_vars(Deliver(r))
Spec == Init /\ [][Next]_vars /\ Fairness
=============================================================================
\* Modification History
\* Last modified Sat Aug 31 15:58:24 CST 2019 by xhdn
\* Created Fri May 24 14:12:26 CST 2019 by xhdn