ironfleet.tex

% This is LLNCS.DEM the demonstration file of
% the LaTeX macro package from Springer-Verlag
% for Lecture Notes in Computer Science,
% version 2.4 for LaTeX2e as of 16. April 2010
%
\documentclass{llncs}
%
\usepackage{makeidx}  % allows for indexgeneration
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{dafny}
%
\begin{document}
%
\mainmatter              % start of the contributions
%
\title{Study of Liveness Verification in IronFleet}
%
\author{Lucas Pe\~{n}a and Manasvi Saxena}
%
\institute{University of Illinois at Urbana-Champaign, \\
\email{\{lpena7, msaxena2\}@illinios.edu}}

\maketitle              % typeset the title of the contribution

\begin{abstract}
  As more complicated software systems are becoming prevalent in today's world,
  more sophisticated program verification techniques are needed to reason about
  these. In particular, verification of liveness properties, or asserting that a
  property must occur, is traditionally difficult. In this paper, we survey the
  IronFleet methodology~\cite{ironfleet}, a technique for verifying safety and
  liveness properties in practical distributed systems. 
  We consider the embedding of the Temporal Logic of Actions used in
  IronFleet, and discuss some limitations in their implementation.
\end{abstract}
%
\section{Introduction}
Many tools are used for ensuring correctness of a system. These range from
testing to full formal verification. Formal verification is obviously the most
desirable, but the most difficult in practice. One generally requires a formal
specification of the property he or she is proving correct. This often makes
large-scale formal verification a difficult and cumbersome task. Still, many
success stories exist in the area of large-scale formal verification, such as
the CompCert compiler~\cite{compcert} and the Verve operating
system~\cite{verve}.  However, formal verification of 
large-scale distributed systems presents many challenges, such as network
complexity and interactions between nodes. Even with single node system, proving 
liveness properties in general is harder than just proving safety properties.
Add to that the inherent complexity of distributed systems over single node systems,
and the problem of proving distributed systems correct becomes significantly harder.


\subsection{Safety Verification}
Most formal verification techniques focus on verifying safety
properties. Informally, a safety property asserts that ``nothing bad ever
happens.'' More formally, this means if a system violates a safety property $P$
at any point in its execution, the full execution must also violate $P$. Thus,
safety properties have \textit{finite length counterexamples}. Because of this
crucial fact, many techniques such as model checking and monitoring focus
specifically on verifying safety properties.

\subsection{Liveness Verification}\label{sec:liveness-description}
In contrast, a liveness property asserts that ``something good will happen.''
This means one must have the entire execution in hand in order to assert the
absence of a liveness property. Thus, liveness properties have \textit{infinite
  length counterexamples}.  Therefore, though liveness verification has the same
theoretical complexity as safety verification~\cite{simulation-liveness}, in
practice it is much more difficult to verify liveness properties. Clearly, it is
fruitless to do any kind of brute force search for the absence of such a
counterexample. Instead, specific techniques for verifying liveness properties
have been developed, which we discuss in Section~\ref{sec:rel-work}.

The IronFleet methodology uses a proof strategy based on Lamport's Temporal
Logic of Actions (TLA) that chains smaller proofs together to assert the
existence of some final condition (see
Section~\ref{sec:liveness-ironfleet}). Unlike the related work on liveness
verification, IronFleet is the first to verify nontrivial liveness properties on
a large-scale distributed system.
%

\section{Temporal Logic of Actions}\label{sec:tla}
The Temporal Logic of Actions (TLA)~\cite{tla-lamport} is an extension of Linear Temporal
Logic introduced to reason about concurrent systems. TLA introduces ``primed''
variables, which represents the value of a variable in the next state. For
example, the TLA \textit{action} $$x' = x + y$$ specifies that the value of $x$
in the next state is equal to the value of $x + y$ in the current state. An
action is satisfied by a pair of states $\langle s, t \rangle$, where $s$ is a
valuation on the unprimed variables and $t$ is a valuation on the primed
variables. The notion of primed variables allow us to specify a rich class of
formulas not expressible in normal LTL.

