freespek · konnov · Oct 25, 2024
diff --git a/reports/discussion.tex b/reports/discussion.tex
@@ -1,8 +1,5 @@
 %! TeX root = report.tex
 
-\section{Discussion}%
-\label{sec:discussion}
-
 We have presented a series of specifications modeling the 3SF protocol from
 various perspectives. Initially, we developed a direct translation of the
 protocol's Python specification into \tlap{}, but this approach proved
@@ -14,7 +11,8 @@ \section{Discussion}%
 
 In addition to the \tlap{} specifications, we also introduced an SMT encoding
 and an Alloy specification. The SMT encoding proved to be fairly performant,
-while the Alloy specification demonstrated exceptional performance.
+while the Alloy specification demonstrated exceptional performance in
+combination with the Kissat solver~\cite{SAT-Competition-2024-solvers}.
 
 We summarize the key outcomes of the project:
 
@@ -23,11 +21,12 @@ \section{Discussion}%
 protocol. Model-checking this property proved to be computationally challenging
 due to the unexpectedly high combinatorial complexity of the protocol.
 Nonetheless, we performed systematic experiments across various specifications
-in \tlap{}, Alloy, and SMT, representing both a direct translation and different
-levels of abstraction of the protocol. The largest instances we exhaustively
-verified to satisfy \textit{AccountableSafety} include up to 7 checkpoints and
-24 validator votes (see Table~\ref{tab:alloy-mc}). This comprehensive
-verification gives us absolute confidence that the modeled protocol satisfies
+in \tlap{}, Alloy, and SMT (CVC5), representing both a direct translation and
+different levels of abstraction of the protocol. The largest instances we
+exhaustively verified to satisfy \textit{AccountableSafety} include up to 7
+checkpoints and 24 validator votes (see Table~\ref{tab:alloy-mc} in
+Section~\ref{sec:alloy-results}). This comprehensive verification gives us
+absolute confidence that the modeled protocol satisfies
 \textit{AccountableSafety} for systems up to this size.
 
 \paragraph{No falsification of \textit{AccountableSafety}.} In addition to the
@@ -51,11 +50,32 @@ \section{Discussion}%
 
 \paragraph{Value of \tlap{}.} \tlap{} is a powerful language for specifying and
 verifying distributed systems. Although our most promising experimental results
-were derived from the Alloy specification, the insights gained through iterative
-abstraction in \tlap{} were indispensable.\ \tlap{} enabled us to start with an
-almost direct translation of the Python code and progressively refine it into
-higher levels of abstraction. This iterative process provided a deeper
-understanding of the protocol and laid the groundwork for the more efficient
-Alloy specification.
-
-\colorbox{yellow}{TODO: anything else?}
+were derived from the Alloy specification, the insights gained through
+iterative abstraction in \tlap{} were indispensable.\ \tlap{} enabled us to
+start with an almost direct translation of the Python code and progressively
+refine it into higher levels of abstraction. This iterative process provided a
+deeper understanding of the protocol and laid the groundwork for the more
+efficient Alloy specification. The connection between the Python specification
+and the Alloy specification is definitely less obvious than the tower of
+abstractions that we have built in~\tlap{}.
+
+\paragraph{Value of producing examples.} Even though checking accountable
+safety proved to be challenging, our specifications are not limited to proving
+the properties. They are also quite useful for producing examples. For
+instance, both Apalache and Alloy were able to quickly produce examples of
+configurations that contain justified and finalized checkpoints. We highlight
+this unique value of specifications that are supported by model checkers:
+
+\begin{itemize}
+
+  \item Executable specifications in Python require the user to provide program
+    inputs. These inputs can be also generated randomly, though in the case of
+    3SF, this would be challenging.
+
+  \item Specifications in the languages supported by proof systems usually do
+    not support model finding. The TLAPS Proof System is probably a unique
+    exception here, as~\tlap{} is the common playground for the prover and the
+    model checkers~\cite{KonnovKM22}.
+
+\end{itemize}
+
diff --git a/reports/future.tex b/reports/future.tex
@@ -0,0 +1,24 @@
+%! TeX root = report.tex
+
+\begin{enumerate}
+
+  \item \emph{Generating inputs to the Python specification.} As we have noted,
+    the power of our~\tlap{} specifications is the ability to generate examples
+    with Apalache. This could help the authors of the Python specification to
+    produce tests for their specifications.
+
+  \item \emph{Specifications of a refined protocol.} The current version of
+    the Python specification is very abstract. On one hand, it is usually
+    beneficial to specify a high-level abstraction. On the other hand, as we
+    found, this level of abstraction is quite close to the general inductive
+    definitions of justified and finalized checkpoints. We should have better
+    chances at model checking more refined protocol specifications.
+
+  \item \emph{Transferring the Alloy encoding to Apalache.} As we have found in
+    this project, Alloy offers richer options for fine tuning in terms of
+    search scope. Moreover, given steady advances in SAT solving, this gives us
+    hope for achieving a faster feedback loop with model checking of
+    distributed protocols such as the 3SF protocol.
+
+\end{enumerate}
+
diff --git a/reports/intro.tex b/reports/intro.tex
@@ -6,11 +6,24 @@ \section{Introduction}
 
 \paragraph{}\colorbox{yellow}{TODO:}
 
