%% background
\section{Background} \label{sec:background}
%% HOARE LOGIC
\subsection{Hoare Logic} \emph{Hoare logic} \cite{hoare:1969:axiomatic}
is the basis of deductive verification.  It provides a proof system
for showing safety properties of sequential programs.

The key
notion in Hoare logic is the \emph{Hoare triple}: $\{P\}~S~\{Q\}$,
where $S$ is a program statement and $P, Q$ are the \emph{pre-} and
\emph{post-conditions} respectively.  The Hoare triple is valid if $S$
is executed from a \emph{pre-state} where $P$ holds, and is
eventually terminated at a \emph{post-state}, then $Q$ will
hold on the post-state.

A set of inference rules are defined for reasoning about Hoare
triples.  This rule set is called the \emph{Hoare calculus}.  Every
inference rule also formally describes the semantics of a statement
kind.  Four rules are selected from Hoare calculus to be presented in
Fig.\ \ref{fig:intro:hoare:rules} as examples.  The \emph{assignment}
rules states that the post-condition $Q$ of the assignment \texttt{$a$
  := $e$} can be ensured, if the pre-condition is obtained by
substituting $a$ with $x$ in $Q$.  The \emph{sequence} rule states
that if there is a condition that can serve as the post-condition of a
statement $S_0$ as well as the pre-condition of another statement
$S_1$, a Hoare triple for the composite statement $S_0\texttt{;}S_1$
can be inferred.  The \emph{consequence} rule introduces a \emph{side
  condition}, which is a logic formula over the pre- and
post-conditions of two Hoare triples.  The rule states that for a
statement $S$, one triple can be inferred from the other if the side
condition is valid.  The \emph{branch} rule expresses that a Hoare
triple of a branch statement can be inferred from the Hoare triples of
its two branches.

\begin{figure}
  \begin{center}
\begin{tabular}{p{7cm} p{7cm}}
$\frac{}{ \{Q[e / a]\}~a\texttt{ := }e~\{Q\} }$ (assignment) &
$\frac{\{P\}~S_0~\{R\},\,
\{R\}~S_1~\{Q\}}{\{P\}~S_0\texttt{;}S_1~\{Q\}}$ (sequence)\\ \\

$\frac{\{P'\}~S~\{Q'\}}{\{P\}~S~\{Q\}}$ (consequence) &

