TLA+ spec does not model a retiring Follower

[lemmy]

The TLA+ spec misses to model the transition described in raft.h; the TLA+ action AdvanceCommitIndex is only enabled for the leader, but raft::add_configuration allows a follower to retire.

nodes,0,1,2
connect,0,1
connect,0,2
connect,2,1

periodic_one,0,110
dispatch_all

assert_is_primary,0
assert_is_backup,1
assert_is_backup,2

state_all

replicate_new_configuration,1,0,1 # New configuration: [0, 1] in term 1, 2 is expected to retire.

periodic_all,10
dispatch_all

assert_is_primary,0
assert_is_backup,1
assert_is_retired,2

state_all

sequenceDiagram
  n[0]-->n[1]: connect
  n[0]-->n[2]: connect
  n[2]-->n[1]: connect
  n[0]->>n[0]: periodic for 110 ms
  n[0]->>n[2]: request_vote for term 1, at tx 0.0
  n[2]->>n[2]: [KV] rolling back to 0.0, in term 1
  n[2]->>n[2]: [ledger] truncating to 0
  n[0]->>n[1]: request_vote for term 1, at tx 0.0
  n[1]->>n[1]: [KV] rolling back to 0.0, in term 1
  n[1]->>n[1]: [ledger] truncating to 0
  n[1]-->>n[0]: request_vote_response for term 1 = Y
  n[0]->>n[0]: [KV] initialising in term 1
  n[2]-->>n[0]: request_vote_response for term 1 = Y
  n[0]->>n[2]: append_entries (0.0, 0.0] (term 1, commit 0)
  n[0]->>n[1]: append_entries (0.0, 0.0] (term 1, commit 0)
  n[1]-->>n[0]: append_entries_response ACK for 1.0
  n[2]-->>n[0]: append_entries_response ACK for 1.0
  Note right of n[0]: leadership P membership A @1.0 (committed 0)
  Note right of n[1]: leadership F membership A @1.0 (committed 0)
  Note right of n[2]: leadership F membership A @1.0 (committed 0)
  n[0]->>n[0]: replicate 1.1 = [0 bytes]  [reconfiguration]
  n[0]->>n[0]: [ledger] appending: 1.1=[92 bytes] {"data":"eyIwIj
  n[0]->>n[0]: periodic for 10 ms
  n[1]->>n[1]: periodic for 10 ms
  n[2]->>n[2]: periodic for 10 ms
  n[0]->>n[2]: append_entries (0.0, 1.1] (term 1, commit 0)
  n[2]->>n[2]: [ledger] appending: 1.1=[92 bytes] {"data":"eyIwIj
  n[0]->>n[1]: append_entries (0.0, 1.1] (term 1, commit 0)
  n[1]->>n[1]: [ledger] appending: 1.1=[92 bytes] {"data":"eyIwIj
  n[1]-->>n[0]: append_entries_response ACK for 1.1
  n[0]->>n[0]: [KV] compacting to 1
  n[2]-->>n[0]: append_entries_response ACK for 1.1
  Note right of n[0]: leadership P membership A @1.1 (committed 1)
  Note right of n[1]: leadership F membership A @1.1 (committed 0)
  Note right of n[2]: leadership F membership R @1.1 (committed 0)

Loading

Test output requires: #4811

Originally posted by @lemmy in #4582 (comment)

[lemmy]

There is more to this than what I thought; the retirement of a follower in raft.h has two stages (retiring and retired).

[achamayou]

@lemmy yes, this is described under https://microsoft.github.io/CCF/main/architecture/consensus/1tx-reconfig.html#retirement-details

Another subtlety is that it's not safe to shut down a node, even after their retirement is committed, as highlighted in #1713, and solved in #4008. So after a primary has observed that a node's retirement is committed, another KV write takes place to set a "retired_committed" flag on that node.

It's only when the write that sets this flag is committed itself that the node can safely be removed, because any eligible primary at that point would "know" that this node's retirement is committed, and that none of the transactions this new eligible primary needs to commit can include this node in their quorum.

A REMOVED state could have been added, but for implementation and ease of upgrade reasons, a flag was used instead.

[achamayou]

Resolved by #5919.