Safety of Raft single-server membership changes

raft-single-server-changes-safety

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