$\frac{ \{P \wedge{}
C\}~S_0~\{Q\},\, \{P \wedge{} \neg{}C\}~S_1~\{Q\}}{\{P\}~
\texttt{if }C\texttt{ then }S_0\texttt{ else }S_1~\{Q\}}$ (branch) \\
\text{if $P' \Rightarrow P
\wedge{} Q \Rightarrow{} Q'$} &
\end{tabular}
\end{center}
\caption{Four selected inference rules in Hoare calculus.}
\label{fig:intro:hoare:rules}
\end{figure}

%%% verification condition generation
The proof process of applying Hoare calculus to Hoare triples can be
automated with the \emph{verification condition generation} (VCG)
\cite{barnett:2006:boogie,gordon:1989:mechanizing,leino:1999:checkingjava}
technique.  Given a statement, a pair of pre- and post-conditions and
a set of assumptions, a VCG algorithm automatically computes the
\emph{weakest pre-condition} (WP) of the statement that ensures the
post-condition according to the rules in Hoare calculus.  Then the
validity of the triple can be represented by a generated condition
stating that the given pre-condition is stronger than the WP.  Most of
the deductive verification tools for sequential programs are
established on VCG.

\begin{exmp}
  Figure \ref{fig:intro:hoare:derive} shows a derivation for a Hoare
  triple of a C code using Hoare calculus.  The
  VCG process for this example is given by Fig.\
  \ref{fig:intro:hoare:wp}.  Note that the term $abs(\texttt{y})$ in
  the code stands for the absolute value of \texttt{y}.  By VCG, the
  validity of the Hoare triple is represented by the following
  condition:
    \begin{center}
        $(\texttt{x} = X \wedge{} \texttt{y} = Y) \Rightarrow{}$
        $\mymath{WP}($\texttt{\ccode{if} (x >= 0) y = x;
    \ccode{else} y = -x;}$,\, \{\texttt{x} = abs(\texttt{y})\})$
    \end{center}
        $\qed$
\end{exmp}

\begin{figure}[t]
    \fbox{
    \parbox{\textwidth}{
    \begin{itemize}
    \item $\{\texttt{x} = X \wedge{} \texttt{y} = Y\}$\texttt{\ccode{if}
    (x>=0) y = x; \ccode{else} y = -x;}$\{\texttt{x} =
    abs(\texttt{y})\}$ (branch 1, 2)

    \begin{itemize}
    \item[1.]   $\{\texttt{x} = X \wedge{} \texttt{y} = Y \wedge{} X
    \geq 0\}$ \texttt{y = x} $\{\texttt{x} =
    abs(\texttt{y})\}$ (consequence)
    
    %% FINAL-ASSIGNMENT-1
    \begin{itemize}
    \item[] $\{\texttt{x} \geq{} 0\}$ \texttt{y = x} $\{\texttt{x} =
    abs(\texttt{y})\}$ (assignment)
    \end{itemize}

    \item[2.]  $\{\texttt{x} = X \wedge{} \texttt{y} = Y \wedge{} X <
    0\}$ \texttt{y = -x} $\{\texttt{x} = abs(\texttt{y})\}$


    %% FINAL-ASSIGNMENT-2
    \begin{itemize}
    \item[] $\{\texttt{x} < 0\}$ \texttt{y = -x} $\{\texttt{x} =
    abs(\texttt{y})\}$ (assignment)
    \end{itemize}
    \end{itemize}
    
  \end{itemize}
  }}
      \caption{The derivation of a Hoare triple.  Note that
        $\mymath{abs(\texttt{y})}$ denotes the absolute value of \texttt{y}.}
          \label{fig:intro:hoare:derive}      
\end{figure}

\begin{figure}[t]
    \fbox{
    \parbox{\textwidth}{
      \begin{itemize}
      \item[Let] $\mymath{WP(s, q)}$ denote the WP of
    the statement $s$ for a post-condition $q$,
    
      \item[] $\mymath{WP}($\texttt{\ccode{if} (x >= 0) y = x;
    \ccode{else} y = -x;}$,\, \{\texttt{x} = abs(\texttt{y})\})$

    \item[$=$] $\texttt{x} \geq{} 0 \Rightarrow{} \mymath{WP}($\texttt{y = x} $,\,\{\texttt{x} =
    abs(\texttt{y})\})$ \text{and} $\texttt{x} < 0 \Rightarrow{} \mymath{WP}($\texttt{y = -x} $,\,\{\texttt{x} =
    abs(\texttt{y})\})$

    \item[$=$] $(\texttt{x} \geq{} 0 \Rightarrow{} \texttt{x} =
    abs(\texttt{x})) \wedge{} (\texttt{x} < 0 \Rightarrow{} \texttt{x} =
    abs(\texttt{-x}))$

    \item[$=$] $\mymath{true}$
    \end{itemize}
    }}
      \caption{The computation of the WP for a desired post-condition
    of the given code. }
          \label{fig:intro:hoare:wp}
\end{figure}


\emph{Design by Contract}$^{\small{\texttt{TM}}}$ (DbC) a methodology
originated with Hoare logic.  It was coined by Bertrand Meyer in
\cite{Meyer:1992:ADC} and is now a trademark owned by Eiffel Software.
The idea of DbC is to use pre- and post-conditions to document, as
well as check the correctness of, program procedures.  A pair of a
pre- and post-conditions for a procedure is called a \emph{procedure
  contract}.  Procedure contracts are built-in constructs in the
Eiffel \cite{Meyer:1988:eiffel} programming language.  They will be
checked as assertions during runtime executions.  Other than Eiffel,
procedure contracts are widely used by deductive verification tools.

Why3 \cite{filliatre:2013:why3} and Boogie \cite{barnett:2006:boogie} are
verification programming languages with rich built-in specification
constructs, including procedure contracts.  Both of them at the same
time also refer to the deductive verifiers that can prove the
functional correctness of Why3 and Boogie programs respectively.  A
number of verification tools for higher level programming languages
are built on top of Why3 and Boogie, such as HAVOC
\cite{lahiri2012security, ball:2010:towards} and Frama-C
\cite{cuoq2012framac} with its plug-in \emph{WP}
\cite{cuoq:2011:wp} for C, Spark-2014 \cite{spark} for Ada, KeY
\cite{beckert:2007:KeY} for Java, Spec\#
\cite{barnett:2005:specsharp} for C\# and the verifier for Dafny
\cite{leino:2010:dafny}.



\subsection{Formal Methods For Concurrency}
Hoare logic is not suitable for specifying and proving concurrent
programs. A Hoare triple describes a statement in terms of its input
and output.  However, in a concurrent program, the behavior of a
process executing a statement depends on not only the input but also
the behaviors of other processes that run in parallel.  Besides, Hoare
logic cannot describe \emph{liveness properties}, which are crucial
for concurrent programs.

Owicki and Gries \cite{Owicki1976}, Lamport \cite{lamport1980hoare}
and Takaoka \cite{Takaoka:1994:PPV:326619.326811} introduced their
techniques inheriting Hoare's style for proving properties of
concurrent programs.

%% Owicki & Gries:
Owicki and Gries introduced their technique in \cite{Owicki1976} based
on Hoare logic for proving \emph{safety properties} of concurrent
programs.  In their work, concurrency is enabled by two general
statements: 1) \texttt{cobegin $S_0 //\ ...\ // S_n$ coend} means that
each statement $S_i$, $0 \leq i \leq n$, is executed by a separate
process and all these processes are run in parallel; 2) \texttt{await $B$
  then $S$} means that the process has to stop at $S$ unless $B$ is
