13 Civl: concurrency and refinement🔗

Civl is the concurrency extension of Boogie. It adds three new kinds of top-level declaration — action, yield procedure and yield invariant — an integer layer annotation that runs through almost every declaration, a notion of mover type for actions, asynchronous and parallel calls, and a linear permission discipline on variables. A Civl program is not a sequential program with concurrency bolted on: it is a specification of a concurrent system as a tower of abstractions, and Boogie discharges the proof that each level is a sound abstraction of the one below it.

This is Boogie 2 (2008) contains none of this. The keywords yield, atomic, linear and mover do not appear in the paper at all (yield occurs twice, both times as the ordinary English verb); its §8 (Procedures and implementations) and §9 (Statements) describe only the sequential procedure/implementation/call language. Everything in this chapter postdates the paper, and nothing in this chapter contradicts it — Civl is a strict addition. The one place where an existing construct changes meaning is call: the grammar’s CallCmd production now admits an async prefix and a |-separated list of callees, both of which are rejected outside Civl declarations.

The Civl phases always run. There is no /civl flag: after resolution and type checking, ExecutionEngine constructs a CivlTypeChecker and then calls CivlRewriter.Transform. On a program with no yield/action declarations both are no-ops.

13.1 The model🔗

Read a Civl program as a family of programs, one per layer.

• Global variables are introduced at one layer and hidden at another; var {:layer 0,2} b: bool; means b exists in the layer-1 and layer-2 programs and nowhere else.

• A yield procedure carries a single layer n, its disappearing layer. Its body is a program of the layer-n system. At layer n+1 and above the procedure no longer has a body: it is the atomic action named in its refines clause. Boogie’s job is to prove that the body really does behave like that one atomic step.

• An action is a specification of an atomic step. It has a layer range {:layer m,n} giving the layers at which it exists.

• Between two yields, the code of a yield procedure runs without interference. At a yield, every other thread may run any number of atomic actions. Yields are not written with a statement; they arise from calls (see Yield sufficiency (the atomicity check)).

• Mover types say how an action commutes with the actions of other threads, and are what makes a multi-statement body collapse into one atomic step.

Here is the smallest interesting program. Incr is a layer-0 procedure with no body: it is a primitive, whose meaning at layer 1 is the action AtomicIncr. Main is a layer-1 procedure that calls it twice.

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

atomic action {:layer 1} AtomicIncr()

modifies x;

{

x := x + 1;

}

yield procedure {:layer 0} Incr();

refines AtomicIncr;

yield procedure {:layer 1} Main()

{

call Incr();

call Incr();

}

boogie incr-no-yield.bpl

incr-no-yield.bpl(12,27): Error: Implementation Main fails atomicity check at layer 1. Transactions must be separated by yields.

1 type checking errors detected in incr-no-yield.bpl

Main does not refine anything, so it must refine the built-in Skip action (see refines) — one atomic step that does nothing. Two calls to a non-mover action cannot be one step, so Civl rejects the program. There are two fixes. Put a yield between them:

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

atomic action {:layer 1} AtomicIncr()

modifies x;

{

x := x + 1;

}

yield procedure {:layer 0} Incr();

refines AtomicIncr;

yield invariant {:layer 1} Yield();

yield procedure {:layer 1} Main()

{

call Incr();

call Yield();

call Incr();

}

Boogie program verifier finished with 2 verified, 0 errors

or declare AtomicIncr a both mover, so that the two increments commute with everything and collapse into one transaction:

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

both action {:layer 1} AtomicIncr()

modifies x;

{

x := x + 1;

}

yield procedure {:layer 0} Incr();

refines AtomicIncr;

yield procedure {:layer 1} Main()

{

call Incr();

call Incr();

}

Boogie program verifier finished with 2 verified, 0 errors

13.2 Layers🔗

13.2.1 Where a layer annotation may appear🔗

The attribute is {:layer ...}. Two readers consume it, and they disagree about what a list means.

• Absy.ToLayer accepts exactly one number, and is used for yield procedure and yield invariant. Anything else is "expected single layer number".

• Absy.ToLayerRange accepts zero, one or two numbers and yields a closed range; two numbers must be non-decreasing or it is "invalid layer range". It is used for global variables, action declarations, and local variables and formals of yield procedures. With zero numbers the default applies.

• ICarriesAttributes.FindLayers returns the raw list, and assert/requires/ensures inside Civl declarations use it as a set: the assertion is checked at exactly the listed layers.

Omitting the layer where it is required is a resolution error, and a local variable may not outlive its procedure:

yield procedure P()

{

var {:layer 2} a: int;

}

yield invariant Q();

atomic action A() { }

missing-layer.bpl(1,16): Error: expected single layer number

missing-layer.bpl(6,16): Error: expected single layer number

missing-layer.bpl(3,17): Error: hidden layer of local variable may not be more than the layer of its procedure

3 name resolution errors detected in missing-layer.bpl

Note that atomic action A() { } is accepted: an action without {:layer} exists at every layer. That is how pure action Assert in the standard library (Source/Core/base.bpl) is declared.

13.2.2 Global variables🔗

var {:layer m,n} g: T; means g is introduced at layer m and hidden at layer n. The rule enforced on every occurrence of g in an action whose layer range is [a,b] is:

• m < a — "a global variable introduced at layer n is visible to an action only at layers greater than n" (AbsyExpr.cs); and

• [a,b] ⊆ [m,n].

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

atomic action {:layer 0,1} Bad()

modifies x;

{

x := x + 1;

}

atomic action {:layer 1,3} AlsoBad()

modifies x;

{

x := x + 1;

}

action-layers.bpl(4,9): Error: global variable must be introduced below the lower layer 0 of action Bad: x

action-layers.bpl(6,2): Error: global variable must be introduced below the lower layer 0 of action Bad: x

action-layers.bpl(6,7): Error: global variable must be introduced below the lower layer 0 of action Bad: x

action-layers.bpl(10,9): Error: global variable must be available across all layers ([1, 3]) of action AlsoBad: x

action-layers.bpl(12,2): Error: global variable must be available across all layers ([1, 3]) of action AlsoBad: x

action-layers.bpl(12,7): Error: global variable must be available across all layers ([1, 3]) of action AlsoBad: x

6 type checking errors detected in action-layers.bpl