First, we can represent the action $Unchanged\;f \equiv f' = f$ for any 
function $f$  without primed variables, which states that $f$ is a
stuttering step. Using this, we can also represent the derived actions
$[\mathcal A]_f$ and $\langle \mathcal A \rangle_f$ for any action
$\mathcal A$. These respectively represent that an action either satisfies $\mathcal A$ or
stutters (w.r.t. $f$), and that an action that satisfies $\mathcal A$
necessarily changes $f$. These are defined as follows:
\begin{align*}
  [\mathcal A]_f \equiv \mathcal A \vee Unchanged\;f \hspace{1.5cm}
  & \langle \mathcal A \rangle_f \equiv \mathcal A \wedge \neg(Unchanged\;f)
\end{align*}
TLA also introduces the action $Enabled\;\mathcal A$ which specifies that for
any $s$, there is a $t$ such that $\langle s, t \rangle$ satisfies $\mathcal A$.

TLA \textit{formulas} add the temporal operator $\square$, like in LTL. In
addition, quantification over formulas is allowed. Derived formulas such as
$\lozenge$ are as in LTL. Other derived formulas include $F \leadsto G$
(\textit{leads to}), WF$_f(\mathcal A)$ (\textit{weak fairness}), and
SF$_f(\mathcal A)$ (\textit{strong fairness}). These are defined as follows:
\begin{align*}
  F \leadsto G &\equiv \square(F \Rightarrow \lozenge G) \\
  \text{WF}_f(\mathcal A) &\equiv \square\lozenge\langle\mathcal A\rangle_f \vee \square\lozenge\neg Enabled\;\langle\mathcal A\rangle_f \\
  \text{SF}_f(\mathcal A) &\equiv \square\lozenge\langle\mathcal A\rangle_f \vee \lozenge\square\neg Enabled\;\langle\mathcal A\rangle_f
\end{align*}
For use in verification, these derived formulas can express most liveness
properties a user may want to express. Of course, for verification, we need
proof rules allowing us to reason about these formulas, which we present below.

\begin{figure}
\includegraphics[scale=0.6]{tla-rules}
\centering
\end{figure}

These rules allow us to reason about both strong fairness and weak fairness,
both as a hypothesis and a conclusion. The use of these rules is demonstrated
via a simple program that nondeterministically chooses one of two variables to
increment ad infinitum. One can define a naive implementation of this program,
as well as a more complex one using semaphores.

The TLA rules above can be used to prove weak fairness of the first
implementation, strong fairness of the second, and it can even be used to prove
that the semaphore implementation is a refinement of the naive implementation.
Notably, all four of the above rules must be used for these proofs.

\section{IronFleet}
Microsoft's IronFleet methodology, is claimed to be the first complete suite of 
solutions that can perform automated, machine checked verification 
in nontrivial and distributed systems. IronFleet supports 
verification of both safety and liveness properties. We discuss, in detail, the 
approach used by IronFleet. We use the IronRSL system for further analysis.

\subsection{Dafny}
Dafny~\cite{leino-dafny} is a programming language with built-in specification constructs.
The Dafny
ecosystem consists of a static program verifier used for proving correctness of
programs and their specifications. The IronFleet methodology relies 
on Dafny for describing specifications and proving correctness of implementations. 

\subsection{End-to-end Verification}
Verification techniques employed in the IronFleet suite are not novel. IronFleet's 
motivation is to use existing verification techniques on large, complicated, and practical distributed
systems. In this regard, IronFleet breaks new ground. The software codebases that IronFleet
has been used to verify have features and performance comparable to similar non-verified solutions. 
IronFleet supports both safety and liveness verification. When liveness verification is taken into account, 
the IronFleet methodology is supposedly the first successful attempt at verifying liveness of both
the protocol, and the conforming implementation. 

