Civl Syntax

Layered Concurrent Programs

Introducing and Hiding Variables

Refinement Checking

Mover Types

Yield Invariants

Linear Typing and Permissions

Summarizing Asynchrony

Quantifier-Instantiation Pools

# Civl Syntax

Civl is an extension of Boogie. In Boogie, (almost every) abstract syntax tree node can be annotated with attributes of the form `{:attr e1, e2, ...}`, where `attr` is the attribute name and `e1, e2, ...` are expressions (denoting parameters of the attribute). Running `boogie -attrHelp` prints all supported attributes. Civl programs are specified using syntactic extensions to Boogie as well as attributes. This section provides a brief overview of Civl syntax.

## Types, Functions, Constants

Types, functions, and constants are declared just as in Boogie.

## Global Variables

Global variables have a layer range.

``````var {:layer 0,10} x:int;
``````

Global variable `x` is introduced at layer `0` and hidden at layer `10`. We call `0` the introduction/lower layer of `x`, and `10` the disappearing/upper layer of `x`. The layer range `{:layer n}` on a global variable is identical to `{:layer n,n}`.

## Actions

Atomic actions are the building blocks of a Civl program, encapsulating all accesses to global variables.

An atomic action typically has a mover type and a layer range. The mover type is either `atomic` (non-mover), `right` (right mover), `left` (left mover), or `both` (both mover). The body of an atomic action consists of a sequence of assert commands, called the gate, followed by a loop-free block of code, denoting a transition relation.

``````atomic action {:layer 2,5} FOO (i: int) returns (j: int)
modifies x;
{
assert x > 0;
j := x;
x := x + i;
}
``````

Atomic action `FOO` is available from layer `2` up to layer `5` (introduced at layer `2` and disappearing at layer `5`). The gate of `FOO` is `x > 0`, and the transition relation states that output parameter `j` returns the current value of global variable `x`, and the value of input parameter `i` is added to `x`. The layer range `{:layer n}` on an action is identical to `{:layer n,n}`. Actions may call other actions as long as the call graph is acyclic and for each call the caller’s layer range is contained in the callee’s layer range.

It is possible to declare an atomic action without a mover type. Civl does not add such an action to the pool of actions over which the checking of mover types is performed. Consequently, such actions are used in a restricted manner, notably for linking two layers across which the set of global variables differ and for providing auxiliary invariants and abstractions as proof hints.

## Yield Invariants

A yield invariant has a layer number and a sequence of `invariant` clauses (but no body).

``````yield invariant {:layer 1} yield_x(i: int);
invariat i <= x;
``````

Yield invariant `yield_x` states that global variable `x` is greater than or equal to parameter `i`. This invariant is applicable to reasoning only at layer `1`.

## Yielding Procedures

Yielding procedures describe the actual concurrent program. There are two kinds: action procedures that get summarized by atomic actions, and mover procedures that get summarized by pre/postconditions.

### Action Procedure

An action procedure has a disappearing layer and a refined atomic action. The `modifies` clause is implicit and contains all global variables.

``````yield procedure {:layer 1} foo (...) returns (...);
refines FOO;
``````

Action procedure `foo` disappears at layer `1` and refines the atomic action `FOO`.

If no `refines` clause is given, then the procedure is called a skip procedure which refines the implicitly declared atomic action `SKIP`.

``````both action {:layer 0,∞} SKIP () { }
``````

### Mover Procedure

A mover procedure has a disappearing layer and a mover type. The `modifies` clause has to be provided.

``````yield right procedure {:layer 1} foo (...) returns (...);
modifies ...;
``````

## Implementations

The implementations (i.e., bodies) of yielding procedures support the following additional commands.

• Parallel call: `par i := A(j) | k := B(l)`
• Asynchronous call: `async call A(i)`

## Specifications

Every precondition, postcondition, assertion, and loop invariant is annotated with a list of layer numbers (`{:layer l1, l2, ...}`).

Yield invariants can be invoked in calls, parallel calls, as preconditions (`requires call`), postconditions (`ensures call`), and loop invariants (`invariant call`).

Every loop is either non-yielding or yielding (denoted with `:yields` on a loop invariant with condition `true`).

A call may be annotated with `:mark`.

## Parameters

Every input and output parameter of a yielding procedure has a layer range. Implicitly, it ranges from the lowest layer up to the disappearing layer of the procedure. A different layer range can be assigned to every parameter using the `:layer` attribute.

Parameters of action procedures can be annotated with `:hide` to declare that the parameter does not occur in the refined atomic action.

## Pure Procedures

Pure procedures do not read or modify global variables. These procedures support the injection of (potentially unverified) facts and proof hints. In particular, this is a useful alternative to global quantified axioms.

``````pure procedure Lemma_add_to_set (x: X, set: [X]bool);
requires !set[x];
ensures card(set[x := true]) == card(set) + 1;
``````