true and once $B$ is true, the process executes $S$ in an atomic step.
Formal semantics of the two statements is defined as reasoning rules,
just like what Hoare logic does.  Then for a concurrent program $S$
that consists of the extended set of statements, the validity of
$\{P\}~S~\{Q\}$ can be derived using the rules.

The most important idea in this work is the semantics of the
\texttt{cobegin ...\ coend} statement,
\begin{align}
  \frac{\{P_1\}S_1\{Q_1\},  \{P_2\}S_2\{Q_2\},  ...\ \text{ are
  interference-free}}
  {\{P_1\wedge{}P_2\wedge{}...\ \} \texttt{cobegin}~S_1 // S_2 // ...\ \texttt{coend}
  \{Q_1\wedge{}Q_2\wedge{}...\ \} }\nonumber
\end{align}
which is straightforward except for the term ``interference-free''.
Let $\mymath{pre}(S)$ be the pre-condition of a statement $S$, a
statement $T$ is said to not interfere $\{P\}~S~\{Q\}$, iff

\begin{enumerate}
\item  $\{Q \wedge{} \mymath{pre}(T)\}~T~\{Q\}$, i.e., $T$ does not break post-condition of $S$;
    
\item for any sub-statement $S' $of $S$, such that $\{P'\}~S'~\{Q'\}$,
  $\{\mymath{pre}{S'} \wedge{} \mymath{pre}{T}\}~T~\{\mymath{pre}(S')\}$, i.e., $T$ does not
  break the pre-condition of any sub-statement $S'$.