Choosing the hiding layer is not cosmetic. An unannotated global has range [0, MaxInt], so it is still visible at the layer where the procedure’s abstraction is supposed to have no effect, and refinement fails:

var g: int;

atomic action {:layer 1} A()

modifies g;

{

g := g + 1;

}

yield procedure {:layer 0} a();

refines A;

yield procedure {:layer 1} P()

{

call a();

}

no-hiding-layer.bpl(12,28): Error: A yield-to-yield fragment modifies layer-2 state in a way that does not match the refined atomic action

Execution trace:

no-hiding-layer.bpl(14,3): anon0

no-hiding-layer.bpl(6,5): inline$A$0$anon0

(0,0): Civl_ReturnChecker

Boogie program verifier finished with 1 verified, 1 error

P has no refines, so it refines Skip, which changes nothing; but g still exists at layer 2 and P changes it. Writing var {:layer 0,1} g: int; makes the same program verify — at layer 2 there is no g left to change:

13.2.3 Layers on assertions and specifications🔗

Inside a yield procedure or an action, every assert, requires and ensures must carry layers, and they are a set, not a range. The expression is nevertheless type-checked against the range that the set spans, so all variables mentioned must be available across the whole span.

yield invariant {:layer 2} Y();

yield procedure {:layer 3} P()

{

assert {:layer 1,3} false;

}

assert-layer-set.bpl(5,3): Error: this assertion could not be proved

Execution trace:

assert-layer-set.bpl(5,3): anon0

assert-layer-set.bpl(5,3): Error: this assertion could not be proved

Execution trace:

assert-layer-set.bpl(5,3): anon0

Boogie program verifier finished with 2 verified, 2 errors

Two failures, not three: the assertion was checked at layers 1 and 3, not at layer 2 (the yield invariant is only there to make layer 2 exist at all). The layers on an assert may not exceed the enclosing procedure’s layer, and on an action’s requires they must lie inside the action’s layer range.

13.3 Atomic actions🔗

13.3.1 Declaring an action🔗

BoogiePL

= { ...

| InvariantDecl

| "yield" ( InvariantDecl | YieldProcedureDecl )

| Pure ( Procedure | ActionDecl )

| ...

}

EOF .

Pure = [ "pure" ] .

ActionDecl

= [ MoverQualifier ]

"action"

{ Attribute }

Ident

ProcFormals [ "returns" ProcFormals ]

( ";"  { SpecAction }

|      { SpecAction } ImplBody

)

.

MoverQualifier = "left" | "right" | "both" | "atomic" .

SpecAction

= ( SpecRefinedActionForAtomicAction

| SpecModifies

| SpecYieldRequires

| SpecAsserts

)

.

SpecRefinedActionForAtomicAction = "refines" { Attribute } Ident ";" .

SpecAsserts = "asserts" { Attribute } Proposition ";" .

(Source/Core/BoogiePL.atg, with semantic actions elided.)

Two consequences of the productions above are easy to miss.

• The mover qualifier comes before the keyword: left action, right action, both action, atomic action, pure action. Omitting it entirely (action Foo() { ... }) is legal and means atomic.

• pure and a mover qualifier are mutually exclusive, because a pure action is a both mover by definition:

  pure both action {:layer 1} Bad(i: int) { }

  pure-mover.bpl(1,43): error: mover type unnecessary for pure action since it is a both mover

  1 parse errors detected in pure-mover.bpl

13.3.2 The gate🔗

An action denotes a pair: a gate (a predicate on the pre-state) and a transition relation. The gate is computed by Wlp.HoistAsserts, which takes the weakest liberal precondition of the body with respect to its assert statements, quantifying away locals and out-parameters. Assertions therefore need not come first, and they may sit behind branches. Here the gate works out to b ==> i + 1 > 0, which the caller’s precondition discharges:

yield procedure {:layer 1} P(b: bool, i: int) returns (o: int)

requires {:layer 1} b ==> i >= 0;

{

call o := bar(b, i);

}

atomic action {:layer 1} BAR(b: bool, i: int) returns (o: int)

{

call o := FOO(b, i);

}

atomic action {:layer 1} FOO(b: bool, i: int) returns (o: int)

{

if (b) {

o := i + 1;

assert o > 0;

}

}

yield procedure {:layer 0} bar(b: bool, i: int) returns (o: int);

refines BAR;

yield procedure {:layer 0} foo(b: bool, i: int) returns (o: int);

refines FOO;

Boogie program verifier finished with 2 verified, 0 errors

The gate is assumed by the environment in mover checks and asserted at the point where the action is invoked. If it fails at a call site you get "an assertion for this call could not be proved" with the assert inside the action as the related location.

An asserts clause states the gate explicitly instead of leaving it to be inferred. Civl then generates an extra <Action>_GateSufficiencyChecker obligation: the stated gate must be strong enough to discharge every assert in the body.

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

atomic action {:layer 1} Gated()

asserts x > 0;

modifies x;

{

assert x != 0;

x := x - 1;

}

Boogie program verifier finished with 1 verified, 0 errors

Weaken the asserts clause and the sufficiency check fires:

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

atomic action {:layer 1} Gated()

asserts x >= 0;

modifies x;

{

assert x != 0;

x := x - 1;

}

asserts-weak.bpl(7,3): Error: this assertion could not be proved

Execution trace:

asserts-weak.bpl(7,3): anon0

Boogie program verifier finished with 0 verified, 1 error

An action’s requires clauses are not part of the gate. They are preconditions checked at the point where the action is invoked from a yielding procedure, they must mention globals only inside old(...), and their presence turns a left mover into a conditional left mover (The four mover checks). An action with preconditions must exist at a single layer.

13.3.3 modifies🔗

An action’s modifies clause is what its callers see as its frame, exactly as for an ordinary procedure (modifies). Writing it is optional: Boogie’s modifies-set inference runs between resolution and type checking, so it is computed from the body if omitted. The examples in this chapter write it out, but this also verifies:

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

both action {:layer 1} AtomicIncr()

{

x := x + 1;

}

yield procedure {:layer 0} Incr();

refines AtomicIncr;

yield procedure {:layer 1} Main()

{

call Incr();

}

Boogie program verifier finished with 2 verified, 0 errors

13.3.4 Calls between actions🔗