The pure procedure `Lemma_add_to_set` states the fact about set cardinality, that adding an element to a set increases the sets cardinality by one.

# Layered Concurrent Programs

Civl takes as input a layered concurrent program. A layered concurrent program represents a sequence of concurrent programs, from most concrete (e.g., a low-level implementation) to most abstract (e.g., a high-level specification). Civl verifies a layered concurrent program by verifying each layer and the connection between adjacent layers separately.

In this section we show a basic example to explain how a layered concurrent program represents a sequence of increasingly simpler concurrent programs. Understanding this foundational aspect of Civl will make it easier to understand everything explained later.

## A Simple Layered Concurrent Program

``````var {:layer 0,2} x: int;

pure action Add(a: int, b: int) returns (c: int)
{ c := a + b; }

yield procedure {:layer 0} Incr(val: int)
refines AtomicIncr;
{
call {:layer 0} x := Add(x, val);
}
left action {:layer 1} AtomicIncr(val: int)
modifies x;
{ x := x + val; }

yield procedure {:layer 1} IncrBy2()
refines AtomicIncrBy2;
{
par Incr(1) | Incr(1);
}
atomic action {:layer 2} AtomicIncrBy2()
modifies x;
{ x := x + 2; }

yield procedure {:layer 2} Main()
{
call IncrBy2();
}
``````

The program above represents three concurrent programs, at layers 0, 1, and 2, that share parts of their code. Layer 0 is the most concrete and layer 2 is the most abstract. The annotation `{:layer 0,2}` on global variable `x` is a range of layers from 0 to 2 indicating that `x` exists at all layers in this layer range. The global variable `x` is introduced at layer 0 via a call to the pure action `Add` and hidden at layer 2. Introduction and hiding of global and local variables is explained in detail in a later section. The annotation `{:layer 0}` on `Incr` indicates that 0 is the highest layer on which `Incr` exists. The annotation `refines AtomicIncr` on `Incr` indicates that on layers greater than 0 a call to `Incr` is rewritten to a call to `AtomicIncr`. Similarly, procedure `IncrBy2` exists on layers 1 and lower and is replaced by `AtomicIncrBy` at layers above 1.

### Program at Layer 0

``````var x: int;

pure action Add(a: int, b: int) returns (c: int)
{ c := a + b; }

yield procedure Incr(val: int)
{
}

yield procedure IncrBy2()
{
par Incr(1) | Incr(1);
}

yield procedure Main()
{
call IncrBy2();
}
``````

The layer-0 program is shown above. Procedure `IncrBy2` creates two tasks via a parallel call to `Incr`, each instance of which makes a single call to the atomic action `Intro_x`. Preemptions can occur at entry into or exit from `Main`, `IncrBy2`, or `Incr`.

### Program at Layer 1

``````var x: int;

atomic action AtomicIncr(val: int)
modifies x;
{ x := x + val; }

yield procedure IncrBy2()
{
call AtomicIncr(1);
call AtomicIncr(1);
}

yield procedure Main()
{
call IncrBy2();
}
``````

In the layer-1 program, shown above, the parallel call to `Incr` is rewritten to a sequence of calls to `AtomicIncr`. The justification for this rewrite is that `Incr` refines `AtomicIncr` and `AtomicIncr` is a left mover. Explanation for these concepts is presented later.

### Program at Layer 2

``````var x: int;

atomic action AtomicIncrBy2()
modifies x;
{ x := x + 2; }

yield procedure Main()
{
call AtomicIncrBy2();
}
``````

In the layer-2 program, shown above, the call to procedure `IncrBy2` in `Main` is rewritten to a call to atomic action `AtomicIncrBy2`. The justification for this rewrite is that `IncrBy2` refines `AtomicIncrBy2`.

## Layer Checking

The well-formedness of a layered concurrent programs is governed by a set of layer type-checking rules. These rules ensure that the individual program layers can be extracted and that the verification guarantees are justified. We can loosely distinguish between “data layering” and “control layering”.

Data layering concernes the variables (both global and local) that exist on each layer. In the example above, both global variable `x` and local variable `val` (the input parameter to `Incr` and `AtomicIncr`) exist on all program layers. In a later section we show how variables can be introduced and hidden, such that different layers have different state.

Control layering concerns the actions and yielding procedures that exist on each layer. As one of the most central aspects of Civl, this controls how the bodies of yielding procedures changes across layers. In a layered concurrent program, atomic actions cannot be called directly. Instead, yielding procedures can call other yielding procedures. For example, recall that `IncrBy2` in the layered program above makes calls to procedure `Incr`, as opposed to `AtomicIncr`. In the layer 0 program we still see this calls to `Incr`. Then, since `Incr` disappears at layer 0 and is abstracted by `AtomicIncr`, we see these calls replaced by calls to `AtomicIncr` in the layer 1 program. In general, a yielding procedure that disappears at layer `n` cannot make calls to yielding procedures that disappear on a layer greater than `n`. The simple case is that there are only calls to procedures that disappear on layers smaller than `n`. Then there are only calls to atomic actions left at layer `n`. There are only three exceptions when a yielding procedure can make calls to another yielding procedure with the same disappearing layer: (1) calls to skip procedures, (2) calls to mover procedures, and (3) calls that are annotated with `:mark`.

