mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
abf99d05fc
Restructured from flat .tex/.pdf files into per-paper subdirectories. Added Antje Worring as co-author on all papers. Synced PDFs to pdfs/ for download site.
75 lines
2.4 KiB
TeX
75 lines
2.4 KiB
TeX
\section{Modeling Consensus Protocols}
|
|
|
|
|
|
\subsection{The Consensus Specification Pattern}
|
|
|
|
Every BFT consensus spec follows this pattern:
|
|
|
|
\begin{lstlisting}[language=TLA,caption={BFT consensus specification pattern}]
|
|
---- MODULE BFTConsensus ----
|
|
EXTENDS Integers, FiniteSets, Sequences
|
|
|
|
CONSTANTS
|
|
Validators, \* Set of all validators
|
|
MaxFaulty, \* Maximum Byzantine validators
|
|
MaxRound \* Bound for model checking
|
|
|
|
VARIABLES
|
|
round, \* Current round per validator
|
|
lockedValue, \* Locked value per validator
|
|
lockedRound, \* Round of lock per validator
|
|
decision, \* Decision per validator (or NONE)
|
|
messages, \* Set of in-flight messages
|
|
faulty \* Set of Byzantine validators
|
|
|
|
vars == <<round, lockedValue, lockedRound,
|
|
decision, messages, faulty>>
|
|
|
|
N == Cardinality(Validators)
|
|
Q == 2 * N \div 3 + 1 \* Quorum size
|
|
|
|
\* Type invariant
|
|
TypeOK ==
|
|
/\ round \in [Validators -> 0..MaxRound]
|
|
/\ decision \in [Validators -> {"NONE"} \union Values]
|
|
/\ Cardinality(faulty) <= MaxFaulty
|
|
|
|
\* Safety: no two honest validators decide differently
|
|
Safety ==
|
|
\A v1, v2 \in Validators \ faulty :
|
|
decision[v1] # "NONE" /\ decision[v2] # "NONE"
|
|
=> decision[v1] = decision[v2]
|
|
====
|
|
\end{lstlisting}
|
|
|
|
\subsection{Modeling Byzantine Behavior}
|
|
|
|
Byzantine validators can send arbitrary messages. In TLA+, we model this by allowing
|
|
faulty validators to perform any action without constraints:
|
|
|
|
\begin{lstlisting}[language=TLA,caption={Byzantine behavior model}]
|
|
\* Honest validator: follows protocol
|
|
HonestVote(v) ==
|
|
/\ v \notin faulty
|
|
/\ \E msg \in messages :
|
|
/\ msg.type = "PROPOSE"
|
|
/\ msg.round = round[v]
|
|
/\ \* Vote for proposed value if not locked
|
|
\/ lockedRound[v] = -1
|
|
\/ lockedValue[v] = msg.value
|
|
/\ messages' = messages \union
|
|
{[type |-> "VOTE", round |-> round[v],
|
|
value |-> msg.value, sender |-> v]}
|
|
|
|
\* Byzantine validator: can send any vote
|
|
ByzantineVote(v) ==
|
|
/\ v \in faulty
|
|
/\ \E val \in Values, r \in 0..MaxRound :
|
|
messages' = messages \union
|
|
{[type |-> "VOTE", round |-> r,
|
|
value |-> val, sender |-> v]}
|
|
/\ UNCHANGED <<round, lockedValue, lockedRound, decision>>
|
|
\end{lstlisting}
|
|
|
|
%% ============================================================
|