Re: [tlaplus] How to understand onTimeOutxxx in this TenderMint spec's?

[Igor Konnov <igor.konnov@xxxxxxxxx>]

Hi Anthony,

The specification [2] that you pointed to is an extension of [1],
which enumerates assumptions in more detail in the comments. In [1],
we only modelled onTimeoutPropose, but not onTimeoutPrevote and
onTimeoutPrecommit. This decision was made in the conversations with
the algorithm designers, since they wanted to check the safety
properties with Apalache, namely, Agreement and Accountability. The
action onTimeoutPropose is entirely non-deterministic. It may fire as
soon as the conditions hold true, no clock conditions are checked. In
this sense, the action onTimeoutPropose in [1] is an overapproximation
of the handler in the pseudo-code [3]. This kind of overapproximation
is quite common, if we focus on safety properties. It would lead to
false positives, when we want to check liveness.

It is quite easy to add non-deterministic versions of onTimeoutPrevote
and onTimeoutPrecommit, similar to onTimeoutPropose. However, it
should not change anything with respect to safety. If you want to
check liveness, you would have to: (1) Add three local timers per
process and constraints over them, and (2) add timestamps to the sent
messages, (3) add constraints on which messages can be received using
the timestamps and message delays. It is less obvious how to specify
the period of asynchrony that precedes the global stabilization time
(GST).

It may seem confusing that [2] contains clocks but no timeouts. The
clocks in [2] serve a different purpose. They are modeling timestamps
that are sent by the block proposers. As a result, the processes not
only have to agree on the proposed block but also on the timestamp
attached to that block.

[1] https://github.com/cometbft/cometbft/blob/main/spec/light-client/accountability/TendermintAcc_004_draft.tla
[2] https://github.com/cometbft/cometbft/blob/main/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_001_draft.tla
[3] https://arxiv.org/pdf/1807.04938

Cheers,
Igor

On Fri, Dec 6, 2024 at 10:06 PM Anthony Lee <anthonynlee@xxxxxxxxx> wrote:
>
> In paper "The latest gossip on BFT consensus"  Tendermint algorithm is descried in pseudocode, and here is a TLA+ spec for it.
>
> I'm confused in how the timer for step Propose/Prevote/PreCommit is scheduled.
>
> OnTimeoutPropose action condition shows that when step is propose but Proposer is not p
> then it is timeout. Each round has its own proposer, so I searched to see where a new round can be started, I found that UponQuorumOfPrecommitsAny(p) and OnRoundCatchup(p) trigger StartRound(p,r);
>
> For UponQuorumOfPrecommitsAny, there is comment saying that it should be called in onTimeoutPrecommit, but there is no onTimeoutPrecommit in the TLA.
>
>  I don't understand how timeout is implemented in this TLA and why there is no need to define onTimeoutPrevote or onTimeoutPrecommit.
>
> Please help to explain.
>
> Thanks.
> Anthony
>
>
>
> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
> To view this discussion visit https://groups.google.com/d/msgid/tlaplus/1bd42a42-9e22-408f-8c53-293ce699f136n%40googlegroups.com.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CACooHMC1ySALbZga1fUh38F-cbbancb33LqnEeBakU6OkqHasg%40mail.gmail.com.