An action body may call other actions and the linear primitives, and nothing else:

Called actions are inlined (CivlTypeChecker.InlineAtomicActions adds {:inline 1} to every action and runs the inliner), so the call graph over actions must be acyclic:

The caller’s layer range must be a subset of the callee’s, and async calls are never allowed inside an action, even though the resolver has a code path for them:

13.3.5 An action refining an action🔗

An action may itself carry a refines clause. If A has layer range ending at n, then refines B requires B to exist at layer n+1, and Civl generates an A_RefinementCheck obligation: every behaviour of A must be a behaviour of B. The two signatures must match exactly, including linearity annotations.

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

var {:layer 0,1} y: int;

atomic action {:layer 1} A()

modifies x, y;

refines B;

{

x := x + 1;

call X();

}

action {:layer 1} X()

modifies y;

{

y := y + 1;

}

atomic action {:layer 2} B()

modifies x;

{

x := x + 1;

}

Boogie program verifier finished with 1 verified, 0 errors

y is hidden at layer 2, so B does not have to mention it. Changing B to x := x + 2:

action-refines-fail.bpl(10,1): Error: a postcondition could not be proved on this return path

(0,0): Related location: Refinement check of A failed

Execution trace:

action-refines-fail.bpl(8,5): anon0

Boogie program verifier finished with 0 verified, 1 error

13.3.6 pure actions and procedures🔗

pure may prefix either an action or an ordinary procedure. Both are ghost code: they may not touch global state, and a yielding procedure may call them at a chosen layer without that counting as a step of the concurrent program.

• A pure action is a both mover, has a gate (its asserts), may have no modifies clause and may not mention globals.

• A pure procedure is an ordinary procedure with requires/ensures; it may only call other pure procedures.

A working use. Note the {:layer 1} on the calls and on the local: the actual parameters and results of a pure call must be available exactly across the call’s layer range.

pure procedure Helper(x: int) returns (y: int);

ensures y == x + 1;

pure action Check(b: bool)

{

assert b;

}

yield procedure {:layer 1} P()

{

var {:layer 1} a: int;

call {:layer 1} a := Helper(1);

call {:layer 1} Check(a == 2);

}

Boogie program verifier finished with 2 verified, 0 errors

The precondition of a pure procedure is checked at the call site as an ordinary precondition; the gate of a pure action is checked as an assertion. The standard library ships pure procedure Copy<T>(v: T) returns (v’: T), pure procedure Assume(b: bool) and pure action Assert(b: bool) for exactly this purpose.

13.4 Yield procedures🔗

13.4.1 Declaring a yield procedure🔗

YieldProcedureDecl

= [ MoverQualifier ]

"procedure"

{ Attribute }

Ident

ProcFormals [ "returns" ProcFormals ]

( ";"  { SpecYieldPrePost }

|      { SpecYieldPrePost } ImplBody

)

.

SpecYieldPrePost

= ( SpecRefinedActionForYieldProcedure

| SpecYieldRequires

| SpecYieldPreserves

| SpecYieldEnsures

| SpecYieldMeasure

| SpecModifies

)

.

SpecYieldRequires  = "requires"  ( { Attribute } Proposition | CallCmd ) ";" .

SpecYieldPreserves = "preserves" ( { Attribute } Proposition | CallCmd ) ";" .

SpecYieldEnsures   = "ensures"   ( { Attribute } Proposition | CallCmd ) ";" .

SpecRefinedActionForYieldProcedure

= "refines" { Attribute }

( [ MoverQualifier ] "action" { Attribute } Ident ImplBody

| Ident ";"

)

.

The whole declaration is prefixed by the keyword yield, and the mover qualifier sits between: yield left procedure {:layer 2} A() ....

13.4.2 refines🔗

A yield procedure at layer n is replaced, at layers above n, by the action named in its refines clause. That action must exist at layer n+1:

If the body does not implement the action, the refinement obligation fails at the point where the yield-to-yield fragment ends:

If a non-mover yield procedure has no refines clause, Civl gives it one: the CivlTypeChecker constructor synthesises a both-mover action Civl_Skip with an empty body and range [0, MaxInt] and assigns it to every such procedure. This is why a procedure that quietly modifies still-visible state fails refinement (see Global variables).

The refined action may be written inline instead of being named. The name _ makes it anonymous; any other identifier declares a real top-level action that can be referred to elsewhere.

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

yield procedure {:layer 0} Incr();

refines both action {:layer 1,2} AtomicIncr {

x := x + 1;

}

yield procedure {:layer 1} IncrTwice()

refines atomic action {:layer 2} _ {

x := x + 2;

}

{

call Incr();

call Incr();

}

yield procedure {:layer 1} AlsoIncr()

refines AtomicIncr;

{

call Incr();

}

Boogie program verifier finished with 6 verified, 0 errors

Note the asymmetry in the grammar: the named form ends with ;, the inline form ends with the action’s body and no semicolon.

A yield procedure without a body is a primitive: there is nothing to check, and its refined action simply is its meaning. This is the standard idiom for the layer-0 hardware operations.

13.4.3 {:hide} and visible formals🔗

YieldProcedureDecl.Resolve computes VisibleFormals: the formals whose layer range ends exactly at the procedure’s layer and that do not carry {:hide}. Only visible formals appear in the refined action’s signature. Both mechanisms work on in- and out-parameters.

Despite the shared word, this attribute has nothing to do with the hide and reveal statements, which control axiom pruning and are described in Hiding and revealing function definitions.

atomic action {:layer 2} A() { }

yield procedure {:layer 1} p({:hide} i: int)

refines A;

{

}

yield procedure {:layer 1} q({:layer 0} j: int)

refines A;

{

}

yield procedure {:layer 1} r(k: int)

refines A;

{

}

hide.bpl(13,27): Error: mismatched number of in-parameters in A

1 type checking errors detected in hide.bpl

p and q are accepted; only r, whose formal has the default range [0,1] and no {:hide}, is required to pass k on to A. When the action is written inline, {:hide} formals are stripped from the generated action by the parser itself:

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

yield procedure {:layer 1} P(i: int, {:hide} dbg: int) returns (r: int, {:hide} trace: int)

refines atomic action {:layer 2} _ {

r := i;

}

{

r := i;

trace := 0;

}

