Browse Source

Align protocol with Tendermint code and add find valid value mechanism

pull/7804/head
Zarko Milosevic 7 years ago
parent
commit
2866ba1a2c
7 changed files with 243 additions and 131 deletions
  1. +25
    -0
      README.md
  2. +155
    -94
      consensus.tex
  3. +40
    -32
      definitions.tex
  4. +18
    -0
      lit.bib
  5. +3
    -1
      paper.tex
  6. +2
    -0
      proof.tex
  7. +0
    -4
      readme.md

+ 25
- 0
README.md View File

@ -0,0 +1,25 @@
# Tendermint-spec
The repository contains the specification (and the proofs) of the Tendermint
consensus protocol.
## How to install Latex on Mac OS
MacTex is Latex distribution for Mac OS. You can download it [here](http://www.tug.org/mactex/mactex-download.html).
Popular IDE for Latex-based projects is TexStudio. It can be downloaded
[here](https://www.texstudio.org/).
## How to build project
In order to compile the latex files (and write bibliography), execute
`$ pdflatex paper` <br/>
`$ bibtex paper` <br/>
`$ pdflatex paper` <br/>
`$ pdflatex paper` <br/>
The generated file is paper.pdf. You can open it with
`$ open paper.pdf`

+ 155
- 94
consensus.tex View File

@ -2,10 +2,13 @@
\section{Tendermint}
\label{sec:tendermint}
\newcommand\Propose{\mathsf{PROPOSAL}}
\newcommand\Disseminate{\textbf{Disseminate}}
\newcommand\Proposal{\mathsf{PROPOSAL}}
\newcommand\ProposalPart{\mathsf{PROPOSAL\mbox{-}PART}}
\newcommand\PrePrepare{\mathsf{INIT}}
\newcommand\Prepare{\mathsf{PREVOTE}}
\newcommand\Commit{\mathsf{PRECOMMIT}}
\newcommand\Prevote{\mathsf{PREVOTE}}
\newcommand\Precommit{\mathsf{PRECOMMIT}}
\newcommand\Decision{\mathsf{DECISION}}
\newcommand\ViewChange{\mathsf{VC}}
@ -13,13 +16,17 @@
\newcommand\NewPrePrepare{\mathsf{VC\mbox{-}INIT}}
\newcommand\coord{\mathsf{proposer}}
\newcommand\initState{init}
\newcommand\preVoted{pre\mbox{-}voted}
\newcommand\preCommitted{pre\mbox{-}committed}
\newcommand\newHeight{newHeight}
\newcommand\newRound{newRound}
\newcommand\nil{nil}
\newcommand\prevote{prevote}
\newcommand\precommit{precommit}
\newcommand\commit{commit}
\newcommand\timeoutPropose{timeoutPropose}
\newcommand\timeoutPrevote{timeoutPrevote}
\newcommand\timeoutCommit{timeoutPreCommit}
\newcommand\timeoutPrecommit{timeoutPrecommit}
\newcommand\proofOfLocking{proof\mbox{-}of\mbox{-}locking}
\begin{algorithm}[htb!]
\def\baselinestretch{1}
@ -27,14 +34,13 @@
\begin{algorithmic}[1]
\SHORTSPACE
\INIT{}
\STATE $v_p := v \in V$ \COMMENT{value considered for consensus}
\STATE $height_p := 0$ \COMMENT{current height, or consensus instance we are currently executing}
\STATE $round_p := 0$ \COMMENT{current round number}
\STATE $vote_p := nill$ \COMMENT{locked value}
\STATE $ts_p := -1$ \COMMENT{ if $ts_p \ge 0$, it represents round in which $vote_p$ has been locked}
\STATE $proof_p := \emptyset$ \COMMENT{set of signed messages as a proof that $vote_p$ has been locked in round $ts_p$}
\STATE $state_p \in \set{\initState=0,\preVoted=1,\preCommitted=2}$, initially $\initState$
\STATE $decision_p = nill$
\STATE $step_p \in \set{\propose=0, \prevote=1, \precommit=2, \commit=3}$, initially $\propose$ \COMMENT{current round step}
\STATE $lockedValue := nil$
\STATE $lockedRound := -1$
\STATE $validValue := nil$
\STATE $validRound := -1$
\ENDINIT
\SPACE
@ -45,144 +51,199 @@
\SPACE
\FUNCTION{$StartRound(round)$} \label{line:tab:startRound}
\STATE $round_p \assign round$
\STATE $state_p \assign init$
\IF{$\coord(round_p) = p$}
\IF{$ts_p \ge 0$}
\STATE $proposal \assign vote_p$
\ELSE
\STATE $proposal \assign v_p$
\ENDIF
\STATE \PBroadcast\ $\li{\Propose,round_p,proposal,ts_p, proof_p}$ to all \label{line:tab:send-propose}
\STATE $state_p \assign \propose$
\IF{$\coord(height_p, round_p) = p$}
\IF{$lockedValue_p \neq \nil$}
\STATE $proposal \assign lockedValue$
\ELSIF{$validValue_p \neq \nil$}
\STATE $proposal \assign validValue$
\ELSE
\STATE $proposal \assign getValue()$
\ENDIF
\STATE \PBroadcast\ $\li{\Proposal,height_p, round_p, proposal}$ to all \label{line:tab:send-proposal}
\ENDIF
\STATE \textbf{after} $\timeoutPropose$ execute $OnTimeoutPropose(round_p)$
\STATE \textbf{after} $\timeoutPropose$ execute $OnTimeoutPropose(height_p, round_p)$
\ENDFUNCTION
\SPACE
\UPON{receiving $\li{\Propose,round_p, vote, ts, proof}$ \From\ $\coord(round_p)$ \With\ $state_p = \initState$} \label{line:tab:recvInit}
\IF{$isValidProposal(vote,ts,proof)$}
\STATE \PBroadcast \ $\li{\Prepare,round_p,vote}$ to all \label{line:tab:send-echo}
\STATE $state_p \assign \preVoted$ \label{line:tab:setStateToEchoed}
\IF{$vote \neq vote_p \wedge ts > ts_p$}
\STATE $vote_p \assign nill$
\STATE $ts_p \assign -1$
\ENDIF
\UPON{receiving $\li{\Proposal,height_p,round_p, proposal}$ \From\ $\coord(height_p,round_p)$ \With\ $state_p = \propose$} \label{line:tab:recvProposal}
\IF{$lockedValue_p \neq \nil$} \label{line:tab:hasLockedValue}
\STATE \PBroadcast \ $\li{\Prevote,height_p,round_p,lockedValue_p}$ to all \label{line:tab:send-locked-value}
\ELSIF{$valid(proposal))$} \label{line:tab:locked-value-nil}
\STATE \PBroadcast \ $\li{\Prevote,height_p,round_p,proposal}$ to all \label{line:tab:send-prevote}
\ELSE
\STATE \PBroadcast \ $\li{\Prevote,height_p,round_p,\nil}$ to all \label{line:tab:send-prevote-nil}
\ENDIF
\STATE $state_p \assign \prevote$ \label{line:tab:setStateToPrevote}
\ENDUPON
\SPACE
\FUNCTION{$OnTimeoutPropose(round)$} \label{line:tab:onTimeoutPropose}
\IF{$round = round_p \wedge state_p = \initState$}
\STATE \PBroadcast \ $\li{\Prepare,round_p,nill}$ to all
\STATE $state_p \assign \preVoted$
\FUNCTION{$OnTimeoutPropose(height,round)$} \label{line:tab:onTimeoutPropose}
\IF{$height = height_p \wedge round = round_p \wedge state_p = \propose$}
\STATE \PBroadcast \ $\li{\Prevote,height_p,round_p,\nil}$ to all
\STATE $state_p \assign \prevote$
\ENDIF
\ENDFUNCTION
\SPACE
\UPON{receiving $\li{\Prepare,round,vote}$ \From\ $2f+1$ processes \With\
($round = round_p \wedge state_p \le \preVoted$) or $round > round_p$} \label{line:tab:recvEcho}
\STATE $vote_p \assign vote$ \label{line:tab:setV}
\IF{$vote = nill$}
\STATE $ts_p \assign -1$
\UPON{receiving $\li{\Prevote,height_p, round_p,*}$ \From\ at least $2f+1$ processes \With\
$state_p \le \prevote$} \label{line:tab:recvAny2/3Prevote}
\STATE \textbf{after} $\timeoutPrevote$ execute $OnTimeoutPrevote(height_p, round_p)$ \label{line:tab:timeoutPrevote}
\ENDUPON
\SPACE
\UPON{receiving $\li{\Prevote,height_p, round_p,v}$ \From\ at least $2f+1$ processes \With\
$state_p \le \prevote$} \label{line:tab:recvPrevote}
\IF{$v \neq \nil$}
\STATE $lockedValue_p \assign v$ \label{line:tab:setLockedValue}
\STATE $lockedRound_p \assign round_p$ \label{line:tab:setLockedRound}
\STATE \PBroadcast \ $\li{\Precommit,height_p,round_p,lockedValue_p}$ to all \label{line:tab:send-precommit}
\ELSE
\STATE $ts_p \assign round$ \label{line:tab:setTs}
\STATE \PBroadcast \ $\li{\Precommit,height_p,round_p,\nil}$ to all \label{line:tab:send-precommit-nil}
\ENDIF
\STATE $round_p \assign round$
\STATE \PBroadcast \ $\li{\Commit,round_p,vote_p}$ to all \label{line:tab:send-commit}
\STATE $state_p \assign \preCommitted$ \label{line:tab:setStateToCommitted}
\STATE $proof_p \assign$ \{set of received signed messages\}
\STATE $state_p \assign \precommit$ \label{line:tab:setStateToCommit}
\ENDUPON
\SPACE
\UPON{receiving $\li{\Prepare,round_p,*}$ \From\ $2f+1$ processes \With\
$state_p = \preVoted$ \COMMENT{a sign * denotes any value}}
\STATE \textbf{after} $\timeoutPrevote$ execute $OnTimeoutPrevote(round_p)$
\UPON{receiving $\li{\Prevote,height_p,round,v}$ \From\ at least $2f+1$ processes \With\
$round > lockedRound_p$} \label{line:tab:unlockRule}
\IF{$v \neq lockedValue_p$}
\STATE $lockedValue_p \assign \nil$
\STATE $lockedRound_p \assign -1$
\ENDIF
\ENDUPON
\SPACE
\FUNCTION{$OnTimeoutPrevote(round)$} \label{line:tab:onTimeoutPrevote}
\IF{$round = round_p \wedge state_p = \preVoted$}
\STATE \PBroadcast \ $\li{\Commit,round_p,nill}$ to all
\STATE $state_p \assign \preCommitted$
\UPON{receiving $\li{\Prevote,height_p,round,v}$ \From\ at least $2f+1$ processes \With\
$v \neq \nil \wedge round > validRound_p$} \label{line:tab:validValueRule}
\STATE $validValue_p \assign v$ \label{line:tab:setValidValue}
\STATE $validRound_p \assign round$ \label{line:tab:setValidRound}
\ENDUPON
\SPACE
\FUNCTION{$OnTimeoutPrevote(height,round)$} \label{line:tab:onTimeoutPrevote}
\IF{$height = height_p \wedge round = round_p \wedge state_p = \prevote$}
\STATE \PBroadcast \ $\li{\Precommit,height_p,round_p,\nil}$ to all \label{line:tab:precommit-nil-onTimeout}
\STATE $state_p \assign \precommit$
\ENDIF
\ENDFUNCTION
\SPACE
\UPON{receiving ($\li{\Commit,round,vote}$ \From\ $2f+1$ processes \With\ $round \ge round_p$} \label{line:tab:recvCommit}
\IF{$vote \neq nill \wedge decision_p = nill$}
\STATE $decision_p \assign vote$ \label{line:tab:setStateToDecided}
\UPON{receiving $\li{\Precommit,height_p,round,v}$ \From\ at least $2f+1$ processes \With\ $state_p < \commit$} \label{line:tab:onPrecommitRule}
\IF{$vote \neq \nil$}
\STATE $decide(height_p, v)$ \label{line:tab:decide}
\STATE$height_p \assign height_p + 1$
\STATE reset $round_p$, $step_p$, $lockedRound_p$, $lockedValue_p$, $validValue_p$ and $validRound$ to init values
\STATE $StartRound(0)$
\ENDIF
\STATE $StartRound(round+1)$
\IF{$round_p = round$}
\STATE $StartRound(round_p+1)$
\ENDIF
\ENDUPON
\SPACE
\UPON{receiving $\li{\Commit,round_p,*}$ \From\ $2f+1$ processes \With\
$state_p = \preCommitted$ \COMMENT{a sign * denotes any value}}
\STATE \textbf{after} $\timeoutPreCommit$ execute $OnTimeoutPreCommit(round_p)$
\UPON{receiving $\li{\Precommit,height_p,round_p,*}$ \From\ at least $2f+1$ processes \With\ $state_p = \precommit$} \label{line:tab:startTimeoutPrecommit}
\STATE \textbf{after} $\timeoutPrecommit$ execute $OnTimeoutPrecommit(height_p, round_p)$
\ENDUPON
\SPACE
\FUNCTION{$OnTimeoutPreCommit(round)$} \label{line:tab:onTimeoutCommit}
\IF{$round = round_p \wedge state_p = \preCommitted$}
\STATE $StartRound(round+1)$
\FUNCTION{$OnTimeoutPrecommit(height,round)$} \label{line:tab:onTimeoutPrecommit}
\IF{$height = height_p \wedge round = round_p \wedge state_p = \precommit$}
\STATE $StartRound(round_p+1)$
\ENDIF
\ENDFUNCTION
\SPACE
\UPON{receiving message \textbf{with} $round > round_p$ \From\ $f+1$ processes} \label{line:tab:skipViews}
\STATE $StartRound(round)$
\UPON{receiving message \textbf{with} $height = height_p$ and $round > round_p$ \From\ at least $f+1$ processes} \label{line:tab:skipRounds}
\STATE $StartRound(round)$
\ENDUPON
\SPACE
\FUNCTION{$isValidProposal(vote, ts, proof)$} \label{line:tab:isValidProposal}
\IF{$vote = vote_p \vee ts_p = -1$}
\STATE \textbf{return} true
\ENDIF
\IF{$ts > ts_p$ \textbf{and} $proof$ confirms that $vote$ was locked at round $ts$}
\STATE \textbf{return} true
\ENDIF
\STATE \textbf{return} false
\ENDFUNCTION
\end{algorithmic}
\caption{Tendermint consensus algorithm}
\label{alg:tendermint}
\end{algorithm}
\textbf{NOTE: The algorithm description and the corresponding proofs refers to the previous version of the pseudocode and needs to be updated!}
In this section we present a new Byzantine consensus algorithm called Tendermint\footnote{https://github.com/tendermint/tendermint}
(see Algorithm~\ref{alg:tendermint}).
The algorithm requires $n > 3f$ processes to tolerate at most f Byzantine faults, but for simplicity we present the algorithm for the case $n = 3f + 1$. The upon rules of Algorithm~\ref{alg:tendermint} are executed atomically.
The algorithm requires $N > 3f$, i.e., faulty processes have together the voting power that is smaller than one third of the total voting power. For simplicity we present the algorithm for the case $N = 3f + 1$. We use the notation "upon receiving message $\li{TAG, h, r, v}$ from at least $X$ processes", to denote that a message with the given field values (* denotes any value) has been received from number of processes with the aggregate voting power equals at least $X$.
The upon rules of Algorithm~\ref{alg:tendermint} are executed atomically.
Algorithm shares the basic mechanisms called the locking and the unlocking of a value with the DLS algorithm for authenticated faults (the Algorithm 2 from \cite{DLS88:jacm}), but the algorithm structure and the implementation of these mechanisms is different in Tendermint.
Tendermint consensus algorithm is optimized for the gossip based communication so the consensus layer creates a minimum number of information that needs to be gossiped. Processes exchange only three message types: $\Proposal$, $\Prevote$ and $\Precommit$, and there is only a single mode of execution, i.e., there is no separation between the normal and the recovery mode, which is the case in PBFT-like protocols (e.g., \cite{CL02:tcs}, \cite{Ver09:spinning} or \cite{Cle09:aardvark}). We believe that this makes the protocol simpler to understand and implement correctly, as one of the Tendermint goals is proposing \emph{understandable} Byzantine consensus protocol following Raft path~\cite{Ongaro14:raft}.
The algorithm proceeds in a sequence of rounds, where each round has a dedicated coordinator (called proposer). The assignment scheme of rounds to coordinators is known to all processes and is given as a function $\coord(height, round)$ returning the coordinator for round $r$ in the consensus instance $height$. In the algorithm~\ref{alg:tendermint} processes agree (decides) on a sequence of values (solves multiple instances problem) by sequentially executing one consensus instances after the other.
Tendermint decomposes the consensus problem into four relatively independent mechanisms (or subproblems) which are discussed in the following subsections:
\begin{itemize}
\item locking mechanism
\item unlocking mechanism
\item finding the right value to propose
\end{itemize}
\subsection{Locking mechanism}
\label{sec:locking}
A process in Tendermint initially does not have any preference about what the decided value should be ($lockedValue := nil$). The process learns about possible decision value from the coordinator of the current round. As a proposer might be a faulty process, different processes
might receive different suggestions. Using the locking mechanism, correct processes try to converge to a single value within the single round boundary\footnote{We will explain in the part related to safety how we will build on this mechanism to ensure safety across round boundaries.}.
If during the locking phase, a sufficient number of correct processes succeed in agreeing on the common value, then they will later decide on that value.
More formally, the locking mechanism ensures that two correct processes can lock only a single value in some round $r$ (they can however potentially lock different values in distinct rounds). In Algorithm~\ref{alg:tendermint}, a correct process $p$ locks a value $v$ in round $r$ by setting a variable $lockedValue_p$ to $v$ and a variable $lockedRound_p$ to $r$ (see line~\ref{line:tab:setLockedValue} and \ref{line:tab:setLockedRound}). A correct process can have only a single value locked at a particular point of the algorithm execution.
However, before a value is decided, a process might change his mind and unlock its current value using the unlocking mechanism.
It shares the basic mechanisms called locking and unlocking of a value with DSL algorithm for authenticated faults (Algorithm 2 from \cite{DLS88:jacm}), but algorithm structure and implementation of these mechanisms is different in Tendermint.
Locking phase starts by a process suggesting what value should be locked in the current round. This is achieved by sending a $\Prevote$ message to all processes. If a correct process has locked some value $v$ ($lockedValue = v \neq \nil$), he votes for $v$ and ignores the suggested value by the proposer (see lines~\ref{line:tab:hasLockedValue}-\ref{line:tab:send-locked-value}). Otherwise, a process might accept the value suggested by the proposer if the proposal is valid\footnote{Validity of a value is an application specific and defined by the function \emph{valid()}.}, and vote for that value (see lines~\ref{line:tab:locked-value-nil}-\ref{line:tab:setStateToPrevote}). In case the suggested value is invalid or a process has not received any proposal from the current coordinator within $\timeoutPropose$ from the start of the current round, it votes with $\nil$ value (see line~\ref{line:tab:send-prevote-nil} and line \ref{line:tab:onTimeoutPropose}). Note that $\nil$ is special value that can not be locked, and it is used to inform others that the algorithm step has not completed successfully; in case of the locking phase, a process has not received a valid value from the proposer on time.
The algorithm proceeds in a sequence of rounds, where each round has a dedicated coordinator (called also proposer), that is defined with a deterministic function $\coord$. A correct process moves to a higher round either if a round timeout has expired (line 37) or if process receives a message from a correct process that is in a higher round (lines 26-27). We assume that messages from higher rounds are internally stored by the messaging layer (in case the rule from line 26 is satisfied, round transition is triggered), and then delivered to a process when it enters the corresponding round. Messages from lower rounds are dropped.
A process locks value $v$ if it receives at least $2f+1$ $\Prevote$ messages for the value $v$ in the current round (see lines~\ref{line:tab:recvPrevote}-\ref{line:tab:setLockedRound}). A correct process sends only a single $\Prevote$ message in every round. Algorithm relies on the $state$ variable to prevent correct processes from sending more than one $\Prevote$ message in a single round. As a correct process sends a single $\Prevote$ message in a round, and $f$ is the total voting power of faulty processes, two correct processes cannot receive $2f+1$ $\Prevote$ messages for different values in a single round. So if two correct processes lock some value in a given round $r$, then it must be the same value. We will prove this formally in the section~\ref{sec:proof}.
The locking mechanism has a role in ensuring agreement property of consensus, while the unlocking mechanism is related to termination property. Locking guarantees that two correct processes can lock only single value in some round $r$ (they can however potentially lock different values in distinct rounds). A correct process can have only a single value locked at a particular point of algorithm execution. In Algorithm~\ref{alg:tendermint}, a correct process $p$ locks a value $v$ in round $r$ by setting a variable $vote_p$ to $v$ and a variable $ts_p$ to $r$. The unlocking mechanism ensures that eventually (after GST) all correct processes can have only single value $v$ locked. This helps to bring system into univalent configuration~\cite{FLP85:jacm}. In Algorithm~\ref{alg:tendermint}, a process $p$ unlocks a value by setting $vote_p$ to $null$ and $ts_p$ to -1. Initially, all correct process do not lock any value.
The locking phase ends by processes informing others if they locked some value in the current round (or not) by sending $\Precommit$ message. If a process has locked some value $v$ in the current round, then this value is sent in the $\Precommit$ message (see line~\ref{line:tab:send-precommit}); otherwise $\nil$ is sent (line~\ref{line:tab:send-precommit-nil} and \ref{line:tab:precommit-nil-onTimeout}). A correct process sends only single $\Precommit$ message in every round. Similarly as with the $\Prevote$ message, the algorithm relies on the $state$ variable to prevent correct processes from sending more than one $\Precommit$ message in a single round.
Each round is composed of three phases (steps) called propose, prepare and commit. A round starts with a propose phase (lines 28-37) in which a dedicated proposer sends its proposal to all processes. If a proposer $p$ has locked some value $v$, then it proposes $v$; otherwise it proposes it's initial value $v_p$ (lines 32-35). In addition to proposed value, $\Propose$ message also contains $ts$ and a proof of locking a value (in case proposal is equal to locked value), that consist of a set of signed messages received by the process $p$ in the round in which the value was locked.
\subsection{Unlocking mechanism}
\label{sec:unlocking}
When a correct process receives a proposal message from a designated proposer (lines 11-17), it checks if the message is a valid proposal (lines 41-46). A correct process $p$ considers proposal as valid if (i) proposal value is equal to process locked value ($vote_p$) or if $p$ hasn't locked any value ($ts_p = -1$), or (ii) if proposal is different value but from a higher round and with a valid proof of locking. If a process accepts proposal as valid, it enters prepare phase by sending proposed value in $\Prepare$ message to all processes. In case (ii), as there is a valid locked value in a higher round, the process unlocks it's value.
Initially, a correct process does not lock any value. During the algorithm execution, processes might end up locking different values in different rounds. As we discussed in the locking section (section~\ref{sec:locking}), a correct process that has locked some value will vote
only for that value at the beginning of the locking phase. With correct processes voting for different values during the locking phase, it is not possible to reach an agreement what value should be locked, and later decided. Without unlocking mechanism in place, the algorithm could loop forever in that state, and no decision will be reached. The unlocking mechanism is therefore essential for the algorithm termination as it allows processes to release locks and try to converge to a common value in the following rounds. In Algorithm~\ref{alg:tendermint}, a correct process $p$ unlocks a value by setting $lockedValue_p$ to $\nil$ and $lockedRound_p$ to $-1$.
A correct process $p$ releases its locked value if he observes that some correct process might\footnote{We say that other process \emph{might} have locked different value as we do not get a direct message from that process claiming that he locked a value with the corresponding proof of locking. We infer this information by observing $\Prevote$ messages.} have locked a different value in the round $r$ higher than the current $lockedRound_p$ ($r > lockedRound_p$). This is the case if a process $p$ receives at least $2f+1$ $\Prevote$ messages with value $v' \neq lockedValue_p$ and $round > lockedRound_p$ (see the rule starting at line~\ref{line:tab:unlockRule}). The process also implicitly releases a lock on its current value by locking a different value at lines~\ref{line:tab:setLockedValue} and \ref{line:tab:setLockedRound}.
The unlocking mechanism, together with the underlying gossip layer, ensures the following properties:
\begin{itemize}
\item (i) if a correct process $p$ locks a value $v$ in a round $r$ during a good period (period of synchrony), then at the end of the round $r$ all correct processes will lock either $v$ or they will not lock any value
\item (ii) if a correct process $p$ locks a value $v$ in a round $r$, then every correct process $q$ that has locked a different value in some of the previous rounds, i.e., $lockedValue_q \neq v$ and $lockedRound_q < r$, will eventually unlock it's value.
\end{itemize}
From the property (ii) follows that after a sufficiently big good period in which no correct process manages to lock a value, all correct processes will lock either some common value $v$ or they will not lock any value (where $v$ is the value locked in the highest round $r$ by some correct process). This follows from the fact that processes keep resending messages at the gossip layer, so during good periods, $\Prevote$ messages that led to the correct process locking the value $v$ in the round $r$ are received by all correct processes. Therefore, they either stay with $v$ as its locked value, or unlock its current value.
Both properties ensure that during a sufficiently long good period, there will eventually be a round, such that at the beginning of this round, all correct processes will lock the same value or they will not lock any value. As we will explain in the following section (\ref{sec:findRighValue}), this is one of the essential mechanisms for ensuring termination of the Tendermint consensus algorithm.
\subsection{Finding the right value to propose}
\label{sec:findRighValue}
When a correct process $p$ receives $2f+1$ $\Prepare$ messages for the same value $v$, then the process locks a value $v$ (and saves a proof of locking into variable $proof_p$) and enters commit step by sending $v$ in $\Commit$ message (lines 18-23). When process received $2f+1$ $\Commit$ messages for some value $v$, it decides value $v$.
As we discussed in section~\ref{sec:locking}, a correct process in Tendermint votes always for its locked value (if it exists) or for the \emph{valid} value suggested by the coordinator of the current round. In order to reach a decision in some round $r$ it is necessary that all correct processes vote for the same value in that round (we do not depend on faulty processes for termination). Then correct processes can lock that value, and later decide. Tendermint relies on the coordinator to ensure that processes that have not locked any value, vote for the same value. As a correct process always votes for its locked value, then several conditions need to be fulfilled just before the round $r$ starts so we can achieve such preferable scenario:
Note that algorithm relies on $state$ variable to prevent correct processes from sending more than one $\Prepare$ and $\Commit$ messages in a single round $r$. For simplicity, the current version of the algorithm does not provide termination condition, i.e., processes continue round execution even after deciding. We also assume that round timeout is being incremented in each round so that eventually all correct processes are able to receive all messages from correct processes in a round, before the round timeout expires.
Furthermore, the algorithm solves only single instance consensus problem. The multi-instance version of Tendermint will be addressed in the next version of the document. However, it should be relatively straightforward to modify Algorithm~\ref{alg:tendermint} to get multi-instance version with the following modifications: (i) adding consensus instance number in each message, (ii) having per instance algorithm state variables and (iii) adding logic for starting next consensus instance.
\begin{enumerate}
\item if a correct process $p$ has locked some value $v$ at the beginning of the round $r$, then all other correct processes have either locked $v$ or they have not locked any value. \label{enum:termination:v-is-locked}
\item the proposer is a correct process, and a value suggested by the proposer is $v$. \label{enum:termination:v-is-proposed}
\end{enumerate}
\subsection{Proof of correctness (sketch)}
In case those conditions hold, all correct processes will lock $v$ in the round $r$ and later decide.
\textbf{Agreement} Let assume that a first correct process that decides is $p$ and that $p$ decides value $v$ in round $r$. As $p$ decided $v$ this means that $p$ receives at least $2f+1$ $\Commit$ messages with value $v$ in the round $r$ (line 24). This means that at least $f+1$ correct processes have locked value $v$ in round $r$ and have it's variable $vote$ set to $v$ and $ts$ variable set to $r$. As correct processes can send only single $\Commit$ message per round, and there are at most $f$ faulty processes, then no correct process can receive $2f+1$ $\Commit$ messages in the round $r$ for some other value $v' \neq v$. Therefore, no correct process can decide value different than $v$ in the round $r$.
The existence of a round where the condition \ref{enum:termination:v-is-locked}) holds, follows from the unlocking mechanism. The first part of the condition \ref{enum:termination:v-is-proposed}) follows from the fact that $\coord$ function eventually provides a correct proposer. The second part of the condition \ref{enum:termination:v-is-proposed}) is more tricky as the proposer needs to suggest exactly the value that is locked by correct processes. If the proposer has locked $v$ at the beginning of the round $r$, then it trivially follows from the condition \ref{enum:termination:v-is-locked}). Otherwise, we need an additional mechanism that ensures that the correct proposer suggests $v$.
Now let consider the smallest round $r' > r$ in which correct process $q$ locks some value $v'$. As $q$ locks value $v'$ this means that $q$ has received at least $2f+1$ $\Prepare$ messages equal to $v'$ in the round $r'$. Therefore, at least $f+1$ correct processes has sent $v'$ in $\Prepare$ message in the round $r'$. As $f+1$ correct process $q'$ locked value $v$ in the round $r$, this means that one of those processes sent $PROPOSE$ message with value $v'$ in the round $r'$. According to function $isValidProposal$, $q'$ received valid proof of locking for value $v'$. This is in contradiction with the assumption that $r'$ is the smallest round in which some correct process locks some value (TODO: improve this part, it is not very precise as it could be reasoned that a Byzantine process could create correct proof of locking for some value $v'$ and round greater than $r'$ which can be proved impossible with the similar reasoning). As no correct process can lock any value different from $v$ in rounds $r' > r$, then no correct process can decide value different from $v$.
In order to ensure this condition, Tendermint has an additional mechanism for determining what is the good value to suggest such that this condition holds. It is implemented using variables $validValue$ and $validRound$. Using these two variables every process tracks the highest round ($validRound$) in which correct process might have locked some value ($validValue$). So whenever process observes at least $2f+1$ $\Prevote$ messages with $round > validRound_p$ (see the rule at line~\ref{line:tab:validValueRule}) for some value $v \neq \nil$,
it updates $validValue$ and $validRound$ variables.
\textbf{Termination}
This mechanism, together with the underlying gossip layer, ensures the following properties:
\begin{itemize}
\item (i) if a correct process $p$ locks a value $v$ in a round $r$ during a good period (period of synchrony), then at the end of the round $r$ all correct processes will have $validValue$ equal to $v$ and $validRound$ equal to $r$.
\item (ii) if no correct process $p$ locks some value during a sufficiently long good period, then all correct processes will eventually have $validValue$ equal to the same value $v$.
\end{itemize}
The Algorithm~\ref{alg:tendermint} does not terminate as the following scenario is possible: we consider rounds after GST, starting from round $r$ and at round $r$ a correct process $p$ is the only process that locks some value $v$ among the correct processes ($0 \le ts_p \le r$). Assume that no correct process has decided. Let assume that $p$ would coordinate the round $r'>r$. In rounds smaller than $r'$ $p$ will reject any proposal from correct processes if it's not equal to $v$ (which is possible if all correct processes have different initial values), so it will not send $PREPARE$ message. As faulty processes could decide not to send any message, no correct processes will be able to lock a value and to decide in those rounds. Now let assume that in round $r'-1$ some correct process $q$ locks value $v' \neq v$ because a faulty process (together with all correct processes except $p$) sends $\Prepare$ message with $v'$ to $q$. As $q$ locks value $v'$ in round higher than $r$, $q$ will reject proposal from $p$ in round $r'$ so if faulty processes stay silent, again no correct processes can decide in that round. This scenario can be repeated also with the rounds $k-1$ and $k$, in which the process $q$ is proposer.
If during a good period, no correct process locks a value during a sufficiently long period (so the property i) does not hold), then
all correct processes will have $validValue$ equal to $v$ due to the following reasoning: During this time period, all correct processes will receive delayed $\li{Prevote}$ messages from previous rounds (because of resending messages at the gossip layer). Now let denote with $r$ and $v$, a round and a value, such that there are at least $2f+1$ $\li{Prevote}$ messages with $r$ and $v$, and $r$ is the highest among such $(*, r)$ pairs. Then all correct processes will receive those messages and set $validValue$ to $v$.
The property that needs to be ensured is the following: after GST, there exist a round such that a proposal from a correct process is accepted by all correct processes. The solution could be adding one more step (lock-release step) at the end of each round where correct processes would send it's locked value (together with ts and proof) to all processes, and then a correct process will release lock upon reception of proof of locking for a different value from higher round. We will also need to modify lines 35 and 36 to propose the value with the valid proof of locking from the highest round (if process is aware of such value) or initial value.
In both cases, during sufficiently long good period, there will eventually be a round, such that at the beginning of this round, all correct processes will have $validValue$ equal to the same value; and in case some correct process has locked some value $v$, then the $validValue$ will be equal to $v$.
The unlocking mechanism and the mechanism for determining the right proposal value ensures that during a period of synchrony, there will be a round $r$ such that (i) all correct processes either lock the same value $v$ or they do not lock any value, and (ii) the $validValue$ is equal to $v$ at all correct processes. If a proposer of such round $r$ is correct, then he proposes $v$, all correct processes vote for $v$ during the locking phase; therefore they lock $v$, send a $\Precommit$ message with $v$ and later decide. The formal proof of termination is provided in section~\ref{sec:proof}.