IronFleet achieves end to end verification of distributed systems by structuring the system into layers and 
developing proofs on them. IronFleet blends TLA-style refinement to reason about protocol-level concurrency, 
while ignoring the implementation. It then uses Floyd-Hoare style verification to reason about implementation,
while ignoring concurrency. This allows the IronFleet to reason about both the high-level specification, and
the implementation. We briefly describe the layers used in IronFleet to structure reasoning about systems - 
\begin{itemize}
\item At the top layer, a high level specification for the entire system's behavior is provided. 
\item The middle layer contains the specification for the distributed protocol implemented by the
    system. IronFleet uses TLA-style techniques to prove that the middle layer 
    refines (see Section~\ref{sec:refinement}) the top layer.
\item The third layer contains the implementation details of the protocol, or the code to be run on each node.
    IronFleet uses refinement to prove that the implementation layer refines the protocol description layer. 
\end{itemize}

The layering methodology allows IronFleet to deal with complexities of the system effectively. 

\subsection{Refinement}\label{sec:refinement}
We present a brief overview of the concept of Refinement, with an emphasis of its use in
IronFleet. Refinement mappings are used to prove that a low level specification correctly
implements a high level one~\cite{Abadi}. In the context of IronFleet, refinement is directly 
used to prove that a layer refines, or in other words, correctly implements the layer above it.

\subsection{Always Enabled Actions}\label{sec:always-enabled}
Liveness can be achieved by satisfying fairness, i.e. showing actions are available and occur 
at the right time. One way of specification can be of the form ``if Action a 
becomes enabled, the system must eventually do it'' ~\cite{lamport-tla-book}. However, 
such specification result in complicated formulas that are hard to prove. Thus, 
IronFleet adopts ``Always Enabled Actions'', or relies only on actions that are 
always available to the system. In order to briefly explain the problem, we present
a segment of example Dafny code taken from \cite{ironfleet} used in protocol level 
specification of a safety property- 
\begin{dafny}
datatype Host = Host(held:bool,epoch:int)

predicate HostGrant(s_old:Host,s_new:Host, spkt:Packet) 
{ s_old.held && !s_new.held && spkt.msg.transfer?
&& spkt.msg.epoch == s_old.epoch+1 }
\end{dafny}
The action HostGrant cannot be used as is, since it's not always enabled. 
Instead, one use a predicate like ``if you hold the lock, grant it to the next host;
otherwise, do nothing'', which is always enabled~\cite{ironfleet}. Always enabled
actions may lead to machine closed specification, or specifications for which there can be no 
conforming implementations~\cite{lamport-tla-book}. However, in IronFleet, since the implementation already exists,
machine closed specifications are not a problem.

\subsection{Liveness Verification in IronFleet}\label{sec:liveness-ironfleet}
As mentioned in Section~\ref{sec:liveness-description}, liveness verification involves
reasoning with infinite series of systems states, which creates challenges for 
provers, often causing them to time out rather than produce a result. IronFleet addresses
this problem by using a custom embedding of Lamport's Temporal Logic of Action (see Section 
~\ref{sec:tla}) in Dafny. IronFleet models the system's behavior B as a mapping from Integer to
States, where $B[0]$ represents the first state, and $B[i]$ represents the $ith$~\cite{ironfleet}. 
Since state of the art SMT solvers like Z3 do not provide direct support for temporal operators
$\square$ and $\lozenge$, explicit quantification over states is used instead ($\square$ universally
quantifies over all future states, while $\lozenge$ existentially quantifies over some future states).
IronFleet uses Z3's support for triggers to control the quantification with heuristics. 
Using heuristics, IronFleet can efficiently use the embedding of TLA rules in Dafny. Often, a liveness proof in 
IronFleet can involve multiple invocations of the WF1 rule. We discuss the proof strategy briefly
in following sections.

