Do we break validBlock property if a process can leave round upon receiving 2f+1 Precommit nil messages?

[milosevic]

Let assume that we are in the period after GST. A correct process p sent Precommit id(v) message at time t in round r. By validBlock property, every correct process that enters round r+1 should receive the same Polka p received before leaving round r.

The process p received valid Proposal and 2f+1 matching Prevote messages at time t. At least f+1 of those Prevote messages is from correct processes, and let denote this set of correct processes with C. By majority intersection property, any set of 2f+1 Prevote messages in round r contains at least single message from the set C. Let denote with time t1, the earliest point in time a process from C sent it's Prevote message in round r.

Note that a correct process can't send Precommit message before receiving 2f+1 Prevote messages. Therefore, no correct process can send Precommit message in round r before time t1.
If a correct process q send Precommit nil message, this implies that he waited timeoutPrevote before. Therefore, no correct process can send Precommit nil before time t1 + timeoutPrevote. Let assume that some correct process q received 2f+1 Precommit nil messages at time t1 + timeoutPrevote. According to current version of algorithm, q will start round r+1 at time t1 + timeoutPrevote.

If a correct process has started timeoutPrevote at time t1, this implies it receives 2f+1 Prevote messages. Therefore, every correct process will start timeoutPrevote the latest at time t1 + Delta (as we are in period after GST). So the latest point in time p can send Precommit v is t1 + Delta + timeoutPrevote.

Note that if a faulty process sends Prevote v to p just before timeout expires, p might send Precommit v at time t1 + Delta + timeoutPrevote, and process q at that point in time already left round r.

The potential solution for this issue is introducing timeoutPrecommit in case a process receives 2f+1 Precommit nil before it starts round r+1.

[jaekwon]

Awesome, thank you. Here’s a stab at the proof in terms of the updated protocol.

Say that the earliest a correct processor sends a precommit is time T_a. The last time a correct process precommits is T_a + Delta due to gossiping of prevotes (after GST, Delta is finite and defined by network conditions and number of validators etc). Delta is thus also the maximum bound between when the first correct process and last correct process can pre-commit.

There exists some round R after GST where Delta (prevotes) + Delta (polka) < timeout_precommit where precommit_timeout is sufficiently long for the polka to be broadcast from the victim correct validator to all correct validators before round r+1. And if the proposer at r+1 is correct then we’re going to terminate at r+1. So there exists some r after GST where all conditions are satisfied and we terminate.

[jaekwon]

Here's the corresponding update to the consensus algo:

diff --git a/consensus/state.go b/consensus/state.go
index 338a14a9..2ae49b8d 100644
--- a/consensus/state.go
+++ b/consensus/state.go
@@ -1524,7 +1524,9 @@ func (cs *ConsensusState) addVote(vote *types.Vote, peerID p2p.ID) (added bool,
                blockID, ok := precommits.TwoThirdsMajority()
                if ok {
                        if len(blockID.Hash) == 0 {
-                               cs.enterNewRound(height, vote.Round+1)
+                               cs.enterNewRound(height, vote.Round)
+                               cs.enterPrecommit(height, vote.Round)
+                               cs.enterPrecommitWait(height, vote.Round)
                        } else {
                                cs.enterNewRound(height, vote.Round)
                                cs.enterPrecommit(height, vote.Round)

[jaekwon]

Just noting that this is related to but distinct from #1745 which is already merged in. The above issue is about prevotes/precommits of +2/3 any, where as this issue is about precommits of +2/3 nil, two separate issues.

[ebuchman]

Done in #2493