\end{enumerate}
A proof of interference-free can be mechanized by showing that every
atomic sub-statement $S_i$ in a \texttt{cobegin} statement cannot be
interfered by another one $S_j$.  Usually, in order to prevent a
triple $\{P\}~S~\{Q\}$ from being interfered, the user needs to weaken
$P$ to accept the behaviors of other parallel statements.

% Lamport: concurrent hoare logic:
Lamport \cite{lamport1980hoare} generalizes Hoare logic by refining
the meaning of the triple $\{P\}~S~\{Q\}$ to that 1) $P$ must be
strong enough to guarantee that $Q$ will hold upon termination even if
the execution starts from any location inside $S$; and 2) $P$ must
remain true as long as the control is in $S$, where $S$ is a
concurrent program composed of sequential statements as well as the
\texttt{cobegin} statement used by Owicki and Gries.
There are three predicates that refer to program locations with
respect to a statement $S$: immediately before $S$, inside $S$ and
immediately after $S$.  For a sub-statement $S$ in a \texttt{cobegin}
structure, a strong enough pre-condition usually takes program
locations of different processes into consideration.

% Directed graph based proof technique:
Takaoka \cite{Takaoka:1994:PPV:326619.326811} proves a triple
$\{P\}~S~\{Q\}$ for a parallel program $S$ by analyzing a program
graph representing $S$, where vertices are sets of locations of
running processes and arrows bridging vertices are labeled by program
statements.  In addition, each vertex will be attached with an
assertion.  Initial locations are attached with pre-conditions and
final locations are attached with post-conditions.  Then for every
arrow, the assertion of the destination vertex can be derived from the
assertion of the source vertex with respect to the statement labeling
the arrow.  The rules for the assertion derivation are defined in
Hoare style.  The triple $\{P\}~S~\{Q\}$ is valid iff such a graph is
successfully constructed.  In Takaoka's work, parallel programs
contains synchronous statements.  A process can ``wait for '' another
process by executing \texttt{call} until the waited process executes
\texttt{accept}.  A similar program graph based analysis was done by
Newton \cite{Newton1975} earlier.  In \cite{Newton1975}, program
locations can be used to express properties in assertions though the
parallel programs have no synchronous statement.

A more intuitive approach was suggested by Ashcroft
\cite{Ashcroft:1975:PAP:1739967.1740302}.  In
\cite{Ashcroft:1975:PAP:1739967.1740302}, safety properties of a
concurrent program are expressed as a set of \emph{global invariants},
i.e., a set of assertions that are suppose to hold at any location of
the program.  The proof is constructed by showing the validity of
those assertions for every program location.

Liveness properties, such as the \emph{fairness} property, can be
expressed with \emph{temporal logic}.  Techniques for proving liveness
properties including the \emph{well-founded set} approach, which was
originally applied by Floyd \cite{Floyd1993} and later adapted by
Manna and Puneli in \cite{Manna:1984:APP:2731.2734}, the \emph{proof
  lattice} approach \cite{Owicki:1982:PLP:357172.357178} and the
\emph{rely-guarantee} approach \cite{Stark:1985:PTR:646823.706907}.

Modern tools for verifying concurrent programs in an axiomatic way
include VCC \cite{cohen-etal:2009:vcc}, COMPLX
\cite{amani:2017:complex}, KeY
\cite{beckert:2007:KeY}, Chalice \cite{leino:2009:verification}
and VeriFast \cite{Jacobs:2010:QTV:1947873.1947902}.  VCC is a static
verifier for concurrent C programs.  The user of VCC needs to annotate
invariants and other specifications for programs.  COMPLEX is a
verification framework that targets general imperial programming
languages.  It is based on the aforementioned proof system proposed by
Owicki and Gries.  KeY verifies Java programs against their
specifications written in JML \cite{Gosling:2014:JLS:2636997}.  It
generalizes Hoare logic for Java to the \emph{first order Java Dynamic
  Logic}.  Chalice uses a permission based approach to reason about
multi-threaded concurrent programs.  VeriFast utilizes separation
logic \cite{reynolds2002separation} for verifying multi-threaded C and
Java programs.


%% MODEL CHECKING
\subsection{Model Checking}
Model checking \cite{clarke:2000:modelchecking} is an algorithmic method
for checking correctness of a system by searching all reachable states
in a finite state space.  The system is abstracted to a \emph{model}
where irrelavant details are removed.  A state space represents all
possible behaviors of the model.  A state space is a directed graph,
where a node is a state and an edge is a transition which alters a
state in an atomic step.

The model checking technique is effective for verifying properties of
concurrent systems. A concurrent system can be abstracted to an
\emph{interleaving model}. In an interleaving model, the real-world
asynchronous executions are represented by non-deterministic choices
on atomic transitions. For example, the parallel execution of two
atomic commands $a$ and $b$ can be modeled as two non-deterministic
choices: $a$ followed by $b$ or $b$ followed by $a$.

A challenge in model checking is the state explosion problem. The
number of states grows exponentially when the number of components in
a concurrent system increases.  Hence, many model checkers can only
scale to programs whose inputs are bounded with small concrete
values. But model checking is still widely used to solve real problems
for two reasons.  First, there is a belief in the \emph{Small Scope
  Hypothesis} \cite{Jackson:2006:SAL}, which states that bugs can be
found by exploring all possible program executions with inputs being
in small scopes.  Second, many sophisticated \emph{reduction}
techniques allow model checkers to only search in a sub-space of the
full state space without loss of soundness.  For example, using the
\emph{partial-order reduction} (POR) technique
\cite{godefroid:1993:refining, 10.1007/BFb0013032,Valmari1992}, a
model checker usually only needs to explore one among a number of
commutative executions.

%% SYMBOLIC EXECUTION
\subsection{Symbolic Execution} Symbolic execution is an approach for
testing and analyzing programs \cite{king:1976:symbolic}. It replaces
the concrete program inputs with symbols, each of which represents a
set of concrete values.  During the symbolic execution, a boolean
formula, \emph{path condition} (PC), is maintained.  PC denotes the
condition, under which an execution path is feasible.  Due to the
existence of symbols, the PC and values stored in variables are all
\emph{symbolic expressions}.

Symbolic execution is able to explore all possible paths of a program
that a concrete execution may take.  Different paths are generated
from the different choices that a concrete execution can make at
branches.  During the exploration of each path, PC initially is
assigned the true value and gets updated at each branch.  The updated
value is a conjunction of the old PC value and the branch condition
corresponding to the choice made in the path.  Once PC becomes
unsatisfiable, the exploring path is infeasible and will be ignored
immediately.  Automated theorem provers \cite{Z3Prover,
  barrett-etal:2011:cvc4, alt-ergo} are used to reason about symbolic
expressions during the exploration.

\begin{exmp}

Considering the following C code:

\begin{center}
  \begin{program}
\ccode{if}~(x~>=~0)\\
~~y~=~x;\\
\ccode{else}\\
~~y~=~-x;\\
\end{program}
\end{center}

Suppose the variable \texttt{x} holds a symbol $X$.  A symbolic
execution engine will explore two paths for this code snippet: one
path leads to a result where the variable \texttt{y} has value $X$ and
its PC becomes $X \ge 0$; The other path leads to a result where the
variable \texttt{y} has value $-X$ and its PC becomes $X < 0$. $\qed$
\label{exmp:intro:symexe}
\end{exmp}

%% MPI
\subsection{MPI}
The Message-Passing Interface (MPI) standard specifies a library for
writing message-passing parallel programs in different languages such
as C and Fortran.  This library includes a large number of functions,
constants, and data types.  For an MPI program, every process has its
private storage but shares nothing with others.  Communication among
processes is carried out by transferring data using different MPI
functions.  An MPI program is written, compiled, and linked to
generate an executable file. The program is executed by instantiating
a number of processes, each of which runs a copy of the executable.

In MPI programs, a \emph{communicator} is an abstraction of a
``communication universe'' for processes.  A communicator comprises an
ordered group of $n$ ($1 \leq{} n$) processes.  Processes are
identified by $0, 1, ..., n-1$.  The numerical identifier of a process
in a communicator is called the \emph{rank} of the process.  A process
may belong to multiple communicators and is assigned different
identifiers in each of them.  But there is a default communicator,
which contains all processes that are invoked when a program is
launched.  The rank of a process in the default communicator can be
used as the unique ID.  By branching on process ranks, different
processes may behave differently even though they run the same
program.

Communicaton operations are performed through communicators.
Conceptually, a communicator includes a set of message channels.
Every message channel can be identified by an ordered pair $(i, j)$
($0 \leq i, j < n$).  It behaves like a First-In-First-Out (FIFO)
queue for bufferring messages that were sent from a process $i$ but
have not been received by a process $j$.

In MPI, communication can be non-deterministic.  A process can perform
a receive operation without specifying an exact sender.  Such a
receive operation is called a wildcard receive.  In concept, a
wildcard receive performed by process $i$ non-deterministically picks
up a message from the set $\{(j, i) | 0 \leq j < n\}$ of message channels
that contain appropriate messages.

\begin{exmp}
  Figure \ref{fig:mpi:simple} is a simple C/MPI program.  Constructs
  defined in MPI library all start with a ``\texttt{MPI\U{}}'' prefix.
  \texttt{MPI\U{}COMM\U{}WORLD} is the constant that refers to the
  default communicator.  The \texttt{MPI\U{}Init} function initiates
  the message-passing environment.  Every process can obtain its rank
  in a communicator by calling \texttt{MPI\U{}Comm\U{}rank}.  The
  \texttt{MPI\U{}Finalize} function terminates the environment.

In this example, process of rank 0 sends a message to process of rank
1.  The point-to-point (P2P) communication is carried out by a pair of
standard P2P send and receive functions:

\begin{figure}[t]
  \begin{program}
    \ccode{\#include}~<mpi.h>\\
    \ccode{int}~main(\ccode{int}~argc,~\ccode{char}~*argv[])~\lb~\\
    ~~\ccode{int}~rank,~dat~=~0;~\\
    ~~MPI\civlU{}Init(\&argc,~\&argv);~\\
    ~~MPI\civlU{}Comm\civlU{}rank(MPI\civlU{}COMM\civlU{}WORLD,~\&rank);
\mycomment{//gets the rank of this
  process}\\
~~\ccode{if}~(rank~==~0)~\\
~~~~MPI\civlU{}Send(\&dat,~1,~MPI\civlU{}INT,~1,~0,~MPI\civlU{}COMM\civlU{}WORLD);\\
~~\ccode{else~if}~(rank~==~1)\\
~~~~MPI\civlU{}Recv(\&dat,~1,~MPI\civlU{}INT,~0,~0,~MPI\civlU{}COMM\civlU{}WORLD,
MPI\civlU{}STATUS\civlU{}IGNORE);\\
~~MPI\civlU{}Finalize();\\
\rb\\
\end{program}
\caption{A simple MPI program. Process 0 sends and process 1 receives
  a message. The remaining processes perform no operation.}
\label{fig:mpi:simple}
\end{figure}
\end{exmp}

\begin{enumerate}
  \item the \texttt{MPI\U{}Send} function (at line 7) sends the data,
  which is stored in \texttt{dat} and of the size of one
  \texttt{MPI\U{}INT}, to process of rank 1 in the default communicator
  with a tag 0.
  
 \item the \texttt{MPI\U{}Recv} function (at line 9) receives the
 message tagged by 0, in which the data is expected to be no larger
 than the size of one \texttt{MPI\U{}INT} and will be saved in
 \texttt{dat}, from process of rank 0 in the default communicator.
\end{enumerate}

No communication action is performed by any other process. $\qed$

