From a49325e4e09839afcba9910b5636b4013938e0bc Mon Sep 17 00:00:00 2001 From: Daniel Date: Mon, 2 May 2022 10:22:03 +0200 Subject: [PATCH] PBTS: system model made more precise (#8096) * PBTS model: precision, accuracy, and delay defs * PBTS model: consensus properties reviewed * PBTS model: reinforcing alignment with UTC * PBTS model: precision parameter embodies accuracy * PBTS model: discussion about accuracy shortened * PBTS model: proposal time monotonocity rephrased * PBTS model: precision, accuracy, and delay defs * PBTS model: consensus properties reviewed * PBTS model: reinforcing alignment with UTC * PBTS model: precision parameter embodies accuracy * PBTS model: discussion about accuracy shortened * PBTS model: proposal time monotonocity rephrased * PBTS model: Safety Invariants subsection * PBTS model: MSGDELAY description shortened * PBTS model: timely proposals definition refined * PBTS model: some formatting changes * PBTS model: timely predicate definition * PBTS model: timely proof-of-lock re-defined * PBTS model: derived proof-of-lock requirements * The property needs to be properly demonstrated. * Apply suggestions from William Co-authored-by: William Banfield <4561443+williambanfield@users.noreply.github.com> * PBTS model: reference to arXiv algorithm on timely * PBTS model: typos fixed * PBTS model: derived POL "demonstration" * PBTS model: fix formatting, r' renamed to vr * PBTS model: minor fixes * PBTS model: derived POL proof ammended * PBTS safety: consensus validity with time inequalty * PBTS: renamed receiveTime to proposalReceptionTime * PBTS safety: short intro, some links * PBTS model: safety refactored again * PBTS model: liveness condition stated * PBTS liveness: minor change * Update spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md Co-authored-by: William Banfield <4561443+williambanfield@users.noreply.github.com> * Update spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md Co-authored-by: William Banfield <4561443+williambanfield@users.noreply.github.com> * Update spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md * Update spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> * Update spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> * Update spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> * PBTS sysmodel: formmatting typo fixed Co-authored-by: William Banfield <4561443+williambanfield@users.noreply.github.com> Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com> --- .../pbts-sysmodel_002_draft.md | 353 +++++++++++------- 1 file changed, 226 insertions(+), 127 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index 832d11c9a..d6fcb54b6 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -1,16 +1,31 @@ # PBTS: System Model and Properties +## Outline + + - [System model](#system-model) + - [Synchronized clocks](#synchronized-clocks) + - [Message delays](#message-delays) + - [Problem Statement](#problem-statement) + - [Protocol Analysis - Timely Proposals](#protocol-analysis---timely-proposals) + - [Timely Proof-of-Locks](#timely-proof-of-locks) + - [Derived Proof-of-Locks](#derived-proof-of-locks) + - [Temporal Analysis](#temporal-analysis) + - [Safety](#safety) + - [Liveness](#liveness) + ## System Model #### **[PBTS-CLOCK-NEWTON.0]** -There is a reference Newtonian real-time `t` (UTC). +There is a reference Newtonian real-time `t`. No process has direct access to this reference time, used only for specification purposes. +The reference real-time is assumed to be aligned with the Coordinated Universal Time (UTC). ### Synchronized clocks -Processes are assumed to be equipped with synchronized clocks. +Processes are assumed to be equipped with synchronized clocks, +aligned with the Coordinated Universal Time (UTC). This requires processes to periodically synchronize their local clocks with an external and trusted source of the time (e.g. NTP servers). @@ -27,43 +42,35 @@ and drifts of local clocks from real time. #### **[PBTS-CLOCK-PRECISION.0]** There exists a system parameter `PRECISION`, such that -for any two processes `p` and `q`, with local clocks `C_p` and `C_q`, -that read their local clocks at the same real-time `t`, we have: +for any two processes `p` and `q`, with local clocks `C_p` and `C_q`: -- If `p` and `q` are equipped with synchronized clocks, then `|C_p(t) - C_q(t)| < PRECISION` +- If `p` and `q` are equipped with synchronized clocks, + then for any real-time `t` we have `|C_p(t) - C_q(t)| <= PRECISION`. `PRECISION` thus bounds the difference on the times simultaneously read by processes from their local clocks, so that their clocks can be considered synchronized. #### Accuracy -The [first draft][sysmodel_v1] of this specification included a second clock-related parameter, `ACCURACY`, -that relates the values read by processes from their synchronized clocks with real time: +A second relevant clock parameter is accuracy, which binds the values read by +processes from their clocks to real time. -- If `p` is a process is equipped with a synchronized clock, then at real time - `t` it reads from its clock time `C_p(t)` with `|C_p(t) - t| < ACCURACY` +##### **[PBTS-CLOCK-ACCURACY.0]** -The adoption of `ACCURACY` as the upper bound on the difference between clock -readings and real time, however, renders the `PRECISION` parameter redundant. -In fact, if we assume that clocks readings are at most `ACCURACY` from real -time, we would therefore be assuming that they cannot be more than `2 * ACCURACY` -apart from each other, thus establishing a worst-case upper bound for `PRECISION`. - -The approach we take is to assume that processes clocks are periodically -synchronized with an external source of time, thus improving their accuracy. -This allows us to adopt a relaxed version of the above `ACCURACY` definition: - -##### **[PBTS-CLOCK-FAIR.0]** +For the sake of completeness, we define a parameter `ACCURACY` such that: - At real time `t` there is at least one correct process `p` which clock marks - `C_p(t)` with `|C_p(t) - t| < ACCURACY` + `C_p(t)` with `|C_p(t) - t| <= ACCURACY`. -Then, through [PBTS-CLOCK-PRECISION] we can extend this relation of clock times -with real time to every correct process, which will have a clock with accuracy -bound by `ACCURACY + PRECISION`. -But, for the sake of simpler specification we can assume that the `PRECISION`, -which is a worst-case parameter that applies to all correct processes, -includes the best `ACCURACY` achieved by any of them. +As a consequence, applying the definition of `PRECISION`, we have: + +- At real time `t` the synchronized clock of any correct process `p` marks + `C_p(t)` with `|C_p(t) - t| <= ACCURACY + PRECISION`. + +The reason for not adopting `ACCURACY` as a system parameter is the assumption +that `PRECISION >> ACCURACY`. +This allows us to consider, for practical purposes, that the `PRECISION` system +parameter embodies the `ACCURACY` model parameter. ### Message Delays @@ -79,172 +86,264 @@ defining a lower bound, a *minimum time* that a correct process assigns to propo While *minimum delay* for delivering a proposal to a destination allows defining an upper bound, the *maximum time* assigned to a proposal. -#### **[PBTS-MSG-D.0]** +#### **[PBTS-MSG-DELAY.0]** -There exists a system parameter `MSGDELAY` for end-to-end delays of messages carrying proposals, -such for any two correct processes `p` and `q`, and any real time `t`: +There exists a system parameter `MSGDELAY` for end-to-end delays of proposal messages, +such for any two correct processes `p` and `q`: -- If `p` sends a message `m` carrying a proposal at time `ts`, -then if `q` receives the message and learns the proposal, -`q` does that at time `t` such that `ts <= t <= ts + MSGDELAY`. +- If `p` sends a proposal message `m` at real time `t` and `q` receives `m` at + real time `t'`, then `t <= t' <= t + MSGDELAY`. -While we don't want to impose particular restrictions regarding the format of `m`, -we need to assume that their size is upper bounded. -In practice, using messages with a fixed-size to carry proposals allows -for a more accurate estimation of `MSGDELAY`, and therefore is advised. +Notice that, as a system parameter, `MSGDELAY` should be observed for any +proposal message broadcast by correct processes: it is a *worst-case* parameter. +As message delays depends on the message size, the above requirement implicitly +indicates that the size of proposal messages is either fixed or upper bounded. ## Problem Statement In this section we define the properties of Tendermint consensus -(cf. the [arXiv paper][arXiv]) in this new system model. +(cf. the [arXiv paper][arXiv]) in this system model. -#### **[PBTS-PROPOSE.0]** +### **[PBTS-PROPOSE.0]** -A proposer proposes a consensus value `v` with an associated proposal time `v.time`. +A proposer proposes a consensus value `v` that includes a proposal time +`v.time`. + +> We then restrict the allowed decisions along the following lines: #### **[PBTS-INV-AGREEMENT.0]** -[Agreement] No two correct processes decide on different values `v`. (This implies that no two correct processes decide on different proposal times `v.time`.) +- [Agreement] No two correct processes decide on different values `v`. + +This implies that no two correct processes decide on different proposal times +`v.time`. #### **[PBTS-INV-VALID.0]** -[Validity] If a correct process decides on value `v`, -then `v` satisfies a predefined `valid` predicate. +- [Validity] If a correct process decides on value `v`, then `v` satisfies a + predefined `valid` predicate. + +With respect to PBTS, the `valid` predicate requires proposal times to be +[monotonic](./pbts-algorithm_002_draft.md#time-monotonicity) over heights of +consensus: + +##### **[PBTS-INV-MONOTONICITY.0]** + +- If a correct process decides on value `v` at the height `h` of consensus, + thus setting `decision[h] = v`, then `v.time > decision[h'].time` for all + previous heights `h' < h`. + +The monotonicity of proposal times, and external validity in general, +implicitly assumes that heights of consensus are executed in order. #### **[PBTS-INV-TIMELY.0]** -[Time-Validity] If a correct process decides on value `v`, -then the associated proposal time `v.time` satisfies a predefined `timely` predicate. +- [Time-Validity] If a correct process decides on value `v`, then the proposal + time `v.time` was considered `timely` by at least one correct process. -> Both [Validity] and [Time-Validity] must be observed even if up to `2f` validators are faulty. +PBTS introduces a `timely` predicate that restricts the allowed decisions based +on the proposal time `v.time` associated with a proposed value `v`. +As a synchronous predicate, the time at which it is evaluated impacts on +whether a process accepts or reject a proposal time. +For this reason, the Time-Validity property refers to the previous evaluation +of the `timely` predicate, detailed in the following section. -### Timely proposals +## Protocol Analysis - Timely proposals + +For PBTS, a `proposal` is a tuple `(v, v.time, v.round)`, where: + +- `v` is the proposed value; +- `v.time` is the associated proposal time; +- `v.round` is the round at which `v` was first proposed. + +We include the proposal round `v.round` in the proposal definition because a +value `v` and its associated proposal time `v.time` can be proposed in multiple +rounds, but the evaluation of the `timely` predicate is only relevant at round +`v.round`. + +> Considering the algorithm in the [arXiv paper][arXiv], a new proposal is +> produced by the `getValue()` method, invoked by the proposer `p` of round +> `round_p` when starting its proposing round with a nil `validValue_p`. +> The first round at which a value `v` is proposed is then the round at which +> the proposal for `v` was produced, and broadcast in a `PROPOSAL` message with +> `vr = -1`. + +#### **[PBTS-PROPOSAL-RECEPTION.0]** The `timely` predicate is evaluated when a process receives a proposal. -Let `now_p` be time a process `p` reads from its local clock when `p` receives a proposal. -Let `v` be the proposed value and `v.time` the proposal time. -The proposal is considered `timely` by `p` if: +More precisely, let `p` be a correct process: -#### **[PBTS-RECEPTION-STEP.1]** +- `proposalReceptionTime(p,r)` is the time `p` reads from its local clock when + `p` is at round `r` and receives the proposal of round `r`. -1. `now_p >= v.time - PRECISION` and -1. `now_p <= v.time + MSGDELAY + PRECISION` +#### **[PBTS-TIMELY.0]** + +The proposal `(v, v.time, v.round)` is considered `timely` by a correct process +`p` if: + +1. `proposalReceptionTime(p,v.round)` is set, and +1. `proposalReceptionTime(p,v.round) >= v.time - PRECISION`, and +1. `proposalReceptionTime(p,v.round) <= v.time + MSGDELAY + PRECISION`. + +A correct process at round `v.round` only sends a `PREVOTE` for `v` if the +associated proposal time `v.time` is considered `timely`. + +> Considering the algorithm in the [arXiv paper][arXiv], the `timely` predicate +> is evaluated by a process `p` when it receives a valid `PROPOSAL` message +> from the proposer of the current round `round_p` with `vr = -1`. ### Timely Proof-of-Locks -We denote by `POL(v,r)` a *Proof-of-Lock* of value `v` at the round `r` of consensus. -`POL(v,r)` consists of a set of `PREVOTE` messages of round `r` for the value `v` -from processes whose cumulative voting power is at least `2f + 1`. +A *Proof-of-Lock* is a set of `PREVOTE` messages of round of consensus for the +same value from processes whose cumulative voting power is at least `2f + 1`. +We denote as `POL(v,r)` a proof-of-lock of value `v` at round `r`. -#### **[PBTS-TIMELY-POL.1]** +For PBTS, we are particularly interested in the `POL(v,v.round)` produced in +the round `v.round` at which a value `v` was first proposed. +We call it a *timely* proof-of-lock for `v` because it can only be observed +if at least one correct process considered it `timely`: + +#### **[PBTS-TIMELY-POL.0]** If -- there is a valid `POL(v,r*)` for height `h`, and -- `r*` is the lowest-numbered round `r` of height `h` for which there is a valid `POL(v,r)`, and -- `POL(v,r*)` contains a `PREVOTE` message from at least one correct process, +- there is a valid `POL(v,r)` with `r = v.round`, and +- `POL(v,v.round)` contains a `PREVOTE` message from at least one correct process, -Then, where `p` is a such correct process: +Then, let `p` is a such correct process: -- `p` received a `PROPOSE` message of round `r*` and height `h`, and -- the `PROPOSE` message contained a proposal for value `v` with proposal time `v.time`, and -- a correct process `p` considered the proposal `timely`. +- `p` received a `PROPOSAL` message of round `v.round`, and +- the `PROPOSAL` message contained a proposal `(v, v.time, v.round)`, and +- `p` was in round `v.round` and evaluated the proposal time `v.time` as `timely`. -The round `r*` above defined will be, in most cases, -the round in which `v` was originally proposed, and when `v.time` was assigned, -using a `PROPOSE` message with `POLRound = -1`. -In any case, at least one correct process must consider the proposal `timely` at round `r*` -to enable a valid `POL(v,r*)` to be observed. +The existence of a such correct process `p` is guaranteed provided that the +voting power of Byzantine processes is bounded by `2f`. ### Derived Proof-of-Locks -#### **[PBTS-DERIVED-POL.1]** +The existence of `POL(v,r)` is a requirement for the decision of `v` at round +`r` of consensus. + +At the same time, the Time-Validity property establishes that if `v` is decided +then a timely proof-of-lock `POL(v,v.round)` must have been produced. + +So, we need to demonstrate here that any valid `POL(v,r)` is either a timely +proof-of-lock or it is derived from a timely proof-of-lock: + +#### **[PBTS-DERIVED-POL.0]** If -- there is a valid `POL(v,r)` for height `h`, and +- there is a valid `POL(v,r)`, and - `POL(v,r)` contains a `PREVOTE` message from at least one correct process, Then -- there is a valid `POL(v,r*)` for height `h`, with `r* <= r`, and -- `POL(v,r*)` contains a `PREVOTE` message from at least one correct process, and -- a correct process considered the proposal for `v` `timely` at round `r*`. +- there is a valid `POL(v,v.round)` with `v.round <= r` which is a timely proof-of-lock. -The above relation derives from a recursion on the round number `r`. -It is trivially observed when `r = r*`, the base of the recursion, -when a timely `POL(v,r*)` is obtained. -We need to ensure that, once a timely `POL(v,r*)` is obtained, -it is possible to obtain a valid `POL(v,r)` with `r > r*`, -without the need of satisfying the `timely` predicate (again) in round `r`. -In fact, since rounds are started in order, it is not likely that -a proposal time `v.time`, assigned at round `r*`, -will still be considered `timely` when the round `r > r*` is in progress. +The above relation is trivially observed when `r = v.round`, as `POL(v,r)` must +be a timely proof-of-lock. +Notice that we cannot have `r < v.round`, as `v.round` is defined as the first +round at which `v` was proposed. -In other words, the algorithm should ensure that once a `POL(v,r*)` attests -that the proposal for `v` is `timely`, -further valid `POL(v,r)` with `r > r*` can be obtained, -even though processes do not consider the proposal for `v` `timely` any longer. +For `r > v.round` we need to demonstrate that if there is a valid `POL(v,r)`, +then a timely `POL(v,v.round)` was previously obtained. +We observe that a condition for observing a `POL(v,r)` is that the proposer of +round `r` has broadcast a `PROPOSAL` message for `v`. +As `r > v.round`, we can affirm that `v` was not produced in round `r`. +Instead, by the protocol operation, `v` was a *valid value* for the proposer of +round `r`, which means that if the proposer has observed a `POL(v,vr)` with `vr +< r`. +The above operation considers a *correct* proposer, but since a `POL(v,r)` was +produced (by hypothesis) we can affirm that at least one correct process (also) +observed a `POL(v,vr)`. -> This can be achieved if the proposer of round `r' > r*` proposes `v` in a `PROPOSE` message -with `POLRound = r*`, and at least one correct processes is aware of a `POL(v,r*)`. -> From this point, if a valid `POL(v,r')` is achieved, it can replace the adopted `POL(v,r*)`. +> Considering the algorithm in the [arXiv paper][arXiv], `v` was proposed by +> the proposer `p` of round `round_p` because its `validValue_p` variable was +> set to `v`. +> The `PROPOSAL` message broadcast by the proposer, in this case, had `vr > -1`, +> and it could only be accepted by processes that also observed a `POL(v,vr)`. -### SAFETY +Thus, if there is a `POL(v,r)` with `r > v.round`, then there is a valid +`POL(v,vr)` with `v.round <= vr < r`. +If `vr = v.round` then `POL(vr,v)` is a timely proof-of-lock and we are done. +Otherwise, there is another valid `POL(v,vr')` with `v.round <= vr' < vr`, +and the above reasoning can be recursively applied until we get `vr' = v.round` +and observe a timely proof-of-lock. -The safety of the algorithm requires a *timely* proof-of-lock for a decided value, -either directly evaluated by a correct process, -or indirectly received through a derived proof-of-lock. +## Temporal analysis -#### **[PBTS-CONSENSUS-TIME-VALID.0]** +In this section we present invariants that need be observed for ensuring that +PBTS is both safe and live. + +In addition to the variables and system parameters already defined, we use +`beginRound(p,r)` as the value of process `p`'s local clock +when it starts round `r` of consensus. + +### Safety + +The safety of PBTS requires that if a value `v` is decided, then at least one +correct process `p` considered the associated proposal time `v.time` timely. +Following the definition of [timely proposals](#pbts-timely0) and +proof-of-locks, we require this condition to be asserted at a specific round of +consensus, defined as `v.round`: + +#### **[PBTS-SAFETY.0]** If -- there is a valid commit `C` for height `k` and round `r`, and +- there is a valid commit `C` for a value `v` - `C` contains a `PRECOMMIT` message from at least one correct process -Then, where `p` is one such correct process: +then there is a correct process `p` (not necessarily the same above considered) such that: -- since `p` is correct, `p` received a valid `POL(v,r)`, and -- `POL(v,r)` contains a `PREVOTE` message from at least one correct process, and -- `POL(v,r)` is derived from a timely `POL(v,r*)` with `r* <= r`, and -- `POL(v,r*)` contains a `PREVOTE` message from at least one correct process, and -- a correct process considered a proposal for `v` `timely` at round `r*`. +- `beginRound(p,v.round) <= proposalReceptionTime(p,v.round) <= beginRound(p,v.round+1)` and +- `proposalReceptionTime (p,v.round) - MSGDELAY - PRECISION <= v.time <= proposalReceptionTime(p,v.round) + PRECISION` -### LIVENESS +That is, a correct process `p` started round `v.round` and, while still at +round `v.round`, received a `PROPOSAL` message from round `v.round` proposing +`v`. +Moreover, the reception time of the original proposal for `v`, according with +`p`'s local clock, enabled `p` to consider the proposal time `v.time` as +`timely`. +This is the requirement established by PBTS for issuing a `PREVOTE` for the +proposal `(v, v.time, v.round)`, so for the eventual decision of `v`. -In terms of liveness, we need to ensure that a proposal broadcast by a correct process -will be considered `timely` by any correct process that is ready to accept that proposal. -So, if: +### Liveness -- the proposer `p` of a round `r` is correct, -- there is no `POL(v',r')` for any value `v'` and any round `r' < r`, -- `p` proposes a valid value `v` and sets `v.time` to the time it reads from its local clock, +The liveness of PBTS relies on correct processes accepting proposal times +assigned by correct proposers. +We thus present a set of conditions for assigning a proposal time `v.time` so +that every correct process should be able to issue a `PREVOTE` for `v`. -Then let `q` be a correct process that receives `p`'s proposal, we have: +#### **[PBTS-LIVENESS.0]** -- `q` receives `p`'s proposal after its clock reads `v.time - PRECISION`, and -- if `q` is at or joins round `r` while `p`'s proposal is being transmitted, -then `q` receives `p`'s proposal before its clock reads `v.time + MSGDELAY + PRECISION` +If -> Note that, before `GST`, we cannot ensure that every correct process receives `p`'s proposals, nor that it does it while ready to accept a round `r` proposal. +- the proposer of a round `r` of consensus is correct +- and it proposes a value `v` for the first time, with associated proposal time `v.time` -A correct process `q` as above defined must then consider `p`'s proposal `timely`. -It will then broadcast a `PREVOTE` message for `v` at round `r`, -thus enabling, from the Time-Validity point of view, `v` to be eventually decided. +then the proposal `(v, v.time, r)` is accepted by every correct process provided that: -#### Under-estimated `MSGDELAY`s +- `min{p is correct : beginRound(p,r)} <= v.time <= max{p is correct : beginRound(p,r)}` and +- `max{p is correct : beginRound(p,r)} <= v.time + MSGDELAY + PRECISION <= min{p is correct : beginRound(p,r+1)}` -The liveness assumptions of PBTS are conditioned by a conservative and clever -choice of the timing parameters, specially of `MSGDELAY`. -In fact, if the transmission delay for a message carrying a proposal is wrongly -estimated, correct processes may never consider a valid proposal as `timely`. +The first condition establishes a range of safe proposal times `v.time` for round `r`. +This condition is trivially observed if a correct proposer `p` sets `v.time` to the time it +reads from its clock when starting round `r` and proposing `v`. +A `PROPOSAL` message sent by `p` at local time `v.time` should not be received +by any correct process before its local clock reads `v.time - PRECISION`, so +that condition 2 of [PBTS-TIMELY.0] is observed. -To circumvent this liveness issue, which could result from a misconfiguration, -we assume that the `MSGDELAY` parameter can be increased as rounds do not -succeed on deciding a value, possibly because no proposal is considered -`timely` by enough processes. -The precise behavior for this workaround is under [discussion](https://github.com/tendermint/spec/issues/371). +The second condition establishes that every correct process should start round +`v.round` at a local time that allows `v.time` to still be considered timely, +according to condition 3. of [PBTS-TIMELY.0]. +In addition, it requires correct processes to stay long enough in round +`v.round` so that they can receive the `PROPOSAL` message of round `v.round`. +It assumed here that the proposer of `v` broadcasts a `PROPOSAL` message at +time `v.time`, according to its local clock, so that every correct process +should receive this message by time `v.time + MSGDELAY + PRECISION`, according +to their local clocks. Back to [main document][main].