atomic action {:layer 2} Q(i: int) returns (r: int)

{

r := i;

}

yield procedure {:layer 1} R(i: int, {:hide} dbg: int) returns (r: int, {:hide} trace: int)

refines Q;

{

r := i;

trace := 0;

}

Boogie program verifier finished with 4 verified, 0 errors

13.4.4 Mover procedures🔗

A yield procedure may carry a mover qualifier instead of a refines clause. Such a mover procedure is not summarised by an atomic action; instead its requires/ensures contract is used directly, and the atomicity check (Yield sufficiency (the atomicity check)) is run against the declared mover type rather than against "one transaction".

• A mover procedure may have a modifies clause; a non-mover yield procedure may not. Every variable listed must be available at the procedure’s layer. Boogie’s modifies-set inference runs between resolution and type checking, so writing the clause is optional — and because the "non-empty modifies clause but no mover type" error is raised during resolution, it only fires on a clause you wrote yourself.

• A mover procedure may not have a refines clause.

• Callers must be at exactly the same layer.

• In a mover procedure’s specifications at its own layer, globals may be mentioned without old(...); at lower layers they may not.

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

yield procedure {:layer 0} Incr();

refines both action {:layer 1} _ {

x := x + 1;

}

yield both procedure {:layer 1} IncrTwice()

modifies x;

ensures {:layer 1} x == old(x) + 2;

{

call Incr();

call Incr();

}

yield procedure {:layer 1} Client()

{

call IncrTwice();

call IncrTwice();

}

Boogie program verifier finished with 3 verified, 0 errors

The preserves E; form (as distinct from preserves call I();) is only available on mover procedures, and only at the procedure’s own layer. On an ordinary yield procedure it is rejected outright:

13.4.5 What a yield procedure body may do🔗

A yield procedure may not assign to a global variable, and may not read one outside old(...):

All state change happens through calls, and the set of legal callees is small:

Note that a non-pure action may not be called from a yield procedure: actions are reached only indirectly, through the refines clause of a called yield procedure.

13.4.6 Introducing state🔗

The only way to write to a global from a yield procedure is a pure call whose output is that global, at the layer at which it is introduced. This is how abstract (ghost) state is coupled to concrete state.

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

var {:layer 1,2} n: int;

yield procedure {:layer 0} Incr();

refines both action {:layer 1} _ {

x := x + 1;

}

both action {:layer 2} AtomicTick()

modifies n;

{

n := n + 1;

}

yield procedure {:layer 1} Tick()

refines AtomicTick;

{

call Incr();

call {:layer 1} n := Copy(n + 1);

}

yield invariant {:layer 1} Coupled();

preserves x == n;

Boogie program verifier finished with 2 verified, 0 errors

n is introduced at layer 1: Tick’s body updates it, and from layer 2 upwards only n exists. Change the update to n := Copy(n + 2) and both the non-interference check for Coupled and the refinement check for Tick fail:

introduce-fail.bpl(23,1): Error: Non-interference check failed

Execution trace:

introduce-fail.bpl(18,3): anon0

introduce-fail.bpl(6,5): inline$AnonymousAction_36$0$anon0

introduce-fail.bpl(18,3): anon0$1

(0,0): inline$Civl_NoninterferenceChecker_yield_Coupled$0$L

introduce-fail.bpl(15,28): Error: A yield-to-yield fragment modifies layer-2 state in a way that does not match the refined atomic action

Execution trace:

introduce-fail.bpl(18,3): anon0

introduce-fail.bpl(6,5): inline$AnonymousAction_36$0$anon0

introduce-fail.bpl(18,3): anon0$1

(0,0): Civl_ReturnChecker

Boogie program verifier finished with 0 verified, 2 errors

The layer on the call must be the introduction layer of every global it assigns:

If the call’s layer is strictly below the enclosing procedure’s layer, the variable must additionally be hidden at that layer — a variable can only be written by ghost code in the single layer where it exists but the enclosing procedure has already disappeared.

13.5 Yield invariants🔗

13.5.1 Declaration🔗

InvariantDecl

= "invariant"

{ Attribute }

Ident

ProcFormals ";"

{ Invariant }

.

Invariant = "preserves" { Attribute } Proposition ";" .

InvariantDecl is reachable two ways from the top level, and they mean different things:

• invariant {:layer n} I(...); preserves ...; declares a global yield invariant.

• yield invariant {:layer n} I(...); preserves ...; declares a local one. The parser sets IsGlobal = false on this branch and nothing else distinguishes them.

The layer is a single number. Parameters may be annotated {:linear} but never {:linear_in} or {:linear_out}. The body is a sequence of preserves clauses; global variables mentioned must be available at the invariant’s layer, and a global invariant at layer n may not mention a global introduced at layer n.

13.5.2 What a yield invariant obliges🔗

This is the part of Civl that most often surprises. A local yield invariant at layer n is checked for non-interference at every yield of every yield procedure that exists at layer n — not only in the procedures that mention it. The generated checker (NoninterferenceChecker.CreateNoninterferenceCheckerDecls) turns the invariant’s parameters into unconstrained locals, assumes the invariant held in a snapshot of the pre-state, and asserts it in the post-state. So it reads: whatever this thread just did, it must not falsify the invariant for any other thread.

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

yield invariant {:layer 1} PositiveX();

preserves x > 0;

both action {:layer 1} AtomicIncr()

modifies x;

{

x := x + 1;

}

both action {:layer 1} AtomicDecr()

modifies x;

{

x := x - 1;

}

yield procedure {:layer 0} Incr();

refines AtomicIncr;

yield procedure {:layer 0} Decr();

refines AtomicDecr;

yield procedure {:layer 1} P()

preserves call PositiveX();

{

call Incr();

}

yield procedure {:layer 1} Q()

{

call Decr();

}

noninterference.bpl(4,1): Error: Non-interference check failed

Execution trace:

noninterference.bpl(32,3): anon0

noninterference.bpl(15,5): inline$AtomicDecr$0$anon0

(0,0): inline$Civl_NoninterferenceChecker_yield_PositiveX$0$L

Boogie program verifier finished with 5 verified, 1 error

Q never names PositiveX, and is still rejected for breaking it. The error is reported at the declaration of the invariant, and the execution trace names the offending procedure and the generated checker.