Data layering and control layering obviously interact, since the variables accessed by the control of a particular layer must indeed exist on that layer.

## Semantics

Civl considers two semantics for a concurrent program, the preemptive and the non-preemptive semantics. The preemptive semantics is the standard interleaving semantics, where context switches can happen at any time between the execution of atomic actions. This is the semantics that models the acutal behaviors of the concurrent program; the behaviors that we want to verify. By contrast, the non-preemptive semantics allows a context switch only at the entry to or exit from a procedure and at a call to a yield invariant. In particular, a context switch is not introduced just before or just after executing an atomic action. The non-preemptive semantics simplifies reasoning, because fewer interleavings have to be considered. Civl justifies going from the preemptive to the non-preemptive semantics using mover types.

A program location where a context switch may happen is called a yield location. Any execution path in a procedure from its entry to its exit is partitioned into a sequence of execution fragments from one yield location to the next. Each such execution fragment is called a yield-to-yield fragment. Notice that these yield-to-yield fragments are dynamically scoped. Yield locations specify the non-preemtive semantics. Civl checks that there are “sufficiently many” yield locations such that reasoning about the non-preemtive semantics is sufficient to reason about the preemptive semantics.

Going from preemtive to non-preemptive semantics simplifies the reasoning at one particular program layer. In going from the layer-0 program to the layer-2 program, the set of yield locations progressively reduces because invocations of yielding procedures are replaced by invocations of atomic actions, thereby leading to simplified reasoning at the higher layer.

# Introducing and Hiding Variables

In a multi-layered refinement proof it is not only useful to change the granularity of atomicity, but also the state representation, i.e., the set of variables over which different program layers are expressed. In this section, we describe how Civl supports introduction and hiding of both global and local variables.

In the following example program, the usage of variable `x` is changed into the usage of variable `y`.

``````var {:layer 1,2} y:int;
var {:layer 0,1} x:int;

atomic action {:layer 2} atomic_read_y () returns (v:int)
{ v := y; }
yield procedure {:layer 1} read_y () returns (v:int)
requires {:layer 1} x == y;
{
}