\subsubsection{Liveness Verification in IronRSL}
We attempt to further describe liveness verification in IronFleet using the IronRSL project as 
an example. IronRSL demonstrates the strength in IronFleet's methodology, as it's a 
complicated and feature-rich distributed system. IronRSL is a replicated state machine library
based on the Paxos algorithm~\cite{paxos}. We now briefly describe the layers of IronRSL specification
and implementation, with a focus on IronFleet's role.
\begin{itemize}
\item \textbf{High Level Specification Layer} The high level specification for IronRSL is simply linearizability.
    It must generate the same output when run on a single node, as it would when run across a cluster in a 
    distributed fashion.

\item \textbf{Protocol Specification Layer} The protocol layer specifies the Paxos algorithm. Each host's state 
    consists of four components: a proposer, an accepter, a learner, and an executor. The host's action 
    predicates correspond to the above mentioned components, for instance, proposing a batch of requests 
    . The invariant for the protocol is agreement, or that any pair of learners don't 
    decide different batches for the same slot~\cite{ironfleet}. Refinement of the High-Level abstract state machine
    occurs not when a replica executes a batch, but when a quorum of replicas decide on the next batch.

\item \textbf{Implementation Layer} IronRSL uses IronFleet's generic refinement library to ensure that 
    the implementation refines the protocol. It also allows the implementation to focus on the implementation
    details, helping abstract details the proof of refinement.    

\end{itemize}


\textbf{Generic Refinement Library} $-$ IronFleet's generic refinement library allows for proving the implementation 
layer refines the protocol specification. For instance, in IronRSL's implementation uses a map from $uint64$ to 
IP addresses, while the protocol description uses a map from mathematical integers to to abstract node identifiers.
In the proof, it must be established that removing an element from the concrete map corresponds to a similar 
operation in the abstract protocol description. The generic refinement library allows reasoning over 
refinement between common data structures, such as sequence and maps. Given basic properties between concrete and
abstract data structures, the library can show that operations on the concrete structures refine similar operations
on their abstract counterparts~\cite{ironfleet}.

Liveness is proved in IronRSL by showing the following property holds - if if a client repeatedly
sends a request to all replicas, it eventually receives
a reply~\cite{ironfleet}. The proof relies on the following assumptions - 
\begin{itemize} 
    \item There exists a quorum of replicas $Q$, a
        minimum scheduler frequency $F$, a maximum network delay
        $\Delta$, a maximum burst size $B$, and a maximum clock error E.
    \item The scheduler on each replica runs with at least frequency F.
    \item Messages exchanged between nodes take at most time $\Delta$.
    \item No node receives a burst of packages, i.e. no node receives more
          than $B$ packets per $\frac{10B}{F} + 1$ time units.
    \item The clock of every node is off by the global clock by at most $E$.
\end{itemize}

The proof strategy works as follows~\cite{ironfleet} - 
\begin{itemize}
    \item The TLA library has proofs showing that if a round robin scheduler (that 
        schedules the actions) runs infinitely, then each action occurs
        infinitely often. In IronRSL, the round robin scheduler is used to prove that
        the protocol fairly schedules each action.
    \item It is proven that eventually no replica in $Q$ 
        has a backlog of packets in its queue, so
        thereafter sending a message among replicas in $Q$ leads to
        the receiver acting on that message within a certain bound.
    \item Next, using WF1 it's proven that if the client’s request
        is never executed, then for any time period $T$, eventually a
        replica in Q becomes the undisputed leader for that period.
    \item Finally, it's shown that there exists a time period $T$ s.t. 
        an undisputed leader can ensure execution of the request and 
        provide a response within $T$.
\end{itemize}

