-
Notifications
You must be signed in to change notification settings - Fork 0
/
follower.maude
80 lines (69 loc) · 3.11 KB
/
follower.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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
load ./node
mod FOLLOWER is
--- a follower node is the most usual state - they wait for a message (commit, become leader, etc) and respond or change accordingly
pr NODE .
var C : Command .
var oids : OidSet .
var cli lea fol : Oid .
var fols : OidSet .
vars log log2 oldlog comlog : Log .
var AS : AttributeSet .
var N1 N2 N3 term new-term term-res : Nat .
var E E1 E2 : Entry .
var M : Msg .
var B : Bool .
--- propagate Request
rl [request-follower] :
(msg Request(C) from cli to fol)
< fol : FollowerNode | next-neighbor : lea, AS > =>
< fol : FollowerNode | next-neighbor : lea, AS >
(msg Request(C) from cli to lea) .
--- set the log of the leader
crl [append-entry-follower] :
(msg AppendEntry(new-term, log) from lea to fol)
< fol : FollowerNode | currentTerm : term , log : oldlog, AS > =>
< fol : FollowerNode | currentTerm : new-term, log : log, AS >
(msg AppendEntryResponse(new-term, true) from fol to lea)
if new-term >= term .
--- commit up to entry E if not committed (and update state machine with log ; E, if modelog)
crl [commit-follower] :
(msg Commit(new-term, E) from lea to fol)
< fol : FollowerNode | currentTerm : term , log : comlog ; log ; E ; log2, committed : comlog , AS > =>
< fol : FollowerNode | currentTerm : new-term, log : comlog ; log ; E ; log2, committed : comlog ; log ; E, AS >
if new-term >= term .
--- if log doesn't have E or E is already committed, ignore
crl [cant-commit-follower] :
(msg Commit(new-term, E) from lea to fol)
< fol : FollowerNode | currentTerm : term , log : log, committed : comlog, AS > =>
< fol : FollowerNode | currentTerm : new-term, log : log, committed : comlog, AS >
if (new-term >= term) and ((not contains(log, E)) or (contains(comlog, E))) .
--- go offline
rl [die] :
(msg Die from cli to fol)
< fol : FollowerNode | AS > =>
< fol : OfflineNode | AS >
(msg Die from fol to cli) .
--- delete AppendEntryresponse messages
rl [follower-append-entry-response] :
(msg AppendEntryResponse(term, B) from lea to fol)
< fol : FollowerNode | AS > =>
< fol : FollowerNode | AS > .
--- delete vote messages
rl [follower-vote-result] :
(msg Vote(term, B) from lea to fol)
< fol : FollowerNode | AS > =>
< fol : FollowerNode | AS > .
--- send new term and last entry to request vote
rl [become-leader] :
(msg BecomeLeader(new-term) from lea to fol)
< fol : FollowerNode | currentTerm : term , log : log ; E, neighbors : fols, yes : N1, number-response : N2, AS > =>
< fol : CandidateNode | currentTerm : new-term, log : log ; E, neighbors : fols, yes : 1 , number-response : 0 , AS >
(multicast RequestVote(new-term, E) from fol to fols) .
--- vote yes if log not as up-to-date
crl [follower-vote] :
(msg RequestVote(new-term, E2) from lea to fol)
< fol : FollowerNode | currentTerm : term , log : log ; E1, AS > =>
< fol : FollowerNode | currentTerm : new-term, log : log ; E1, AS >
(msg Vote(new-term, (E1 < E2)) from fol to lea)
if (new-term >= term) .
endm