atomic action {:layer 2} atomic_write_y (y':int)
modifies y;
{ y := y'; }
yield procedure {:layer 1}  write_y (y':int)
refines atomic_write_y;
{
call write_x(y');
call {:layer 1} y := Copy(x);
}

atomic action {:layer 1} atomic_read_x () returns (v:int)
{ v := x; }
yield procedure {:layer 0} read_x () returns (v:int)
{
call {:layer 0} v := Copy(x);
}

atomic action {:layer 1} atomic_write_x (x':int)
modifies x;
{ x := x'; }
yield procedure {:layer 0} write_x (x':int)
refines atomic_write_x;
{
call {:layer 0} x := Copy(x');
}
``````

First, consider the layer ranges of `x` and `y`. Variable `x` is introduced at layer 0 and hidden at layer 1, while `y` is introduced at layer 1 and hidden at layer 2. Thus, they “overlap” at layer 1. At layer 1 we have the atomic actions `atomic_read_x` and `atomic_write_x`, which read from and write to `x`, respectively. These actions are called by the yielding procedures `read_y` and `write_y`, respectively. Now we want to show that `read_y` refines `atomic_read_y`, and `write_y` refines `atomic_write_y`. Since `read_y` has the precondition `x == y` (the invariant that expresses our intended connection between `x` and `y`), we know that after reading `x` into the output variable `v`, also `v == y` holds, which is all we need to prove that `read_y` refines `atomic_read_y`. In `write_y`, the input variable `y'` is written to `x` by `write_x`. But what about `y`? To express our intention for `y` we call the action `Copy`, a pure action defind in the Civl base library which copies its input into its output. We often use calls to `Copy`, together with a layer annotation to introduce computation. This particular call sets `y` to the current value of `x`, which at the time of invocation is `y'`. Thus we get `y == y'` and we can prove that `write_y` refines `atomic_write_y`.

Invocation of `Copy` has the specific purpose of assigning meaning to introduced variables. Such a call is a kind of ghost code that does not cause a context switch; recall that `atomic_write_x` and `Copy` need to execute without context switch to ensure `y == y'`.

We have the following layering constraints:

• An action can access any global variable that exists throughout the layer range of the action. For example, `x` is introduced at layer 0 before `atomic_read_x` at layer 1, and is hidden at layer 1 together with `atomic_read_x`. It is not permissible to introduce `atomic_read_x` at layer 0.
• A pure action may not access any global variable and must not block. A pure action may be directly called by a yield procedure to introduce computation at a layer indicated by an attribute `{:layer n}` on the call. For such a call, the inputs may refer to any variable that exists at `n` or is introduced at `n`. Any output of the call must be received in a variable that is introduced at `n`.

Variable introduction and hiding create the possibility of two different programs at each layer, called the low program and the high program of the layer. The high program at layer n contains all the code of the low program at n together with calls to actions without mover types that introduce variables at layer n. Neither the low nor the high program at layer n contains the variables hidden at n. The variables introduced at layer n and the actions that introduce them are present in the high program but not the low program at layer n. Refinement checking at a layer is performed on the high program of that layer.

The earlier example only showed the high program at each layer. In that example, since the only layer at which variables are introduced is layer 0, the low and high programs coincide at all layers except 0. In the program described in this section, `x` is introduced at layer 0 and `y` is introduced at layer 1. Consequently, we have the following:

• The low program at layer 0 does not contain any variables; the high program at layer 0 contains only `x`.
• The low program at layer 1 contains only `x`; the high program at layer 1 contains both `x` and `y`.
• The low and high programs at layer 2 are identical and contain only `y`.

# Refinement Checking

We now explain how the specification `refines AtomicIncrBy2` is checked on the implementation of the procedure `IncrBy2`. This refinement checking justifies the transformation of the layer-1 program to the layer-2 program. Civl checks that along each execution path in `IncrBy2` from entry to exit, there is exactly one yield-to-yield fragment that behaves like `AtomicIncrBy2`. (In this particular example, `IncrBy2` consists of only a single yield-to-yield fragment at layer 1.) All other yield-to-yield fragments before and after this unique fragment leave state visible to the environment of `IncrBy2` unchanged. The visible state for `IncrBy2` includes only the global variable `x`. In general, visible state for a procedure includes global variables and output variables of the procedure.

The signature of a procedure and its refined action must match unless a parameter of the procedure is annotated with `:hide` in which case this parameter may be omitted from the signature of the refined action. If a global variable is hidden at the disappearing layer of a procedure, then the visible state over which refinement is checked does not include this variable. Similary, any output parameter of the procedure annotated with `:hide` is excluded from the visible state.

If a yield procedure omits the refines clause, it is expected to refine the SKIP action. This is tantamount to annotating each parameter of the procedure with `:hide`. Since the SKIP action does not modify any variable, every yield-to-yield fragment in the procedure is allowed to modify only those global variables that are hidden at the disappearing layer of the procedure.

A call marked by `:mark` attribute is treated specially during refinement checking. Such a call must be to a callee procedure with the same disappearing layer as the caller. It is expected that the refined action of the callee, when substituted at the call site, is the unique step at which the caller’s refined action appears to happen.

# Mover Types

In this section, we explain how Civl exploits commutativity of atomic actions to justify reasoning about non-preemptive semantics at each layer. Civl allows each atomic action to be labeled by one of four mover types: `atomic`, `left`, `right`, and `both`. The following code illustrates mover types for atomic actions.

``````var {:layer 0,1} x:int;

yield invariant {:layer 1} yield_x(n: int);
invariant x >= n;

yield procedure {:layer 0} Incr(val: int);
refines AtomicIncr;
both action {:layer 1} AtomicIncr(val: int)
modifies x;
{ x := x + val; }

yield procedure {:layer 1} p()
requires call yield_x(5);
ensures call yield_x(8);
{
call Incr(1);
call Incr(1);
call Incr(1);
}
``````

The atomic action `AtomicIncr` is labeled with the mover type `both`, indicating that it is both a left mover and a right mover. Consequently, the calls to `Incr` in `p` do not have to be separated by a yield. The calls to `Incr` in `p` commute with atomic actions executed by other threads so that they all appear to execute together. The use of mover types leads to fewer yields and more efficient verification of the body of `p`.

In general, Civl checks that the sequence of mover types of the atomic actions in every yield-to-yield fragment matches the expression `(right-mover)*;(non-mover)?;(left-mover)*`, i.e., a sequence of right movers, followed by at most one non-mover, followed by a sequence of left movers. The mover types of atomic actions are validated using pairwise commutativity checks between all atomic actions that exist together on some layer.

## Mover Procedures

Sometimes it can be convenient to reason about a yielding procedure without abstracting it to an atomic action. For this purpose, Civl supports mover procedures, which we illustrate in the following example.

``````var {:layer 0,2} x : int;

yield left procedure {:layer 1} inc(i : int)
modifies x;
requires {:layer 1} i >= 0;
ensures {:layer 1} x == old(x) + i;
{
if (i > 0)
{
call inc_x(1);
call inc(i-1);
}
}

yield procedure {:layer 0} inc_x(n: int);
refines atomic_inc_x;
both action {:layer 1} atomic_inc_x(n: int)
modifies x;
{ x := x + n; }
``````

In the program above, the mover procedure `inc` is annotated with the mover type `left`. This annotation is applicable to `inc` only at its disappearing layer 1. This annotation indicates that, at layer 1, any execution of the implementation of `inc` can be considered an indivisible computation that behaves like a left mover and is summarized by the layer-1 preconditions and postconditions of `inc`. A mover procedure that disappears at layer `n` can only be called by yielding procedures that also disappear at layer `n`.

## Abstraction aids Commutativity

Often, a program may use atomic actions that are neither right nor left movers and hence cannot be commuted with actions performed by other threads. However, it may be possible to create abstractions of the program’s atomic actions so that important actions achieve a commuting mover type.

``````var {:layer 0,2} x:int;

yield procedure {:layer 0} Incr(val: int);
refines AtomicIncr;
atomic action {:layer 1} AtomicIncr(val: int)
modifies x;
{ x := x + val; }

yield procedure {:layer 0} Read() returns (v: int);
atomic action {:layer 1} AtomicRead() returns (v: int)
{ v := x; }

yield procedure {:layer 1} _Incr(val: int)
refines AbstractAtomicIncr;
{
call Incr(val);
}
right action {:layer 2} AbstractAtomicIncr(val: int)
{ assert 0 <= val; x := x + val; }

yield procedure {:layer 1} _Read() returns (v: int)
{
}
left action {:layer 2} AbstractAtomicRead() returns (v: int)
{ assume x <= v; }
``````

In the code above, atomic actions `AtomicIncr` and `AtomicRead` at layer 1 are neither right nor left movers. At layer 2, we create abstractions `AbstractAtomicIncr` and `AbstractAtomicRead` of `AtomicIncr` and `AtomicRead` respectively. The abstractions are chosen so that `AbstractAtomicIncr` is a right mover and `AbstractAtomicRead` is a left mover.

# Yield Invariants

Reasoning about concurrent programs is difficult because of the possibility of interference among concurrently-executing procedures. Invariants are useful to express the possible interference and thus set up the context for refinement checking. Civl introduces yield invariants, a specification idiom that allows the programmer to factor out similar noninterference specifications into a single named and parameterized specification.

``````var {:layer 0,1} x:int;

yield procedure {:layer 0} Incr(val: int);
refines AtomicIncr;
atomic action {:layer 1} AtomicIncr(val: int)
modifies x;
{ x := x + val; }

yield invariant {:layer 1} yield_x(n: int);
invariant x >= n;

yield procedure {:layer 1} p()
requires call yield_x(old(x));
ensures call yield_x(old(x)+3);
{
call Incr(1);
call yield_x(x);
call Incr(1);
call yield_x(x);
call Incr(1);
}

yield procedure {:layer 1} q()
preserves call yield_x(old(x));
{
while (*)
invariant {:yields} true;
invariant call yield_x(old(x));
{
call Incr(3);
}
}
``````

The yield invariant `yield_x` is parameterized by `n` and states that the global variable `x` is no smaller than `n`. To use `yield_x`, the caller must supply an argument for the parameter `n`. There are six invocations of `yield_x` in the program, 4 in `p` and 2 in `q`. Let us first understand how `p` uses `yield_x`.

Procedure `p` invokes `yield_x` at entry using the annotation `requires call yield_x(old(x))` indicating that `old(x)` is passed for parameter `n`. The expression `old(x)` refers to the value of `x` just before `p` is invoked. The caller of `p` must ensure that `yield_x(old(x))` holds at entry to `p`, which is trivial given the meaning of `old(x)`. Procedure `p` also invokes `yield_x` at exit using the annotation `ensures call yield_x(old(x)+3)`, guaranteeing that `yield_x(old(x) + 3)` must hold at exit from `p`.

Procedure `q` uses the annotation `preserves call yield_x(old(x))` which is a shorthand for a pair of annotations `requires call yield_x(old(x))` and `ensures call yield_x(old(x))`. Procedure `q` also uses `invariant call yield_x(old(x))` to supply the noninterference condition at the yield at the head of the loop in `q`.

# Linear Typing and Permissions

Civl exploits linear typing to automatically inject logical assumptions when proving that a location or yield invariant is inteference-free or two actions commute with each other.

``````type {:linear "X"} Tid;
var {:layer 0,1} a:[Tid]int;

yield procedure {:layer 0} Read({:linear "X"} tid: Tid, i: int) returns (val: int);
both action {:layer 1} AtomicRead({:linear "X"} tid: Tid, i: int) returns (val: int)
{
val := a[tid];
}

yield procedure {:layer 0} Write({:linear "X"} tid: Tid, i: int, val: int);
refines AtomicWrite;
both action {:layer 1} AtomicWrite({:linear "X"} tid: Tid, i: int, val: int)
modifies a;
{
a[tid] := val;
}

yield procedure {:layer 1} YieldInv({:linear "X"} tid: Tid, v: int);
requires a[tid] == v;
``````

In the program above, the declaration of type `Tid` has the annotation `{:linear "X"}`. This annotation indicates that values of type `Tid` are permissions that must be distributed among the variables of the program without duplication. As the program executes, the permissions stored in the program variables may be redistributed but not duplicated, a condition that is verified by Civl. These permissions are associated with a domain called `X`; disjointness is enforced within a domain but not across domains. Different domains may use the same permission type. For example, if `Tid` is the permission type for a domain `Y` also, then we would use the declaration `type {:linear "X", "Y"} Tid;`.

It is not required for all variables of type `Tid` to contain permissions. To indicate that a variable contains permissions for domain `X`, it must have the annotation `{:linear "X"}`. The parameter `tid` of atomic action `AtomicRead` contains permissions. So does the parameter `tid` of `AtomicWrite`. Consequently, if a thread is executing `AtomicRead(tid1, i1)` and another is executing `AtomicWrite(tid2, i2, val2)`, `tid1` and `tid2` must be distinct from each other. This assumption is used to prove that `AtomicRead` and `AtomicWrite` are both movers.

Permissions are useful also for proving interference-freedom for location and yield invariants. The yield invariant `YieldInv` is proved interference-free against any yield-to-yield code fragment that mutates `a` using `AtomicWrite`.

## Permission Collectors

In some programs, it is helpful to make a distinction between the value stored in a variable and the permission associated with it. This increase in expressiveness is achieved by using a collector function from the type of the variable to the type of permissions.

``````datatype {:linear "perm"} Perm { Left(i: int), Right(i: int) }

function {:inline}{:linear "perm"} IntCollector(i: int) : [Perm]bool
{
MapConst(false)[Left(i) := true][Right(i) := true]
}
function {:inline}{:linear "perm"} IntSetCollector(iset: [int]bool) : [Perm]bool
{
(lambda p: Perm :: is#Left(p) && iset[i#Left(p)])
}

var {:layer 0,1} barrierOn: bool;
var {:layer 0,1} barrierCounter: int;
var {:layer 0,1} {:linear "perm"} mutatorsInBarrier: [int]bool;

atomic action {:layer 1} AtomicEnterBarrier({:linear_in "perm"} i: int)
returns ({:linear "perm"} p: Perm)
modifies barrierCounter, mutatorsInBarrier;
{
assert IsMutator(i);
mutatorsInBarrier[i] := true;
barrierCounter := barrierCounter - 1;
p := Right(i);
}

atomic action {:layer 1} AtomicWaitForBarrierRelease(
{:linear_in "perm"} p: Perm,
{:linear_out "perm"} i: int)
modifies barrierCounter, mutatorsInBarrier;
{
assert p == Right(i) && mutatorsInBarrier[i];
assume !barrierOn;
mutatorsInBarrier[i] := false;
barrierCounter := barrierCounter + 1;
}
``````

In the program above, the type `Perm` is a datatype with two constructors, `Left` and `Right`. `Perm` is the permission type for domain `perm`. The program variable that contain permissions in `Perm` are of type `int` and `[int]bool`. The latter type represents a set of integers encoded as a map from `int` to `bool`; the set contains exactly those integers that are mapped to `true`. The program defines two collectors, `IntCollector` and `IntSetCollector`. The former collects permissions for a variable of type `int` and the latter collects permissions for a variable of type `[int]bool`. The return type of each of these functions is `[Perm]bool`, representing a set of `Perm` values. There are two implicitly-defined and auto-generated collector functions for each permission type. These two collectors for the `Perm` type are shown below.

``````function {:inline} PermCollector(x: Perm) : [Perm]bool {
MapConst(false)[x := true]
}
function {:inline} PermSetCollector(xs: [Perm]bool) : [Perm]bool {
xs
}
``````

Permissions obtained by applying the collector function of the appropriate type to program variables continue to be distributed without being duplicated. The enforced invariant states that permissions obtained from two distinct variables are disjoint.

## Permission Redistribution

A variable that is annotated with `{:linear "D"}` for any domain `D` is a linear variable. Permissions are stored in a subset of the program’s linear variables and may be redistributed among them as the program executes. Civl performs a dataflow analysis to compute at each program location a set of available variables such that permissions in these variables are guaranteed to be disjoint. The set of available variables at a program location contains every global linear variable but may contain only a subset of the local linear variables in scope.

Consider the atomic action `AtomicEnterBarrier` in the program above. Input `i` of this action is annotated `{:linear_in "perm"}` indicating that the actual input variable corresponding to `i` at the call site must be available before the call and becomes unavailable after the call. Output `p` is annotated `{:linear "perm"}` indicating that the actual output variable corresponding to `p` at the call site becomes available after the call. The code of `AtomicEnterBarrier` redistributes the permissions stored in global variable `mutatorsInBarrier` and the input `i` among `mutatorsInBarrier` and output `p`. Civl checks that this redistribution does not cause duplication.

The atomic action `AtomicWaitForBarrierRelease` has an input `i` annotated `{:linear_out "perm"}`. This annotation indicates that the actual input variable corresponding to `i` at the call site will become available after the call.

Finally, the annotation `{:linear "perm"}` on an input parameter, although not used in the program above, would indicate that the correspoding actual input variable at the call site must be available before the call and remains available after the call.

# Summarizing Asynchrony

In this section, we focus on Civl features for summarizing asynchronous procedure calls.

``````yield procedure {:layer 1} Service()
{
async call Callback();
}

yield procedure {:layer 0} Callback();
``````

In the program above, the procedure `Service` makes an asynchronous call to the procedure `Callback`. Both procedures `Callback` and `Service` refine the `SKIP` action. At layer 1, the target of the asynchronous call to `Callback` in `Service` is rewritten to `SKIP`. Since `SKIP` does not have any visible effect, the Civl refinement checker is able to show that `Service` refines `SKIP` despite the asynchronous call in its implementation.

Next, we show how to synchronize an asynchronous call to an atomic action with visible side effects.

``````var {:layer 0,2} x:int;

yield procedure {:layer 1} Service()
refines A_Inc;
{
async call {:sync} Callback();
}

both action {:layer 1,2} A_Inc()
modifies x;
{ x := x + 1; }
yield procedure {:layer 0} Callback();
refines A_Inc;
``````

In the program above, the procedure `Service` makes an asynchronous call to the procedure `Callback`, similar to the first program shown in this section. The difference in this example is that both `Service` and `Callback` refine the atomic action `A_Inc` that increments a global variable `x`. Since `A_Inc` is a left mover (in fact, a both mover) it is possible to execute it exactly at the point of its asynchronous invocation. This intention is indicated by the `:sync` annotation on the asynchronous call.

## Pending asyncs

As described in the last section, Civl allows a procedure to make an asynchronous procedure call. Additionally and symmetrically, Civl also allows an atomic action to make an asynchronous call to an atomic action. Such a call is called a pending async, for brevity, to indicate that the effect of the asynchronous call is pending and becomes visible only once the side effects of the caller atomic action have been applied.

Pending asyncs increase the expressiveness of refinement in Civl. Without pending asyncs, summarizing the effect of a procedure that makes an asynchronous procedure call required synchronization of the call. With pending asyncs, it is possible to achieve this summarization via a pending async in the refined action. Civl also allows a pending async in an atomic action to be eliminated subsequently. The next example illustrates the Civl features that allow the user to create and eliminate pending asyncs.

``````var {:layer 0,3} x:int;

yield procedure {:layer 2} Client()
refines A_Inc;
{
call Service();
}

atomic action {:layer 1} A_Service()
creates A_Inc;
refines A_Inc;
{
call create_async(A_Inc());
}
yield procedure {:layer 0} Service()
refines A_Service;
{
async call Callback();
}

async both action {:layer 1,3} A_Inc()
modifies x;
{ x := x + 1; }
yield procedure {:layer 0} Callback();
refines A_Inc;
``````

The call to `Callback` in procedure `Service` is not annotated with `:sync`. Therefore, Civl infers that this call must be converted into a pending async to `A_Inc` in the refined action `A_Service`. The action `A_Inc` is qualified with the declaration `async` to indicate that it may be used as a pending async. An async action is not allowed to have any output parameters. A datatype declaration corresponding to the signature of such an action is automatically created by Civl. A value of this datatype may be used as parameter to the primitive `create_async` in atomic action specifications to create a pending async. The `creates` specification contains the name of each atomic action that may be created as a pending async. The atomic action `A_Service` creates a single pending async `A_Inc()`.

To complete the round trip, the pending async in the action `A_Service` is eliminated to get back the atomic action `A_Inc`. This elimination is indicated by the `refines A_Inc` specification on `A_Service`. Since `A_Inc` is a left mover, the verifier may pretend that the asynchronous call can be executed synchronously.

Finally, the procedure `Client` which itself calls `Service` is shown to refine `A_Inc` also. The target of this call is rewritten to `A_Service` at layer 1 and to `A_Inc` at layer 2.

## Inductive sequentialization

In the last example, we saw how to eliminate a single pending async from an action. Civl also provides a feature to eliminate unboundedly many pending asyncs from an action. We now show this technique, known as inductive sequentialization, using an example.

``````var {:layer 0,2} x:int;

both action {:layer 2} A_Add (n: int)
modifies x;
{ assert 0 <= n; x := x + n; }

action {:layer 1} INV(n: int)
creates A_Inc;
modifies x;
{
var {:pool "A"} i: int;
assert 0 <= n;
assume {:add_to_pool "A", i} {:add_to_pool "A", i+1} 0 <= i && i <= n;
x := x + i;
call create_multi_asyncs(MapConst(0)[A_Inc() := n - i]);
}

atomic action {:layer 1} Async_Add(n: int)
creates A_Inc;
{
assert 0 <= n;
call create_multi_asyncs(MapConst(0)[A_Inc() := n]);
}

async both action {:layer 1,2} A_Inc ()
modifies x;
{ x := x + 1; }
``````

The action `Async_Add` uses the primitive `create_multi_asyncs` to create `n` pending asyncs of action `A_Inc` each of which asynchronously increments the global variable `x` by 1. As before, the action `A_Inc` is a left mover. We would like to use the mover type of `A_Inc` to show that `Async_Add` refines an action `A_Add` that increments `x` by `n` in one atomic step.

To do this proof we use an auxiliary invariant `INV` and indicate it should be used for the refinement proof in the refines specification for `Async_Add`. The action `INV` is a generalization of `Async_Add`. `INV` includes every behavior of `Async_Add` and is also closed under extension by the eliminated action `A_Inc`. It is important to understand how `INV` is specified. The local variable `i` is initialized nondeterministically and constrained to be between `0` and `n`, both inclusive. The nondeterministic initialization choice represents the number of pending asyncs that have already executed, as indicated by the increment of `x` by `i`. Finally, the remaining `n-i` pending asyncs of `A_Inc` are created to indicate those pending asyncs that remain to be executed.

# Quantifier-Instantiation Pools

The example in the last section used attributes `:pool` and `:add_to_pool`. These attributes are used to provide hints for instantiating quantifiers, which are a notorious source of incompleteness and unpredictable performance in SMT solvers. In this section, we explain the use of these attributes.

We introduce these attributes using the following simpler example.

``````function F(int): bool;

procedure A0()
{
assume (forall {:pool "L"} x: int :: F(x-1));
assert (forall y: int :: {:add_to_pool "L", y+1} F(y));
}
``````

To prove the first assert in procedure `A0`, the quantifier in the assume statement must be instantiated at 1. Without the pool hints, this assert will not be verified because the SMT solver underlying Boogie is unable to deduce the usefulness of this instantiation. To help with quantifier instantiation, we use instantiation pools where each pool is a set of terms. This example uses a single pool `"L"`. A bound variable expresses interest in being instantiated by terms in `"L"` by using the attribute `:pool "L"`. Terms are added to a pool using the attribute `:add_to_pool`. For example, the first assert statement adds the term `1` to the pool `"L"`.

The second assert statement illustrates a more sophisticated use of instantiation pools. Unlike the first assert statement, the expression is this assert has a universal quantifier. The verification condition generator in Boogie detects that this quantifier may be skolemized using a fresh constant `y0`. The `add_to_pool` hint in the body of the quantier tells Boogie to add the term `y0+1` to the pool `"L"`. Another way to think about this explanation is that Boogie automatically generates the following intermediate program whose correctness implies the correctness of the original program.

``````function F(int): bool;

procedure A0()
{
var y0: int;
assume (forall {:pool "L"} x: int :: F(x-1));
}
``````

The following example shows how instantiation pools handle nested quantifiers. In this example, two pools `"A"` and `"B"` are used.

``````function P(int, int): bool;
procedure B1()
{
assume (exists x: int :: {:add_to_pool "B", x+1} (forall {:pool "A"} y: int :: P(x,y)));
assert (forall y: int :: {:add_to_pool "A", y} (exists {:pool "B"} x: int :: P(x-1,y)));
}
``````

Ignoring the pool annotations, the verification problem amounts to proving the following implication, where the bound variables `x` and `y` have been renamed to distinguish their use in the antecedent and the consequent:

``````(exists x1: int :: (forall y1: int :: P(x1,y1)))
==>
(forall y2: int :: (exists x2: int :: P(x2-1,y2)))
``````

The following proof steps are automatically carried out by Boogie using the instantiation hints:

• skolemize `x1` to `x1'` and `y2` to `y2'`
• add `x1'+1` to pool `"B"` and `y2'` to pool `"A"`
• instantiate `y1` with `y2'` and `x2` with `x1'+1`

We now turn our attention back to the example in the last section. This example does not appear to have any quantified expression; yet the attribute `:pool "A"` is used on the local variable `i` of action `INV`. However, Civl internally generates the transition relation of action `INV` which existentially quantifies the nondeterministically-initialized local variable `i`. The pool hints in this example are targeted towards this internally-generated quantifier.