CIVL: The Concurrency Intermediate Verification Language

------------------------------ Overview -------------------------------

CIVL is a framework encompassing...

 * a programming language, CIVL-C, which adds to C a number of
    concurrency primitives, as well as the ability to define
    functions in any scope.  Together, these features make for
    a very expressive concurrent language that can faithfully
    represent programs using various APIs and parallel languages,
    such as MPI, OpenMP, CUDA, and Chapel. CIVL-C also provides
    a number of primitives supporting verification.
 * a model checker> which uses symbolic execution to verify a
    number of safety properties of CIVL-C programs.   The model
    checker can also be used to verify that two CIVL-C programs
    are functionally equivalent.
 * a number of translators from various commonly-used languages
   and APIs to CIVL-C. (This part is still a work in progress.)

CIVL is developed by the Verified Software Laboratory at the
University of Delaware Department of Computer Science.
For more information, visit http://vsl.cis.udel.edu/civl

Developers:

Stephen F. Siegel
Timothy K. Zirkel

---------------------------- Installation -----------------------------

You must have a Java virtual machine (version 7) installed on your 
system and "java" should be in your path.

Installation for Mac OS X:

The complete distribution for Mac OS X 64-bit Intel
comes in a folder named CIVL-TAG, where TAG is some version
id string.  This folder contains the following:

 - README : this file
 - bin : containing one executable sh script called "civl"
 - lib : containing civl-TAG.jar and native libraries
         used by CIVL
 - doc : containing some documentation about CIVL
 - licenses : licenses for CIVL and included libraries
 - examples : some example CIVL programs

Installation instructions:
  1. Move folder CIVL-TAG into the /Applications folder
  2. Put the civl script in your path however you like to put things
     into your path.   Either move it to a directory in your path,
     or create a symlink to it, or edit your .profile or equivalent
     to put it in your path.

Now you should be able to run CIVL from the command line by 
typing "civl <filename>".

Installation for Linux:

Same as above, except the folder goes into /usr/local.

------------------------------- License -------------------------------

CIVL is open source software distributed under the GNU
General Public License.  However, the libraries used by CIVL
(and incorporated into the complete distribution) use various
licenses.  See directory licenses for the license of each component.


The CIVL-C code will not have an explicit "Root" procedure.  Instead,
a Root procedure will be implicitly wrapped around the enitre code.
The global input variables will become the inputs to the Root
procedure.  A "main" procedure must be delcared that takes
no parameters but can have any return type.   The body of the
main procedure becomes the body of the Root procedure.   The return
type of the main procedure becomes the return type of the body.
The main procedure disappears.

------------------------ Language Summary -----------------------------

Summary of new keywords:

  $proc : the process type
  $self : the process invoking the statement (constant of type $proc)
  $input : type qualifier declaring variable to be a program input
  $output : type qualifier declaring variable to be a program output
  $spawn : create a new process running procedure
  $wait : wait for a process to terminate
  $assert : check something holds
  $true : boolean value true, used in assertions
  $false: boolean value false, used in assertions
  $assume : assume something holds
  $when : guarded statement
  $choose : nondeterministic choice statement
  $invariant : declare a loop invariant
  $requires : procedure precondition
  $ensures : procedure postcondition
  $result : refers to result returned by procedure in contracts
  @ : refer to variable in other process, e.g., p@x
  $collective : a collective expression

Other syntactic changes:

  - procedure definitions may occur in any scope

------------------------------------------------------------------------

Detailed description:

$proc : this is a primitive object type and functions like any other
primitive C type (e.g., int).  An object of this type refers
to process.  It can be thought of as a process ID, but it is not
an integer and cannot be cast to one.  Certain expressions take
an argument of $proc type and some return something of $proc type.

------------------------------------------------------------------------

$self: this is a constant of type $proc.  It can be used wherever
an argument of type $proc is called for.  It refers to the process
that is evaluating the expression containing "$self".

------------------------------------------------------------------------

$input : A variable in the global scope only may be declared with this
type modifier indicating it is an "input" variable, as in

$input int n;

As explained above, the variable becomes a parameter to the Root
procedure.  This is used when comparing two programs for functional
equivalence.  The two programs are functionally equivalent if,
whenever they are given the same inputs (i.e., corresponding $input
variables are initialized with the same values) they will produce the
same outputs (i.e., corresponding $output variables will end up with
the same values at termination).

------------------------------------------------------------------------

$output : A variable in the global scope may be declared with
this type modifier to declare it to be an output variable.

------------------------------------------------------------------------

$spawn : this is an expression with side-effects.  It spawns a new
process and returns a reference to the new process, i.e., an object of
type $proc.  The syntax is the same as a procedure invocation with the
keyword "$spawn" inserted in front:

