From 6924b71dd89b45f7eacf45159477826450eb627d Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Wed, 11 Oct 2023 16:04:35 +0200 Subject: [PATCH 01/13] consensus: draft of state machine for algorithm --- consensus/protocol-state-machine.md | 158 ++++++++++++++++++++++++++++ 1 file changed, 158 insertions(+) create mode 100644 consensus/protocol-state-machine.md diff --git a/consensus/protocol-state-machine.md b/consensus/protocol-state-machine.md new file mode 100644 index 0000000..72d2e39 --- /dev/null +++ b/consensus/protocol-state-machine.md @@ -0,0 +1,158 @@ +# Consensus protocol: state-machine + +The consensus protocol consists of a sequence of **heights**, +identified by natural numbers `h`. + +Each height of consensus consists of a number of **rounds**, +identified by natural numbers `r`. + +Each round consists of essentially three **round steps**: +`propose`, `prevote`, and `precommit`. + +## Height state-machine + +Proposed states for the state machine for each height `h`: + +- Unstarted: + - Initial state + - Can be used to store messages for unstarted height `h` + - In the algorithm when `hp < h` and `decisionp[h] == nil` +- Started + - Actual consensus execution + - In the algorithm when `hp == h` and `decisionp[h] == nil` +- Decided: + - Final state + - May also include the commit/execution of decided value + - In the algorithm when `hp >= h` and `decisionp[h] != nil` + + +### Transition: `Unstarted` -> `Started` + +``` +10: upon start do StartRound(0) + +54: StartRound(0) +``` + +The node has started this height `h == hp`. +This transaction should initialize the consensus variables. + +### Transition: `Started` -> `Decided` + +``` +49: upon ⟨PROPOSAL, hp, r, v, ∗⟩ from proposer(hp, r) AND 2f + 1 ⟨PRECOMMIT, hp, r, id(v)⟩ while decisionp[hp] = nil do +``` + +The height of consensus is decided. +The node is ready to move to the next height. + +## Current height state machine + +The state machine for the `Started` state of a height `h`, which is the current's node height `hp`: + +- NewHeight + - Initial state +- Round `r`, with `r` being a natural number + +### Transition `NewHeight` -> `Round(0)` + +``` +52: hp ← hp+1 +53: reset lockedRoundp , lockedV aluep , validRoundp and validV aluep to initial values and empty message log +54: StartRound(0) +``` + +### Transition `Round(r)` -> `Round(r+1)`: failed round + +The current round of the node `roundp` has not succeeded, +so that it starts the next round `roundp + 1`: + +``` +65: Function OnTimeoutPrecommit(height, round): +66: if height = hp ∧ round = roundp then +67: StartRound(roundp + 1) +``` + +### Transition `Round(r)` -> `Round(r')`: round skipping + +The node receives a number of messages from a future round `round > roundp`, +so that it skips to that round: + +``` +55: upon f + 1 ⟨∗, hp, round, ∗, ∗⟩ with round > roundp do +56: StartRound(round) +``` + +> This is not really implemented like that: +> - We require 2f+1 PREVOTEs or PRECOMMITs, instead of f+1 messages +> - We only skip to the next round `roundp + 1` + +## Round state-machine + +Proposed states for the state machine for each rond `r` of a height `h`: + +- Unstarted + - Initial state + - Can be used to store messages early receives for this round + - In the algorithm when `roundp < r` or `hp < h` +- Started + - Actual consensus single-round execution + - In the algorithm when `roundp == r` +- Concluded + - State must be preserved while `hp == h` + - In the algorithm when `roundp > r` or `hp > h` + +Those states are part of the `Started` state of `Round(r)`. + +## Current Round state-machine + +Proposed states for the state machine for the current round `roundp` of the current height `hp`: + +- NewRound +- Propose +- Prevote +- Precommit + +### Transition `NewRound` -> `Propose` + +If the node is the round's proposer, it broadcasts a `PROPOSAL` message. + +``` +14: if proposer(hp, roundp) = p then +(...) +19: broadcast ⟨PROPOSAL, hp, roundp, proposal, validRoundp⟩ +20: else +21: schedule OnTimeoutPropose(hp,roundp) to be executed after timeoutPropose(roundp) +``` + +### Transition `Propose` -> `Prevote` + +The node broadcasts a `PREVOTE` vote message for the current round. +If the `PROPOSAL` for the round is properly received, possibly accompanied by a +quorum of associated `PREVOTE` votes, it is valid and it can be accepted by the +node, it votes for the proposed value ID. +Otherwise, it votes for `nil`: + +``` +22: upon ⟨PROPOSAL, hp, roundp, v, −1⟩ from proposer(hp, roundp) while stepp = propose do + +28: upon ⟨PROPOSAL, hp, roundp, v, vr⟩ from proposer(hp, roundp) AND 2f + 1 ⟨PREVOTE, hp, vr, id(v)⟩ while stepp = propose∧(vr ≥ 0∧vr < roundp) do + +57: Function OnTimeoutPropose(height, round): +58: if height = hp ∧ round = roundp ∧ stepp = propose +``` + +### Transition `prevote` -> `precommit` + +The node broadcasts a `PRECOMMIT` vote message for the current round. +If the `PROPOSAL` for the round is received, accompanied by a quorum of +associated `PREVOTE` votes for the current round, +the node votes for the proposed value. +Otherwise, it votes for `nil`. + +``` +36: upon ⟨PROPOSAL, hp, roundp, v, ∗⟩ from proposer(hp, roundp) AND 2f + 1 ⟨PREVOTE, hp, roundp, id(v)⟩ while valid(v) ∧ stepp ≥ prevote for the first time do + +61: Function OnTimeoutPrevote(height, round) : +62: if height = hp ∧ round = roundp ∧ stepp = prevote then +``` From 1008e09baca381864fd2e07a628317fd077f352a Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Fri, 13 Oct 2023 14:23:39 +0200 Subject: [PATCH 02/13] consensus: SM simplified with transitions table --- consensus/protocol-state-machine.md | 128 +++++++++++----------------- 1 file changed, 48 insertions(+), 80 deletions(-) diff --git a/consensus/protocol-state-machine.md b/consensus/protocol-state-machine.md index 72d2e39..cd2b9cc 100644 --- a/consensus/protocol-state-machine.md +++ b/consensus/protocol-state-machine.md @@ -9,7 +9,9 @@ identified by natural numbers `r`. Each round consists of essentially three **round steps**: `propose`, `prevote`, and `precommit`. -## Height state-machine + + +## Height state machine + +State machine `Height(r)` representing the operation of a height `h` of consensus. -The state machine for the `Started` state of a height `h`, which is the current's node height `hp`: +The considered set of states are: - NewHeight - Initial state - Round `r`, with `r` being a natural number -### Transition `NewHeight` -> `Round(0)` - -``` -52: hp ← hp+1 -53: reset lockedRoundp , lockedV aluep , validRoundp and validV aluep to initial values and empty message log -54: StartRound(0) -``` - -### Transition `Round(r)` -> `Round(r+1)`: failed round - -The current round of the node `roundp` has not succeeded, -so that it starts the next round `roundp + 1`: - -``` -65: Function OnTimeoutPrecommit(height, round): -66: if height = hp ∧ round = roundp then -67: StartRound(roundp + 1) -``` - -### Transition `Round(r)` -> `Round(r')`: round skipping +The table below summarizes the state transitions between the multiple `Round(r)` state machines. +The `Ref` column refers to the line of the pseudo-code where the events can be found. -The node receives a number of messages from a future round `round > roundp`, -so that it skips to that round: +| State | NextState | Condition | Action | Ref | +|-------|-----------|-----------|--------|-----| +| NewHeight | Round(0) | | | L10, L54 | +| Round(r) | Decided | `⟨PROPOSAL, h, r, v, *⟩` and `2f + 1 ⟨PRECOMMIT, h, r, id(v)⟩` | decide `v` | L49 | +| Round(r) | Round(r) | `2f + 1 ⟨PRECOMMIT, h, r, *⟩` for the first time | schedule `TimeoutPrecommit(h, r)` | L47 | +| Round(r) | Round(r+1) | `TimeoutPrecommit(h, r)` | failed round | L65 | +| Round(r) | Round(r') | `2f + 1 ⟨PREVOTE, h, r', *, *⟩` with `r' > r` | round skipping | L55 | +| Round(r) | Round(r') | `2f + 1 ⟨PRECOMMIT, h, r', *, *⟩` with `r' > r` | round skipping | L55 | -``` -55: upon f + 1 ⟨∗, hp, round, ∗, ∗⟩ with round > roundp do -56: StartRound(round) -``` + -### Transition `NewRound` -> `Propose` - -If the node is the round's proposer, it broadcasts a `PROPOSAL` message. - -``` -14: if proposer(hp, roundp) = p then -(...) -19: broadcast ⟨PROPOSAL, hp, roundp, proposal, validRoundp⟩ -20: else -21: schedule OnTimeoutPropose(hp,roundp) to be executed after timeoutPropose(roundp) -``` - -### Transition `Propose` -> `Prevote` - -The node broadcasts a `PREVOTE` vote message for the current round. -If the `PROPOSAL` for the round is properly received, possibly accompanied by a -quorum of associated `PREVOTE` votes, it is valid and it can be accepted by the -node, it votes for the proposed value ID. -Otherwise, it votes for `nil`: - -``` -22: upon ⟨PROPOSAL, hp, roundp, v, −1⟩ from proposer(hp, roundp) while stepp = propose do - -28: upon ⟨PROPOSAL, hp, roundp, v, vr⟩ from proposer(hp, roundp) AND 2f + 1 ⟨PREVOTE, hp, vr, id(v)⟩ while stepp = propose∧(vr ≥ 0∧vr < roundp) do - -57: Function OnTimeoutPropose(height, round): -58: if height = hp ∧ round = roundp ∧ stepp = propose -``` - -### Transition `prevote` -> `precommit` - -The node broadcasts a `PRECOMMIT` vote message for the current round. -If the `PROPOSAL` for the round is received, accompanied by a quorum of -associated `PREVOTE` votes for the current round, -the node votes for the proposed value. -Otherwise, it votes for `nil`. - -``` -36: upon ⟨PROPOSAL, hp, roundp, v, ∗⟩ from proposer(hp, roundp) AND 2f + 1 ⟨PREVOTE, hp, roundp, id(v)⟩ while valid(v) ∧ stepp ≥ prevote for the first time do +## Round state-machine -61: Function OnTimeoutPrevote(height, round) : -62: if height = hp ∧ round = roundp ∧ stepp = prevote then -``` +State machine `Round(r)` representing the operation of a round `r` of consensus from height `h`. + +The considered set of states are: + +- `newRound` (not represented in the pseudo-code) +- `propose` +- `prevote` +- `precommit` + +The table below summarizes the state transitions within `Round(r)`. +The `Ref` column refers to the line of the pseudo-code where the events can be found. + +| State | NextState | Condition | Action | Ref | +|-------|-----------|-----------|--------|-----| +| newRound | propose | `proposer(h, r) = p` | broadcast `⟨PROPOSAL, h, r, proposal, validRound⟩` | L19 | +| newRound | propose | `proposer(h, r) != p` (optional) | schedule `TimeoutPropose(h, r)` | L21 | +| propose | prevote | `⟨PROPOSAL, h, r, v, −1⟩` | broadcast `⟨PREVOTE, h, r, {id(v), nil}⟩` | L22 | +| propose | prevote | `⟨PROPOSAL, h, r, v, vr⟩` and `2f + 1 ⟨PREVOTE, h, vr, id(v)⟩` | broadcast `⟨PREVOTE, h, r, {id(v), nil}⟩` | L28 | +| propose | prevote | `TimeoutPropose(h, r)` | broadcast `⟨PREVOTE, h, r, nil⟩` | L57 | +| prevote | prevote | `2f + 1 ⟨PREVOTE, h, r, *⟩` for the first time | schedule `TimeoutPrevote(h, r)⟩` | L34 | +| prevote | precommit | `⟨PROPOSAL, h, r, v, ∗⟩` and `2f + 1 ⟨PREVOTE, h, r, id(v)⟩` for the first time | broadcast `⟨PRECOMMIT, h, r, id(v)⟩`
update `lockedValue, lockedRound, validValue, validRound` | L36 | +| prevote | precommit | `2f + 1 ⟨PREVOTE, h, r, nil⟩` | broadcast `⟨PRECOMMIT, h, r, nil⟩` | L44 | +| prevote | precommit | `TimeoutPrevote(h, r)` | broadcast `⟨PRECOMMIT, h, r, nil⟩` | L61 | +| precommit | precommit | `⟨PROPOSAL, h, r, v, ∗⟩` and `2f + 1 ⟨PREVOTE, h, r, id(v)⟩` for the first time | update `validValue, validRound` | L36 | From 6b951d1196f6233a3fae0fcf5ecf3b0a12a2d1a5 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Fri, 13 Oct 2023 16:46:37 +0200 Subject: [PATCH 03/13] consensus: more detailed state machine --- consensus/protocol-state-machine.md | 63 +++++++++++++++++------------ 1 file changed, 38 insertions(+), 25 deletions(-) diff --git a/consensus/protocol-state-machine.md b/consensus/protocol-state-machine.md index cd2b9cc..e3e5762 100644 --- a/consensus/protocol-state-machine.md +++ b/consensus/protocol-state-machine.md @@ -52,25 +52,23 @@ The node is ready to move to the next height. ## Height state machine -State machine `Height(r)` representing the operation of a height `h` of consensus. +State machine `Height(h)` representing the operation of a height `h` of consensus. The considered set of states are: -- NewHeight - - Initial state -- Round `r`, with `r` being a natural number +- Unstarted +- Round(r), where `r` is a natural number +- Decided -The table below summarizes the state transitions between the multiple `Round(r)` state machines. +The table below summarizes the state transitions in the `Height(h)` state machine. The `Ref` column refers to the line of the pseudo-code where the events can be found. -| State | NextState | Condition | Action | Ref | +| From | To | Event | Action | Ref | |-------|-----------|-----------|--------|-----| -| NewHeight | Round(0) | | | L10, L54 | -| Round(r) | Decided | `⟨PROPOSAL, h, r, v, *⟩` and `2f + 1 ⟨PRECOMMIT, h, r, id(v)⟩` | decide `v` | L49 | -| Round(r) | Round(r) | `2f + 1 ⟨PRECOMMIT, h, r, *⟩` for the first time | schedule `TimeoutPrecommit(h, r)` | L47 | -| Round(r) | Round(r+1) | `TimeoutPrecommit(h, r)` | failed round | L65 | -| Round(r) | Round(r') | `2f + 1 ⟨PREVOTE, h, r', *, *⟩` with `r' > r` | round skipping | L55 | -| Round(r) | Round(r') | `2f + 1 ⟨PRECOMMIT, h, r', *, *⟩` with `r' > r` | round skipping | L55 | +| Unstarted | Round(0) | `start` | send `start` to `Round(0)` | L10, L54 | +| Round(r) | Decided | `decide(v)` | send `start` to `Height(h+1)` | L49 | +| Round(r) | Round(r+1) | `next_round(r+1)` | send `start` to `Round(r+1)` | L65 | +| Round(r) | Round(r') | `next_round(r')` | send `start` to `Round(r')` | L55 | - - -## Height state machine - -State machine `Height(h)` representing the operation of a height `h` of consensus. - -The considered set of states are: - -- Unstarted -- Round(r), where `r` is a natural number -- Decided - -The table below summarizes the state transitions in the `Height(h)` state machine. +The table below summarizes the major state transitions in the `Height(h)` state machine. The `Ref` column refers to the line of the pseudo-code where the events can be found. | From | To | Event | Action | Ref | |-------|-----------|-----------|--------|-----| -| Unstarted | Round(0) | `start` | send `start` to `Round(0)` | L10, L54 | -| Round(r) | Decided | `decide(v)` | send `kill` to every `Round(r)`
send `start` to `Height(h+1)` | L49 | -| Round(r) | Round(r+1) | `next_round(r+1)` | send `start` to `Round(r+1)` | L65 | -| Round(r) | Round(r') | `next_round(r')` | send `start` to `Round(r')` | L55 | +| Unstarted | InProgress | `start_height` | send `start` to `Round(0)` | L10, L54 | +| InProgress | Decided | `decide(r, v)` | emit `decide(h, v)`
stop to every `Round(r)` | L49 | A height `h` consists of multiple rounds of consensus, always starting from round `0`. -The `Unstarted` state is intented to store events and messages regarding height `h` +The `Unstarted` state is intended to store events and messages regarding height `h` before its execution is actually started. -Each round `r` of consensus is represented by a state machine `Round(r)`. -There is a single round _in progress_ at a time, which is always the last -`Round(r)` state machine to receive the `start` command. - The height is concluded when a decision is reached in _any_ of its rounds. -The `Decided` state is intented to represent that a decision has been reached, +The `Decided` state is intended to represent that a decision has been reached, while it also allows storing the summary of a decided height. Once the node moves to the `Decided` state of a height, the operation of @@ -88,6 +58,21 @@ _every_ round `Round(r)` should be concluded. The representation of this transition needs to be improved, for now it is considered that the corresponding `Round(r)` state machines are killed. +### InProgress height + +The table below represents transitions within the `InProgress` state, +representing the events that lead a node to start new round of consensus: + +| From | To | Event | Action | Ref | +|-------|-----------|-----------|--------|-----| +| Round(r) | Round(r+1) | `next_round(r+1)` | send `start` to `Round(r+1)` | L65 | +| Round(r) | Round(r') | `next_round(r')` | send `start` to `Round(r')` | L55 | + +Each round `r` of consensus is represented by a state machine `Round(r)`. +There is a single round _in progress_ at a time, which is always the last +`Round(r)` state machine to receive the `start` command. + + A round `r` may not succeed on reaching a decision. In this case, the successive round `r+1` is started. The uncessful `Round(r)` state machine is not killed at this point, as messages From ce6172d22fc2a00330127ca668ec8e4eb1aa937a Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Wed, 18 Oct 2023 09:23:10 +0200 Subject: [PATCH 07/13] consensus: updated description for the round SM --- consensus/protocol-state-machine.md | 68 +++++++++++++++-------------- 1 file changed, 36 insertions(+), 32 deletions(-) diff --git a/consensus/protocol-state-machine.md b/consensus/protocol-state-machine.md index 1699559..e410565 100644 --- a/consensus/protocol-state-machine.md +++ b/consensus/protocol-state-machine.md @@ -26,7 +26,7 @@ The considered set of states are: - Unstarted - Initial state - Can be used to store messages for unstarted height `h` - - In the algorithm when `hp < h` and `decisionp[h] == nil` + - In the algorithm when `hp < h`, where `hp` is the node's current round, and `decisionp[h] == nil` - InProgress: - Actual consensus execution - In the algorithm when `hp == h` and `decisionp[h] == nil` @@ -83,47 +83,47 @@ future round `r' > r`. When this happens, the node switches to round `r'`, skipping both the current and the possible intermediate rounds. - +- Stalled + - Final state for an unsuccessful round + - In the algorithm when `roundp > r` + - Consists of the substates: `propose`, `prevote`, and `precommit` +- Decided + - Final state for an successful round -## Round state-machine +The table below summarizes the major state transitions in the `Round(r)` state machine. +The `Ref` column refers to the line of the pseudo-code where the events can be found. -State machine `Round(r)` representing the operation of a round `r` of consensus from height `h`. +| From | To | Event | Action | Ref | +|-------|-----------|-----------|--------|-----| +| Unstarted | InProgress | `start` from `Height(h)` state machine | | | +| InProgress | Decided | `⟨PROPOSAL, h, r, v, *⟩`
`2f + 1 ⟨PRECOMMIT, h, r, id(v)⟩` | emit `decide(r, v)` | L49 | +| InProgress | Stalled | `TimeoutPrecommit(h, r)` | emit `next_round(r+1)` | L65 | +| InProgress | Stalled | `next_round(r')` with `r' > r` from `Height(h)` state machine | | | +| Stalled | Decided | `⟨PROPOSAL, h, r, v, *⟩`
`2f + 1 ⟨PRECOMMIT, h, r, id(v)⟩` | emit `decide(r, v)` | L49 | -The considered set of states are: +The following two state transitions are associated with the round-skipping mechanism. +**TODO:** They need to be reviewed. -- Unstarted -- InProgress - - propose - - prevote - - precommit -- Stalled -- Decided +| From | To | Event | Action | Ref | +|-------|-----------|-----------|--------|-----| +| InProgress | Stalled | `2f + 1 ⟨PREVOTE, h, r', *, *⟩` with `r' > r` | emit `next_round(r')` | L55 | +| InProgress | Stalled | `2f + 1 ⟨PRECOMMIT, h, r', *, *⟩` with `r' > r` | emit `next_round(r')` | L55 | -### Core transitions +### InProgress round The table below summarizes the state transitions within the `InProgress` state of the `Round(r)` state machine. @@ -151,15 +151,17 @@ The conditions for concluding a round of consensus, therefore for leaving the `InProgress` state, are presented in the next sub-section. All the state transitions represented in the table on consider message and -events referring to the nodes's current round `r`. +events referring to the node's current round `r`. In the pseudo-code this current round of a node is referred as `round_p`. -There is, however, an execption: the transition `L28` requires the node to have +There is, however, an exception: the transition `L28` requires the node to have access to `PREVOTE` messages from a previous round `r' < r`. Ideally, messages for each round `r` should be handled by the corresponding `Round(r)` state machine. This transition constitutes an exception that have to be handled in a proper way. + From 748b60f020130d4b2412e67c81a856f78c928972 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Wed, 18 Oct 2023 09:48:51 +0200 Subject: [PATCH 08/13] consensus: initial list of events for state machines --- consensus/protocol-state-machine.md | 90 ++++++++++++++++++++++------- 1 file changed, 70 insertions(+), 20 deletions(-) diff --git a/consensus/protocol-state-machine.md b/consensus/protocol-state-machine.md index e410565..3ade3bc 100644 --- a/consensus/protocol-state-machine.md +++ b/consensus/protocol-state-machine.md @@ -10,13 +10,6 @@ identified by natural numbers `r`. We define a [`Round(r)` state machine](#round-state-machine) to represent the operation of each of the rounds `r` of a height. - - ## Height state machine The state machine `Height(h)` represents the operation of a height `h` of consensus. @@ -72,7 +65,6 @@ Each round `r` of consensus is represented by a state machine `Round(r)`. There is a single round _in progress_ at a time, which is always the last `Round(r)` state machine to receive the `start` command. - A round `r` may not succeed on reaching a decision. In this case, the successive round `r+1` is started. The uncessful `Round(r)` state machine is not killed at this point, as messages @@ -120,8 +112,18 @@ The following two state transitions are associated with the round-skipping mecha | From | To | Event | Action | Ref | |-------|-----------|-----------|--------|-----| -| InProgress | Stalled | `2f + 1 ⟨PREVOTE, h, r', *, *⟩` with `r' > r` | emit `next_round(r')` | L55 | -| InProgress | Stalled | `2f + 1 ⟨PRECOMMIT, h, r', *, *⟩` with `r' > r` | emit `next_round(r')` | L55 | +| InProgress | Stalled | `f + 1 ⟨PREVOTE, h, r', *, *⟩` with `r' > r` | emit `next_round(r')` | L55 | +| InProgress | Stalled | `f + 1 ⟨PRECOMMIT, h, r', *, *⟩` with `r' > r` | emit `next_round(r')` | L55 | + +> There is an open question in this specification related to the round-skipping +> state transitions, as they are the only to have as input messages from a round +> `r'` that is not the state machine round `r`. +> It would be possible to have these events processed by the `Round(r')` state +> machine, instead, as this is the round to which the messages belong. +> In this case, if the `Round(r')` state machine is on the `Unstarted` state and +> the events are observed, the round skip event `next_round(r')` could be produced. +> The `Round(r)` state machine, in this case, could process this event instead, +> moving to the `Stalled` state in the same way as it is now. ### InProgress round @@ -196,14 +198,62 @@ The last two transitions are associated with the decision of a value in round `r It might occur while this is the current round (`InProgress` state) or after it was concluded without success (`Stalled` state). -There is an open question in this specification related to the round-skipping -state transitions, as they are the only to have as input messages from a round -`r'` that is not the state machine round `r`. -It would be possible to have these events processed by the `Round(r')` state -machine, instead, as this is the round to which the messages belong. -In this case, if the `Round(r')` state machine is on the `Unstarted` state and -the events are observed, the round skip event `next_round(r')` could be produced. -The `Round(r)` state machine, in this case, could process this event instead, -moving to the `Stalled` state in the same way as it is now. - ---> + +## Events + +Description of the events considered by the algorithm. + +We should consider renaming them for more clarity. +The production of such events requires, in most cases, the definition of a +state machine to produce them. + +### `⟨PROPOSAL, h, r, v, *⟩` + +A `PROPOSAL` message for round `(h,r)`. +Must be received from (i.e., signed by) `proposer(h, r)`. + +The algorithm considers that this message carries the (full) value `v`. +This specification should consider that the carried value can be obtained in a +different way. +This event, in this case, consists of the combination of possible multiple +message or events that have as a result the production of this event for the +algorithm. + +### `2f + 1 ⟨PREVOTE, h, r, *⟩` + +Quorum of `PREVOTE` messages for a round `(h, r)`. + +The last field value can be: + +- `id(v)`: quorum of votes for a value +- `nil`: quorum of votes for nil +- `any`: quorum of votes for multiple values and/or nil + +### `2f + 1 ⟨PRECOMMIT, h, r, *⟩` + +Quorum of `PRECOMMIT` messages for a round `(h, r)`. + +The last field value can be: + +- `id(v)`: quorum of votes for a value +- `nil`: quorum of votes for nil +- `any`: quorum of votes for multiple values and/or nil + +### `Timeout*(h, r)` + +Timeout events. +They must be scheduled in order to be triggered. + +### `f + 1 ⟨*, h, r, *⟩` + +For round-skipping, needs to be properly evaluated. + +## Pending of description + +- [ ] Events considered by every state machine + - Events produced by one state machine and processed by another + - External events, produced by the environment (e.g. messages and timeouts) +- [ ] State machine producing complex events (e.g. `2f + 1` message X) +- [ ] Routing of events from the higher-level state machine to lower-level state machines + From 9f1c8dfc402f2b69149dc764b2d78961c9d46a26 Mon Sep 17 00:00:00 2001 From: Anca Zamfir Date: Wed, 18 Oct 2023 18:37:30 -0400 Subject: [PATCH 09/13] Add event name column to match agnes implementation --- consensus/protocol-state-machine.md | 41 +++++++++++++++-------------- 1 file changed, 21 insertions(+), 20 deletions(-) diff --git a/consensus/protocol-state-machine.md b/consensus/protocol-state-machine.md index 3ade3bc..8c8f1ef 100644 --- a/consensus/protocol-state-machine.md +++ b/consensus/protocol-state-machine.md @@ -134,18 +134,19 @@ time, which represents the node's current round of consensus. The following state transitions therefore represent the core of the consensus algorithm. The `Ref` column refers to the line of the pseudo-code where the events can be found. -| From | To | Event | Action | Ref | -|-------|-----------|-----------|--------|-----| -| Unstarted | propose | `start` with `proposer(h, r) = p` | `proposal = getValue()`
**broadcast** `⟨PROPOSAL, h, r, proposal, validRound⟩` | L19 | -| Unstarted | propose | `start` with `proposer(h, r) != p` (optional restriction) | schedule `TimeoutPropose(h, r)` | L21 | -| propose | prevote | `⟨PROPOSAL, h, r, v, −1⟩` | broadcast `⟨PREVOTE, h, r, {id(v), nil}⟩` | L22 | -| propose | prevote | `⟨PROPOSAL, h, r, v, vr⟩`
`2f + 1 ⟨PREVOTE, h, vr, id(v)⟩` with `vr < r` | broadcast `⟨PREVOTE, h, r, {id(v), nil}⟩` | L28 | -| propose | prevote | `TimeoutPropose(h, r)` | broadcast `⟨PREVOTE, h, r, nil⟩` | L57 | -| prevote | prevote | `2f + 1 ⟨PREVOTE, h, r, *⟩`
for the first time | schedule `TimeoutPrevote(h, r)⟩` | L34 | -| prevote | precommit | `⟨PROPOSAL, h, r, v, ∗⟩`
`2f + 1 ⟨PREVOTE, h, r, id(v)⟩`
for the first time | broadcast `⟨PRECOMMIT, h, r, id(v)⟩`
update `lockedValue, lockedRound`
update `validValue, validRound` | L36 | -| prevote | precommit | `2f + 1 ⟨PREVOTE, h, r, nil⟩` | broadcast `⟨PRECOMMIT, h, r, nil⟩` | L44 | -| prevote | precommit | `TimeoutPrevote(h, r)` | broadcast `⟨PRECOMMIT, h, r, nil⟩` | L61 | -| precommit | precommit | `⟨PROPOSAL, h, r, v, ∗⟩`
`2f + 1 ⟨PREVOTE, h, r, id(v)⟩`
for the first time | update `validValue, validRound` | L36 | + +| From | To | Ev Name | Ev Details | Actions and Return | Ref | +| ----------- | ----------- | ------------------ | --------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------- | ----- | +| Unstarted | propose | StartProposer(v) | `start` with `proposer(h, r) = p` and `v` | `proposal⟨h, r, proposal, validRound⟩` | L19 | +| Unstarted | propose | StartNonProposer | `start` with `proposer(h, r) != p` (optional restriction) | `timeout_propose(h, r)` | L21 | +| propose | prevote | Proposal(v, -1) | `⟨PROPOSAL, h, r, v, −1⟩` | `prevote(h, r, {id(v), nil}⟩` | L22 | +| propose | prevote | Proposal(v, vr) | `⟨PROPOSAL, h, r, v, vr⟩`
`2f + 1 ⟨PREVOTE, h, vr, id(v)⟩` with `vr < r` | `prevote(h, r, {id(v), nil}⟩` | L28 | +| propose | prevote | TimeoutPropose | `TimeoutPropose(h, r)` | `prevote(h, r, nil⟩` | L57 | +| prevote | prevote | PolkaAny | `2f + 1 ⟨PREVOTE, h, r, *⟩`
for the first time | `timeout_prevote(h, r)⟩` | L34 | +| prevote | precommit | PolkaValue(v) | `⟨PROPOSAL, h, r, v, ∗⟩`
`2f + 1 ⟨PREVOTE, h, r, id(v)⟩`
for the first time | update`lockedValue, lockedRound, validValue, validRound`,
`precommit(h, r, id(v)⟩` | L36 | +| prevote | precommit | PolkaNil | `2f + 1 ⟨PREVOTE, h, r, nil⟩` | `prcommit(h, r, nil⟩` | L44 | +| prevote | precommit | TimeoutPrevote | `TimeoutPrevote(h, r)` | `precommit(h, r, nil⟩` | L61 | +| precommit | precommit | PolkaValue(v) | `⟨PROPOSAL, h, r, v, ∗⟩`
`2f + 1 ⟨PREVOTE, h, r, id(v)⟩`
for the first time | update`validValue, validRound` | L36 | The ordinary operation of a round of consensus consists on the sequence of round steps `propose`, `prevote`, and `precommit`, represented in the table. @@ -171,14 +172,14 @@ The transactions from state `InProgress` consider that node can be at any of its substates, whose transitions were covered in the previous section. The `Ref` column refers to the line of the pseudo-code where the events can be found. -| From | To | Event | Action | Ref | -|-------|-----------|-----------|--------|-----| -| InProgress | InProgress | `2f + 1 ⟨PRECOMMIT, h, r, *⟩`
for the first time | schedule `TimeoutPrecommit(h, r)` | L47 | -| InProgress | Stalled | `TimeoutPrecommit(h, r)` | emit `next_round(r+1)` | L65 | -| InProgress | Stalled | `2f + 1 ⟨PREVOTE, h, r', *, *⟩` with `r' > r` | emit `next_round(r')` | L55 | -| InProgress | Stalled | `2f + 1 ⟨PRECOMMIT, h, r', *, *⟩` with `r' > r` | emit `next_round(r')` | L55 | -| InProgress | Decided | `⟨PROPOSAL, h, r, v, *⟩`
`2f + 1 ⟨PRECOMMIT, h, r, id(v)⟩` | emit `decide(v)` | L49 | -| Stalled | Decided | `⟨PROPOSAL, h, r, v, *⟩`
`2f + 1 ⟨PRECOMMIT, h, r, id(v)⟩` | emit `decide(v)` | L49 | + +| From | To | Ev Name | Event Details | Action | Ref | +| ------------ | ------------ | ------------------- | --------------------------------------------------------------------- | --------------------------- | ----- | +| InProgress | InProgress | PrecommitAny | `2f + 1 ⟨PRECOMMIT, h, r, *⟩`
for the first time | `timeout_precommit(h, r)` | L47 | +| InProgress | Unstarted | TimeoutPrecommit | `TimeoutPrecommit(h, r)` | `next_round(r+1)` | L65 | +| InProgress | Unstarted | RoundSkip(r') | `f + 1 ⟨PREVOTE, h, r', *, *⟩` with `r' > r` | `next_round(r')` | L55 | +| InProgress | Decided | PrecommitValue(v) | `⟨PROPOSAL, h, r, v, *⟩`
`2f + 1 ⟨PRECOMMIT, h, r, id(v)⟩` | `commit(v)` | L49 | +| | | | | | | The first two transitions are associated to unsuccessful rounds. To leave an unsuccessful round, a node has to schedule a `TimeoutPrecommit` From edc03f902ee179a0d72fd52157bce6345e2b3475 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Thu, 19 Oct 2023 19:02:49 +0200 Subject: [PATCH 10/13] consensus: producing events from messages, intro --- consensus/messsages-to-events.md | 111 +++++++++++++++++++++++++++++++ 1 file changed, 111 insertions(+) create mode 100644 consensus/messsages-to-events.md diff --git a/consensus/messsages-to-events.md b/consensus/messsages-to-events.md new file mode 100644 index 0000000..d01f588 --- /dev/null +++ b/consensus/messsages-to-events.md @@ -0,0 +1,111 @@ +# Messages to Events + +The consensus state-machine operates on complex `Event`s that reflect the +reception of one or multiple `Message`s, combined with state elements and the +interaction with other modules. + +This document overviews how messages should be handled at different stages of +the protocol. + +It is assume that a process is at round `r` of height `h` of consensus, or in +short, at round `(h, r)`. + +## Pending + +- [ ] How to handle messages from [different heights](#different-heights) in general +- [ ] Definitions and details regarding the [round skipping](#round-skipping) mechanism +- [ ] How to limit the amount of messages from [future rounds](#future-rounds) stored +- [ ] Full mapping between messages of the [current round](#current-round) and the produced events + +## Different heights + +Messages with heights `h'` with either `h' < h` (past) or `h' > h` (future). + +The pseudo-code description of the algorithm ignores messages from different +heights. +If we take the same approach in this specification, we have to specified +separatedly modules responsible to handle those messages. + + +- Past heights (`h' < h`): the consensus state machine is not affected by such + messages. However, their reception might indicate that a peer is lagging + behind in the protocol, and need to be synchronized. + - In CometBFT's implementation we handle message from the previous height + (`h' = h - 1`) for the `LastCommit` vote set. This only happens during the + first step of the first round (`r = 0`) of a height. +- Future heights (`h' > h`): the consensus state machine is not able to process + message from future heights in a proper way, as the validator set for them is + not known. However, once the process reaches this height `h'`, those messages + are _required_ for proper operation. There are two options here: + 1. Buffer a limited amount of such messages + 2. Assume that the communication subsystem (p2p) is able to retrieve (ask for + retransmission) of them when the process reaches height `h'`. + Notice that this option implies that processs keeps a minimal set of + consensus messages that enables peers lagging behind to decide a past height. + +## Previous rounds + +Messages from rounds `(h, r')` with `r' < r`: same height `h` but previous round `r'`. + +The consensus state machine requires receiving and processing messages from +previous rounds: + +- `PREVOTE` messages can produce a Proof of Lock (POL) `2f + 1 ⟨PREVOTE, h, vr, id(v)⟩` + needed for accepting `PROPOSAL(h, r, v, vr)` message from the current round, + where `vr == r' < r` (L28). +- `PRECOMMIT` messages can produce a Precommit quorum `2f + 1 ⟨PRECOMMIT, h, r', id(v)⟩` + that leads to the decision of `v` at round `r'` (L49). +- `PROPOSAL` messages can be required to match a produced Precommit quorum (L49). + - Associated full value messages are required to produce the `⟨PROPOSAL, h, r', v, *⟩` event + +The production of the enumerated events from previous rounds should be +identitical to the production of events from messages from the [current round](#current-round). + +## Future rounds + +Messages from rounds `(h, r')` with `r' > r`: same height `h` but future round `r'`. + +### Round skipping + +The consensus state machine requires receiving and processing messages from +future rounds for enabling the _round skipping_ mechanism, defined as follows +in the pseudo-code: + +``` +55: upon f + 1 ⟨∗, hp, round, ∗, ∗⟩ with round > roundp do +56: StartRound(round) +``` + +The current interpretation of this rule is that messages from a round `r' > r` +are received from `f + 1` voting-power equivalent distint senders. +This means, that at least `1` correct process is at round `r'`. + +While this threshould does not need to be adopted (it can be configurable), +messages from a future round should initially have their unique senders counted. +Once the round skip treshould of processs is reached, the corresponding event +should be produced. + +### Limits + +The same reasoning applied for messages from [future heights](#different-heights) +applies for messages from future rounds. + +Messages from future rounds are _required_ for the proper operation of the +consensus state machine once the process reaches their round `r'`. +There are two options, which can in particular be combined: + +1. Buffer a limited amount of such messages, or messages from a limited amount + of future rounds `r'` + - In CometBFT's implementation, only messages from round `r' = r + 1` are tracked. +2. Assume that the communication subsystem (p2p) is able to retrieve (ask for + retransmission) of messages from future rounds when the process reaches round `r'`. + Since messages from [previous rounds](#previous-rounds) are stored by + default, peers that have reached the future round `r'` should be able to + retransmit them. + +## Current round + +Messages matching the current round `(h, r)` of a process produce most of the +relevants events for the consensus state machine. + +TODO: From 9b4c33af25b52f39d94719088d6c905240da87b0 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Fri, 20 Oct 2023 13:07:06 +0200 Subject: [PATCH 11/13] consensus: couting votes, general assumptions --- consensus/messsages-to-events.md | 77 ++++++++++++++++++++++++++++---- 1 file changed, 68 insertions(+), 9 deletions(-) diff --git a/consensus/messsages-to-events.md b/consensus/messsages-to-events.md index d01f588..a8ce85b 100644 --- a/consensus/messsages-to-events.md +++ b/consensus/messsages-to-events.md @@ -23,8 +23,8 @@ Messages with heights `h'` with either `h' < h` (past) or `h' > h` (future). The pseudo-code description of the algorithm ignores messages from different heights. -If we take the same approach in this specification, we have to specified -separatedly modules responsible to handle those messages. +If we take the same approach in this specification, we have to specify +separately modules responsible to handle those messages. - Past heights (`h' < h`): the consensus state machine is not affected by such @@ -40,8 +40,8 @@ separatedly modules responsible to handle those messages. 1. Buffer a limited amount of such messages 2. Assume that the communication subsystem (p2p) is able to retrieve (ask for retransmission) of them when the process reaches height `h'`. - Notice that this option implies that processs keeps a minimal set of - consensus messages that enables peers lagging behind to decide a past height. + Notice that this option implies that processes keep a minimal set of + consensus messages that enables peers lagging behind to decide a past height. ## Previous rounds @@ -59,7 +59,7 @@ previous rounds: - Associated full value messages are required to produce the `⟨PROPOSAL, h, r', v, *⟩` event The production of the enumerated events from previous rounds should be -identitical to the production of events from messages from the [current round](#current-round). +identical to the production of events from messages from the [current round](#current-round). ## Future rounds @@ -77,12 +77,12 @@ in the pseudo-code: ``` The current interpretation of this rule is that messages from a round `r' > r` -are received from `f + 1` voting-power equivalent distint senders. +are received from `f + 1` voting-power equivalent distinct senders. This means, that at least `1` correct process is at round `r'`. -While this threshould does not need to be adopted (it can be configurable), +While this threshold does not need to be adopted (it can be configurable), messages from a future round should initially have their unique senders counted. -Once the round skip treshould of processs is reached, the corresponding event +Once the round skip threshold of processes is reached, the corresponding event should be produced. ### Limits @@ -106,6 +106,65 @@ There are two options, which can in particular be combined: ## Current round Messages matching the current round `(h, r)` of a process produce most of the -relevants events for the consensus state machine. +relevant events for the consensus state machine. TODO: + +## Counting votes + +Messages `⟨PREVOTE, h, r, *⟩` and `⟨PRECOMMIT, h, r, *⟩` are generically called votes. +They refer to a round step `(h, r, s)` of consensus, where `s` is defined by +the vote type, either `PREVOTE` or `PRECOMMIT`. + +The processing of _individual_ vote messages don't produce events relevant for +the consensus state machine. +But when the number of unique vote messages referring to a given round step +`(h, r, s)` reaches a given _threshold_, relevant events are produced; +the produced event depends on the value carried by such votes. + +General assumptions regarding vote messages: + +- Vote messages are produced, signed and broadcast by a validator, which is its + *sender* + - To define whether a vote message for round step `(h, r, s)` is valid, the + validator set for height `h` must to be known. + The validator set can change over heights, but it is the same within a height. +- To each validator in the validator set of a height `h` is associated a *voting power* + - Thresholds are computed from the voting power associated to the + sender of each vote message +- A vote message carries a value: either a reference to a proposed value + `id(v)`, or the special `nil` value + - For practical effects, it should be considered that the size of vote + messages is constant +- Correct validators produce at most one vote message per round step: either + for a `id(v)` or for `nil` +- Byzantine validators may equivocate and produce multiple distinct vote + messages for the same round step. Equivocating vote messages differ on the + value they carry: for `nil`, `id(v)`, `id(v')`, etc. + - This possibility constitutes an attack vector. A process must thus restrict + the number of distinct vote messages from the same sender and referring to + the same round step that can be stored. + +### `f + 1` threshold + +This threshold represents that vote messages referring to a round step were +received from a enough number of unique senders, so that it is guaranteed that +_at least one_ of the senders is a _correct_ validator. + +The rationale here is that the cumulative voting power of Byzantine validators +cannot exceed `f`, so that at least one of the considered vote messages must +have been produced by a correct validator. + +### `2f + 1` threshold + +This threshold represents that vote messages referring to a round step were +received from a enough number of unique senders, so that it is guaranteed that +_the majority_ of the senders are _correct_ validators. + +The rationale here is that the cumulative voting power of Byzantine validators +cannot exceed `f`, so that the subset of considered vote messages that must +have been produced by correct validators have a cumulative voting power of at +least `f + 1`, which is strictly greater than `f`. + +> TODO: this also means that the majority of the voting power hold by correct +> validators is represented in the considered set of vote messages. From c25ca7029d64c3eee1799f7f98a3f6fd207491e5 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Tue, 24 Oct 2023 20:52:09 +0200 Subject: [PATCH 12/13] Fixing merging conflicts --- consensus/protocol-state-machine.md | 36 ++++++++++++++--------------- 1 file changed, 17 insertions(+), 19 deletions(-) diff --git a/consensus/protocol-state-machine.md b/consensus/protocol-state-machine.md index 8c8f1ef..3d95d2a 100644 --- a/consensus/protocol-state-machine.md +++ b/consensus/protocol-state-machine.md @@ -99,13 +99,13 @@ The considered set of states are: The table below summarizes the major state transitions in the `Round(r)` state machine. The `Ref` column refers to the line of the pseudo-code where the events can be found. -| From | To | Event | Action | Ref | -|-------|-----------|-----------|--------|-----| -| Unstarted | InProgress | `start` from `Height(h)` state machine | | | -| InProgress | Decided | `⟨PROPOSAL, h, r, v, *⟩`
`2f + 1 ⟨PRECOMMIT, h, r, id(v)⟩` | emit `decide(r, v)` | L49 | -| InProgress | Stalled | `TimeoutPrecommit(h, r)` | emit `next_round(r+1)` | L65 | -| InProgress | Stalled | `next_round(r')` with `r' > r` from `Height(h)` state machine | | | -| Stalled | Decided | `⟨PROPOSAL, h, r, v, *⟩`
`2f + 1 ⟨PRECOMMIT, h, r, id(v)⟩` | emit `decide(r, v)` | L49 | +| From | To | Ev Name | Event Details | Action | Ref | +| ------------ | ------------ | ------------------- | --------------------------------------------------------------------- | --------------------------- | ----- | +| InProgress | InProgress | PrecommitAny | `2f + 1 ⟨PRECOMMIT, h, r, *⟩`
for the first time | schedule `TimeoutPrecommit(h, r)` | L47 | +| InProgress | Unstarted | TimeoutPrecommit | `TimeoutPrecommit(h, r)` | `next_round(r+1)` | L65 | +| InProgress | Unstarted | RoundSkip(r') | `f + 1 ⟨PREVOTE, h, r', *, *⟩` with `r' > r` | `next_round(r')` | L55 | +| InProgress | Decided | PrecommitValue(v) | `⟨PROPOSAL, h, r, v, *⟩`
`2f + 1 ⟨PRECOMMIT, h, r, id(v)⟩` | `commit(v)` | L49 | + The following two state transitions are associated with the round-skipping mechanism. **TODO:** They need to be reviewed. @@ -134,19 +134,18 @@ time, which represents the node's current round of consensus. The following state transitions therefore represent the core of the consensus algorithm. The `Ref` column refers to the line of the pseudo-code where the events can be found. - | From | To | Ev Name | Ev Details | Actions and Return | Ref | | ----------- | ----------- | ------------------ | --------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------- | ----- | -| Unstarted | propose | StartProposer(v) | `start` with `proposer(h, r) = p` and `v` | `proposal⟨h, r, proposal, validRound⟩` | L19 | -| Unstarted | propose | StartNonProposer | `start` with `proposer(h, r) != p` (optional restriction) | `timeout_propose(h, r)` | L21 | -| propose | prevote | Proposal(v, -1) | `⟨PROPOSAL, h, r, v, −1⟩` | `prevote(h, r, {id(v), nil}⟩` | L22 | -| propose | prevote | Proposal(v, vr) | `⟨PROPOSAL, h, r, v, vr⟩`
`2f + 1 ⟨PREVOTE, h, vr, id(v)⟩` with `vr < r` | `prevote(h, r, {id(v), nil}⟩` | L28 | -| propose | prevote | TimeoutPropose | `TimeoutPropose(h, r)` | `prevote(h, r, nil⟩` | L57 | -| prevote | prevote | PolkaAny | `2f + 1 ⟨PREVOTE, h, r, *⟩`
for the first time | `timeout_prevote(h, r)⟩` | L34 | -| prevote | precommit | PolkaValue(v) | `⟨PROPOSAL, h, r, v, ∗⟩`
`2f + 1 ⟨PREVOTE, h, r, id(v)⟩`
for the first time | update`lockedValue, lockedRound, validValue, validRound`,
`precommit(h, r, id(v)⟩` | L36 | -| prevote | precommit | PolkaNil | `2f + 1 ⟨PREVOTE, h, r, nil⟩` | `prcommit(h, r, nil⟩` | L44 | -| prevote | precommit | TimeoutPrevote | `TimeoutPrevote(h, r)` | `precommit(h, r, nil⟩` | L61 | -| precommit | precommit | PolkaValue(v) | `⟨PROPOSAL, h, r, v, ∗⟩`
`2f + 1 ⟨PREVOTE, h, r, id(v)⟩`
for the first time | update`validValue, validRound` | L36 | +| Unstarted | propose | StartProposer(v) | `start` with `proposer(h, r) = p` and `v = getValue()` | broadcast `⟨PROPOSAL, h, r, v, validRound⟩` | L19 | +| Unstarted | propose | StartNonProposer | `start` with `proposer(h, r) != p` (optional restriction) | schedule `TimeoutPropose(h, r)` | L21 | +| propose | prevote | Proposal(v, -1) | `⟨PROPOSAL, h, r, v, −1⟩` | broadcast `⟨PREVOTE, h, r, {id(v), nil}⟩` | L22 | +| propose | prevote | Proposal(v, vr) | `⟨PROPOSAL, h, r, v, vr⟩`
`2f + 1 ⟨PREVOTE, h, vr, id(v)⟩` with `vr < r` | broadcast `⟨PREVOTE, h, r, {id(v), nil}⟩` | L28 | +| propose | prevote | TimeoutPropose | `TimeoutPropose(h, r)` | broadcast `⟨PREVOTE, h, r, nil⟩` | L57 | +| prevote | prevote | PolkaAny | `2f + 1 ⟨PREVOTE, h, r, *⟩`
for the first time | schedule `TimeoutPrevote(h, r)⟩` | L34 | +| prevote | precommit | PolkaValue(v) | `⟨PROPOSAL, h, r, v, ∗⟩`
`2f + 1 ⟨PREVOTE, h, r, id(v)⟩`
for the first time | update `lockedValue, lockedRound, validValue, validRound`,
broadcast `⟨PRECOMMIT, h, r, id(v)⟩` | L36 | +| prevote | precommit | PolkaNil | `2f + 1 ⟨PREVOTE, h, r, nil⟩` | broadcast `⟨PRECOMMIT, h, r, nil⟩` | L44 | +| prevote | precommit | TimeoutPrevote | `TimeoutPrevote(h, r)` | broadcast `⟨PRECOMMIT, h, r, nil⟩` | L61 | +| precommit | precommit | PolkaValue(v) | `⟨PROPOSAL, h, r, v, ∗⟩`
`2f + 1 ⟨PREVOTE, h, r, id(v)⟩`
for the first time | update `validValue, validRound` | L36 | The ordinary operation of a round of consensus consists on the sequence of round steps `propose`, `prevote`, and `precommit`, represented in the table. @@ -172,7 +171,6 @@ The transactions from state `InProgress` consider that node can be at any of its substates, whose transitions were covered in the previous section. The `Ref` column refers to the line of the pseudo-code where the events can be found. - | From | To | Ev Name | Event Details | Action | Ref | | ------------ | ------------ | ------------------- | --------------------------------------------------------------------- | --------------------------- | ----- | | InProgress | InProgress | PrecommitAny | `2f + 1 ⟨PRECOMMIT, h, r, *⟩`
for the first time | `timeout_precommit(h, r)` | L47 | From 28e2e54a96c8d7485ed0c64e2b6946bac4c331cf Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Tue, 24 Oct 2023 20:55:59 +0200 Subject: [PATCH 13/13] Merging some events tables for simpler spec --- consensus/protocol-state-machine.md | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/consensus/protocol-state-machine.md b/consensus/protocol-state-machine.md index 3d95d2a..13c5c41 100644 --- a/consensus/protocol-state-machine.md +++ b/consensus/protocol-state-machine.md @@ -35,7 +35,9 @@ The `Ref` column refers to the line of the pseudo-code where the events can be f | From | To | Event | Action | Ref | |-------|-----------|-----------|--------|-----| | Unstarted | InProgress | `start_height` | send `start` to `Round(0)` | L10, L54 | -| InProgress | Decided | `decide(r, v)` | emit `decide(h, v)`
stop to every `Round(r)` | L49 | +| Round(r) | Decided | `decide(r', v)` | emit `decide(h, v)`
stop to every `Round(r)` | L49 | +| Round(r) | Round(r+1) | `next_round(r+1)` | send `start` to `Round(r+1)` | L65 | +| Round(r) | Round(r') | `next_round(r')` | send `start` to `Round(r')` | L55 | A height `h` consists of multiple rounds of consensus, always starting from round `0`. @@ -51,16 +53,13 @@ _every_ round `Round(r)` should be concluded. The representation of this transition needs to be improved, for now it is considered that the corresponding `Round(r)` state machines are killed. + + ## Round state-machine The state machine `Round(r)` represents the operation of a round `r` of consensus. @@ -102,11 +103,13 @@ The `Ref` column refers to the line of the pseudo-code where the events can be f | From | To | Ev Name | Event Details | Action | Ref | | ------------ | ------------ | ------------------- | --------------------------------------------------------------------- | --------------------------- | ----- | | InProgress | InProgress | PrecommitAny | `2f + 1 ⟨PRECOMMIT, h, r, *⟩`
for the first time | schedule `TimeoutPrecommit(h, r)` | L47 | -| InProgress | Unstarted | TimeoutPrecommit | `TimeoutPrecommit(h, r)` | `next_round(r+1)` | L65 | -| InProgress | Unstarted | RoundSkip(r') | `f + 1 ⟨PREVOTE, h, r', *, *⟩` with `r' > r` | `next_round(r')` | L55 | +| InProgress | Unstarted (?) | TimeoutPrecommit | `TimeoutPrecommit(h, r)` | `next_round(r+1)` | L65 | +| InProgress | Unstarted (?) | RoundSkip(r') | `f + 1 ⟨*, h, r', *, *⟩` with `r' > r` | `next_round(r')` | L55 | | InProgress | Decided | PrecommitValue(v) | `⟨PROPOSAL, h, r, v, *⟩`
`2f + 1 ⟨PRECOMMIT, h, r, id(v)⟩` | `commit(v)` | L49 | + + ### InProgress round The table below summarizes the state transitions within the `InProgress` state