PBTS: new system model and problem statement #375
Conversation
cason
requested review from
ebuchman,
josef-widder,
konnov and
milosevic
as code owners
cason
requested review from
josef-widder and
williambanfield
and removed request for
josef-widder
spec/consensus/proposer-based-timestamp/pbts-algorithm_002_draft.md
Outdated
Show resolved
Hide resolved
spec/consensus/proposer-based-timestamp/pbts-algorithm_002_draft.md
Outdated
Show resolved
Hide resolved
spec/consensus/proposer-based-timestamp/pbts-algorithm_002_draft.md
Outdated
Show resolved
Hide resolved
spec/consensus/proposer-based-timestamp/pbts-algorithm_002_draft.md
Outdated
Show resolved
Hide resolved
spec/consensus/proposer-based-timestamp/pbts-algorithm_002_draft.md
Outdated
Show resolved
Hide resolved
|
|
||
| The adoption of an `ACCURACY` was intended to formalize the relation between a block time and the real time. | ||
| We observe, however, that clients will compare the block time to their local time, | ||
| or to the time they retrieve from a trusted source of time, not to a physical clock. |
There was a problem hiding this comment.
not to a physical clock
I'm not totally sure I understand what this phrase means since their local time is generated from a physical clock. I think this sentence is attempting to describe the fact that processes local clocks are not perfectly accurate, is that roughly correct?
There was a problem hiding this comment.
I don't like this description either. I will try to fix it.
There was a problem hiding this comment.
Please take a look on the new version.
spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md
Outdated
Show resolved
Hide resolved
There was a problem hiding this comment.
Looks great. Thanks! There are a couple a small issues raised by me and @williambanfield. Once they are fixed we should move forward and merge.
| The restriction imposed by the `PRECISION` parameter can then be used, indirectly, | ||
| to bound the difference block times and real time. |
There was a problem hiding this comment.
It would be good to be more explicit about "can then be used, indirectly".
spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md
Outdated
Show resolved
Hide resolved
| 1. `now_p >= v.time - PRECISION` and | ||
| 1. `now_p <= v.time + MSGDELAY + PRECISION` | ||
|
|
||
| ### Timely Proof-of-Locks |
There was a problem hiding this comment.
If I understand the structure of the document correctly, the following text is about analysis / correctness arguments. If this is right, perhaps we should add a header making this more explicit.
There was a problem hiding this comment.
Not sure that it is TLA+ related. I guess the point is just that the following text is more interesting when one wants to understand correctness (rather than protocol details). Perhaps we can discuss this synchronously.
There was a problem hiding this comment.
I've added some headers to the latest version.
|
We merge the current state. @cason will add a README that explains the status of the files that is
|
|
I think this branch is still not mergeable with master, needing a rebase. Can you confirm that? I don't have the option to merge the branch, @williambanfield can you help me (again) with this :D |
…ft.md Co-authored-by: William Banfield <4561443+williambanfield@users.noreply.github.com>
Co-authored-by: William Banfield <4561443+williambanfield@users.noreply.github.com>
Co-authored-by: Josef Widder <44643235+josef-widder@users.noreply.github.com>
It seems that some of the changes listed here were already addressed by the previous PR.
This PR essentially adds
pbts-sysmodel_002_draft.md, a new version ofpbts-sysmodel_001_draft.md.Not all the properties and references to the TLA spec are included, and this PR will probably require more commits and some discussions.