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 +41,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`.
For the sake of completeness, we define a parameter `ACCURACY` such that:
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:
- At real time `t` there is at least one correct process `p` which clock marks
`C_p(t)` with `|C_p(t) - t| <= ACCURACY`.
##### **[PBTS-CLOCK-FAIR.0]**
As a consequence, applying the definition of `PRECISION`, we have:
- At real time `t` there is at least one correct process `p` which clock marks
`C_p(t)` with `|C_p(t) - t| < ACCURACY`
- At real time `t` the synchronized clock of any correct process `p` marks
`C_p(t)` with `|C_p(t) - t| <= ACCURACY + PRECISION`.
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.
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,116 +85,191 @@ 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.
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
For PBTS, a `proposal` is a tuple `(v, v.time, v.round)`, where:
> Both [Validity] and [Time-Validity] must be observed even if up to `2f` validators are faulty.
- `v` is the proposed value;
- `v.time` is the associated proposal time;
- `v.round` is the round at which `v` was first proposed.
### Timely proposals
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:
- `receiveTime_p[r]` is the time `p` reads from its local clock when `p` is at
round `r` and receives the proposal of round `r`.
#### **[PBTS-TIMELY.0]**
The proposal `(v, v.time, v.round)` is considered `timely` by a correct process
`p` if:
1. `receiveTime_p[v.round]` is set, and
1. `receiveTime_p[v.round] >= v.time - PRECISION`, and
Daniel
3 years ago
GitHub