PBTS: using proper Markdown subscripts in spec

This commit is contained in:
Daniel Cason
2022-05-12 16:54:04 +02:00
parent 858358aa8d
commit 444ed8c679
@@ -24,17 +24,14 @@ Since the originally proposed value and its associated time were considered vali
Values decided in successive heights of consensus must have increasing times, so:
- Monotonicity: for any process `p` and any two decided heights `h` and `h'`, if `h > h'` then `decision_p[h].time > decision_p[h'].time`.
- Monotonicity: for any process `p` and any two decided heights `h` and `h'`, if `h > h'` then `decision<sub>p</sub>[h].time > decision<sub>p</sub>[h'].time`.
For ensuring time monotonicity, it is enough to ensure that a value `v` proposed by process `p` at height `h_p` has `v.time > decision_p[h_p-1].time`.
So, if process `p` is the proposer of a round of height `h_p` and reads from its clock a time `now_p <= decision_p[h_p-1]`,
it should postpone the generation of its proposal until `now_p > decision_p[h_p-1]`.
For ensuring time monotonicity, it is enough to ensure that a value `v` proposed by process `p` at height `h<sub>p</sub>` has `v.time > decision<sub>p</sub>[h<sub>p</sub>-1].time`.
So, if process `p` is the proposer of a round of height `h<sub>p</sub>` and reads from its clock a time `now<sub>p</sub> <= decision<sub>p</sub>[h<sub>p</sub>-1]`,
it should postpone the generation of its proposal until `now<sub>p</sub> > decision<sub>p</sub>[h<sub>p</sub>-1]`.
> Although it should be considered, this scenario is unlikely during regular operation,
as from `decision_p[h_p-1].time` and the start of height `h_p`, a complete consensus instance need to terminate.
Notice that monotonicity is not introduced by this proposal, being already ensured by [`BFTTime`][bfttime].
In `BFTTime`, the `Timestamp` field of every `Precommit` message of height `h_p` sent by a correct process is required to be larger than `decision_p[h_p-1].time`, as one of such `Timestamp` fields becomes the time assigned to a value proposed at height `h_p`.
as from `decision<sub>p</sub>[h<sub>p</sub>-1].time` and the start of height `h<sub>p</sub>`, a complete consensus instance need to terminate.
The time monotonicity of values proposed in heights of consensus is verified by the `valid()` predicate, to which every proposed value is submitted.
A value rejected by the `valid()` implementation is not accepted by any correct process.
@@ -50,18 +47,18 @@ It is a temporal requirement, associated with the following synchrony (that is,
#### **[PBTS-RECEPTION-STEP.1]**
Let `now_p` be the time, read from the clock of process `p`, at which `p` receives the proposed value `v`.
Let `now<sub>p</sub>` be the time, read from the clock of process `p`, at which `p` receives the proposed value `v`.
The proposal is considered `timely` by `p` when:
1. `now_p >= v.time - PRECISION`
1. `now_p <= v.time + MSGDELAY + PRECISION`
1. `now<sub>p</sub> >= v.time - PRECISION`
1. `now<sub>p</sub> <= v.time + MSGDELAY + PRECISION`
The first condition derives from the fact that the generation and sending of `v` precedes its reception.
The minimum receiving time `now_p` for `v` be considered `timely` by `p` is derived from the extreme scenario when
The minimum receiving time `now<sub>p</sub>` for `v` be considered `timely` by `p` is derived from the extreme scenario when
the clock of `p` is `PRECISION` *behind* of the clock of the proposer of `v`, and the proposal's transmission delay is `0` (minimum).
The second condition derives from the assumption of an upper bound for the transmission delay of a proposal.
The maximum receiving time `now_p` for `v` be considered `timely` by `p` is derived from the extreme scenario when
The maximum receiving time `now<sub>p</sub>` for `v` be considered `timely` by `p` is derived from the extreme scenario when
the clock of `p` is `PRECISION` *ahead* of the clock of the proposer of `v`, and the proposal's transmission delay is `MSGDELAY` (maximum).
## Updated Consensus Algorithm