A global yield invariant carries a stronger obligation still: in addition to the yield-to-yield checks it is checked against every atomic action that exists at its layer (YieldingProcInstrumentation.ActionNoninterferenceCheckers), so it really is an invariant of the whole layer, independent of any control flow.

13.5.3 requires call, ensures call, preserves call🔗

A yield invariant is attached to a procedure by calling it in a specification position. The three forms differ in direction and in what is in scope:

The caller is obliged to establish a requires call / preserves call at the call site, and may assume an ensures call / preserves call afterwards. Arguments of ensures call and preserves call are type-checked in a two-state context in which globals must appear under old(...); arguments of requires call are not. Actual arguments must be available at exactly the invariant’s layer:

(This is Test/civl/regression-tests/yield-requires-ensures-errors.bpl with its two leading RUN: comment lines and the blank line after them stripped; in the test file itself the same two errors are reported at lines 12 and 13.)

A plain call I(); in a procedure body is also legal and is a yield: it both asserts and assumes the invariant at that point.

13.5.4 Yielding loops🔗

A loop inside a yield procedure is a yielding loop only if its header carries an invariant {:yields} annotation.

WhileCmd

= "while" Guard

{ [ "free" ] "invariant" { Attribute } ( Expression | CallCmd ) ";"

| "measure" { Attribute } Expressions ";"

}

"{" StmtList

.

(The measure clause in that production is not a Civl construct: it is checked by MeasureChecker in the ordinary pipeline and is described in measure clauses and measure.)

• invariant {:yields} E; marks the loop as yielding up to the enclosing procedure’s layer. The expression E is discarded. Implementation.TypecheckLoopAnnotations finds the first predicate command carrying {:yields} and removes it from the header without ever looking at its condition. invariant {:yields} false; is therefore harmless and idiomatic code writes true:

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

  yield procedure {:layer 0} Incr();

  refines atomic action {:layer 1} _ {

  x := x + 1;

  }

  yield procedure {:layer 1} P()

  {

  while (*)

  invariant {:yields} false;

  {

  call Incr();

  }

  }

  Boogie program verifier finished with 2 verified, 0 errors

• invariant {:yields} {:layer k} E; restricts yielding to layers ≤ k. A single layer number is expected here; more than one is an error.

• invariant call I(e); attaches a yield invariant to the loop. All such calls must be the first commands of the header, and the loop must already be marked {:yields} — otherwise "expected :yields attribute on this loop".

• An ordinary invariant whose layers include a yielding layer of the loop may not mention a global variable.

Without {:yields} an iteration is just straight-line code, so the loop body has to be a single transaction:

The global-variable restriction:

The way to say something about shared state across a yielding loop is a yield invariant, which brings its non-interference obligation with it:

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

yield invariant {:layer 1} NonNeg();

preserves x >= 0;

yield procedure {:layer 0} Incr();

refines both action {:layer 1} _ {

x := x + 1;

}

yield procedure {:layer 1} P()

preserves call NonNeg();

{

while (*)

invariant {:yields} true;

invariant call NonNeg();

{

call Incr();

}

}

Boogie program verifier finished with 2 verified, 0 errors

13.6 Calls🔗

CallCmd

= [ "async" ] [ "free" ] "call"

CallParams { "|" CallParams }

.

A |-separated list is a parallel call. The parser rejects it in a specification position and in combination with async or free ("parallel call not allowed").

13.6.1 Synchronous calls🔗

The callee’s layer must not exceed the caller’s. If the callee is a non-mover yield procedure at a strictly lower layer, the call is replaced by the callee’s refined action at the caller’s layer; if that chain does not reach the caller’s layer the call is rejected.

Extending AtomicIncr to {:layer 1,2} fixes it. Other layer rules for calls from a yield procedure at layer m to a yield procedure at layer n:

• n > m: "layer of callee must not be more than layer of caller".

• n = m and the callee is a non-mover: the call is a yield. The caller must not be a mover procedure.

• The callee is a mover procedure: n must equal m ("layer of caller must be equal to layer of callee").

• The callee is a yield invariant at layer n: n ≤ m, and n < m if the caller is a mover procedure.

13.6.2 Asynchronous calls🔗

async call P(...) models forking a thread. The callee must be a yield procedure and may not have out-parameters.

An unsynchronised async call is only allowed to a callee that has neither a mover type nor a refines clause — that is, one whose abstraction is Skip. This is the "fire and forget" case: at layers up to the callee’s own, the call is desugared into a call to a generated Civl_AsyncCall_<P>_<n> procedure carrying the callee’s preconditions and nothing else; the new thread’s behaviour is then accounted for by the environment. Anything else must be marked {:sync}:

async call {:sync} P(...) asks Civl to treat the forked action as if it ran immediately at the call site. Three conditions apply.

• The callee’s layer must be strictly below the caller’s (for a callee that refines an action):

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

  left action {:layer 2} A()

  modifies x;

  {

  x := x + 1;

  }

  yield procedure {:layer 1} P()

  refines A;

  {

  }

  yield procedure {:layer 1} Q()

  {

  async call {:sync} P();

  }

  async-sync-same-layer.bpl(16,8): Error: layer of callee in synchronized call must be less than layer of caller

  1 type checking errors detected in async-sync-same-layer.bpl

• Every action in the callee’s refinement chain up to the caller’s layer must be a left mover — not just the topmost one:

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

  atomic action {:layer 1} AtomicIncr()

  modifies x;

  {

  x := x + 1;

  }

  yield procedure {:layer 0} Incr();

  refines AtomicIncr;

  yield procedure {:layer 1} P()

  {

  async call {:sync} Incr();

  }

  sync-not-left.bpl(14,8): Error: callee abstraction in synchronized call must be a left mover: AtomicIncr

  1 type checking errors detected in sync-not-left.bpl

  Declaring AtomicIncr left or both makes it verify:

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

  left action {:layer 1,2} AtomicIncr()

  modifies x;

  {

  x := x + 1;

  }

  yield procedure {:layer 0} Incr();

  refines AtomicIncr;

  yield procedure {:layer 1} AsyncIncr()

  refines AtomicIncr;

  {

  async call {:sync} Incr();

  }

  Boogie program verifier finished with 2 verified, 0 errors

• If the callee is a mover procedure, it must itself be a left mover, and its layer must equal the caller’s.