-\begin{itemize}
-  \item what we want to model-check
-  \item why \tlap{}
-  \item introduce Apalache
-\end{itemize}
+We have started this project with the Python specification of accountable
+safety in the 3SF Protocol\footnote{URL to the Python specification:
+\url{https://github.com/freespek/ssf-mc/3sf.txt}}. The main goal of the project
+was to demonstrate accountable safety of this protocol by the means of model
+checking.
+
+We have chosen the specification language~\tlap{} and the model checker
+Apalache for the following reasons.\ \tlap{} remains a goto language for
+specifying consensus algorithms. Among the rich spectrum of
+specifications~\cite{tla-examples}, the most notable for our project are the
+specifications of Paxos~\cite{lamport2001paxos}, Raft~\cite{Ongaro14}, and
+Tendermint~\cite{abs-1807-04938,TendermintSpec2020}. Since consensus algorithms
+are quite challenging for the classical model checkers such as TLC, we chose
+Apalache~\cite{Apalache2024,KT19,KonnovKM22}. Apalache was used for model
+checking of agreement and accountable safety of
+Tendermint~\cite{TendermintSpec2020}. As an added benefit, four of the project
+participants worked on Apalache in the past and know its strenghts and
+weaknesses.
 
 \paragraph{Complexity of (model-checking) the protocol.} The 3SF protocol is
 intricate, with a high degree of combinatorial complexity, making it challenging
@@ -35,50 +48,68 @@ \section{Introduction}
     reasoning.
 \end{itemize}
 
-\subsection{Key Outcomes}
+\subsection{Key Outcomes}\label{sec:discussion}
 
-\colorbox{yellow}{TODO: summarize the key outcomes from Section~\ref{sec:discussion}}
+% we embed the discussion right in the introduction
+\input{discussion}
 
-\subsection{Overview of the report}
+\subsection{Structure of the report}
+
+\begin{figure}
+  \input{artifacts}
+  \caption{The relation between the specification artifacts}\label{fig:artifacts}
+\end{figure}
 
 Figure~\ref{fig:artifacts} depicts the relations between the specifications
 that we have produced in the project:
 
 \begin{enumerate}
     \item We have started with the executable specification in Python.
 
-    \item \textbf{Spec 1}: This is the specification
+    \item \SpecOne{}: This is the specification
         \texttt{spec1-2/ffg\_recursive.tla}. It is the result of a manual
         mechanical translation of the original executable specification in
         Python, which can be found in \texttt{ffg.py}. This specification is
         using mutually recursive operators, which are not supported by
         Apalache. As a result, we are not checking this specification. This
         specification is the result of our work in Milestone 1.
-
-    \item \textbf{Spec 2}: This is the specification \texttt{spec1-2/ffg.tla}. It
-        is a manual adaptation of Spec 1. The main difference between Spec 2
-        and Spec 1 is that Spec 2 uses ``folds'' (also known as ``reduce'')
-        instead of recursion.
-
-      \item \colorbox{yellow}{TBD}
+        This specification is discussed in Section~\ref{sec:spec1}.
+
+    \item \SpecTwo{}: This is the specification \texttt{spec1-2/ffg.tla}. It is
+        a manual adaptation of Spec 1. The main difference between Spec 2 and
+        Spec 1 is that Spec 2 uses ``folds'' (also known as ``reduce'') instead
+        of recursion. This specification is discussed in
+        Section~\ref{sec:spec2}.
+
+    \item \SpecThree{}: This is the further abstraction of~\SpecTwo{} that uses
+        the concept of a state machine, instead of a purely sequential
+        specification (such as the Python code). This specification is
+        discussed in Section~\ref{sec:spec3}.
+
+    \item \SpecFour{}: This is an extension of~\SpecThree{} that contains
+        an inductive invariant in~\texttt{spec4/ffg\_inductive.tla}.
+        This specification is discussed in Section~\ref{sec:spec4}.
+
+    \item \SpecFourB{} contains further abstractions and decomposition of
+        configurations. This is the first~\tlap{} specification that allowed us
+        to show accountable safety for models of very small sizes. This
+        specification is discussed in Section~\ref{sec:spec4b}.
+
+    \item \SpecThreeB{} contains a specification in SMT using the theory of
+        finite sets and cardinalities. In combination with the solver
+        CVC5~\cite{BarbosaBBKLMMMN22}, this specification allowed us to push
+        verification of accountable safety even further. This specification is
+        discussed in Section~\ref{sec:smt}.
+
+    \item \SpecThreeC{} contains a specification in
+        Alloy~\cite{jackson2012software,alloytools}. With this specification,
+        we managed to check all small configurations that cover the base case
+        and one inductive step of the definitions.  This specification is
+        discussed in Section~\ref{sec:alloy}.
 
 \end{enumerate}
 
-\begin{figure}
-  \input{artifacts}
-  \caption{The relation between the specification artifacts}\label{fig:artifacts}
-\end{figure}
-
-Figure~\ref{fig:block-graphs} shows small graphs, most of which form one or
-more chains. In the simple cases~\ref{fig:three}--\ref{fig:single}, we have one
-or two chains that form a tree. In a more general case like in
-Figure~\ref{fig:forest}, a graph is a forest. The graphs in
-Figures~\ref{fig:tricky1}--\ref{fig:tricky2} do not represent chains.  The
-graph~\texttt{I1} is a direct-acyclic graph but not a forest. The
-graph~\texttt{I2} has a loop.
+\subsection{Potential extensions of this project}\label{sec:future}
 
-\begin{figure}
-  \input{block-graphs}
-  \caption{Small instances of chains and non-chains}\label{fig:block-graphs}
-\end{figure}
+\input{future}
 
diff --git a/reports/preambule.tex b/reports/preambule.tex
@@ -9,6 +9,8 @@
 \newcommand{\SpecOne}{\texttt{Spec~1}}
 \newcommand{\SpecTwo}{\texttt{Spec~2}}
 \newcommand{\SpecThree}{\texttt{Spec~3}}
+\newcommand{\SpecThreeB}{\texttt{Spec~3b}}
+\newcommand{\SpecThreeC}{\texttt{Spec~3c}}
 \newcommand{\SpecFour}{\texttt{Spec~4}}
 \newcommand{\SpecFourB}{\texttt{Spec~4b}}
 \lstset{%

diff --git a/reports/ref.bib b/reports/ref.bib
@@ -1,3 +1,17 @@
+@misc{Apalache2024,
+  title = { The {Apalache} model checker},
+  howpublished = {\url{https://apalache-mc.org}},
+  year         = 2024,
+  note         = {Accessed: 2024-10-25}
+}
+
+@misc{tla-examples,
+  title = { A collection of {TLA}$^+$ specifications of varying complexities },
+  howpublished = {\url{https://github.com/tlaplus/Examples}},
+  year         = 2024,
+  note         = {Accessed: 2024-10-25}
+}
+
 @article{DBLP:journals/lmcs/BansalBRT18,
   author       = {Kshitij Bansal and
                   Clark W. Barrett and
@@ -10,12 +24,9 @@ @article{DBLP:journals/lmcs/BansalBRT18
   year         = {2018},
   url          = {https://doi.org/10.23638/LMCS-14(4:12)2018},
   doi          = {10.23638/LMCS-14(4:12)2018},
-  timestamp    = {Sat, 30 Sep 2023 10:20:49 +0200},
-  biburl       = {https://dblp.org/rec/journals/lmcs/BansalBRT18.bib},
-  bibsource    = {dblp computer science bibliography, https://dblp.org}
 }
 
-@inproceedings{DBLP:conf/tacas/BarbosaBBKLMMMN22,
+@inproceedings{BarbosaBBKLMMMN22,
   author       = {Haniel Barbosa and
                   Clark W. Barrett and
                   Martin Brain and
@@ -34,21 +45,15 @@ @inproceedings{DBLP:conf/tacas/BarbosaBBKLMMMN22
                   Yoni Zohar},
   editor       = {Dana Fisman and
                   Grigore Rosu},
-  title        = {cvc5: {A} Versatile and Industrial-Strength {SMT} Solver},
-  booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems
-                  - 28th International Conference, {TACAS} 2022, Held as Part of the
-                  European Joint Conferences on Theory and Practice of Software, {ETAPS}
-                  2022, Munich, Germany, April 2-7, 2022, Proceedings, Part {I}},
-  series       = {Lecture Notes in Computer Science},
+  title        = {{CVC5}: {A} Versatile and Industrial-Strength {SMT} Solver},
+  booktitle    = {TACAS, Part {I}},
+  series       = {LNCS},
   volume       = {13243},
   pages        = {415--442},
   publisher    = {Springer},
   year         = {2022},
   url          = {https://doi.org/10.1007/978-3-030-99524-9\_24},
   doi          = {10.1007/978-3-030-99524-9\_24},
-  timestamp    = {Fri, 29 Apr 2022 14:50:36 +0200},
-  biburl       = {https://dblp.org/rec/conf/tacas/BarbosaBBKLMMMN22.bib},
-  bibsource    = {dblp computer science bibliography, https://dblp.org}
 }
 
 @book{jackson2012software,
@@ -70,11 +75,8 @@ @inproceedings{SAT-Competition-2024-solvers
   author       = {Armin Biere and Tobias Faller and Katalin Fazekas and Mathias Fleury and Nils Froleyks and Florian Pollitt},
   title	       = {{CaDiCaL}, {Gimsatul}, {IsaSAT} and {Kissat} Entering the {SAT Competition 2024}},
   editor       = {Marijn Heule and Markus Iser and Matti J{\"a}rvisalo and Martin Suda},
-  booktitle    = {Proc.~of {SAT Competition} 2024 -- Solver, Benchmark and
-                  Proof Checker Descriptions},
+  booktitle    = {SAT Competition},
   volume       = {B-2024-1},
-  series       = {Department of Computer Science Report Series B},
-  publisher    = {University of Helsinki},
   year	       = 2024,
   pages	       = {8-10},
 }
@@ -96,3 +98,74 @@ @article{cayley1878theorem
   pages={376--378},
   year={1878}
 }
+
+@inproceedings{KonnovKM22,
+  author       = {Igor Konnov and
+                  Markus Kuppe and
+                  Stephan Merz},
+  editor       = {Tiziana Margaria and
+                  Bernhard Steffen},
+  title        = {Specification and Verification with the {TLA}\({}^{\mbox{+}}\)
+                  Trifecta: TLC, Apalache, and {TLAPS}},
+  booktitle    = {ISoLA},
+  series       = {LNCS},
+  volume       = {13701},
+  pages        = {88--105},
+  publisher    = {Springer},
+  year         = {2022},
+  url          = {https://doi.org/10.1007/978-3-031-19849-6\_6},
+  doi          = {10.1007/978-3-031-19849-6\_6}
+}
+
+@article{KT19,
+  author       = {Igor Konnov and
+                  Jure Kukovec and
+                  Thanh{-}Hai Tran},
+  title        = {{TLA+} model checking made symbolic},
+  journal      = {Proc. {ACM} Program. Lang.},
+  volume       = {3},
+  number       = {{OOPSLA}},
+  pages        = {123:1--123:30},
+  year         = {2019},
+  url          = {https://doi.org/10.1145/3360549},
+  doi          = {10.1145/3360549}
+}
+
+@book{Lamport2002,
+  author       = {Leslie Lamport},
+  title        = {Specifying Systems, The {TLA+} Language and Tools for Hardware and
+                  Software Engineers},
+  publisher    = {Addison-Wesley},
+  year         = {2002},
+  url          = {http://research.microsoft.com/users/lamport/tla/book.html},
+  isbn         = {0-3211-4306-X}
+}
+
+@phdthesis{Ongaro14,
+  author       = {Diego Ongaro},
+  title        = {Consensus: bridging theory and practice},
+  school       = {Stanford University, {USA}},
+  year         = {2014},
+  url          = {https://searchworks.stanford.edu/view/10608105}
+}
+
+@article{lamport2001paxos,
+  title={Paxos made simple},
+  author={Lamport, Leslie},
+  journal={ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001)},
+  pages={51--58},
+  year={2001}
+}
+
+@article{abs-1807-04938,
+  author       = {Ethan Buchman and
+                  Jae Kwon and
+                  Zarko Milosevic},
+  title        = {The latest gossip on {BFT} consensus},
+  journal      = {CoRR},
+  volume       = {abs/1807.04938},
+  year         = {2018},
+  url          = {http://arxiv.org/abs/1807.04938},
+  eprinttype    = {arXiv},
+  eprint       = {1807.04938}
+}