mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
4a753bb639
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.
59 lines
1.9 KiB
TeX
59 lines
1.9 KiB
TeX
\section{State Space Explosion}
|
|
|
|
|
|
\subsection{The Problem}
|
|
|
|
The number of reachable states grows exponentially with the number of components.
|
|
A consensus protocol with $n$ validators, $r$ rounds, and $m$ possible messages has
|
|
roughly $O(n^r \cdot 2^m)$ states. With $n = 7$, $r = 3$, $m = 20$, that is billions
|
|
of states.
|
|
|
|
\subsection{Techniques for Managing It}
|
|
|
|
\paragraph{Symmetry reduction.}
|
|
If all validators are identical (before assigning Byzantine/honest roles), the model
|
|
checker need not explore permutations separately. TLC supports this via symmetry sets:
|
|
|
|
\begin{lstlisting}[language=TLA,caption={Symmetry reduction}]
|
|
\* In TLC configuration:
|
|
\* SYMMETRY Permutations(Validators)
|
|
\end{lstlisting}
|
|
|
|
This reduces the state space by a factor of $n!$.
|
|
|
|
\paragraph{State constraints.}
|
|
Bound variables to small ranges. Use \texttt{MaxRound = 3} instead of unbounded rounds.
|
|
If a bug exists, it usually manifests in small instances.
|
|
|
|
\paragraph{Action constraints.}
|
|
Limit the number of messages in flight:
|
|
|
|
\begin{lstlisting}[language=TLA,caption={Action constraint to limit state space}]
|
|
\* In TLC configuration:
|
|
\* ACTION_CONSTRAINT Cardinality(messages) < 20
|
|
\end{lstlisting}
|
|
|
|
\paragraph{Abstraction.}
|
|
Replace complex data with simpler representations. Instead of modeling full blocks
|
|
with transactions, use abstract block IDs (\texttt{"B1"}, \texttt{"B2"}).
|
|
|
|
\subsection{State Space in Practice}
|
|
|
|
\begin{table}[H]
|
|
\centering
|
|
\small
|
|
\begin{tabular}{@{}lrrr@{}}
|
|
\toprule
|
|
\textbf{Configuration} & \textbf{States} & \textbf{Time} & \textbf{RAM} \\
|
|
\midrule
|
|
4 validators, 2 rounds, no symmetry & 12.3M & 4m & 8GB \\
|
|
4 validators, 2 rounds, with symmetry & 0.5M & 11s & 2GB \\
|
|
7 validators, 3 rounds, with symmetry & 84M & 38m & 24GB \\
|
|
7 validators, 3 rounds, no symmetry & $>$10B & timeout & --- \\
|
|
\bottomrule
|
|
\end{tabular}
|
|
\caption{Effect of symmetry reduction on Teleport model checking.}
|
|
\end{table}
|
|
|
|
%% ============================================================
|