There is one further check, the async check: between an unsynchronised async call and the next yield, the caller may not modify global state. The reason is that the forked thread’s precondition was checked at the fork point; a later modification could invalidate it before the thread runs.

The check is armed only when the callee carries at least one requires call or preserves call clause; an async call to a procedure with no yield specification is unrestricted.

13.6.3 Parallel calls🔗

call A(...) | B(...) | ... runs the callees in parallel. It is also a yield point: YieldingProcInstrumentation splits the block at every parallel call and inserts the non-interference and refinement checks there.

Callees may be yield procedures or yield invariants, mixed freely. A linear variable may be passed to at most one callee, and may not be passed both to a yield invariant and to a procedure:

type Tid;

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

yield invariant {:layer 1} NonNeg();

preserves x >= 0;

yield invariant {:layer 1} Owns({:linear} tid: One Tid);

yield procedure {:layer 0} Incr();

refines both action {:layer 1} _ {

x := x + 1;

}

yield procedure {:layer 1} Worker({:linear} tid: One Tid)

preserves call NonNeg();

{

call Incr();

}

yield procedure {:layer 1} Main({:linear} tid1: One Tid, {:linear} tid2: One Tid)

preserves call NonNeg();

{

call Worker(tid1) | Worker(tid2);

call NonNeg() | Owns(tid1);

}

Boogie program verifier finished with 4 verified, 0 errors

The mover types of the callees are constrained by YieldSufficiencyChecker.CheckParCallCmd:

• (left)*(non)?(right)* is checked on every parallel call. Callees labelled P (pure), B (both mover) or Y (a yield — a yield invariant, or a yielding procedure at this layer) are skipped when matching it.

• If some callee is a yielding procedure at this layer, then additionally: if any callee is a non-mover the call is rejected outright ("Parallel call contains both non-mover and yielding procedure"); otherwise the stronger (left)*(yielding-proc)*(right)* must also hold. Only P callees and yield invariants are skipped when matching this second pattern — a both mover is transparent before the yielding-procedure run and after it, but a both mover appearing during that run ends it.

Both patterns are checked independently, so a bad call can report both errors:

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

right action {:layer 1} R_() modifies x; { x := x + 1; }

left  action {:layer 1} L_() modifies x; { x := x + 1; }

atomic action {:layer 1} N_() modifies x; { havoc x; }

yield procedure {:layer 0} R(); refines R_;

yield procedure {:layer 0} L(); refines L_;

yield procedure {:layer 0} N(); refines N_;

yield procedure {:layer 1} Y();

yield procedure {:layer 1} A()

{

call R() | L();

}

yield procedure {:layer 1} B()

{

call R() | L() | Y();

}

yield procedure {:layer 1} C()

{

call N() | Y();

}

boogie /trustMoverTypes parcall-pattern.bpl

parcall-pattern.bpl(14,2): Error: Mover types in parallel call do not match (left)*(non)?(right)* at layer 1

parcall-pattern.bpl(19,2): Error: Mover types in parallel call do not match (left)*(non)?(right)* at layer 1

parcall-pattern.bpl(19,2): Error: Mover types in parallel call do not match (left)*(yielding-proc)*(right)* at layer 1

parcall-pattern.bpl(19,2): Error: Mover types in parallel call do not match (left)*(yielding-proc)*(right)* at layer 1

parcall-pattern.bpl(24,2): Error: Parallel call contains both non-mover and yielding procedure at layer 1

5 type checking errors detected in parcall-pattern.bpl

13.7 Mover types and their obligations🔗

Every action has one of four mover types. atomic — the default — is the non-mover.

13.7.1 The four mover checks🔗

MoverCheck.AddCheckers enumerates all ordered pairs of actions whose layer ranges overlap and emits checker procedures. Pairs that trivially commute — where the globals modified by one are disjoint from the globals used by the other — are skipped, as is a self-pair of an action with no parameters.

Commutativity. For a right mover R and any action A: running R then A must be a possible behaviour of A then R. For a left mover L and any A: A then L must be a behaviour of L then A.

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

both action {:layer 1} AtomicIncr()

modifies x;

{

x := x + 1;

}

both action {:layer 1} AtomicReset()

modifies x;

{

x := 0;

}

commutativity.bpl(3,24): Error: Commutativity check between AtomicIncr @ commutativity.bpl(3,24) and AtomicReset @ commutativity.bpl(9,24) failed

Execution trace:

commutativity.bpl(3,24): inline$AtomicIncr$0$Entry

commutativity.bpl(6,5): inline$AtomicIncr$0$anon0

commutativity.bpl(9,24): inline$AtomicReset$0$Return

commutativity.bpl(9,24): Error: Commutativity check between AtomicReset @ commutativity.bpl(9,24) and AtomicIncr @ commutativity.bpl(3,24) failed

Execution trace:

commutativity.bpl(9,24): inline$AtomicReset$0$Entry

commutativity.bpl(6,5): inline$AtomicIncr$0$anon0

commutativity.bpl(3,24): inline$AtomicIncr$0$Return

Boogie program verifier finished with 0 verified, 2 errors

Gate preservation. A right mover must not disable any other action; a left mover must not be disabled by any other action. Formally, given that both gates hold, the gate of the first action must still hold after the second runs.

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

var {:layer 0,1} y: int;

right action {:layer 1} Reset()

modifies x;

{

x := 0;

}

atomic action {:layer 1} Bump()

modifies y;

{

assert x > 0;

y := y + 1;

}

gate-preservation.bpl(13,3): Error: Gate of Bump @ gate-preservation.bpl(10,26) not preserved by Reset @ gate-preservation.bpl(4,25)

Execution trace:

gate-preservation.bpl(4,25): inline$Reset$0$Entry

gate-preservation.bpl(4,25): inline$Reset$0$Return

Boogie program verifier finished with 0 verified, 1 error

Failure preservation. A left mover must not enable an action that was disabled: if A’s gate fails, it must still fail after L runs. The check is stated as wp(L, gate(A)) ⇒ gate(A), using Wlp.HoistAsserts.

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

var {:layer 0,1} y: int;

left action {:layer 1} Set()

modifies x;

{

x := 1;

}

atomic action {:layer 1} Bump()

modifies y;

{

assert x > 0;

y := y + 1;

}