+ 40
- 32
definitions.tex View File

@ -4,43 +4,51 @@
\subsection{Model}
We consider a system composed of $n$ server processes $\Pi = \{ 1, \dots, n\}$ that communicate by exchanging messages.
All messages sent between processes are digitally signed.
Processes can be \emph{correct} or \emph{faulty}, where correct processes
follow the algorithm and the faulty one may behave in an arbitrary way, i.e., we consider Byzantine faults.
We assume than the number of faulty servers is limited to $f$.
We consider a partially synchronous system model:
in all executions of the system, there is a bound $\Delta$
and an instant $GST$ (Global Stabilization Time) such that all
communication among correct processes after $GST$ is reliable and $\Delta$-timely, i.e., if a correct process
$p$ sends message $m$ at time $t\ge GST$ to correct process $q$, then $q$ will receive $m$
before $t+\Delta$.
We do not make any assumption
before $GST$. For example, messages among correct processes can be
delayed, dropped or duplicated before $GST$. Spoofing/impersonation attacks are
assumed to be impossible also before $GST$.
We assume that process steps (which might include
sending and receiving messages)
take zero time.
Processes are equipped with clocks able to measure local timeouts.
We consider a system composed of $n$ server processes $\Pi = \{ 1, \dots, n\}$.
Server processes can be correct or faulty, where a faulty process can behave in an arbitrary way,
i.e., we consider Byzantine faults. We assume that each process has some amount of voting power, and we denote with $N$ the total voting power of all processes in the system.
Furthermore, we assume that the total voting power of faulty processes is bounded with a system parameter $f$.
Processes communicate by exchanging messages. We assume a model where processes are not part of the single administration domain; therefore we cannot enforce a direct network connectivity between all server processes.
Instead, we assume that each server process is connected to a small number of processes called peers,
such that there is an indirect communication channel between all correct server processes. Communication between processes is established using gossip protocol.
We assume that processes communicate over wide-area network. Formally, we model the network communication using the partially synchronous system model~\cite{DLS88:jacm}, or rather a slightly weaker variant of this model: we assume that the system alternates between good periods (during which the system is synchronous) and bad periods (during which the system is asynchronous and messages can be lost). During good periods, there is a bound $\Delta$ such that all
communication among correct processes is reliable and $\Delta$-timely, i.e., if a correct process
$p$ sends message $m$ at time $t$ to a correct process $q$, then $q$ will receive $m$
before $t+\Delta$. Note that as we do not assume direct communication channels among all correct processes, this implies that before the message $m$ reaches $q$, it will pass through a number of
correct servers that will forward the message $m$ using gossip protocol towards $q$.
Messages among correct processes can be
delayed, dropped or duplicated during bad periods. Spoofing/impersonation attacks are assumed to be impossible also during bad periods.
The bound $\Delta$ is a system parameter whose value is not required to be known for the safety of the algorithm presented. However, the timing bounds derived for our algorithm, and thus the guaranteed latency requires knowledge of $\Delta$.
We assume that process steps (which might include sending and receiving messages) take zero time.
Processes are equipped with clocks so they can measure local timeouts.
We assume integrity of direct communication channels between peers, that is if a process $p$ received a message $m$ from process $q$, then $q$ sent message $m$ to $p$ before. All protocol messages are signed, i.e., when a correct process $q$ receives a signed message $m$ from its peer, the process $q$ can verify who was the original message sender.
The details of the Tendermint gossip protocol will be discussed in a separate technical report. For the sake of this report it is sufficient to assume the following properties provided by the gossip protocol (in addition to the properties about partial synchrony of the network stated above):
\begin{itemize}
\item Messages that are being gossiped come from the consensus layer. We can think about consensus protocol as a content creator, which defines what messages should be disseminated using the gossip protocol. A correct process creates the message for dissemination either i) explicitly, by invoking \emph{send} function as part of the consensus protocol or ii) implicitly, by receiving a message from some other process. Note that in the case ii) gossiping of messages is implicit, i.e., it happens without explicit send clause in the consensus algorithm whenever a correct process receives some messages in the consensus algorithm\footnote{If a message is received by a correct process at the consensus level then it is considered valid from the protocol point of view, i.e., it has a correct signature, a proper message structure and a valid height and round number.}.
\item Processes keep resending messages (in case of failures or message loss) until all its peers get them. This ensures that every message sent or received by a correct process is eventually received by all correct processes.
\end{itemize}
\subsection{Consensus}
\label{sec:consensus}
\newcommand{\propose}{\mathsf{Propose}}
\newcommand{\decide}{\mathsf{Decide}}
\newcommand{\propose}{\mathsf{propose}}
\newcommand{\decide}{\mathsf{decide}}
In the consensus problem, every process has an initial value from a
set $V$ and has eventually to irrevocably decide on a value from
$V$.
The problem is defined by an agreement, a termination, and a validity
property.
We consider a variant of the Byzantine consensus problem called Validity Predicate-based Byzantine consensus that is motivated by blockchain systems~\cite{GLR17:red-belly-bc}. The problem is defined by an agreement, a termination, and a validity
property.
\begin{itemize}
\item \emph{Agreement:} No two correct processes decide differently.
\item \emph{Termination:} All correct processes eventually decide.
\item \emph{Validity:} If all correct processes have the same initial value, and no process
is faulty, then this is the only possible decision value.
\item \emph{Agreement:} No two correct processes decide on different values.
\item \emph{Termination:} All correct processes eventually decide on a value.
\item \emph{Validity:} A decided value is valid, i.e., it satisfies the predefined predicate denoted \emph{valid()}.
\end{itemize}
This variant of the Byzantine consensus problem has an application-specific valid() predicate to indicate whether a value is valid. In the context of blockchain systems, for example, a value is not valid if it does not contain an appropriate hash of the last value (block) added to the blockchain.

