source: CIVL/mods/dev.civl.com/doc/manual/part-introduction.tex@ 1aaefd4

\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.

\subsection*{Notes}

\begin{itemize}
\item The instructions say to install three theorem provers.  In
  reality, each of these is optional.  CIVL will still work without
  any theorem provers, but the results will not be very precise, i.e.,
  it will produce a lot of false warnings.  The more provers you
  install, the more precise the analysis.
\end{itemize}

\subsection*{Instructions}

\begin{enumerate}
\item Install the automated theorem prover CVC3 (if you have not
  already).  The easiest way to do this is to visit
  \url{http://www.cs.nyu.edu/acsys/cvc3/download.html} and download
  the latest, optimized build with static library and executable for
  your OS.  Place the executable file \texttt{cvc3} somewhere in your
  \texttt{PATH}.  You can discard everything else.  Alternatively, on
  some linux systems, CVC3 can be installed using the package manager
  via ``\texttt{sudo apt-get install cvc3}''.  This will place
  \texttt{cvc3} in \texttt{/usr/bin}.

\item Install the automated theorem prover CVC4 (if you have not
  already).  The easiest way to do this is to visit
  \url{http://cvc4.cs.nyu.edu/downloads/} and choose one of the
  installation approaches.  You only need the binary (\texttt{cvc4}),
  and you must put it in your \texttt{PATH}.  Alternatively, on OS X
  you may install using MacPorts by ``\texttt{sudo port install
    cvc4}''.

\item Install the automated theorem prover Z3 (if you have not
  already).  Follow instructions at
  \url{http://z3.codeplex.com/SourceControl/latest#README}.  Make sure
  the executable \texttt{z3} is in your path.

\item Install a Java 7 SDK if you have not already.  Go to
  \url{http://www.oracle.com/technetwork/java/javase/downloads/} for
  the latest from Oracle.  On linux, you can instead use the package
  manager: ``\texttt{sudo apt-get install openjdk-7-jdk}''.

\item Download and unpack the latest stable release of CIVL from
  \url{http://vsl.cis.udel.edu/civl}.

\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
  wherever you like.

\item The JAR file in the \texttt{lib} directory is all you need to
  run CIVL.  You may move this JAR file wherever you want.  You run
  CIVL by typing a command of the form ``\texttt{java -jar
    /path/to/civl-TAG.jar ...}''.  For convenience, you may instead
  use the shell script \texttt{civl} included in the \texttt{bin}
  directory.  This allows you to replace ``\texttt{java -jar
    /path/to/civl-TAG.jar}'' with just ``\texttt{civl}'' on the
  command line.  Simply edit the \texttt{civl} script to reflect the
  path to the JAR file and place the script somewhere in your
  \texttt{PATH}.  Alternatively, you can define an alias in your
  \texttt{.profile}, \verb!.bash_profile!, \texttt{.bashrc}, or
  equivalent, such as
\begin{verbatim}
alias civl='java -jar /path/to/civl-TAG.jar'
\end{verbatim}
  In the following, we will assume that you have defined a command
  \texttt{civl} in one of these ways.

\item From the command line, type ``\texttt{civl help}''.  You should see
  a help message describing the command line syntax.

\item From the command line, type ``\texttt{civl config}''.  This should
  report that \texttt{cvc3}, \texttt{cvc4}, and \texttt{z3} were
  found, and it should create a file called \texttt{.sarl} in your
  home directory.

\end{enumerate}

To test your installation, copy the file
\texttt{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 two processes try to obtain the locks in
opposite order, which can lead to a deadlock if both processes obtain
their first lock before either obtains the second.  Type
``\verb!civl verify locksBad.cvl!''.  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 ``\verb!civl replay locksBad.cvl!''.  You should see a
step-by-step account of how the program arrived at the deadlock.


\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}[t]
  \begin{small}
\begin{verbatim}
#include <civlc.cvh>

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

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

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

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

void main() { 
  $for(int i: 0 .. n-1)
    forks[i] = $true;
  $parfor(int i: 0 .. n-1)
    dine(i);
}
\end{verbatim}
  \end{small}
  \caption{\texttt{diningBad.cvl}: 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 $\cfor$ statement is very similar to a for loop. The main
difference is that it takes a domain and loops over it.

The $\cparfor$ statement is a combination of $\cfor$ and $\cspawn$. 
The latter 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 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}[t]
  \begin{small}
\begin{verbatim}
CIVL v1.5 of 2015-10-31 -- http://vsl.cis.udel.edu/civl

Violation 0 encountered at depth 19:
CIVL execution violation (kind: DEADLOCK, certainty: PROVEABLE)
at diningBad.cvl:31.11-12 ";":
A deadlock is possible:
...

Logging new entry 0, writing trace to CIVLREP/diningBad_0.trace
Restricting search depth to 18

Violation 1 encountered at depth 14:
CIVL execution violation (kind: DEADLOCK, certainty: PROVEABLE)
at diningBad.cvl:31.11-12 ";":
A deadlock is possible:
  Path condition: true
  Enabling predicate: false
process p0 (id=0): false
process p1 (id=1): false
process p2 (id=2): false

Context:
true

Call stacks:
process p0 (id=0):
  _CIVL_system at diningBad.cvl:31.11-12 ";"
process p1 (id=1):
  dine at diningBad.cvl:21.4-9 "$when"
process p2 (id=2):
  dine at diningBad.cvl:21.4-9 "$when"

...

=== Stats ===
   time (s)            : 0.95
   memory (bytes)      : 128974848
   max process count   : 5
   states              : 81
   states saved        : 53
   state matches       : 2
   transitions         : 77
   trace steps         : 56
   valid calls         : 510
   provers             : cvc4, z3, cvc3
   prover calls        : 6

=== Result ===
The program MAY NOT be correct.  See CIVLREP/diningBad_log.txt
\end{verbatim}
  \end{small}
  \caption{Output from \texttt{civl verify -inputB=5 diningBad.cvl}}
  \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 14, i.e.,
involves 15 states and 14 transitions (the depth of 19 is five more
than 14).    It was the 2nd 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 -showTransitions diningBad.cvl
\end{verbatim}

\begin{figure}
  \begin{small}
\begin{verbatim}
...
Step 0: State 0, p0:
  0->1: B=5 at diningBad.cvl:9.0-16 "$input int B = 4"
  1->2: n=InitialValue(n) [n:=X0] at diningBad.cvl:10.0-12 "$input int n"
  2->3: $assume((2<=X0)&&(X0<=5)) at diningBad.cvl:11.0-21 "$assume(2<=n && n ... )"
  3->4: forks=InitialValue(forks) [forks:=(lambda i : int . false)] at diningBad.cvl:13.0-14 "_Bool forks[n]"
--> State 1
...
Step 2: State 2, p0:
  5->6: LOOP_BODY_ENTER(($domain(1)){(0..1#1)} has next for (NULL)) at diningBad.cvl:28.14-22 "0 .. n-1"
  6->7: $for((NULL) has next in ($domain(1)){(0..1#1)} at diningBad.cvl:28.2-6 "$for"
--> State 3
...
Step 6: State 6, p0:
  ...
  9->10: $parfor(i0: ($domain(1)){(0..1#1)}) $spawn dine(i0) at diningBad.cvl:30.2-9 "$parfor"
--> State 7

Step 7: State 7, p1:
  12->13: left=0 at diningBad.cvl:16.2-15 "int left = id"
  13->14: right=(0+1)%2 [right:=1] at diningBad.cvl:17.2-26 "int right = (id  ... n"
--> State 8
...
Step 11: State 11, p1:
  15->16: forks[0]=false at diningBad.cvl:20.24-44 "forks[left] = $false"
--> State 12

Step 12: State 12, p2:
  15->16: forks[1]=false at diningBad.cvl:20.24-44 "forks[left] = $false"
--> State 13
...
Violation of Deadlock found in State 13:
A deadlock is possible:
  Path condition: true
  Enabling predicate: false
process p0 (id=0): false
process p1 (id=1): false
process p2 (id=2): false

Trace ends after 13 trace steps.
Violation(s) found.
...
\end{verbatim}
  \end{small}
  \caption{Output from \texttt{civl replay -showTransitions diningBad.cvl}}
  \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 15 transitions; after the initialization
sequence, each philosopher picks up her left fork.

\section{A Multithreaded MPI Example}

\begin{figure}[t]
  \begin{small}
\begin{verbatim}
#include<civlc.h>
#define TAG 0
#define NPROCS 2
#define NTHREADS 2

$gcomm gcomm = $gcomm_create($here, NPROCS);

void MPI_Process (int rank) {
  $comm comm = $comm_create($here, gcomm, rank);
  $proc threads[NTHREADS];
  
  void Thread(int tid) {
    int x = rank;
    $message in, out = $message_pack(rank, 1-rank, TAG, &x, sizeof(int));
    
    for (int j=0; j<2; j++) {
      if (rank == 1) {
        for (int i=0; i<2; i++) $comm_enqueue(comm, out);
        for (int i=0; i<2; i++) in = $comm_dequeue(comm, 1-rank, TAG);
      } else {
        for (int i=0; i<2; i++) in = $comm_dequeue(comm, 1-rank, TAG);
        for (int i=0; i<2; i++) $comm_enqueue(comm, out);
      }
    }
  }
  
  for (int i=0; i<NTHREADS; i++) threads[i] = $spawn Thread(i);
  for (int i=0; i<NTHREADS; i++) $wait(threads[i]);
  $comm_destroy(comm);
}

void main() {
  $proc procs[NPROCS];

  for (int i=0; i<NPROCS; i++) procs[i] = $spawn MPI_Process(i);
  for (int i=0; i<NPROCS; i++) $wait(procs[i]);
  $gcomm_destroy(gcomm);
}
\end{verbatim}
  \end{small}
  \caption{\texttt{mpi-pthreads.cvl}: CIVL-C model of a (defective)
    multithreaded MPI program.}
  \label{fig:mpithreads}
\end{figure}

Figure \ref{fig:mpithreads} is an example of a CIVL-C model of
multithreaded MPI program.  The program consists of two processes,
each of which spawns two threads.  All four threads issue
message-passing operations.

This example illustrates some of the message-passing primitives
provided in CIVL-C.  A \emph{global communicator} object is allocated
in the root scope.  The constant $\chere$ has type $\cscope$ and
refers to the scope in which the expression occurs; in this case it is
the root (i.e., file) scope.  This global communicator is declared to
have \texttt{NPROCS} \emph{places}; these are points from which
messages can be sent or received.  The function \verb!MPI_Process!  is
used to model an MPI process.  Each instance will create its own
\emph{local communicator} object which specifies the global
communicator and a place; this is the object that will be used to send
or receive messages at that place.

Each process spawns two instances of function \texttt{Thread}.  Each
thread creates a message object from a buffer, specifying the source
and destination places, tag, pointer to the beginning of the buffer,
and the size of the buffer.  The message is \emph{enqueued} into the
communication universe using the local communicator.  Similarly,
messages are dequeued by specifying the local communicator, source
place, and tag.

The program has a subtle defect, which only manifests on very specific
interleavings of the threads.   This defect can be found using
\texttt{civl verify}.

\section{Verifying C programs}
CIVL can be used to verify C programs, with a number of transformers. One can also insert macros to C programs to tune it for verification, which, most of time, involves defining input variables. This is usually accomplished by the default macro \texttt{\_CIVL}.

For example, Figure~\ref{fig:CIVLmacro} is a simple program that computes the sum of a number of positive numbers. The program can be compiled by any C compiler, as long as no \texttt{\_CIVL} macro is defined in the command for compiling. When CIVL runs this program, it will automatically have \texttt{\_CIVL} defined and thus \texttt{N} becomes an input variable and \texttt{sum} becomes an output variable and there is an assertion to check the correctness the sum computed by the program. 

If one wants to CIVL to treat a program as it is originally, then the command line option \texttt{-\_CIVL} can be set to false to disable the \texttt{\_CIVL} macro.

\begin{figure}[h]
\begin{small}
\begin{verbatim}
#ifdef _CIVL
#include<civlc.cvh>
#endif

#ifdef _CIVL
$input int N;
$output int sum;
#else
#define N 100
int sum;
#endif

void main() {
  int localsum = 0;
  for (int i = 1; i <= N; i++) {
    localsum+=i;
  } 
  sum = localsum;
#ifdef _CIVL
  $assert(sum == (N+1)*N/2);
#endif
}

\end{verbatim}
  \end{small}
  \caption{\texttt{\_CIVL}: the default macro}
  \label{fig:CIVLmacro}
\end{figure}


\subsection{Verifying MPI C programs}
CIVL generates default input variables for verifying MPI programs:
\begin{itemize}
\item \texttt{\_mpi\_nprocs}: number of MPI processes to be created;
\item \texttt{\_mpi\_nprocs\_lo}/\texttt{\_mpi\_nprocs\_hi}: lower/upper bound of the number of MPI processes to be created.
\end{itemize}

CIVL requires at least either \texttt{\_mpi\_nprocs} or \texttt{\_mpi\_nprocs\_hi} be specified in the command line in order to verify MPI programs (the default value of \texttt{\_mpi\_nprocs\_lo} is 1). For example, one can specify  \texttt{civl verify -input\_mpi\_nprocs=5 ring.c}. 

\subsection{Verifying OpenMP C programs}
CIVL introduces a default input variables \texttt{\_omp\_thread\_max} for OpenMP programs, and it needs to be specified in the command line. CIVL will create 1 to \texttt{\_omp\_thread\_max-1} threads for all OpenMP parallel region during the verification. If \texttt{\_omp\_thread\_max} is not specified, then somewhere in the OpenMP program must be specifying the number of threads explicitly. By default, CIVL applies simplification to OpenMP based on independent loop analysis, and optimally that might reduce the program to be purely sequential. The option \texttt{ompNoSimplify} can be set to false so as to skip such simplification. Another option, \texttt{ompLoopDecomp} can be used to specify the loop decomposition strategy, which can be \texttt{ALL}, \texttt{ROUND\_ROBIN} or \texttt{RANDOM}.

\subsection{Verifying Pthreads C  and CUDA C programs}
There are no special option or default input variables for Pthreads or CUDA programs.