failure-preservation.bpl(13,3): Error: Gate failure of Bump @ failure-preservation.bpl(10,26) not preserved by Set @ failure-preservation.bpl(4,24)

Execution trace:

(0,0): init

Boogie program verifier finished with 0 verified, 1 error

Non-blocking. A left mover must not block: whenever its gate holds it must have some successor state. The obligation is only generated when the body contains an assume.

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

left action {:layer 1} Take()

modifies x;

{

assume x > 0;

x := x - 1;

}

nonblocking.bpl(3,24): Error: Nonblocking check for Take failed

Execution trace:

(0,0): init

Boogie program verifier finished with 0 verified, 1 error

Conditional left movers. A left mover whose declaration has requires or requires call clauses is a conditional left mover. Its left-mover obligations are not generated in the ordinary way at all: MoverCheck.AddCheckers skips it in the unconditional pass (which demands IsUnconditionalLeftMover) and emits commutativity, gate-preservation and failure-preservation checks for it in a separate pass, at the single layer of its layer range, with those preconditions added as assumptions. The action is therefore only required to be a left mover in the states its callers guarantee. This is why an action with preconditions must exist at a single layer, and why a yield invariant called from an action’s requires call must be a global invariant.

13.7.2 Yield sufficiency (the atomicity check)🔗

For each yield procedure implementation and each refinement layer ≤ its own layer, YieldSufficiencyChecker abstracts the control-flow graph into an automaton whose edges are labelled

and checks that it is simulated by a two-state atomicity automaton whose states are RM (still in the right-mover prefix) and LM (past the non-mover). Its transition relation, taken from AtomicitySpec in Source/Concurrency/YieldSufficiencyChecker.cs, is:

Both states are initial and accepting. In words: between two consecutive yields, the sequence of steps must match R* N? L* (with B and P allowed anywhere). That is one transaction, and it is what makes the whole fragment collapse to a single atomic action.

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

right action {:layer 1} R_() modifies x; { x := x + 1; }

left  action {:layer 1} L_() modifies x; { x := x + 1; }

both  action {:layer 1} B_() modifies x; { x := x + 1; }

atomic action {:layer 1} N_() modifies x; { havoc x; }

yield procedure {:layer 0} R(); refines R_;

yield procedure {:layer 0} L(); refines L_;

yield procedure {:layer 0} B(); refines B_;

yield procedure {:layer 0} N(); refines N_;

yield procedure {:layer 1} Ok()

{

call R();

call R();

call B();

call N();

call L();

call B();

call L();

}

boogie /trustMoverTypes atomicity-ok.bpl

Boogie program verifier finished with 2 verified, 0 errors

(/trustMoverTypes suppresses the commutativity obligations, which these deliberately-contradictory declarations do not satisfy; the atomicity check still runs.) A left mover followed by a right mover breaks the pattern:

For a mover procedure the requirement is different: a right mover procedure must stay in state RM at entry and at every return, a left mover procedure must be able to start in LM, and failure is reported as "The atomicity declared for mover procedure is not valid".

The same pass also runs a loop check. Every edge inside a non-yielding loop — the back edge and every edge of the natural loop’s body — must be labelled P, B, L, R or N, never Y; and a yielding loop may not be nested inside a non-yielding one. Both failures are reported as "Loop header must be yielding at layer n".

13.8 Linear variables🔗

13.8.1 Linear types and permissions🔗

Civl’s disjointness reasoning is driven by types, not by annotations. A type carries permissions if it is One T, or a Map K V whose key type is One T or whose value type already carries permissions, or a datatype one of whose constructor fields has such a type (computed by LinearTypeCollector, which iterates to a fixed point over the datatype declarations). For each such type Civl instantiates a permission collector function, and for each permission type a linear domain with the map operations needed to state disjointness.

The upshot: two parameters of type One int are assumed to denote distinct values, and two of type int are not.

{:linear} on an int buys nothing, because int carries no permissions. Conversely — and this is worth knowing before spending an afternoon on it — at the action level the disjointness assumptions are generated from every parameter whose type carries permissions, regardless of the annotation (MoverCheck.DisjointnessAndWellFormedRequires filters only {:linear_out} out). Dropping {:linear} from the first program above changes nothing:

Inside yield procedures the annotation does matter, because LinearPermissionInstrumentation filters the thread’s permission set by linear kind:

13.8.2 The three annotations🔗

{:linear}, {:linear_in} and {:linear_out} are read by LinearTypeChecker.FindLinearKind and are meaningful on formals and global variables only. A global variable and an out-parameter may only be {:linear}; {:linear_in}/{:linear_out} on either is "variable must be declared linear (as opposed to linear_in or linear_out)". A yield invariant’s parameters may only be {:linear}.

Local variables are not annotated — an annotation there parses and is silently ignored, since FindLinearKind is only ever consulted for globals and formals. Availability of a local is tracked purely by its type, so a local of a permission-carrying type behaves linearly with no syntax at all:

13.8.3 The availability discipline🔗

LinearTypeChecker.VisitImplementation runs a forward dataflow analysis computing, at every program point, the set of available linear variables. The rules:

• On entry: all {:linear}/{:linear_in} in-parameters and all linear globals are available.

• x := y where the type carries permissions transfers availability from y to x; y becomes unavailable. Packing a datatype from linear components does the same for each component. Any other right-hand side makes the left-hand side unavailable.

• unpack distributes the source’s availability to the unpacked components.

• havoc x makes x unavailable.

• A call requires every linear actual to be available; {:linear_in} parameters and all parameters of an async call consume it, {:linear_out} parameters produce it. Out-parameters of a call become available.

• At a join point, the available set is the intersection.

• At a return, all linear globals, all {:linear}/{:linear_out} in-parameters and all out-parameters of permission-carrying type must be available.

• Linear globals must be available at every non-primitive call and at every loop head.

Violations:

Aliasing is caught by the same analysis:

Finally, the linearity annotation is part of a procedure’s signature for refinement purposes:

13.8.4 Linear globals and the primitives🔗

A global variable may be {:linear}. The permissions it holds are pooled with the executing thread’s, so a thread can take permission out of a shared pool and hand it back. The transfers are performed by the linear primitives declared in Source/Core/base.bpl — signatures below, with {:inline 1} attributes, {:pool} hints and bodies elided:

pure procedure Move<T>({:linear_in} u: T, {:linear_out} v: T);

pure procedure Map_MakeEmpty<K,V>() returns ({:linear} m: Map K V);

pure procedure One_Get<K>({:linear} path: UnitMap K, {:linear_out} l: K);

pure procedure One_Put<K>({:linear} path: UnitMap K, {:linear_in} l: K);

pure procedure Map_Get<K,V>({:linear} path: Map K V, {:linear_out} k: K) returns ({:linear} v: V);

pure procedure Map_Put<K,V>({:linear} path: Map K V, {:linear_in} k: K, {:linear_in} v: V);

pure procedure Map_Split<K,V>({:linear} path: Map K V, k: [K]bool) returns ({:linear} l: Map K V);

pure procedure Map_Join<K,V>({:linear} path: Map K V, {:linear_in} l: Map K V);

pure procedure Path_Load<V>(path: V) returns (v: V);

pure procedure Path_Store<V>(path: V, v: V);

pure procedure Loc_New() returns ({:linear} l: One Loc);

pure procedure Tag_New() returns ({:linear} l: One Loc, {:linear} tag: One (Tag Unit));

pure procedure Tags_New<V>(vals: [V]bool) returns ({:linear} l: One Loc, {:linear} tags: UnitMap (One (Tag V)));

These are not ordinary procedures: CivlPrimitives.LinearPrimitives lists them by name — exactly the thirteen above — and LinearRewriter replaces each call with the assertions and assignments that implement the transfer. They differ in what they accept at position 0:

• One_Get, One_Put, Map_Get, Map_Put, Map_Split, Map_Join, Path_Load and Path_Store take an access path at position 0 — a variable followed by field selections and map indices. Illegal paths (reaching through the val field of a One, or the dom field of a Map) are rejected with "illegal path expression at position 0". For all of them except Path_Load the path is written in place, so it is both read and modified by the call (CivlPrimitives.ModifiedArgument).

• Move requires both arguments to be plain variables ("argument at position 0 must be a variable").

• Loc_New, Tag_New, Tags_New and Map_MakeEmpty have no path argument and modify nothing.

A complete allocator:

var {:layer 0,1} {:linear} unallocated: UnitMap (One int);

right action {:layer 1} AtomicAlloc() returns ({:linear} tid: One int)

modifies unallocated;

{

assume Map_Contains(unallocated, tid);

call One_Get(unallocated, tid);

}

yield procedure {:layer 0} Alloc() returns ({:linear} tid: One int);

refines AtomicAlloc;

yield procedure {:layer 1} Client()

{

var t: One int;

var u: One int;

call t := Alloc();

call u := Alloc();

assert {:layer 1} t != u;

}

Boogie program verifier finished with 4 verified, 0 errors

Making AtomicAlloc atomic instead of right breaks the atomicity check in Client — two non-movers in a row:

alloc-atomic.bpl(13,27): Error: Implementation Client fails atomicity check at layer 1. Transactions must be separated by yields.

1 type checking errors detected in alloc-atomic.bpl

13.9 The checks Civl generates🔗

Some checks are purely syntactic and are reported as type-checking errors before any verification condition is built: yield sufficiency, the loop check, the async check, the parallel-call mover patterns, and all the layer and linearity rules. The rest become Boogie procedures, which is why the "n verified" count of a Civl program bears no relation to the number of declarations you wrote.

/civlDesugaredFile:<file> writes the fully desugared program. Running it on the yield-separated program of The model:

boogie /civlDesugaredFile:incr-yield.desugared.bpl incr-yield.bpl

grep '^procedure' incr-yield.desugared.bpl | sed 's/(.*//' | grep Civl_

procedure Civl_Main_1

procedure Civl_ParallelCall_Yield_1

procedure {:inline 1} Civl_Wrapper_YieldToYield_NoninterferenceChecker_1

procedure {:inline 1} Civl_Wrapper_Global_NoninterferenceChecker_1

procedure Civl_Main_Refine_1

procedure Civl_ParallelCall_Yield_Refine_1

procedure {:inline 1} Civl_Wrapper_YieldToYield_NoninterferenceChecker_Refine_1

procedure {:inline 1} Civl_Wrapper_Global_NoninterferenceChecker_Refine_1

and on the spin lock of Worked example: a spin lock:

boogie /civlDesugaredFile:lock.desugared.bpl lock.bpl

grep '^procedure' lock.desugared.bpl | sed 's/(.*//' | grep -E "Checker|RefinementCheck"

procedure Civl_CommutativityChecker_AtomicAcquire_AtomicAcquire

procedure Civl_CommutativityChecker_AtomicAcquire_AtomicRelease

procedure Civl_GatePreservationChecker_AtomicRelease_AtomicAcquire

procedure Civl_CommutativityChecker_AtomicRelease_AtomicRelease

procedure Civl_GatePreservationChecker_AtomicRelease_AtomicRelease

procedure Civl_FailurePreservationChecker_AtomicRelease_AtomicRelease

procedure {:inline 1} Civl_Wrapper_YieldToYield_NoninterferenceChecker_1

procedure {:inline 1} Civl_Wrapper_Global_NoninterferenceChecker_1

procedure {:inline 1} Civl_NoninterferenceChecker_yield_Inv

procedure {:inline 1} Civl_Wrapper_YieldToYield_NoninterferenceChecker_2

procedure {:inline 1} Civl_Wrapper_Global_NoninterferenceChecker_2

procedure {:inline 1} Civl_Wrapper_YieldToYield_NoninterferenceChecker_3

procedure {:inline 1} Civl_Wrapper_Global_NoninterferenceChecker_3

procedure {:inline 1} Civl_Wrapper_YieldToYield_NoninterferenceChecker_Refine_1

procedure {:inline 1} Civl_Wrapper_Global_NoninterferenceChecker_Refine_1

procedure {:inline 1} Civl_Wrapper_YieldToYield_NoninterferenceChecker_Refine_2

procedure {:inline 1} Civl_Wrapper_Global_NoninterferenceChecker_Refine_2

procedure {:inline 1} Civl_Wrapper_YieldToYield_NoninterferenceChecker_Refine_3

procedure {:inline 1} Civl_Wrapper_Global_NoninterferenceChecker_Refine_3