Skip to content

Accept real node bootstrap in consensus replay #8733

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
cjen1-msft wants to merge 1 commit into from
Open

Accept real node bootstrap in consensus replay #8733

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions lean/consensus/Consensus/Replay/Reduction.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,13 +102,21 @@ private def emitObserve (event : Event) (rule : String) : Reduction Unit :=
private def emitObserveSends (event : Event) (sends : List NativeSend) : Reduction Unit :=
appendInstruction (.observeSends sends (event.origin "sends"))

/--
Genesis runs asynchronously after the first node becomes leader, so bare ticks may precede
it; the model starts after genesis, so they are not observed.
`replicate` flushes a genesis entry over the append entries size limit. The node has no peers
yet, so the flush sends nothing.
-/
private def ruleBootstrap : Reduction String := do
let head ← peek
-- consume
event head "become_leader"
many_ (event head "tick")
event head "replicate"
event head "replicate_entry"
event head "add_configuration"
optional_ (event head "batch_flush")
return head.node

private def readAppendContent (head : Event) (config : Option Event)
Expand Down
1 change: 1 addition & 0 deletions lean/consensus/replay/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ The Fluentd tag is `ccf.cft`; packet message names are unprefixed, for example `
## Replay contract

Every protocol event must match a named rule; bootstrap selects the initial singleton membership.
Bootstrap accepts bare ticks before genesis, which native code runs asynchronously after the first node becomes leader, and a flush of the genesis entry.
Rules group related protocol events and read action inputs from those events; only top-level alternatives backtrack.
Actions must be enabled by the model.
After bootstrap, each rule emits one read-only observation before its model actions, comparing the native group's entry snapshot with the current model state.
Expand Down
3 changes: 3 additions & 0 deletions lean/consensus/replay/fixtures/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ Replication failures follow a two-node history with a committed signature, membe
The [valid control](valid/replication.ndjson) continues through follower catch-up, acknowledgement and commit.
Its snapshot installation hooks directly follow the leader's `replicate` batch and include a bare tick, both of which replay must accept.
The [rejected replicate](valid/rejected-replicate.ndjson) control is a `replicate` call that CCF rejected at its first entry, so it traces no `replicate_entry` and appends nothing.
The [bootstrap](valid/bootstrap.ndjson) control starts like a real node: bare ticks before genesis, then a flush of the genesis entry.

| Fixture | Expected failure |
| ----------------------------------------------------------------------- | ------------------------------------------------------- |
Expand All @@ -21,6 +22,8 @@ The [rejected replicate](valid/rejected-replicate.ndjson) control is a `replicat
| [Retirement non-adjacent](invalid/retirement-nonadjacent.ndjson) | An event separates `replicate_entry` and its retirement |
| [Orphan retirement](invalid/retirement-orphan.ndjson) | Retirement without a `replicate_entry` |
| [Uncommitted snapshot](invalid/uncommitted-snapshot.ndjson) | Joiner initializes at an uncommitted signature |
| [Bootstrap event](invalid/bootstrap-event.ndjson) | Non-tick event before genesis |
| [Bootstrap flush send](invalid/bootstrap-flush-send.ndjson) | Send from the genesis flush, which must send nothing |

From `lean/consensus`, inspect a failure directly (exit status 1 is expected):

