-
Notifications
You must be signed in to change notification settings - Fork 0
/
MongoLoglessDynamicRaft.tla
132 lines (109 loc) · 4.48 KB
/
MongoLoglessDynamicRaft.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
126
127
128
129
130
131
132
---- MODULE MongoLoglessDynamicRaft ----
\*
\* Logless protocol for managing configuration state for dynamic reconfiguration
\* in MongoDB replication.
\*
EXTENDS Naturals, Integers, FiniteSets, Sequences, TLC, Defs
CONSTANTS Server
CONSTANTS Secondary, Primary, Nil
VARIABLE currentTerm
VARIABLE state
VARIABLE configVersion
VARIABLE configTerm
VARIABLE config
vars == <<currentTerm, state, configVersion, configTerm, config>>
\*
\* Helper operators.
\*
\* Is the config of node i considered 'newer' than the config of node j. This is the condition for
\* node j to accept the config of node i.
IsNewerConfig(i, j) ==
\/ configTerm[i] > configTerm[j]
\/ /\ configTerm[i] = configTerm[j]
/\ configVersion[i] > configVersion[j]
IsNewerOrEqualConfig(i, j) ==
\/ /\ configTerm[i] = configTerm[j]
/\ configVersion[i] = configVersion[j]
\/ IsNewerConfig(i, j)
\* Compares two configs given as <<configVersion, configTerm>> tuples.
NewerConfig(ci, cj) ==
\* Compare configTerm first.
\/ ci[2] > cj[2]
\* Compare configVersion if terms are equal.
\/ /\ ci[2] = cj[2]
/\ ci[1] > cj[1]
\* Compares two configs given as <<configVersion, configTerm>> tuples.
NewerOrEqualConfig(ci, cj) == NewerConfig(ci, cj) \/ ci = cj
\* Can node 'i' currently cast a vote for node 'j' in term 'term'.
CanVoteForConfig(i, j, term) ==
/\ currentTerm[i] < term
/\ IsNewerOrEqualConfig(j, i)
\* A quorum of servers in the config of server i have i's config.
ConfigQuorumCheck(i) ==
\E Q \in Quorums(config[i]) : \A t \in Q :
/\ configVersion[t] = configVersion[i]
/\ configTerm[t] = configTerm[i]
\* A quorum of servers in the config of server i have the term of i.
TermQuorumCheck(i) ==
\E Q \in Quorums(config[i]) : \A t \in Q : currentTerm[t] = currentTerm[i]
-------------------------------------------------------------------------------------------
\*
\* Next state actions.
\*
\* Update terms if node 'i' has a newer term than node 'j' and ensure 'j' reverts to Secondary state.
UpdateTermsExpr(i, j) ==
/\ currentTerm[i] > currentTerm[j]
/\ currentTerm' = [currentTerm EXCEPT ![j] = currentTerm[i]]
/\ state' = [state EXCEPT ![j] = Secondary]
UpdateTerms(i, j) ==
/\ UpdateTermsExpr(i, j)
/\ UNCHANGED <<configVersion, configTerm, config>>
BecomeLeader(i, voteQuorum) ==
\* Primaries make decisions based on their current configuration.
LET newTerm == currentTerm[i] + 1 IN
/\ i \in config[i]
/\ i \in voteQuorum
/\ \A v \in voteQuorum : CanVoteForConfig(v, i, newTerm)
\* Update the terms of each voter.
/\ currentTerm' = [s \in Server |-> IF s \in voteQuorum THEN newTerm ELSE currentTerm[s]]
/\ state' = [s \in Server |->
IF s = i THEN Primary
ELSE IF s \in voteQuorum THEN Secondary \* All voters should revert to secondary state.
ELSE state[s]]
\* Update config's term on step-up.
/\ configTerm' = [configTerm EXCEPT ![i] = newTerm]
/\ UNCHANGED <<config, configVersion>>
\* A reconfig occurs on node i. The node must currently be a leader.
Reconfig(i, newConfig) ==
/\ state[i] = Primary
/\ ConfigQuorumCheck(i)
/\ TermQuorumCheck(i)
/\ QuorumsOverlap(config[i], newConfig)
/\ i \in newConfig
/\ configTerm' = [configTerm EXCEPT ![i] = currentTerm[i]]
/\ configVersion' = [configVersion EXCEPT ![i] = configVersion[i] + 1]
/\ config' = [config EXCEPT ![i] = newConfig]
/\ UNCHANGED <<currentTerm, state>>
\* Node i sends its current config to node j.
SendConfig(i, j) ==
/\ state[j] = Secondary
/\ IsNewerConfig(i, j)
/\ configVersion' = [configVersion EXCEPT ![j] = configVersion[i]]
/\ configTerm' = [configTerm EXCEPT ![j] = configTerm[i]]
/\ config' = [config EXCEPT ![j] = config[i]]
/\ UNCHANGED <<currentTerm, state>>
Init ==
/\ currentTerm = [i \in Server |-> 0]
/\ state = [i \in Server |-> Secondary]
/\ configVersion = [i \in Server |-> 1]
/\ configTerm = [i \in Server |-> 0]
/\ \E initConfig \in SUBSET Server :
/\ initConfig # {}
/\ config = [i \in Server |-> initConfig]
Next ==
\/ \E s \in Server, newConfig \in SUBSET Server : Reconfig(s, newConfig)
\/ \E s,t \in Server : SendConfig(s, t)
\/ \E i \in Server : \E Q \in Quorums(config[i]) : BecomeLeader(i, Q)
\/ \E s,t \in Server : UpdateTerms(s,t)
Spec == Init /\ [][Next]_vars
=============================================================================