= Contents =

* [#intro Introduction]
* [#lang Language]
* [#semantics Semantics]
* [#tools Tools]

= Introduction = #intro

== What is CIVL? ==

CIVL stands for ''Concurrency Intermediate Verification Language''.  The CIVL platform encompasses:

1. the programming language CIVL-C, a dialect of C with additional primitives supporting concurrency, specification, and modeling;
1. verification and analysis tools, including a symbolic execution-based model checker for checking various properties of, or finding defects in, CIVL-C programs; and
1. tools that translate from commonly-used languages/APIs to CIVL-C.

A user can write programs in CIVL-C directly, or use one of the front-ends that translates from a "real" programming language to CIVL-C.

When used in the first way, CIVL-C may be considered a modeling language, similar to Promela (the language used by the model checker Spin).  This is useful for exploring and verifying algorithms, especially concurrent algorithms.  The main difference between CIVL-C and Promela is that CIVL-C includes almost all of the language constructs in C, including floating-point numbers, arrays of any type, structs, functions, pointers,  dynamic allocation (malloc and free), and pointer arithmetic.    Like Spin, the CIVL verifier can be used to perform an exhaustive search of a state space.  Unlike Spin, the CIVL verifier uses symbolic execution, so in a CIVL state, variables may be assigned symbolic expressions, not just concrete values.   This allows the verifier to check properties of the form ''the assertions hold for all possible inputs'' and ''the two given programs are functionally equivalent.''

When used in the second way, a C program using MPI, CUDA, OpenMP, or Pthreads, (or even some combination of these 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:

1. this introduction, including "quick start" instructions for downloading and installing CIVL and several examples;
1. a complete description of the CIVL-C language;
1. a formal semantics for the language; and
1. a description of the tools in the framework.

== Installation and Quick Start ==

1. Install the automated theorem prover CVC4, following instructions at http://cvc4.cs.stanford.edu/web/.  You only need the binary (`cvc4`), which must be in your `PATH`.
1. Install the automated theorem prover Z3, following instructions at https://github.com/Z3Prover/z3.  You only need the binary (`z3`), which must be in your `PATH`.
1. Install a Java 8 SDK.   Later versions of Java may also work.  See https://www.oracle.com/technetwork/java/javase/downloads/index.html.
1. Download and unpack the latest stable release of CIVL from http://vsl.cis.udel.edu/lib/sw/civl/current/latest/release/.
1. The resulting directory should be named CIVL-tag for some string tag which identifies the version of CIVL you downloaded. Move this directory wherever you like.
1. The JAR file in the `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 `java -jar /path/to/civl-TAG.jar ...`. For convenience, you may instead use the shell script `civl` included in the `bin` directory. This allows you to replace `java -jar /path/to/civl-TAG.jar` with just `civl` on the command line. Simply edit the `civl` script to reflect the path to the JAR file and place the script somewhere in your `PATH`.  In the following, we assume you have done this.
1. From the command line, type `civl help`. You should see a help message describing the command line syntax.
1. From the command line, type `civl config`. This should report that cvc4 and z3 were found, and it should create a file named `.sarl` in your home directory.

To test your installation, copy the file `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 `civl verify locksBad.cvl`. You should see some output culminating in a message 

`The program MAY NOT be correct.  See CIVLREP/locksBad_log.txt.`

Type `civl replay locksBad.cvl`. You should see a step-by-step account of how the program arrived at the deadlock.


== Verifying  Different Kinds of Programs ==

=== Verifying CIVL-C Programs ===

Dijkstra’s well-known Dining Philosophers system can be encoded in CIVL-C as follows:

{{{
$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);
}
}}}

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

Both `B` and `n` are declared as input variables using the type qualifier `$input`. 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 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 `B` on the command line.

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

A `$when` statement encodes a guarded command. The `$when` statement includes a boolean expression called the '''guard''' and a statement body. The `$when` statement is enabled if and only if the guard evaluates to '''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 body of each `$when` statement executes atomically with the guard evaluation.

The `$for` statement is very similar to a '''for''' loop. The main difference is that it takes a '''domain''' and loops over it.

The `$parfor` statement is a combination of `$for` and `$spawn`. 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:

{{{
civl verify -inputB=5 diningBad.cvl
}}}

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 minimal counterexample, i.e., a deadlocking trace of minimal length. To find a minimal counterexample, we issue the command

{{{
civl verify -inputB=5 -min diningBad.cvl
}}}

The result of this command is shown in Figure 4.2. 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

{{{
civl replay -showTransitions diningBad.cvl
}}}

The result of this command is shown in Figure 4.3. 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.



=== Verifying C Programs ===



=== Verifying C/MPI Programs ===



=== Verifying C/OpenMP Programs ===



=== Verifying CUDA-C Programs ===



=== Verifying C/Pthreads Programs ===



=== Verifying Fortran Programs ===



(under development)



= The CIVL-C Language = #lang



= Semantics = #semantics


= Command-line Tools = #tools