+ 18
- 0
lit.bib View File

@ -1560,3 +1560,21 @@
publisher = {USENIX Association},
address = {Berkeley, CA, USA},
}
@article{GLR17:red-belly-bc,
author = {Tyler Crain and
Vincent Gramoli and
Mikel Larrea and
Michel Raynal},
title = {(Leader/Randomization/Signature)-free Byzantine Consensus for Consortium
Blockchains},
journal = {CoRR},
volume = {abs/1702.03068},
year = {2017},
url = {http://arxiv.org/abs/1702.03068},
archivePrefix = {arXiv},
eprint = {1702.03068},
timestamp = {Wed, 07 Jun 2017 14:41:08 +0200},
biburl = {http://dblp.org/rec/bib/journals/corr/CrainGLR17},
bibsource = {dblp computer science bibliography, http://dblp.org}
}

+ 3
- 1
paper.tex View File

@ -121,7 +121,8 @@
\title{Tendermint Byzantine Consensus Algorithm}
\author{\IEEEauthorblockN{Zarko Milosevic}
\author{\IEEEauthorblockN{Ethan Buchman, Jae Kwon and Zarko Milosevic}
% \IEEEauthorblockN{Tendermint}\
}
@ -138,6 +139,7 @@
\input{definitions}
\input{consensus}
\input{proof}
%\section*{Acknowledgment}


+ 2
- 0
proof.tex View File

@ -0,0 +1,2 @@
\section{Formal proof of Tendermint consensus algorithm}
\label{sec:proof}

+ 0
- 4
readme.md View File

@ -1,4 +0,0 @@
# Tendermint-spec
The repository contains the specification (and the proofs) of the Tendermint
blockchain protocol.

Loading…
Cancel
Save