mirrors/tendermint
1
0
Fork 0
mirror of https://github.com/tendermint/tendermint.git synced 2026-09-25 17:34:36 +00:00
Code Issues Packages Projects Releases Wiki Activity

PBTS: using proper Markdown subscripts in spec

Browse Source
This commit is contained in:
Daniel Cason
2022-05-24 18:28:31 +02:00
committed by Daniel
parent e9e2a0c63f
commit 455ad37d4e
1 changed files with 7 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files
spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md
+7 -7
View File
@@ -42,10 +42,10 @@ and drifts of local clocks from real time.
#### **[PBTS-CLOCK-PRECISION.0]** #### **[PBTS-CLOCK-PRECISION.0]**
There exists a system parameter `PRECISION`, such that There exists a system parameter `PRECISION`, such that
for any two processes `p` and `q`, with local clocks `C_p` and `C_q`: for any two processes `p` and `q`, with local clocks <code>C<sub>p</sub></code> and <code>C<sub>q</sub></code>:
- If `p` and `q` are equipped with synchronized clocks, - If `p` and `q` are equipped with synchronized clocks,
then for any real-time `t` we have `|C_p(t) - C_q(t)| <= PRECISION`. then for any real-time `t` we have <code>|C<sub>p</sub>(t) - C<sub>q</sub>(t)| <= PRECISION</code>.
`PRECISION` thus bounds the difference on the times simultaneously read by processes `PRECISION` thus bounds the difference on the times simultaneously read by processes
from their local clocks, so that their clocks can be considered synchronized. from their local clocks, so that their clocks can be considered synchronized.
@@ -60,12 +60,12 @@ processes from their clocks to real time.
For the sake of completeness, we define a parameter `ACCURACY` such that: 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 - At real time `t` there is at least one correct process `p` which clock marks
`C_p(t)` with `|C_p(t) - t| <= ACCURACY`. <code>C<sub>p</sub>(t)</code> with <code>|C<sub>p</sub>(t) - t| <= ACCURACY</code>.
As a consequence, applying the definition of `PRECISION`, we have: As a consequence, applying the definition of `PRECISION`, we have:
- At real time `t` the synchronized clock of any correct process `p` marks - At real time `t` the synchronized clock of any correct process `p` marks
`C_p(t)` with `|C_p(t) - t| <= ACCURACY + PRECISION`. <code>C<sub>p</sub>(t)</code> with <code>|C<sub>p</sub>(t) - t| <= ACCURACY + PRECISION</code>.
The reason for not adopting `ACCURACY` as a system parameter is the assumption The reason for not adopting `ACCURACY` as a system parameter is the assumption
that `PRECISION >> ACCURACY`. that `PRECISION >> ACCURACY`.
@@ -163,7 +163,7 @@ rounds, but the evaluation of the `timely` predicate is only relevant at round
> Considering the algorithm in the [arXiv paper][arXiv], a new proposal is > Considering the algorithm in the [arXiv paper][arXiv], a new proposal is
> produced by the `getValue()` method, invoked by the proposer `p` of round > produced by the `getValue()` method, invoked by the proposer `p` of round
> `round_p` when starting its proposing round with a nil `validValue_p`. > <code>round<sub>p</sub></code> when starting its proposing round with a nil <code>validValue<sub>p</sub></code>.
> The first round at which a value `v` is proposed is then the round at which > 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 > the proposal for `v` was produced, and broadcast in a `PROPOSAL` message with
> `vr = -1`. > `vr = -1`.
@@ -190,7 +190,7 @@ associated proposal time `v.time` is considered `timely`.
> Considering the algorithm in the [arXiv paper][arXiv], the `timely` predicate > Considering the algorithm in the [arXiv paper][arXiv], the `timely` predicate
> is evaluated by a process `p` when it receives a valid `PROPOSAL` message > 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`. > from the proposer of the current round <code>round<sub>p</sub></code> with `vr = -1`.
### Timely Proof-of-Locks ### Timely Proof-of-Locks
@@ -259,7 +259,7 @@ produced (by hypothesis) we can affirm that at least one correct process (also)
observed a `POL(v,vr)`. observed a `POL(v,vr)`.
> Considering the algorithm in the [arXiv paper][arXiv], `v` was proposed by > 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 > the proposer `p` of round <code>round<sub>p</sub></code> because its <code>validValue<sub>p</sub></code> variable was
> set to `v`. > set to `v`.
> The `PROPOSAL` message broadcast by the proposer, in this case, had `vr > -1`, > 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)`. > and it could only be accepted by processes that also observed a `POL(v,vr)`.