\subsection{Discussion of Benefits and Limitations}
IronFleet aims to address the problem of using existing techniques in software verification
to provide end to end verification for complex distributed systems. The motivation for 
making existing solutions work in a practical setting, without compromising on the
feature-richness and performance of the systems being verified. The solutions presented in the IronFleet
methodology present a compelling case. The systems verified using IronFleet worked correctly (barring
the unverified components like the C\# clients)
when they were run, which makes a compelling argument for the effectiveness of the technique.

There are several caveats to the approach however. The first is the reliance of the system on Dafny.
 The entire suite, from the specification, to the implementation is entirely written in Dafny. The 
 authors do make their code, and embedding of TLA available, but it can only be used if the software
 to be verified itself is written in Dafny, which is a limitation.

 One simple limitation is that, of the four fairness rules present in TLA, only
 the WF1 rule is encoded in Dafny. This means there likely will be some
 properties that cannot be proved with this encoding, such as those regarding
 the incrementer program in Section~\ref{sec:tla}. A more sophisticated
 embedding of the TLA rules could help solve this issue.

 The amount of effort required to produce verified software using the techniques presented, is also 
 non-negligible. As the authors themselves acknowledge, in exchange for strong guarantees, developers
 are required to put in considerably more effort. The effort may be exacerbated for developers who're 
 not familiar with Dafny, or its pre-post condition style of specification. 
 It must also be mentioned that the software solutions presented were specifically written with 
 the aim of verification in mind. The IronFleet methodology would not work as smoothly if it were
 employed with legacy code. Hence, as an automated verification solution, it doesn't work for 
 existing distributed systems. 

 Another limitation is the manner in which specifications themselves have to written. The 
 authors mention that actions in protocol specifications have to be written as ``always enabled''
 actions for fairness verification. The authors acknowledge that their methodology is not 
 in compliance with the recommended way of writing specifications in TLA, as it may lead
 to ``machine closed'' specifications. The authors illustrate with an example that an action
 predicate may be converted to an ``always enabled'' predicate 
 (see Section~\ref{sec:always-enabled}). However, they don't provide a proof that any
 action can always be rewritten as an always-enabled action. This leads to the question
 whether all expressible TLA actions can be expressed in IronFleet's Dafny embedding of TLA.

 The IronFleet methodology breaks new ground in distributed systems verification, as it 
 provides usable verified software that can actually be used. Given the lack of proof of 
 correctness of distributed protocols, let alone actual implementations, it certainly 
 pushes the envelope. It's unclear whether other solutions, in verification of single-node and
 sequential software can be adapted along similar lines.


\section{Related Work and Conclusion}\label{sec:rel-work}
Though verification of liveness properties is notoriously difficult and rare,
the IronFleet methodology was of course not the first to formally verify
liveness properties. Previous techniques include BDD-based model
checking~\cite{Ravi2000} as well as converting liveness properties to safety
properties~\cite{Schuppan2006}.

BDD-based model checking relies on Binary Decision Diagrams (BDDs) as a data
structure that can be used to represent boolean functions. Unfortunately, the
size of the BDD can scale exponentially with the size of the system, so this
approach is not scalable.

Converting a liveness property to a safety property is an attractive idea, since
it opens up the use of existing algorithms to verify safety properties. However,
the translation used in~\cite{Schuppan2006} incurs a large increase in problem
size, making this technique not scalable as well.

IronFleet solves the scalability problems above by encoding an embedding of
Lamport's Temporal Logic of Actions, structuring the proof in layers, and using 
refinement. They demonstrate the scalability in
practice by verifying liveness properties of two large-scale distributed systems
they defined, including IronRSL, though this approach is not without its own
limitations.

Future work involves combining techniques from the IronFleet methodology with
other liveness techniques, to verify a potentially richer set of liveness
properties for large-scale distributed systems. Other future work involves using
techniques to verify liveness properties for previously existing systems, rather
than writing a system in a verification-aware language like Dafny.

%
% ---- Bibliography ----
%
\bibliographystyle{ieeetr}

\bibliography{references}

\end{document}