Expand Down
13 changes: 13 additions & 0 deletions lean/consensus/replay/fixtures/invalid/bootstrap-event.ndjson
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
{"msg":{"function":"become_leader","state":{"node_id":"0","current_view":2,"last_idx":0,"commit_idx":0,"leadership_state":"Leader"}}}
{"msg":{"function":"tick","state":{"node_id":"0","current_view":2,"last_idx":0,"commit_idx":0,"leadership_state":"Leader"}}}
{"msg":{"function":"become_follower","state":{"node_id":"0"}}}
{"msg":{"function":"tick","state":{"node_id":"0","current_view":2,"last_idx":0,"commit_idx":0,"leadership_state":"Leader"}}}
{"msg":{"function":"replicate","state":{"node_id":"0","current_view":2,"last_idx":0,"commit_idx":0,"leadership_state":"Leader"}}}
{"msg":{"function":"replicate_entry","state":{"node_id":"0","current_view":2,"last_idx":0,"commit_idx":0,"leadership_state":"Leader"},"seqno":1,"globally_committable":false}}
{"msg":{"function":"add_configuration","state":{"node_id":"0"},"idx":1,"nodes":{"0":{}}}}
{"msg":{"function":"batch_flush","state":{"node_id":"0","current_view":2,"last_idx":1,"commit_idx":0,"leadership_state":"Leader"}}}
{"msg":{"function":"tick","state":{"node_id":"0","current_view":2,"last_idx":1,"commit_idx":0,"leadership_state":"Leader"}}}
{"msg":{"function":"replicate","state":{"node_id":"0","current_view":2,"last_idx":1,"commit_idx":0,"leadership_state":"Leader"}}}
{"msg":{"function":"replicate_entry","state":{"node_id":"0","current_view":2,"last_idx":1,"commit_idx":0,"leadership_state":"Leader"},"seqno":2,"globally_committable":true}}
{"msg":{"function":"commit","state":{"node_id":"0"},"idx":2}}
{"msg":{"function":"tick","state":{"node_id":"0","current_view":2,"last_idx":2,"commit_idx":2,"leadership_state":"Leader"}}}
30 changes: 30 additions & 0 deletions lean/consensus/replay/fixtures/invalid/bootstrap-flush-send.ndjson
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
{"msg":{"function":"become_leader","state":{"node_id":"0"}}}
{"msg":{"function":"replicate","state":{"node_id":"0"}}}
{"msg":{"function":"replicate_entry","state":{"node_id":"0"},"globally_committable":false}}
{"msg":{"function":"add_configuration","state":{"node_id":"0"},"nodes":{"0":{}}}}
{"msg":{"function":"batch_flush","state":{"node_id":"0"}}}
{"msg":{"function":"send_append_entries","state":{"node_id":"0"},"to_node_id":"1","packet":{"msg":"append_entries","term":2,"prev_idx":0,"prev_term":0,"idx":1,"leader_commit_idx":0,"term_of_idx":2,"contains_new_view":false}}}
{"msg":{"function":"replicate","state":{"node_id":"0","current_view":2,"last_idx":1,"commit_idx":0,"leadership_state":"Leader"}}}
{"msg":{"function":"replicate_entry","state":{"node_id":"0","current_view":2,"last_idx":1,"commit_idx":0,"leadership_state":"Leader"},"seqno":2,"globally_committable":true}}
{"msg":{"function":"commit","state":{"node_id":"0"},"idx":2}}
{"msg":{"cmd":"trust_nodes,2,1"}}
{"msg":{"function":"replicate","state":{"node_id":"0","current_view":2,"last_idx":2,"commit_idx":2,"leadership_state":"Leader"}}}
{"msg":{"function":"replicate_entry","state":{"node_id":"0","current_view":2,"last_idx":2,"commit_idx":2,"leadership_state":"Leader"},"seqno":3,"globally_committable":false}}
{"msg":{"function":"add_configuration","state":{"node_id":"0"},"idx":3,"nodes":{"0":{},"1":{}}}}
{"msg":{"function":"send_append_entries","state":{"node_id":"0"},"to_node_id":"1","packet":{"msg":"append_entries","term":2,"prev_idx":2,"prev_term":2,"idx":2,"leader_commit_idx":2,"term_of_idx":2,"contains_new_view":false}}}
{"msg":{"function":"replicate","state":{"node_id":"0","current_view":2,"last_idx":3,"commit_idx":2,"leadership_state":"Leader"}}}
{"msg":{"function":"replicate_entry","state":{"node_id":"0","current_view":2,"last_idx":3,"commit_idx":2,"leadership_state":"Leader"},"seqno":4,"globally_committable":true}}
{"msg":{"function":"add_configuration","state":{"node_id":"1"},"idx":2,"nodes":{"0":{}}}}
{"msg":{"function":"tick","state":{"node_id":"1","current_view":0,"last_idx":0,"commit_idx":0,"leadership_state":"None"}}}
{"msg":{"function":"init_as_backup","state":{"node_id":"1","current_view":0,"last_idx":0,"commit_idx":0,"leadership_state":"None"},"seqno":2,"view":2}}
{"msg":{"function":"become_follower","state":{"node_id":"1"}}}
{"msg":{"function":"recv_append_entries","state":{"node_id":"1","current_view":2,"last_idx":2,"commit_idx":2,"leadership_state":"Follower"},"from_node_id":"0","packet":{"msg":"append_entries","term":2,"prev_idx":2,"prev_term":2,"idx":2,"leader_commit_idx":2,"term_of_idx":2,"contains_new_view":false}}}
{"msg":{"function":"send_append_entries_response","state":{"node_id":"1"},"to_node_id":"0","packet":{"msg":"append_entries_response","term":2,"success":"OK","last_log_idx":2}}}
{"msg":{"function":"recv_append_entries_response","state":{"node_id":"0","current_view":2,"last_idx":4,"commit_idx":2,"leadership_state":"Leader"},"from_node_id":"1","packet":{"msg":"append_entries_response","term":2,"success":"OK","last_log_idx":2}}}
{"msg":{"function":"tick","state":{"node_id":"0","current_view":2,"last_idx":4,"commit_idx":2,"leadership_state":"Leader"}}}
{"msg":{"function":"send_append_entries","state":{"node_id":"0"},"to_node_id":"1","packet":{"msg":"append_entries","term":2,"prev_idx":2,"prev_term":2,"idx":4,"leader_commit_idx":2,"term_of_idx":2,"contains_new_view":false}}}
{"msg":{"function":"recv_append_entries","state":{"node_id":"1","current_view":2,"last_idx":2,"commit_idx":2,"leadership_state":"Follower"},"from_node_id":"0","packet":{"msg":"append_entries","term":2,"prev_idx":2,"prev_term":2,"idx":4,"leader_commit_idx":2,"term_of_idx":2,"contains_new_view":false}}}
{"msg":{"function":"add_configuration","state":{"node_id":"1"},"idx":3,"nodes":{"0":{},"1":{}}}}
{"msg":{"function":"send_append_entries_response","state":{"node_id":"1"},"to_node_id":"0","packet":{"msg":"append_entries_response","term":2,"success":"OK","last_log_idx":4}}}
{"msg":{"function":"recv_append_entries_response","state":{"node_id":"0","current_view":2,"last_idx":4,"commit_idx":2,"leadership_state":"Leader"},"from_node_id":"1","packet":{"msg":"append_entries_response","term":2,"success":"OK","last_log_idx":4}}}
{"msg":{"function":"commit","state":{"node_id":"0"},"idx":4}}
12 changes: 12 additions & 0 deletions lean/consensus/replay/fixtures/valid/bootstrap.ndjson
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
{"msg":{"function":"become_leader","state":{"node_id":"0","current_view":2,"last_idx":0,"commit_idx":0,"leadership_state":"Leader"}}}
{"msg":{"function":"tick","state":{"node_id":"0","current_view":2,"last_idx":0,"commit_idx":0,"leadership_state":"Leader"}}}
{"msg":{"function":"tick","state":{"node_id":"0","current_view":2,"last_idx":0,"commit_idx":0,"leadership_state":"Leader"}}}
{"msg":{"function":"replicate","state":{"node_id":"0","current_view":2,"last_idx":0,"commit_idx":0,"leadership_state":"Leader"}}}
{"msg":{"function":"replicate_entry","state":{"node_id":"0","current_view":2,"last_idx":0,"commit_idx":0,"leadership_state":"Leader"},"seqno":1,"globally_committable":false}}
{"msg":{"function":"add_configuration","state":{"node_id":"0"},"idx":1,"nodes":{"0":{}}}}
{"msg":{"function":"batch_flush","state":{"node_id":"0","current_view":2,"last_idx":1,"commit_idx":0,"leadership_state":"Leader"}}}
{"msg":{"function":"tick","state":{"node_id":"0","current_view":2,"last_idx":1,"commit_idx":0,"leadership_state":"Leader"}}}
{"msg":{"function":"replicate","state":{"node_id":"0","current_view":2,"last_idx":1,"commit_idx":0,"leadership_state":"Leader"}}}
{"msg":{"function":"replicate_entry","state":{"node_id":"0","current_view":2,"last_idx":1,"commit_idx":0,"leadership_state":"Leader"},"seqno":2,"globally_committable":true}}
{"msg":{"function":"commit","state":{"node_id":"0"},"idx":2}}
{"msg":{"function":"tick","state":{"node_id":"0","current_view":2,"last_idx":2,"commit_idx":2,"leadership_state":"Leader"}}}