-
Notifications
You must be signed in to change notification settings - Fork 0
/
leader.maude
58 lines (51 loc) · 2.53 KB
/
leader.maude
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
load ./node
mod LEADER is
--- a leader node handles incoming queries and replication
pr NODE .
var C : Command .
var oids : OidSet .
var cli lea fol : Oid .
var fols : OidSet .
var log log' comlog : Log .
var AS : AttributeSet .
var N1 N2 N3 term term-res : Nat .
var B : Bool .
var M : Msg .
var E : Entry .
--- when given a Request, add to log and send to all other nodes
crl [request-leader] :
(msg Request(C) from cli to lea)
< lea : LeaderNode | currentTerm : term, log : log , neighbors : fols, waiting : false, yes : N1, number-response : N2, AS >
=>
< lea : LeaderNode | currentTerm : term, log : log', neighbors : fols, waiting : true , yes : 1 , number-response : 0 , AS >
(multicast AppendEntry(term, log') from lea to fols)
if log' := log ; entry(index(head(log)) + 1, term, C) .
--- acknowlogge that log was updated
rl [append-entry-response-leader] :
(msg AppendEntryResponse(term, B) from fol to lea)
< lea : LeaderNode | currentTerm : term, log : log, yes : N1, number-response : N2, AS >
=>
< lea : LeaderNode | currentTerm : term, log : log, yes : N1 + to-nat(B), number-response : N2 + 1, AS > .
--- when everyone responds, commit if majority said yes, retry if not
crl [commit] :
< lea : LeaderNode | currentTerm : term, waiting : true , neighbors : oids, log : log, committed : comlog, majority : N1, yes : N2, number-neighbors : N3, number-response : N3, AS >
=>
< lea : LeaderNode | currentTerm : term, waiting : false, neighbors : oids, log : log, committed : log , majority : N1, yes : N2, number-neighbors : N3, number-response : N3, AS >
(multicast Commit(term, head(log)) from lea to oids)
if N2 >= N1 .
--- retry the AppendEntry message - note, this should never occur if a majority of nodes are online!
crl [retry] :
< lea : LeaderNode | currentTerm : term, neighbors : oids, log : log, majority : N1, yes : N2, number-neighbors : N3, number-response : N3, AS >
=>
< lea : LeaderNode | currentTerm : term, neighbors : oids, log : log, majority : N1, yes : 1 , number-neighbors : N3, number-response : 0 , AS >
(multicast AppendEntry(term, log) from lea to oids)
if N2 < N1 .
--- tell the next node to start leader process and become offline
rl [die] :
(msg Die from cli to lea)
< lea : LeaderNode | currentTerm : term, next-neighbor : fol, AS >
=>
< lea : OfflineNode | currentTerm : term, next-neighbor : fol, AS >
(msg Die from lea to cli)
(msg BecomeLeader(term + 1) from lea to fol) .
endm