Skip to content

Instantly share code, notes, and snippets.

@ongardie
Last active July 6, 2023 01:42
Show Gist options
  • Save ongardie/a11f32b70581e20d6bcd to your computer and use it in GitHub Desktop.
Save ongardie/a11f32b70581e20d6bcd to your computer and use it in GitHub Desktop.
Safety of Raft single-server membership changes
This is an attempt to show that Raft's safety is
preserved with single-server membership changes as
described in the dissertation plus the patch that a
leader may not append a new configuration entry to
its log until it's committed an entry from its
current term.
This extends the safety argument in the
paper/dissertation. The only part that's different
(as far as I can tell) for membership changes is Step
2, which claims the existence of "the voter". The
voter is the server that is part of the quorum that
commits the entry in term T and the quorum that votes
for the leader of term U. With a static
configuration, it's easy to see the voter must exist
(overlap of two majorities of the same set). With
membership changes, it's more difficult; this aims to
show it for the dissertation algorithm patched with
the solution described above.
leaderT replicated entry E on majority of CT (its configuration)
leaderU received votes from majority of its config
Show that there exists a voter (there is overlap between these two)
CP, the parent of CT, was committed in term <= T for CT to exist
Then LeaderU has CP
Either LeaderU was elected by CP (parent of CT), CT, CC (child of CT), child+ of CC, CS (child of CP), or child+ of CS.
(I recommend drawing a tree of the above statement.)
Case LeaderU elected by CP (parent of CT):
Q(CP) int Q(CT) nonempty
Done (same as dissertation)
Case LeaderU elected by CT:
Q(CT) int Q(CT) nonempty
Done (same as dissertation)
Case LeaderU elected by CC (child of CT):
Q(CC) int Q(CT) nonempty
Done (same as dissertation)
Case LeaderU elected by child+ of CC:
CC was committed since its child exists
Either CC appears before E in the logs or CC appears after E or neither
Case CC before E:
Then E would have been committed to CC, not to CT
Contradiction
Case CC after E:
Then any log with CC also has E
Contradiction
Case CC and E do not appear in same log:
Then leader to create CC did not have E
Leader to create CC has CT from term T
Leader to create CC missing other term T entry
Then leader to create CC has term > T
Contradiction
Done (same as dissertation)
Case LeaderU elected by CS (child of CP, sibling of CT):
Either term(CT) < term(CS) or term(CT) > term(CS)
Case term(CT) < term(CS):
term(CP) <= term(CT) < term(CS) < T < U
Leader CS committed some entry XA to CP (since it subsequently created CS)
XA is present in T's log by assumption
XA must come after CT in T's log, since term of XA > term of CT
But CS branched from CP, not from CT
Contradiction
Case term(CS) < term(CT):
term(CP) <= term(CS) < term(CT) <= T < U
Leader CT committed some entry XT to CP (since it subsequently created CT)
XT must be present in U's log by assumption
XT must come after CS entry in U's log, since term of XT > term of CS
But CT branched from CP, not from CS
Contradiction
Done (different from dissertation)
Case LeaderU elected by child+ of CS:
CS was committed since its child exists
Either CS committed in term < T or CS committed in term > T
Case CS committed in term < T:
LeaderT must have had CS entry
Then it could not have created CT branching from CP
Contradiction
Case CS committed in term > T:
The leader that committed the CS entry should have had E (by assumption)
Then LeaderU would also have E
Contradiction
Done (same as dissertation)
QED
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment