source: CIVL/doc/manual/part-introduction.tex@ bc05301

\part{Introduction}
\label{part:intro}

\chapter{Acknowledgement}

The CIVL project is funded by the U.S.\ National Science Foundation
under awards CCF-1346769 and CCF-1346756.

\chapter{What is CIVL?}

\textbf{CIVL} stands for \emph{Concurrency Intermediate Verification
  Language}.   The \emph{CIVL platform} encompasses:
\begin{enumerate}
\item the programming language \textbf{CIVL-C}, a dialect of C with
  additional primitives supporting concurrency, specification, and modeling;
\item verification and 
  analysis tools, including a symbolic execution-based model checker for
  checking various properties of, or finding defects in, CIVL-C
  programs; and
\item tools that translate from many commonly used
  languages/APIs to CIVL-C.
\end{enumerate}

The CIVL-C language is primarily intended to be an intermediate
representation for verification. A C program using
MPI~\cite{mpi-forum:2012:mpi30}, CUDA~\cite{cuda-programming-guide},
OpenMP~\cite{openmp-standard}, OpenCL~\cite{opencl-standard}, or
another API (or even some combination of APIs), will be automatically
translated into CIVL-C and then verified. The advantages of such a
framework are clear: the developer of a new verification technique
could implement it for CIVL-C and then immediately see its impact
across a broad range of concurrent programs. Likewise, when a new
concurrency API is introduced, one only needs to implement a
translator from it to CIVL-C in order to reap the benefits of all the
verification tools in the platform. Programmers would have a valuable
verification and debugging tool, while API designers could use CIVL as
a ``sandbox'' to investigate possible API modifications, additions,
and interactions.

This manual covers all aspects of the CIVL framework, and is organized in parts
as follows:
\begin{enumerate}
\item this introduction, including ``quick start'' instructions for
  downloading and installing CIVL and several examples;
\item a complete description of the CIVL-C language;
\item a formal semantics for the language; and
\item a description of the tools in the framework.
\end{enumerate}

\chapter{Installation and Quick Start}

This chapter gives instructions for downloading and installing CIVL,
and running the verification tool on an example.

\begin{enumerate}

\item Download and unpack the appropriate pre-compiled library of CIVL
  dependencies from
  \hbox{\url{http://vsl.cis.udel.edu/tools/vsl_depend/}}.  There are
  versions for Darwin (OS X), 32-bit Linux, and 64-bit Linux.
  After unpacking, you should have a directory named \texttt{vsl}.
\item If you do not already have a directory \texttt{/opt},
  create it; use \texttt{sudo} as needed (\verb!sudo mkdir /opt!).
\item Move the directory \texttt{vsl} into \texttt{/opt}
  (\verb!mv vsl /opt!).
\item Download and unpack the latest stable release of CIVL from 
  \url{http://vsl.cis.udel.edu/civl}.  Again there are versions
  for Darwin, 32-bit Linux, and 64-bit Linux.
\item The resulting directory should be named
  \texttt{CIVL-\textit{tag}} for some string \textit{tag} which
  identifies the version of CIVL you downloaded.  Move this directory
  into \texttt{/opt} (\texttt{mv\ CIVL-\textit{tag}\ /opt}).
\item There should now be an executable script at
  \texttt{/opt/CIVL-\textit{tag}/bin/civl}.  Move this script into
  your path, or create a symlink from somewhere in your path to it, or
  add the directory \texttt{/opt/CIVL-\textit{tag}/bin} to your path.
\end{enumerate}

From the command line, you should now be able to type \texttt{civl
  help} and see a help message describing the command line syntax.

Copy the file
\texttt{CIVL-\textit{tag}/examples/concurrency/locksBad.cvl} to your
working directory.  Look at the program: it is a simple 2-process
program with two shared variables used as locks.  The 2 processes try
to obtain the locks in opposite order, leading to a deadlock.

Type
\begin{verbatim}
civl verify locksBad.cvl
\end{verbatim}
You should see some output culminating in a message 
\begin{verbatim}
The program MAY NOT be correct.  See CIVLREP/locksBad_log.txt
\end{verbatim}

Type
\begin{verbatim}
civl replay locksBad.cvl
\end{verbatim}
You should see a step-by-step account of how the program arrived
at the deadlock.

\textbf{Note.}  You can install \texttt{CIVL-\textit{tag}} and
\texttt{vsl} in any directory you want, not just in \texttt{/opt}.
You just need to edit the script file \texttt{civl} appropriately,
replacing the default paths with the new paths.

\chapter{Examples}

In this section we show a few simple CIVL-C programs which illustrate
some of the pertinent features of the language. We also show the results
of running some of the tools on them.

\section{Dining Philosophers}

Dijkstra's well-known Dining Philosophers system can be encoded in
CIVL-C as shown in Figure \ref{fig:dining}.

\begin{figure}
  \begin{small}
\begin{verbatim}
#include <civlc.h>

$input int B; // upper bound on number of philosophers
$input int n; // number of philosophers
$assume 2<=n && n<=B;

// Each fork will be on the table (0) or in a hand (1).
_Bool forks[n];

void dine(int id) {
  int left = id;
  int right = (id + 1) % n;

  while (1) {
    $when (forks[left] == 0) {forks[left] = 1;}
    $when (forks[right] == 0) {forks[right] = 1;}
    forks[right] = 0;
    forks[left] = 0;
  }
}

/* Put all forks on the table. */
void init() {
  for (int i = 0; i < n; i++) forks[i] = 0;
}

void main() {
  init();
  for (int i = 0; i < n; i++) $spawn dine(i);
}
\end{verbatim}
  \end{small}
  \caption{CIVL-C encoding of Dijkstra's Dining Philosophers}
  \label{fig:dining}
\end{figure}

In this encoding, an upper bound \ct{B} is placed on the number of
philosophers \ct{n}.   When verifying this program, a concrete value
will be specified for \ct{B}.  Hence the result of verification will
apply to all \ct{n} between $2$ and \ct{B}, inclusive.

Both \ct{B} and \ct{n} are delcared as \emph{input} variables using
the type qualifier \cinput.  An input variable may be
initialized with any valid value of its type.  In contrast, non-input
variables declared in file scope will be initialized with a
special \emph{undefined} value; if such a variable is read before it
is defined, an error will be reported. In addition, any input variable
may have a concrete initial value specified on the command line. In
this case, we will specify a concrete value for \ct{B} on the command
line but leave \ct{n} unconstrained.

An $\cassume$ statement restricts the set of executions of the program
to include only those traces in which the assumptions hold. In
contrast with an $\cassert$ statement, CIVL does not check that the
assumed expression holds, and will not generate an error message if it
fails to hold. Thus an $\cassume$ statement allows the programmer to
say to CIVL ``assume that this is true,'' while an $\cassert$
statement allows the programmer to say to CIVL ``check that this is
true.''

A $\cwhen$ statement encodes a \emph{guarded command}. The $\cwhen$
statement includes a boolean expression called the \emph{guard} and a
statement body. The $\cwhen$ statement is enabled if and only if the
\emph{guard} evaluates to \emph{true}, in which case the body may be
executed. The first atomic statement in the body executes atomically
with the evaluation of the guard, so it is guaranteed that the guard
will hold when this initial sub-statement executes. Since assignment
statements are atomic in CIVL, in this example the bodiy of each
$\cwhen$ statement executes atomically with the guard evaluation.

The $\cspawn$ statement is very similar to a function call. The main
difference is that the function called is invoked in a new process
which runs concurrently with the existing processes. The $\cspawn$
statement itself returns immediately.

The program may be verified for an upper bound of $5$ by typing the
following at the command line:
\begin{verbatim}
  civl verify -inputB=5 diningBad.cvl
\end{verbatim}

The output indicates that a deadlock has been found and a
counterexample has been produced and saved. We can examine the
counterexample, but it is more helpful to work with a \emph{minimal}
counterexample, i.e., a deadlocking trace of minimal length. To find a
minimal counterexample, we issue the command

\begin{verbatim}
  civl verify -inputB=5 -min diningBad.cvl
\end{verbatim}

\begin{figure}
  \begin{small}
\begin{verbatim}
CIVL v0.7 of 2014-02-08 -- http://vsl.cis.udel.edu/civl
Error 0 encountered at depth 136:
...
Error 25 encountered at depth 20:
CIVL execution error (kind: DEADLOCK, certainty: PROVEABLE)
A deadlock is possible:
  Path condition: true
  Enabling predicate: false
ProcessState 0: at location 15, f0:40.4-9 "$wait"
  Waiting on process 1
ProcessState 1: at location 28, f0:22.31-43 "forks[right]"
  Enabling predicate: false
ProcessState 2: at location 28, f0:22.31-43 "forks[right]"
  Enabling predicate: false
at f0:40.4-9 "$wait".
State 683
| Path condition
| | true
| Dynamic scopes
| | dyscope 0 (parent=-1, static=0)
| | | reachers = {0,1,2}
| | | variables
| | | | __atomic_lock_var = process<-1>
| | | | B = 5
| | | | n = 2
| | | | forks = X_s0v3[0:=1, 1:=1]
...
| Process states
...
| | process 2
| | | atomicCount = 0
| | | call stack
| | | | Frame[function=dine, location=28, f0:22.31-43 "forks[right]", scope=5]
...
=================== Stats ===================
   validCalls          : 18874
   proverCalls         : 17
   memory (bytes)      : 163577856
   time (s)            : 6.22
   maxProcs            : 6
   statesInstantiated  : 9346
   statesSaved         : 684
   statesSeen          : 1782
   statesMatched       : 1178
   steps               : 3009
   transitions         : 2959

The program MAY NOT be correct.  See CIVLREP/diningBad_log.txt
\end{verbatim}
  \end{small}
  \caption{Output from \texttt{civl verify -inputB=5 -min diningBad.cvl}, excerpt}
  \label{fig:diningOut}
\end{figure}

The result of this command is shown in Figure \ref{fig:diningOut}. The
output indicates that a minimal counterexample has length 19, i.e.,
involves 20 states and 19 transitions (the depth of 20 is one more
than 19).    It was the 26th and shortest trace found.  It was deemed
equivalent to the earlier traces and hence the earlier ones were
discarded and only this one saved.  We can replay the trace with the command
\begin{verbatim}
  civl replay diningBad.cvl
\end{verbatim}

\begin{figure}
  \begin{small}
\begin{verbatim}
...
Step 1: proc 0: 
  0->1: B = 5 at f0:9.0-12 "$input int B"
Step 2: proc 0: 
  35->36: i = 0 at f0:30.7-16 "int i = 0"
Step 3: proc 0: 
  36->38: LOOP_TRUE_BRANCH at f0:30.18-23 "i < n"
Step 4: proc 0: 
  38->40: forks[i] = 0 at f0:30.30-42 "forks[i] = 0"
...
Step 17: proc 2: 
  21->25: LOOP_TRUE_BRANCH at f0:20.9-10 "1"
Step 18: proc 1: 
  25->28: forks[left] = 1 at f0:21.30-45 "forks[left] = 1"
Step 19: proc 2: 
  25->28: forks[left] = 1 at f0:21.30-45 "forks[left] = 1"
...
Violation of Deadlock found in State 20:
A deadlock is possible:
  Path condition: true
  Enabling predicate: false
ProcessState 0: at location 15, f0:40.4-9 "$wait"
  Waiting on process 1
ProcessState 1: at location 28, f0:22.31-43 "forks[right]"
  Enabling predicate: false
ProcessState 2: at location 28, f0:22.31-43 "forks[right]"
  Enabling predicate: false
...
Trace ends after 19 steps.
Violation(s) found.
...
\end{verbatim}
  \end{small}
  \caption{Output from \texttt{civl replay}, excerpt}
  \label{fig:diningReplay}
\end{figure}

The result of this command is shown in Figure \ref{fig:diningReplay}.
The output indicates that a deadlock has been found involving 2
philosophers. The trace has 19 steps; after the initialization
sequence, each philosopher picks up her left fork.