-
Notifications
You must be signed in to change notification settings - Fork 31
/
Copy pathOxiaReplication.tla
1193 lines (1024 loc) · 51.8 KB
/
OxiaReplication.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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
-------------------------- MODULE OxiaReplication --------------------------
EXTENDS MessagePassing, Integers, Sequences, FiniteSets, TLC
(*
Each action has ample comments that describe it. Also each action is
clearly commented to show what the enabling conditions are and what
the state changes are. Enabling conditions are the conditions required
for the action to take place, such as an term being of the right value.
An action wil only occur if all the enabling conditions are true.
This spec includes:
- One or more coordinators
- Multiple nodes
- Leader election
- Data replication
Not modelling:
- Failure detection. There is no need to as:
- the coordinator can start an election at any time.
- for each election, the coordinator has visibility of any arbitrary number of nodes which
simulates an arbitray number of node failures.
The state space is large as expected. Use of simulation for non-trivial numbers of nodes, values
and terms is required.
*)
CONSTANTS Coordinators, \* The set of all coordinators (should only be one but the protocol should handle multiple)
Nodes, \* The set of all nodes
Values, \* The set of all values that can be sent by clients
RepFactor \* The desired initial replication factor
\* State space
CONSTANTS MaxTerms, \* The max number of terms for the model checker to explore
MaxCoordinatorStops \* The max number of coordinator crashes that the model checker will explore
\* Shard statuses
CONSTANTS STEADY_STATE, \* The shard is in data replication mode
ELECTION \* An election is in progress
\* Coordinator statuses
CONSTANTS RUNNING, \* an coordinator is running
NOT_RUNNING \* an coordinator is not running
\* Node statuses
CONSTANTS FENCED, \* denotes a node that has been fenced during an election
LEADER, \* denotes a chosen leader
FOLLOWER, \* denotes a follower ready to receive entries from the leader
NOT_MEMBER \* not a member of the shard ensemble
\* Election phases
CONSTANTS FENCING, \* prevent nodes from making progress
NOTIFY_LEADER, \* a leader has been selected and is being notified by the coordinator
LEADER_ELECTED \* a leader has confirmed its leadership
\* return codes
CONSTANTS OK, \* the request was serviced correctly
INVALID_TERM \* node has rejected a request because it has a higher term than the request
\* follow cursor states
CONSTANTS ATTACHED, \* a follow cursor is attached and operational
PENDING_TRUNCATE \* a follow cursor is inactive but will become active upon follower truncation
\* other model values
CONSTANTS NIL \* used in various places to signify something does not exist
VARIABLES
\* state of the system
metadata_version, \* monotonic counter incremented on each metadata change
metadata, \* the metadata shard state
node_state, \* the nodes and their state
coordinator_state, \* the coordinators and their state
\* auxilliary state required by the spec
confirmed, \* the confirmation status of each written value
coordinator_stop_ctr \* a counter that incremented each time an coordinator crashes/stops
vars == << metadata_version, metadata, node_state, coordinator_state, confirmed, messages, coordinator_stop_ctr >>
view == << metadata_version, metadata, node_state, coordinator_state, confirmed, messages >>
(* -----------------------------------------
TYPE DEFINITIONS
The type definitions for the fundamental structures, messages
and state of the various actors. Required for the optional type invariant
TypeOK and also useful to understand the structure of the protocol.
----------------------------------------- *)
\* Basic types
Term == 0..MaxTerms
NodesOrNil == Nodes \union {NIL}
EntryId == [offset: Nat, term: Term]
LogEntry == [entry_id: EntryId, value: Values]
CursorStatus == { NIL, ATTACHED, PENDING_TRUNCATE }
Cursor == [status: CursorStatus, last_pushed: EntryId, last_confirmed: EntryId]
NodeStatus == { LEADER, FOLLOWER, FENCED, NOT_MEMBER }
\* equivalent of null for various record types
NoEntryId == [offset |-> 0, term |-> 0]
NoLogEntry == [entry_id |-> NoEntryId, value |-> NIL]
NoCursor == [status |-> NIL, last_pushed |-> NoEntryId, last_confirmed |-> NoEntryId]
\* ------------------------------
\* Messages
\* ------------------------------
\* Coordinator -> Nodes
NewTermRequest ==
[type: {NEW_TERM_REQUEST},
node: Nodes,
coordinator: Coordinators,
term: Term]
\* Node -> Coordinator
NewTermResponse ==
[type: {NEW_TERM_RESPONSE},
node: Nodes,
coordinator: Coordinators,
head_entry_id: EntryId,
term: Term]
\* Coordinator -> Node
BecomeLeaderRequest ==
[type: {BECOME_LEADER_REQUEST},
node: Nodes,
coordinator: Coordinators,
term: Term,
rep_factor: Nat,
follower_map: [Nodes -> EntryId \union {NIL}]]
\* Node -> Coordinator
BecomeLeaderResponse ==
[type: {BECOME_LEADER_RESPONSE},
node: Nodes,
coordinator: Coordinators,
term: Term]
\* Coordinator -> Node (Leader)
AddFollowerRequest ==
[type: {ADD_FOLLOWER_REQUEST},
node: Nodes,
follower: Nodes,
head_entry_id: EntryId,
term: Term]
\* Node (Leader) -> Node (Follower)
TruncateRequest ==
[type: {TRUNCATE_REQUEST},
dest_node: Nodes,
source_node: Nodes,
term: Term,
head_entry_id: EntryId]
\* Node (Follower) -> Node (Leader)
TruncateResponse ==
[type: {TRUNCATE_RESPONSE},
dest_node: Nodes,
source_node: Nodes,
term: Term,
head_entry_id: EntryId]
\* Node (Leader) -> Node (Follower)
AppendEntry ==
[type: {APPEND},
dest_node: Nodes,
source_node: Nodes,
entry: LogEntry,
commit_entry_id: EntryId,
term: Term]
\* Node (Follower) -> Node (Leader)
Ack ==
[type: {ACK},
dest_node: Nodes,
source_node: Nodes,
code: {OK, INVALID_TERM},
entry_id: EntryId,
term: Term]
Message ==
NewTermRequest \union NewTermResponse \union
BecomeLeaderRequest \union BecomeLeaderResponse \union
AddFollowerRequest \union
TruncateRequest \union TruncateResponse \union
AppendEntry \union Ack
\* Metadata store state
ShardStatus == { NIL, STEADY_STATE, ELECTION }
Metadata == [shard_status: ShardStatus,
term: Term,
ensemble: SUBSET Nodes,
rep_factor: Nat,
leader: NodesOrNil]
\* Node and Coordinator state
NodeState == [id: Nodes,
status: NodeStatus,
term: Term,
leader: Nodes \union {NIL},
rep_factor: Nat,
log: SUBSET LogEntry,
commit_entry_id: EntryId,
head_entry_id: EntryId,
follow_cursor: [Nodes -> Cursor]]
CoordinatorStatuses == {NOT_RUNNING, RUNNING}
ElectionPhases == { NIL, FENCING, NOTIFY_LEADER, LEADER_ELECTED }
CoordinatorState == [id: Coordinators,
status: CoordinatorStatuses,
md_version: Nat,
md: Metadata \union {NIL},
election_phase: ElectionPhases,
election_leader: Nodes \union {NIL},
election_fence_responses: SUBSET NewTermResponse]
\* Type invariant
TypeOK ==
/\ metadata \in Metadata
/\ node_state \in [Nodes -> NodeState]
/\ coordinator_state \in [Coordinators -> CoordinatorState]
/\ \A v \in DOMAIN confirmed :
/\ v \in Values
/\ confirmed[v] \in BOOLEAN
/\ \A msg \in DOMAIN messages : msg \in Message
(* -----------------------------------------
INITIAL STATE
The only initial state is the shard ensemble
and rep factor. There is no leader, followers
or even a running coordinator.
-----------------------------------------
*)
Init ==
LET ensemble == CHOOSE e \in SUBSET Nodes : Cardinality(e) = RepFactor
IN
/\ metadata_version = 0
/\ metadata = [shard_status |-> NIL,
term |-> 0,
ensemble |-> ensemble,
rep_factor |-> RepFactor,
leader |-> NIL]
/\ node_state = [n \in Nodes |->
[id |-> n,
status |-> NOT_MEMBER,
term |-> 0,
leader |-> NIL,
rep_factor |-> 0,
log |-> {},
commit_entry_id |-> NoEntryId,
head_entry_id |-> NoEntryId,
follow_cursor |-> [n1 \in Nodes |-> NoCursor]]]
/\ coordinator_state = [o \in Coordinators |->
[id |-> o,
status |-> NOT_RUNNING,
md_version |-> 0,
md |-> NIL,
election_phase |-> NIL,
election_leader |-> NIL,
election_fence_responses |-> {}]]
/\ confirmed = <<>>
/\ messages = <<>>
/\ coordinator_stop_ctr = 0
(* -----------------------------------------
HELPER OPERATORS
-----------------------------------------*)
\* Does this set of nodes consistitute a quorum?
IsQuorum(nodes, ensemble) ==
Cardinality(nodes) >= (Cardinality(ensemble) \div 2) + 1
\* Compare two entry ids:
\* entry_id1 > entry_id2 = 1
\* entry_id1 = entry_id2 = 0
\* entry_id1 < entry_id2 = -1
CompareLogEntries(entry_id1, entry_id2) ==
IF entry_id1.term > entry_id2.term THEN 1
ELSE
IF entry_id1.term = entry_id2.term /\ entry_id1.offset > entry_id2.offset THEN 1
ELSE
IF entry_id1.term = entry_id2.term /\ entry_id1.offset = entry_id2.offset THEN 0
ELSE -1
IsLowerId(entry_id1, entry_id2) ==
CompareLogEntries(entry_id1, entry_id2) = -1
IsLowerOrEqualId(entry_id1, entry_id2) ==
CompareLogEntries(entry_id1, entry_id2) \in {-1, 0}
IsHigherId(entry_id1, entry_id2) ==
CompareLogEntries(entry_id1, entry_id2) = 1
IsHigherOrEqualId(entry_id1, entry_id2) ==
CompareLogEntries(entry_id1, entry_id2) \in {0, 1}
IsSameId(entry_id1, entry_id2) ==
CompareLogEntries(entry_id1, entry_id2) = 0
HeadEntry(log) ==
IF log = {}
THEN NoLogEntry
ELSE CHOOSE entry \in log :
\A e \in log : IsHigherOrEqualId(entry.entry_id, e.entry_id)
(*---------------------------------------------------------
Coordinator starts
The coordinator loads the metadata from the metadata store.
The metadata will decide what the coordinator might do
next.
----------------------------------------------------------*)
CoordinatorStarts ==
\* enabling conditions
/\ \E o \in Coordinators :
/\ coordinator_state[o].status = NOT_RUNNING
\* state changes
/\ coordinator_state' = [coordinator_state EXCEPT ![o] =
[id |-> o,
status |-> RUNNING,
md_version |-> metadata_version,
md |-> metadata,
election_phase |-> NIL,
election_leader |-> NIL,
election_fence_responses |-> {}]]
/\ UNCHANGED << confirmed, metadata, metadata_version, node_state, messages, coordinator_stop_ctr >>
(*---------------------------------------------------------
Coordinator stops
The coordinator crashes/stops and loses all local state.
----------------------------------------------------------*)
CoordinatorStops ==
\* enabling conditions
/\ coordinator_stop_ctr < MaxCoordinatorStops
/\ \E o \in Coordinators :
/\ coordinator_state[o].status = RUNNING
\* state changes
/\ coordinator_state' = [coordinator_state EXCEPT ![o].status = NOT_RUNNING,
![o].md_version = 0,
![o].md = NIL,
![o].election_phase = NIL,
![o].election_leader = NIL,
![o].election_fence_responses = {}]
/\ coordinator_stop_ctr' = coordinator_stop_ctr + 1
/\ CoordinatorMessagesLost(o)
/\ UNCHANGED << confirmed, metadata, metadata_version, node_state >>
(*---------------------------------------------------------
Coordinator starts an election
In reality this will be triggered by some kind of failure
detection outside the scope of this spec. This
spec simply allows the coordinator to decide to start an
election at anytime.
The first phase of an election is for the coordinator to
ensure that the shard cannot make progress by fencing
a majority of nodes and getting their head entry_id.
Key points:
- An election increments the term of the shard.
- The message passing module assumes all sent messages are
retried until abandoned by the sender. To simulate some nodes not
responding during an election, a non-deterministic subset of the fencing
ensemble that constitutes an majority is used, this simulates
message loss and dead nodes of a minority.
- In this spec, updating the metadata in the metadata store and sending
fencing requests is one atomic action. In an implementation, the
metadata would need to be updated first, then the fencing requests sent.
- The election phases are local state for the coordinator only. The only
required state in the metadata is the term and that an election is
in-progress. If the coordinator were to fail at any time during an
election then the next coordinator that starts would see the ELECTION
status in the metadata and trigger a new election.
- The metadata update will fail if the version does not match the version
held by the coordinator.
----------------------------------------------------------*)
GetNewTermRequests(o, new_term, ensemble) ==
{ [type |-> NEW_TERM_REQUEST,
node |-> n,
coordinator |-> o,
term |-> new_term] : n \in ensemble }
CoordinatorStartsElection ==
\* enabling conditions
\E o \in Coordinators :
LET ostate == coordinator_state[o]
IN
/\ metadata.term < MaxTerms \* state space reduction
/\ ostate.status = RUNNING
/\ ostate.md_version = metadata_version
/\ \E visible_nodes \in SUBSET metadata.ensemble :
/\ IsQuorum(visible_nodes, metadata.ensemble)
\* state changes
/\ LET new_term == ostate.md.term + 1
new_metadata == [metadata EXCEPT !.term = new_term,
!.shard_status = ELECTION,
!.leader = NIL]
new_md_version == metadata_version + 1
IN
/\ metadata_version' = new_md_version
/\ metadata' = new_metadata
/\ coordinator_state' = [coordinator_state EXCEPT ![o].id = o,
![o].md_version = new_md_version,
![o].md = new_metadata,
![o].election_phase = FENCING,
![o].election_leader = NIL,
![o].election_fence_responses = {}]
/\ SendMessages(GetNewTermRequests(o, new_term, ostate.md.ensemble))
/\ UNCHANGED << node_state, confirmed, coordinator_stop_ctr >>
(*---------------------------------------------------------
Node handles a fence request
A node receives a fencing request, fences itself and responds
with its head entry_id.
When a node is fenced it cannot:
- accept any writes from a client.
- accept add entry requests from a leader.
- send any entries to followers if it was a leader.
Any existing follow cursors are destroyed.
----------------------------------------------------------*)
GetNewTermResponse(nstate, new_term, o) ==
[type |-> NEW_TERM_RESPONSE,
node |-> nstate.id,
coordinator |-> o,
head_entry_id |-> nstate.head_entry_id,
term |-> new_term]
NodeHandlesFencingRequest ==
\* enabling conditions
\E msg \in DOMAIN messages :
/\ ReceivableMessageOfType(messages, msg, NEW_TERM_REQUEST)
/\ LET nstate == node_state[msg.node]
IN /\ nstate.term < msg.term
\* state changes
/\ node_state' = [node_state EXCEPT ![msg.node] =
[@ EXCEPT !.term = msg.term,
!.status = FENCED,
!.rep_factor = 0,
!.follow_cursor = [n \in Nodes |-> NoCursor]]]
/\ ProcessedOneAndSendAnother(msg, GetNewTermResponse(nstate, msg.term, msg.coordinator))
/\ UNCHANGED << metadata, metadata_version, coordinator_state, confirmed, coordinator_stop_ctr >>
(*---------------------------------------------------------
Coordinator handles fence response not yet reaching quorum
The coordinator handles a fence response but has not reached
quorum yet so simply stores the response.
----------------------------------------------------------*)
CoordinatorHandlesPreQuorumFencingResponse ==
\* enabling conditions
\E o \in Coordinators :
LET ostate == coordinator_state[o]
IN
/\ ostate.status = RUNNING
/\ ostate.md.shard_status = ELECTION
/\ ostate.election_phase = FENCING
/\ \E msg \in DOMAIN messages :
/\ ReceivableMessageOfType(messages, msg, NEW_TERM_RESPONSE)
/\ msg.coordinator = o
/\ ostate.md.term = msg.term
/\ LET fenced_res == ostate.election_fence_responses \union { msg }
IN /\ ~IsQuorum(fenced_res, ostate.md.ensemble)
\* state changes
/\ coordinator_state' = [coordinator_state EXCEPT ![o].election_fence_responses = fenced_res]
/\ MessageProcessed(msg)
/\ UNCHANGED << metadata, metadata_version, node_state, confirmed, coordinator_stop_ctr >>
FollowerResponse(responses, f) ==
CHOOSE r \in responses : r.node = f
GetFollowerMap(ostate, leader, responses, final_ensemble) ==
LET followers == { f \in final_ensemble :
/\ f # leader
/\ \E r \in responses : r.node = f }
IN [f \in Nodes |->
IF f \in followers
THEN FollowerResponse(responses, f).head_entry_id
ELSE NIL]
GetBecomeLeaderRequest(n, term, o, follower_map, rep_factor) ==
[type |-> BECOME_LEADER_REQUEST,
node |-> n,
coordinator |-> o,
follower_map |-> follower_map,
rep_factor |-> rep_factor,
term |-> term]
WinnerResponse(responses, final_ensemble) ==
CHOOSE r1 \in responses :
/\ r1.node \in final_ensemble
/\ ~\E r2 \in responses :
/\ IsHigherId(r2.head_entry_id, r1.head_entry_id)
/\ r2.node \in final_ensemble
CoordinatorHandlesQuorumFencingResponse ==
\* enabling conditions
\E o \in Coordinators :
LET ostate == coordinator_state[o]
IN
/\ ostate.status = RUNNING
/\ ostate.md.shard_status = ELECTION
/\ ostate.election_phase = FENCING
/\ \E msg \in DOMAIN messages :
/\ ReceivableMessageOfType(messages, msg, NEW_TERM_RESPONSE)
/\ msg.coordinator = o
/\ ostate.md.term = msg.term
/\ LET fenced_res == ostate.election_fence_responses \union { msg }
max_head_res == WinnerResponse(fenced_res, metadata.ensemble)
new_leader == max_head_res.node
last_term_entry_id == max_head_res.head_entry_id
follower_map == GetFollowerMap(ostate, new_leader, fenced_res, metadata.ensemble)
IN
/\ IsQuorum(fenced_res, metadata.ensemble)
\* state changes
/\ coordinator_state' = [coordinator_state EXCEPT ![o] =
[@ EXCEPT !.election_phase = NOTIFY_LEADER,
!.election_leader = new_leader,
!.election_fence_responses = fenced_res]]
/\ ProcessedOneAndSendAnother(msg,
GetBecomeLeaderRequest(new_leader,
ostate.md.term,
o,
follower_map,
ostate.md.rep_factor))
/\ UNCHANGED << metadata, metadata_version, node_state, confirmed, coordinator_stop_ctr >>
(*---------------------------------------------------------
Node handles a Become Leader request
The node inspects the head entry_id of each follower and
compares it to its own head entry_id, and then either:
- Attaches a follow cursor for the follower the head entry_ids
have the same term, but the follower offset is lower or equal.
- Sends a truncate request to the follower if its head
entry_id term does not match the leader's head entry_id term or has
a higher offset.
The leader finds the highest entry id in its log prefix (of the
follower head entry_id) and tells the follower to truncate it's log
to that entry.
Key points:
- The election only requires a majority to complete and so the
Become Leader request will likely only contain a majority,
not all the nodes.
- No followers in the Become Leader message "follower map" will
have a higher head entry_id than the leader (as the leader was
chosen because it had the highest head entry_id of the majority
that responded to the fencing requests first). But as the leader
receives more fencing responses from the remaining minority,
the new leader will be informed of these followers and it is
possible that their head entry_id is higher than the leader and
therefore need truncating.
----------------------------------------------------------*)
GetHighestEntryOfTerm(nstate, target_term) ==
IF \E entry \in nstate.log : entry.entry_id.term <= target_term
THEN CHOOSE entry \in nstate.log :
/\ entry.entry_id.term <= target_term
/\ \A e \in nstate.log :
\/ e.entry_id.term > target_term
\/ /\ e.entry_id.term <= target_term
/\ IsHigherOrEqualId(entry.entry_id, e.entry_id)
ELSE NoLogEntry
NeedsTruncation(nstate, head_entry_id) ==
\/ /\ head_entry_id.term = nstate.head_entry_id.term
/\ head_entry_id.offset > nstate.head_entry_id.offset
\/ head_entry_id.term # nstate.head_entry_id.term
GetCursor(nstate, head_entry_id) ==
IF NeedsTruncation(nstate, head_entry_id)
THEN [status |-> PENDING_TRUNCATE,
last_pushed |-> NoEntryId,
last_confirmed |-> NoEntryId]
ELSE [status |-> ATTACHED,
last_pushed |-> head_entry_id,
last_confirmed |-> head_entry_id]
GetCursors(nstate, follower_map) ==
[n \in Nodes |->
IF follower_map[n] # NIL
THEN GetCursor(nstate, follower_map[n])
ELSE NoCursor]
GetTruncateRequest(nstate, follower, target_term) ==
[type |-> TRUNCATE_REQUEST,
dest_node |-> follower,
source_node |-> nstate.id,
head_entry_id |-> GetHighestEntryOfTerm(nstate, target_term).entry_id,
term |-> nstate.term]
FollowersToTruncate(nstate, follower_map) ==
{ f \in DOMAIN follower_map :
/\ follower_map[f] # NIL
/\ NeedsTruncation(nstate, follower_map[f]) }
GetTruncateRequests(nstate, follower_map) ==
{
GetTruncateRequest(nstate, f, follower_map[f].term)
: f \in FollowersToTruncate(nstate, follower_map)
}
GetBecomeLeaderResponse(n, term, o) ==
[type |-> BECOME_LEADER_RESPONSE,
term |-> term,
node |-> n,
coordinator |-> o]
NodeHandlesBecomeLeaderRequest ==
\* enabling conditions
\E msg \in DOMAIN messages :
/\ ReceivableMessageOfType(messages, msg, BECOME_LEADER_REQUEST)
/\ node_state[msg.node].term = msg.term
/\ LET truncate_requests == GetTruncateRequests(node_state[msg.node], msg.follower_map)
leader_response == GetBecomeLeaderResponse(msg.node, msg.term, msg.coordinator)
updated_cursors == GetCursors(node_state[msg.node], msg.follower_map)
IN
\* state changes
/\ node_state' = [node_state EXCEPT ![msg.node] =
[@ EXCEPT !.status = LEADER,
!.leader = msg.node,
!.rep_factor = msg.rep_factor,
!.follow_cursor = updated_cursors]]
/\ ProcessedOneAndSendMore(msg, truncate_requests \union {leader_response})
/\ UNCHANGED << metadata, metadata_version, coordinator_state, confirmed, coordinator_stop_ctr >>
(*---------------------------------------------------------
Coordinator handles Become Leader response
The election is completed on receiving the Become Leader
response. The coordinator updates the metadata with the
new leader, the ensemble and that the shard is now back
in steady state.
The election is only able to complete if the metadata
hasn't been modified since the beginning of the election.
Any concurrent change will cause this election to fail.
Key points:
- A minority of followers may still not have been fenced yet.
The coordinator will continue to try to fence these followers
forever until either they respond with a fencing request,
or a new election is performed.
----------------------------------------------------------*)
CoordinatorHandlesBecomeLeaderResponse ==
\* enabling conditions
\E o \in Coordinators :
LET ostate == coordinator_state[o]
IN
/\ ostate.status = RUNNING
/\ ostate.md.shard_status = ELECTION
/\ \E msg \in DOMAIN messages :
/\ ReceivableMessageOfType(messages, msg, BECOME_LEADER_RESPONSE)
/\ msg.coordinator = o
/\ ostate.election_phase = NOTIFY_LEADER
/\ ostate.md.term = msg.term
/\ metadata_version = ostate.md_version
\* state changes
/\ LET new_md == [ostate.md EXCEPT !.shard_status = STEADY_STATE,
!.leader = msg.node,
!.rep_factor = Cardinality(metadata.ensemble)]
IN /\ coordinator_state' = [coordinator_state EXCEPT ![o].election_phase = LEADER_ELECTED,
![o].md_version = metadata_version + 1,
![o].md = new_md]
/\ metadata' = new_md
/\ metadata_version' = metadata_version + 1
/\ MessageProcessed(msg)
/\ UNCHANGED << node_state, confirmed, coordinator_stop_ctr >>
(*---------------------------------------------------------
Coordinator handles post quorum fence response
The coordinator handles a fencing response at a time after
it has selected a new leader. The leader must have confirmed
its leadership before the opertator acts on any late
follower fence responses.
Each fence response will translate to an Add Follower
request being sent to the leader, including the follower's
head entry_id.
----------------------------------------------------------*)
GetAddFollowerRequest(n, term, follower, head_entry_id) ==
[type |-> ADD_FOLLOWER_REQUEST,
node |-> n,
follower |-> follower,
head_entry_id |-> head_entry_id,
term |-> term]
CoordinatorHandlesPostQuorumFencingResponse ==
\* enabling conditions
\E o \in Coordinators :
LET ostate == coordinator_state[o]
IN
/\ ostate.status = RUNNING
/\ ostate.election_phase = LEADER_ELECTED
/\ \E msg \in DOMAIN messages :
/\ ReceivableMessageOfType(messages, msg, NEW_TERM_RESPONSE)
/\ msg.coordinator = o
/\ msg.node \in ostate.md.ensemble \* might be the old_node
/\ ostate.md.term = msg.term
\* state changes
/\ coordinator_state' = [coordinator_state EXCEPT ![o].election_fence_responses = @ \union {msg}]
/\ ProcessedOneAndSendAnother(msg,
GetAddFollowerRequest(ostate.election_leader,
ostate.md.term,
msg.node,
msg.head_entry_id))
/\ UNCHANGED << metadata, metadata_version, node_state, confirmed, coordinator_stop_ctr >>
(*---------------------------------------------------------
Leader handles an Add Follower request
The leader creates a cursor and will send a truncate
request to the follower if their log might need
truncating first.
----------------------------------------------------------*)
LeaderHandlesAddFollowerRequest ==
\* enabling conditions
\E msg \in DOMAIN messages :
/\ ReceivableMessageOfType(messages, msg, ADD_FOLLOWER_REQUEST)
/\ node_state[msg.node].term = msg.term
/\ node_state[msg.node].status = LEADER
/\ node_state[msg.node].follow_cursor[msg.follower].status = NIL
\* state changes
/\ node_state' = [node_state EXCEPT ![msg.node].follow_cursor[msg.follower] =
GetCursor(node_state[msg.node], msg.head_entry_id)]
/\ IF NeedsTruncation(node_state[msg.node], msg.head_entry_id)
THEN ProcessedOneAndSendAnother(msg,
GetTruncateRequest(node_state[msg.node],
msg.follower,
msg.head_entry_id.term))
ELSE MessageProcessed(msg)
/\ UNCHANGED << metadata, metadata_version, coordinator_state, confirmed, coordinator_stop_ctr >>
(*---------------------------------------------------------
Node handles a Truncate request
A node that receives a truncate request knows that it
has been selected as a follower. It truncates its log
to the indicates entry id, updates its term and changes
to a Follower.
----------------------------------------------------------*)
GetTruncateResponse(msg, head_entry_id) ==
[type |-> TRUNCATE_RESPONSE,
dest_node |-> msg.source_node,
source_node |-> msg.dest_node,
head_entry_id |-> head_entry_id,
term |-> msg.term]
TruncateLog(log, last_safe_entry_id) ==
{ entry \in log : IsLowerOrEqualId(entry.entry_id, last_safe_entry_id) }
NodeHandlesTruncateRequest ==
\* enabling conditions
\E msg \in DOMAIN messages :
/\ ReceivableMessageOfType(messages, msg, TRUNCATE_REQUEST)
/\ LET nstate == node_state[msg.dest_node]
truncated_log == TruncateLog(nstate.log, msg.head_entry_id)
head_entry == HeadEntry(truncated_log)
IN
/\ nstate.status = FENCED
/\ nstate.term = msg.term
\* state changes
/\ node_state' = [node_state EXCEPT ![msg.dest_node] =
[@ EXCEPT !.status = FOLLOWER,
!.term = msg.term,
!.leader = msg.source_node,
!.log = truncated_log,
!.head_entry_id = head_entry.entry_id,
!.follow_cursor = [n \in Nodes |-> NoCursor]]]
/\ ProcessedOneAndSendAnother(msg, GetTruncateResponse(msg, head_entry.entry_id))
/\ UNCHANGED << metadata, metadata_version, coordinator_state, confirmed, coordinator_stop_ctr >>
(*---------------------------------------------------------
Leader handles a truncate response.
The leader now activates the follow cursor as the follower
log is now ready for replication.
----------------------------------------------------------*)
LeaderHandlesTruncateResponse ==
\* enabling conditions
\E msg \in DOMAIN messages :
/\ ReceivableMessageOfType(messages, msg, TRUNCATE_RESPONSE)
/\ LET nstate == node_state[msg.dest_node]
IN
/\ nstate.status = LEADER
/\ nstate.term = msg.term
\* state changes
/\ node_state' = [node_state EXCEPT ![msg.dest_node].follow_cursor =
[@ EXCEPT ![msg.source_node] = [status |-> ATTACHED,
last_pushed |-> msg.head_entry_id,
last_confirmed |-> msg.head_entry_id]]]
/\ MessageProcessed(msg)
/\ UNCHANGED << metadata, metadata_version, coordinator_state, confirmed, coordinator_stop_ctr >>
(*---------------------------------------------------------
A client writes an entry to the leader
A client writes a value from Values to a leader node
if that value has not previously been written. The leader adds
the entry to its log, updates its head_entry_id.
----------------------------------------------------------*)
Write ==
\* enabling conditions
\E n \in Nodes, v \in Values :
LET nstate == node_state[n]
IN
/\ node_state[n].status = LEADER
/\ v \notin DOMAIN confirmed
\* state changes
/\ LET entry_id == [offset |-> nstate.head_entry_id.offset + 1,
term |-> nstate.term]
log_entry == [entry_id |-> entry_id,
value |-> v]
IN
/\ node_state' = [node_state EXCEPT ![n] =
[@ EXCEPT !.log = @ \union { log_entry },
!.head_entry_id = entry_id]]
/\ confirmed' = confirmed @@ (v :> FALSE)
/\ UNCHANGED << metadata, metadata_version, coordinator_state, metadata, messages, coordinator_stop_ctr >>
(*---------------------------------------------------------
A leader node sends entries to followers
The leader will send an entry to a follower when it has
entries in its log that is higher than the follow cursor
position of that follower. In this action, the leader
will send the next entry for all followers whose cursor is
lower then the leader's head entry_id.
This action chooses the largest subset of followers that
have an attached cursor and whose cursor is behind the head
of the leaders log. This is a state space reduction
strategy as if we can send multiple requests at the same
time we reduce the number of ways we send messages thus
reducing the state space.
----------------------------------------------------------*)
CanSendToFollower(lstate, follower) ==
/\ node_state[follower].status # NOT_MEMBER
/\ follower # lstate.id
/\ lstate.follow_cursor[follower].status = ATTACHED
/\ IsHigherId(lstate.head_entry_id, lstate.follow_cursor[follower].last_pushed)
\* does this group of followers include all followers that we can send to in this moment?
IncludesAllSendableFollowers(lstate, followers) ==
\* all followers in this group have their cursor behind the head of the leader log
/\ \A f \in followers : CanSendToFollower(lstate, f)
\* there isn't a follower who could be sent to, but is not in this group
/\ ~\E f \in Nodes :
/\ f # lstate.id
/\ f \notin followers
/\ CanSendToFollower(lstate, f)
\* Get the next lowest entry above the current follow cursor position
\* specifically, choose an entry that is higher than the last pushed
\* such that there is not another entry that is also higher than the
\* last pushed but lower than the chosen entry. Only one entry can
\* match that criteria.
NextEntry(lstate, last_entry_id) ==
CHOOSE e1 \in lstate.log :
/\ IsHigherId(e1.entry_id, last_entry_id)
/\ ~\E e2 \in lstate.log :
/\ IsLowerId(e2.entry_id, e1.entry_id)
/\ IsHigherId(e2.entry_id, last_entry_id)
GetAppendEntry(lstate, next_entries, follower) ==
[type |-> APPEND,
dest_node |-> follower,
source_node |-> lstate.id,
entry |-> next_entries[follower],
commit_entry_id |-> lstate.commit_entry_id,
term |-> lstate.term]
GetNextAppendEntries(lstate, next_entries, followers) ==
{ GetAppendEntry(lstate, next_entries, f) : f \in followers }
GetNextEntries(lstate, followers) ==
[f \in followers |-> NextEntry(lstate, lstate.follow_cursor[f].last_pushed)]
LeaderSendsEntriesToFollowers ==
\* enabling conditions
\E leader \in Nodes, followers \in SUBSET Nodes :
/\ followers # {}
/\ LET lstate == node_state[leader]
IN
/\ lstate.status = LEADER
/\ IncludesAllSendableFollowers(lstate, followers)
\* state changes
/\ LET next_entries == GetNextEntries(lstate, followers)
IN /\ node_state' = [node_state EXCEPT ![leader].follow_cursor =
[n \in Nodes |->
IF n \in followers
THEN [lstate.follow_cursor[n] EXCEPT !.last_pushed = next_entries[n].entry_id]
ELSE lstate.follow_cursor[n]]]
/\ SendMessages(GetNextAppendEntries(lstate, next_entries, followers))
/\ UNCHANGED << metadata, metadata_version, coordinator_state, metadata, confirmed, coordinator_stop_ctr >>
(*---------------------------------------------------------
A follower node confirms an entry to the leader
The follower adds the entry to its log, sets the head entry_id
and updates its commit entry_id with the commit entry_id of
the request.
----------------------------------------------------------*)
GetAddEntryOkResponse(msg, fstate, entry) ==
[type |-> ACK,
dest_node |-> msg.source_node,
source_node |-> fstate.id,
code |-> OK,
entry_id |-> entry.entry_id,
term |-> fstate.term]
FollowerConfirmsEntry ==
\* enabling conditions
\E msg \in DOMAIN messages :
/\ IsEarliestReceivableEntryMessage(messages, msg, APPEND)
/\ LET f == msg.dest_node
fstate == node_state[f]
IN
/\ fstate.status \in {FOLLOWER, FENCED}
/\ fstate.term <= msg.term \* reconfig could mean leader has higher term than follower
\* state changes
/\ node_state' = [node_state EXCEPT ![f].status = FOLLOWER,
![f].term = msg.term,
![f].leader = msg.source_node,
![f].log = @ \union { msg.entry },
![f].head_entry_id = msg.entry.entry_id,
![f].commit_entry_id = msg.commit_entry_id]
/\ ProcessedOneAndSendAnother(msg, GetAddEntryOkResponse(msg, fstate, msg.entry))
/\ UNCHANGED << metadata, metadata_version, coordinator_state, metadata, confirmed, coordinator_stop_ctr >>
(*---------------------------------------------------------
A follower node rejects an entry from the leader.
If the leader has a lower term than the follower then the
follower must reject it with an INVALID_TERM response.
Key points:
- The term of the response should be the term of the
request so that the leader will not ignore the response.
----------------------------------------------------------*)
GetAddEntryInvalidTermResponse(nstate, msg) ==
[type |-> ACK,
dest_node |-> msg.source_node,
source_node |-> nstate.id,
code |-> INVALID_TERM,
entry_id |-> msg.entry.entry_id,
term |-> msg.term]
FollowerRejectsEntry ==
\* enabling conditions
\E msg \in DOMAIN messages :
/\ IsEarliestReceivableEntryMessage(messages, msg, APPEND)
/\ LET nstate == node_state[msg.dest_node]
IN
/\ nstate.term > msg.term
\* state changes
/\ ProcessedOneAndSendAnother(msg, GetAddEntryInvalidTermResponse(nstate, msg))
/\ UNCHANGED << metadata, metadata_version, coordinator_state, metadata, node_state, confirmed, coordinator_stop_ctr >>
(*---------------------------------------------------------
A leader node handles an add entry response
The leader updates the follow cursor last_confirmed
entry id, it also may advance the commit entry_id.