source: CIVL/README@ ac5660f

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

For most users, this will be the easiest way to install and use CIVL.

1. Install a Java 7 SDK if you have not already.  Go to
http://www.oracle.com/technetwork/java/javase/downloads/ for the
latest from Oracle.  On linux, you can optionally sudo apt-get install
openjdk-7-jdk.

2. If you already have the VSL dependencies library, you may
skip this step.  Otherwise, download the archive of VSL
dependencies from http://vsl.cis.udel.edu/tools/vsl_depend,
choosing the version for your OS type (32-bit linux,
64-bit linux, or 64-bit OS X).  Unzip and untar the
downloaded .tgz file and you will have a folder named "vsl".
If you do not already have a directory /opt, create one with
"mkdir /opt".  Move vsl into /opt.  Use sudo as needed.

3. Download the appropriate CIVL distribution from
http://vsl.cis.udel.edu/civl.

4. Unzip and untar the downloaded file if this does not happen
automatically.  This should result 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
 - doc : containing some documentation about CIVL
 - licenses : licenses for CIVL and included libraries
 - examples : some example CIVL programs

5. Move CIVL-TAG into /opt.

6. Put the civl script in your path however you like to put things
in 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.

---------------------------- CIVL help -----------------------------

In command line, type just "civl help" for the usage information 
as shown below.

CIVL v0.4 of 2013-12-06 -- http://vsl.cis.udel.edu/civl
Usage: civl <command> <options> filename ...
Commands:
  verify : verify program filename
  run : run program filename
  help : print this message
  replay : replay trace for program filename
  parse : show result of preprocessing and parsing filename
  preprocess : show result of preprocessing filename
Options:
  -debug or -debug=BOOLEAN (default: false)
    debug mode: print very detailed information
  -errorBound=INTEGER (default: 1)
    stop after finding this many errors
  -guided or -guided=BOOLEAN
    user guided simulation; applies only to run, ignored
    for all other commands
  -id=INTEGER (default: 0)
    ID number of trace to replay
  -inputKEY=VALUE
    initialize input variable KEY to VALUE
  -maxdepth=INTEGER (default: 2147483647)
    bound on search depth
  -min or -min=BOOLEAN (default: false)
    search for minimal counterexample
  -por=STRING (default: std)
    partial order reduction (por) choices:
    std (standard por) or scp (scoped por)
  -random or -random=BOOLEAN
    select enabled transitions randomly; default for run,
    ignored for all other commands
  -saveStates or -saveStates=BOOLEAN (default: true)
    save states during depth-first search
  -seed=STRING
    set the random seed; applies only to run
  -showModel or -showModel=BOOLEAN (default: false)
    print the model
  -showProverQueries or -showProverQueries=BOOLEAN (default: false)
    print theorem prover queries only
  -showQueries or -showQueries=BOOLEAN (default: false)
    print all queries
  -showSavedStates or -showSavedStates=BOOLEAN (default: false)
    print saved states only
  -showStates or -showStates=BOOLEAN (default: false)
    print all states
  -showTransitions or -showTransitions=BOOLEAN (default: false)
    print transitions
  -simplify or -simplify=BOOLEAN (default: true)
    simplify states?
  -solve or -solve=BOOLEAN (default: false)
    try to solve for concrete counterexample
  -sysIncludePath=STRING
    set the system include path
  -trace=STRING
    filename of trace to replay
  -userIncludePath=STRING
    set the user include path
  -verbose or -verbose=BOOLEAN (default: false)
    verbose mode

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

------------------------ 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 ;