$spawn f(expr1, ..., exprn)

Typically the returned value is assigned to a variable, e.g.,

$proc p = $spawn f(i);

If the invoked function f returns a value, that value is simply
ignored.

------------------------------------------------------------------------

$wait: this is a statement that takes an argument of type $proc
and blocks until the referenced process terminates:

$wait expr;

------------------------------------------------------------------------

$assert: This is an assertion statement.  It takes as its sole
argument an expression of boolean type.   The expressions have a 
richer syntax than C expressions.  During verification, the
assertion is checked.  If it does not hold, a violation is reported.

$assert expr;

Boolean values $true and $false may be used in assertions
and assumptions.

------------------------------------------------------------------------

$assume: This is an assume statement. Its syntax is the same as that
of $assert.  During verification, the assumed expression is assumed to
hold.  If this leads to a contradiction on some execution, that
execution is simply ignored.  It never reports a violation, it only
restricts the set of possible executions that will be explored by the
verification.

$assume expr;

------------------------------------------------------------------------

$when (expr) stmt;

A guarded command.

All statements have a guard, either implicit or explicit.  For most
statements, the guard is "true".  The $when statement allows one to
attach an explicit guard to a statement.

 When expr is true, the statement is enabled, otherwise it is
disabled.  A disabled statement is "blocked"---it will not be
scheduled for execution.  When it is enabled, it may execute by moving
control to the stmt and executing the first atomic action in the stmt.

If stmt itself has a guard, the guard of the $when statement is
effectively the conjunction of the expr and the guard of the stmt.

The evaluation of expr and the first atomic action of stmt effectively
occur as a single atomic action.  There is no guarantee that execution
of stmt will continue atomically if it contains more than one atomic
action, i.e., other processes may be scheduled.

Examples:

$when (s>0) s--;

This will block until s is positive then decrement s.  The execution
of s-- is guaranteed to take place in an environment in which s is
positive.

$when (s>0) {s--; t++}

The execution of s-- must happen when s>0, but between s-- and t++,
other processes may execute.

$when (s>0) $when (t>0) x=y*t;

This blocks until both x and t are positive then executes
the assignment in that state.  It is equivalent to

$when (s>0 && t>0) x=y*t;

------------------------------------------------------------------------

A $choose statement has the form

$choose {
  stmt1;
  stmt2;
  ...
  default: stmt
}

The "default" clause is optional.

The guards of the statements are evaluated and among those that are
true, one is chosen nondeterministically and executed.  If none are
true and the default clause is present, it is chosen.  The default
clause will only be selected if all guards are false.  If no default
clause is present and all guards are false, the statement blocks.
Hence the implicit guard of the $choose statement without a default
clause is the disjunction of the guards of its sub-statements.
The implicit guard of the $choose statement with a default clause
is "true".

Example: this shows how to encode "low-level" CIVL:

l1: $choose {
  $when (x>0) {x--; goto l2;}
  $when (x==0) {y=1; goto l3;}
  default: {z=1; goto l4;}
}
l2: $choose {
  ...
}
l3: $choose {
  ...
}

------------------------------------------------------------------------

$invariant: indicates a loop invariant.  Each C loop construct has an
optional invariant clause as follows:

while (expr) $invariant (expr) stmt

for (e1; e2; e3) $invariant (expr) stmt

do stmt while (expr) $invariant (expr) ;

The invariant is a claim that if if the expr holds upon entering 
the loop and the loop condition holds, then it will hold
after completion of execution of the loop body.

The invariant is used by certain verification techniques.

------------------------------------------------------------------------

Procedure contracts: $requires and $ensures.  There are optional
elements that may occur in a procedure declaration or definition:

T f(...)
  $requires expr;
  $ensures expr;
;

or

T f(...)
  $requires expr ;
  $ensures expr ;
  {
    ...
  }

The value $result may be used in post-conditions to refer
to the result returned by a procedure.

------------------------------------------------------------------------

expr@x: remote expressions refer to a variable in another process,
e.g., procs[i]@x.  This special kind of expression is used in
collective expressions, which are used to formulate collective
assertions and invariants.

The expr must have $proc type.  The variable x must be a statically 
visible variable in the context in which it is occurs.  When
this expression is evaluated, the evaluation context will be shifted
to the process referred to by the expr.

------------------------------------------------------------------------

$collective(proc_expr, int_expr) expr 

This is a collective expression over a set of processes.  The
proc_expr is a pointer to the first element of an array of $proc.  The
int_expr gives the length of that array, i.e., the number of
processes.  expr is a boolean-valued expression; it may use remote
expressions to refer to variables in the processes specified in the
array.
  
example:

$proc procs[N];
...
$assert $collective(procs, N) i==procs[(pid+1)%N]@i ;