From e3da1bf94a3938cc16d8fdbdf992c1f6d9d663a2 Mon Sep 17 00:00:00 2001 From: Sergio Mena Date: Thu, 13 Jan 2022 11:04:38 +0100 Subject: [PATCH] Handle the distinction between 'any' occurrences (*) and 'infinite' occurrences (omega) in the grammar --- ...bci++_tmint_expected_behavior_002_draft.md | 28 ++++++++++++------- 1 file changed, 18 insertions(+), 10 deletions(-) diff --git a/spec/abci++/abci++_tmint_expected_behavior_002_draft.md b/spec/abci++/abci++_tmint_expected_behavior_002_draft.md index 0b5125f4c..4c3903fa0 100644 --- a/spec/abci++/abci++_tmint_expected_behavior_002_draft.md +++ b/spec/abci++/abci++_tmint_expected_behavior_002_draft.md @@ -34,20 +34,21 @@ Application design should consider _any_ of these possible sequences. The following grammar, written in case-sensitive Augmented Backus–Naur form (ABNF, specified in [IETF rfc7405](https://datatracker.ietf.org/doc/html/rfc7405)), specifies all possible -sequences of calls to ABCI++ across all heights from the genesis block, including recovery runs, -from the point of view of the Application. +sequences of calls to ABCI++, taken by a correct process, across all heights from the genesis block, +including recovery runs, from the point of view of the Application. ```abnf start = clean-start / recovery -clean-start = init-chain [state-sync] *consensus-height +clean-start = init-chain [state-sync] consensus-exec state-sync = *state-sync-attempt success-sync info state-sync-attempt = offer-snapshot *apply-chunk success-sync = offer-snapshot 1*apply-chunk -recovery = info *consensus-replay *consensus-height +recovery = info *consensus-replay consensus-exec consensus-replay = decide +consensus-exec = (inf)consensus-height consensus-height = *consensus-round decide consensus-round = proposer / non-proposer @@ -68,8 +69,6 @@ got-vote = %s"" decide = %s"" ``` ->**TODO** We need to get the grammar reviewed by the people that know block-execution inside out. - >**TODO** Still hesitating... introduce _n_ as total number of validators, so that we can bound the occurrences of >`got-vote` in a round. @@ -107,10 +106,10 @@ Let us now examine the grammar line by line, providing further details. * If the process is starting from scratch, Tendermint first calls `InitChain`, then it may optionally start a _state-sync_ mechanism to catch up with other processes. Finally, it enters normal - consensus execution, which is a sequence of zero or more consensus heights. + consensus execution. >```abnf ->clean-start = init-chain [state-sync] *consensus-height +>clean-start = init-chain [state-sync] consensus-exec >``` * In _state-sync_ mode, Tendermint makes one or more attempts at synchronizing the Application's state. @@ -129,13 +128,22 @@ Let us now examine the grammar line by line, providing further details. * In recovery mode, Tendermint first calls `Info` to know from which height it needs to replay decisions to the Application. To replay a decision, Tendermint simply calls `FinalizeBlock` with the decided - block at that height. After this, Tendermint enters nomal consensus execution: zero or more consensus heights. + block at that height. After this, Tendermint enters nomal consensus execution. >```abnf ->recovery = info *consensus-replay *consensus-height +>recovery = info *consensus-replay consensus-exec >consensus-replay = decide >``` +* The non-terminal `consensus-exec` is a key point in this grammar. It is an infinite sequence of + consensus heights. The grammar is thus an + [omega-grammar](https://dl.acm.org/doi/10.5555/2361476.2361481), since it produces infinite + sequences of terminals (i.e., the API calls). + +>```abnf +>consensus-exec = (inf)consensus-height +>``` + * A consensus height consists of zero or more rounds before deciding via a call to `FinalizeBlock`. In each round, the sequence of method calls depends on whether the local process is the proposer or not.