# Parallel Increment

In this chapter, we look at an example first studied by Susan Owicki
and David Gries, in a classic paper titled Verifying properties of
parallel programs: an axiomatic approach. The problem involves
proving that a program that atomically increments an integer reference
`r`

twice in parallel correctly adds 2 to `r`

. There are many ways
to do this—Owicki & Gries’ approach, adapted to a modern separation
logic, involves the use of additional ghost state and offers a modular
way to structure the proof.

While this is a very simple program, it captures the essence of some of the reasoning challenges posed by concurrency: two threads interact with a shared resource, contributing to it in an undetermined order, and one aims to reason about the overall behavior, ideally without resorting to directly analyzing each of the possible interleavings.

## Parallel Blocks

Pulse provides a few primitives for creating new threads. The most basic one is parallel composition, as shown below:

```
parallel
requires p1 and p2
ensures q1 and q2
{ e1 }
{ e2 }
```

The typing rule for this construct requires:

```
val e1 : stt a p1 q1
val e2 : stt b p2 q2
```

and the `parallel`

block then has the type:

```
stt (a & b) (p1 ** p2) (fun (x, y) -> q1 x ** q2 y)
```

In other words, if the current context can be split into separate
parts `p1`

and `p2`

satisfying the preconditions of `e1`

and
`e2`

, then the parallel block executes `e1`

and `e2`

in
parallel, waits for both of them to finish, and if they both do,
returns their results as a pair, with their postconditions on each
component.

Using `parallel`

, one can easily program the `par`

combinator
below:

```
fn par (#pf #pg #qf #qg:_)
(f: unit -> stt unit pf (fun _ -> qf))
(g: unit -> stt unit pg (fun _ -> qg))
requires pf ** pg
ensures qf ** qg
{
parallel
requires pf and pg
ensures qf and qg
{ f () }
{ g () };
()
}
```

As we saw in the introduction to Pulse, it’s easy to increment two separate references in parallel:

```
fn par_incr (x y:ref int)
requires pts_to x 'i ** pts_to y 'j
ensures pts_to x ('i + 1) ** pts_to y ('j + 1)
{
par (fun _ -> incr x)
(fun _ -> incr y)
}
```

But, what if we wanted to increment the same reference in two separate threads? That is, we wanted to program something like this:

```
fn add2 (x:ref int)
requires pts_to x 'i
ensures pts_to x ('i + 2)
{
par (fun _ -> incr x)
(fun _ -> incr x)
}
```

But, this program doesn’t check. The problem is that we have only a
single `pts_to x 'i`

, and we can’t split it to share among the
threads, since both threads require full permission to `x`

to update
it.

Further, for the program to correctly add `2`

to `x`

, each
increment operations must take place atomically, e.g., if the two
fragments below were executed in parallel, then they may both read the
initial value of `x`

first, bind it to ``v`

, and then both update
it to `v + 1`

.

```
let v = !x; || let v = !x;
x := v + 1; || x := v + 1;
```

Worse, without any synchronization, on modern processors with weak memory models, this program could exhibit a variety of other behaviors.

To enforce synchronization, we could use a lock, e.g., shown below:

```
fn attempt (x:ref int)
requires pts_to x 'i
ensures exists* v. pts_to x v
{
let l = L.new_lock (exists* v. pts_to x v);
fn incr ()
requires L.lock_alive l #0.5R (exists* v. pts_to x v)
ensures L.lock_alive l #0.5R (exists* v. pts_to x v)
{
L.acquire l;
let v = !x;
x := v + 1;
L.release l
};
L.share2 l;
par incr incr;
L.gather2 l;
L.acquire l;
L.free l
}
```

This program is type correct and free from data races. But, since the
lock holds the entire permission on `x`

, there’s no way to give this
function a precise postcondition.

Note

In this section, we use an implementation of spin locks from the
Pulse library, Pulse.Lib.SpinLock. Unlike the version we developed
in the previous chapter, these locks use a fraction-indexed
permission, `lock_alive l #f p`

. The also provide a predicate,
`lock_acquired l`

, that indicates when the lock has been
taken. With full-permission to the lock, and `lock_acquired l`

,
the lock can be freed—reclaiming the underlying
memory. Additionally, the `lock_acquired`

predicate ensures that
locks cannot be double freed. As such, `Pulse.Lib.SpinLock`

fixes
the problems with the spin locks we introduced in the previous
chapter and also provides a solution to the exercises given there.

## A First Take, with Locks

Owicki and Gries’ idea was to augment the program with auxiliary variables, or ghost state, that are purely for specification purposes. Each thread gets its own piece of ghost state, and accounts for how much that thread has contributed to the current value of shared variable. Let’s see how this works in Pulse.

The main idea is captured by `lock_inv`

, the type of the predicate
protected by the lock:

```
let contributions (left right: GR.ref int) (i v:int) : v:vprop { is_big v }=
exists* (vl vr:int).
GR.pts_to left #0.5R vl **
GR.pts_to right #0.5R vr **
pure (v == i + vl + vr)
let lock_inv (x:ref int) (init:int) (left right:GR.ref int) : v:vprop { is_big v } =
exists* v.
pts_to x v **
contributions left right init v
```

Our strawman `lock`

in the `attempt`

shown before had type ```
lock
(exists* v. pts_to x v)
```

. This time, we add a conjunct that refines
the value `v`

, i.e., the predicate `contributions l r init v`

says
that the current value of `x`

protected by the lock (i.e., `v`

) is
equal to `init + vl + vr`

, where `init`

is the initial value of
`x`

; `vl`

is the value of the ghost state owned by the “left”
thread; and `vr`

is the value of the ghost state owned by the
“right” thread. In other words, the predicate ```
contributions l r init
v
```

shows that `v`

always reflects the values of the contributions
made by each thread.

Note, however, the `contributions`

predicate only holds
half-permission on the left and right ghost variables. The other half
permission is held outside the lock and allows us to keep track of
each threads contribution in our specifications.

Here’s the code for the left thread, `incr_left`

:

```
fn incr_left (x:ref int)
(#p:perm)
(#left:GR.ref int)
(#right:GR.ref int)
(#i:erased int)
(lock:L.lock )
requires L.lock_alive lock #p (lock_inv x i left right) ** GR.pts_to left #0.5R 'vl
ensures L.lock_alive lock #p (lock_inv x i left right) ** GR.pts_to left #0.5R ('vl + 1)
{
L.acquire lock;
unfold lock_inv;
unfold contributions;
let v = !x;
x := v + 1;
GR.gather left;
GR.write left ('vl + 1);
GR.share left;
fold (contributions left right i (v + 1));
fold lock_inv;
L.release lock
}
```

Its arguments include

`x`

and the`lock`

, but also both pieces of ghost state,`left`

and`right`

, and an erased value`i`

for the initial value of`x`

.Its precondition holds half permission on the ghost reference

`left`

Its postcondition returns half-permission to

`left`

, but proves that it was incremented, i.e., the contribution of the left thread to the value of`x`

increased by`1`

.

Notice that even though we only had half permission to `left`

, the
specifications says we have updated `left`

—that’s because we can
get the other half permission we need by acquiring the lock.

We acquire the lock and update increment the value stored in

`x`

.And then we follow the increment with several ghost steps:

Gain full permission on

`left`

by combining the half permission from the precondition with the half permission gained from the lock.Increment

`left`

.Share it again, returning half permission to the lock when we release it.

Finally, we

`GR.pts_to left #one_half (`vl + 1)`

left over to return to the caller in the postcondition.

The code of the right thread is symmetrical, but in this, our first take, we have to essentially repeat the code—we’ll see how to remedy this shortly.

```
fn incr_right (x:ref int)
(#p:perm)
(#left:GR.ref int)
(#right:GR.ref int)
(#i:erased int)
(lock:L.lock)
requires L.lock_alive lock #p (lock_inv x i left right) ** GR.pts_to right #0.5R 'vl
ensures L.lock_alive lock #p (lock_inv x i left right) ** GR.pts_to right #0.5R ('vl + 1)
{
L.acquire lock;
unfold lock_inv;
unfold contributions;
let v = !x;
x := v + 1;
GR.gather right;
GR.write right ('vl + 1);
GR.share right;
fold (contributions left right i (v + 1));
fold (lock_inv x i left right);
L.release lock
}
```

Finally, we can implement `add2`

with the specification we want:

```
fn add2 (x:ref int)
requires pts_to x 'i
ensures pts_to x ('i + 2)
{
let left = GR.alloc 0;
let right = GR.alloc 0;
GR.share left;
GR.share right;
fold (contributions left right 'i 'i);
fold (lock_inv x 'i left right);
let lock = L.new_lock (lock_inv x 'i left right);
L.share2 lock;
par (fun _ -> incr_left x lock)
(fun _ -> incr_right x lock);
L.gather2 lock;
L.acquire lock;
L.free lock;
unfold lock_inv;
unfold contributions;
GR.gather left;
GR.gather right;
GR.free left;
GR.free right;
}
```

We allocate

`left`

and`right`

ghost references, initializing them to`0`

.Then we split them, putting half permission to both in the lock, retaining the other half.

Then spawn two threads for

`incr_left`

and`incr_right`

, and get as a postcondition that contributions of both threads and increased by one each.Finally, we acquire the lock, get

`pts_to x v`

, for some`v`

, and`contributions left right i v`

. Once we gather up the permission on`left`

and`right`

, and now the`contributions left right i v`

tells us that`v == i + 1 + 1`

, which is what we need to conclude.

## Modularity with higher-order ghost code

Our next attempt aims to write a single function `incr`

, rather than
`incr_left`

and `incr_right`

, and to give `incr`

a more
abstract, modular specification. The style we use here is based on an
idea proposed by Bart Jacobs and Frank Piessens in a paper titled
Expressive modular fine-grained concurrency specification.

The main idea is to observe that `incr_left`

and `incr_right`

only
differ by the ghost code that they execute. But, Pulse is higher
order: so, why not parameterize a single function by `incr`

and let
the caller instantiate `incr`

twice, with different bits of ghost
code. Also, while we’re at it, why not also generalize the
specification of `incr`

so that it works with any user-chosen
abstract predicate, rather than `contributions`

and `left/right`

ghost state. Here’s how:

```
fn incr (x: ref int)
(#p:perm)
(#refine #aspec: int -> vprop)
(l:L.lock)
(ghost_steps:
(v:int -> vq:int -> stt_ghost unit
emp_inames
(refine v ** aspec vq ** pts_to x (v + 1))
(fun _ -> refine (v + 1) ** aspec (vq + 1) ** pts_to x (v + 1))))
requires L.lock_alive l #p (exists* v. pts_to x v ** refine v) ** aspec 'i
ensures L.lock_alive l #p (exists* v. pts_to x v ** refine v) ** aspec ('i + 1)
{
L.acquire l;
with _v. _;
let vx = !x;
rewrite each _v as vx;
x := vx + 1;
ghost_steps vx 'i;
L.release l;
}
```

As before, `incr`

requires `x`

and the `lock`

, but, this time,
it is parameterized by:

A predicate

`refine`

, which generalizes the`contributions`

predicate from before, and refines the value that`x`

points to.A predicate

`aspec`

, an abstract specification chosen by the caller, and serves as the main specification for`incr`

, which transitions from`aspec 'i`

to`aspec ('i + 1)`

.And, finally, the ghost function itself,

`ghost_steps`

, now specified abstractly in terms of the relationship between`refine`

,`aspec`

and`pts_to x`

—it says, effectively, that once`x`

has been updated, the abstract predicates`refine`

and`aspec`

can be updated too.

Having generalized `incr`

, we’ve now shifted the work to the
caller. But, `incr`

, now verified once and for all, can be used with
many different callers just by instantiating it differently. For
example, if we wanted to do a three-way parallel increment, we could
reuse our `incr`

as is. Whereas, our first take would have to be
completely revised, since `incr_left`

and `incr_right`

assume that
there are only two ghost references, not three.

Here’s one way to instantiate `incr`

, proving the same specification
as `add2`

.

```
fn add2_v2 (x: ref int)
requires pts_to x 'i
ensures pts_to x ('i + 2)
{
let left = GR.alloc 0;
let right = GR.alloc 0;
GR.share left;
GR.share right;
fold (contributions left right 'i 'i);
let lock = L.new_lock (
exists* (v:int).
pts_to x v ** contributions left right 'i v
);
ghost
fn step
(lr:GR.ref int)
(b:bool { if b then lr == left else lr == right })
(v vq:int)
requires
contributions left right 'i v **
GR.pts_to lr #0.5R vq **
pts_to x (v + 1)
ensures
contributions left right 'i (v + 1) **
GR.pts_to lr #0.5R (vq + 1) **
pts_to x (v + 1)
{
unfold contributions;
if b
{
with _p _v. rewrite (GR.pts_to lr #_p _v) as (GR.pts_to left #_p _v);
GR.gather left;
GR.write left (vq + 1);
GR.share left;
with _p _v. rewrite (GR.pts_to left #_p _v) as (GR.pts_to lr #_p _v);
fold (contributions left right 'i (v + 1));
}
else
{
with _p _v. rewrite (GR.pts_to lr #_p _v) as (GR.pts_to right #_p _v);
GR.gather right;
GR.write right (vq + 1);
GR.share right;
with _p _v. rewrite (GR.pts_to right #_p _v) as (GR.pts_to lr #_p _v);
fold (contributions left right 'i (v + 1));
}
};
L.share2 lock;
par (fun _ -> incr x lock (step left true))
(fun _ -> incr x lock (step right false));
L.gather2 lock;
L.acquire lock;
L.free lock;
unfold (contributions left right 'i);
GR.gather left;
GR.gather right;
GR.free left;
GR.free right;
}
```

The code is just a rearrangement of what we had before, factoring the
ghost code in `incr_left`

and `incr_right`

into a ghost function
`step`

. When we spawn our threads, we pass in the ghost code to
either update the left or the right contribution.

This code still has two issues:

The ghost

`step`

function is a bloated: we have essentially the same code and proof twice, once in each branch of the conditional. We can improve this by defining a custom bit of ghost state using Pulse’s support for partial commutative monoids—but that’s for another chapter.We allocate and free memory for a lock, which is inefficient—could we instead do things with atomic operations? We’ll remedy that next.

### Exercise

Instead of explicitly passing a ghost function, use a quantified trade.

## A version with invariants

As a final example, in this section, we’ll see how to program `add2`

using invariants and atomic operations, rather than locks.

Doing this properly will require working with bounded, machine
integers, e.g., `U32.t`

, since these are the only types that support
atomic operations. However, to illustrate the main ideas, we’ll assume
two atomic operations on unbounded integers—this will allow us to
not worry about possible integer overflow. We leave as an exercise the
problem of adapting this to `U32.t`

.

```
assume
val atomic_read (r:ref int) (#p:_) (#i:erased int)
: stt_atomic int emp_inames
(pts_to r #p i)
(fun v -> pts_to r #p i ** pure (reveal i == v))
assume
val cas (r:ref int) (u v:int) (#i:erased int)
: stt_atomic bool emp_inames
(pts_to r i)
(fun b ->
cond b (pts_to r v ** pure (reveal i == u))
(pts_to r i))
```

### Cancellable Invariants

The main idea of doing the `add2`

proof is to use an invariant
instead of a lock. Just as in our previous code, `add2`

starts with
allocating an invariant, putting ```
exists* v. pts_to x v **
contribution left right i v
```

in the invariant. Then call incr twice
in different threads. However, finally, to recover ```
pts_to x (v +
2)
```

, where previously we would acquire the lock, with a regular
invariant, we’re stuck, since the `pts_to x v`

permission is inside
the invariant and we can’t take it out to return to the caller.

An invariant `inv i p`

guarantees that the property `p`

is true
and remains true for the rest of a program’s execution. But, what if
we wanted to only enforce `p`

as an invariant for some finite
duration, and then to cancel it? This is what the library
`Pulse.Lib.CancellableInvariant`

provides. Here’s the relevant part
of the API:

```
[@@ erasable]
val cinv : Type0
val iref_of (c:cinv) : GTot iref
```

The main type it offers is `cinv`

, the name of a cancellable
invariant.

```
ghost
fn new_cancellable_invariant (v:boxable)
requires v
returns c:cinv
ensures inv (iref_of c) (cinv_vp c v) ** active c 1.0R
```

Allocating a cancellable invariant is similar to allocating a regular
invariant, except one gets an invariant for an abstract predicate
`cinv_cp c v`

, and a fraction-indexed predicate `active c 1.0R`

which allows the cancellable invariant to be shared and gathered
between threads.

The `cinv_cp c v`

predicate can be used in conjunction with
`active`

to recover the underlying predicate `v`

—but only when
the invariant has not been cancelled yet—this is what
`unpack_cinv_vp`

, and its inverse, `pack_cinv_vp`

, allow one to
do.

```
ghost
fn unpack_cinv_vp (#p:perm) (#v:vprop) (c:cinv)
requires cinv_vp c v ** active c p
ensures v ** unpacked c ** active c p
ghost
fn pack_cinv_vp (#v:vprop) (c:cinv)
requires v ** unpacked c
ensures cinv_vp c v
```

Finally, if one has full permission to the invariant (```
active c
1.0R
```

) it can be cancelled and the underlying predicate `v`

can be
obtained as postcondition.

```
ghost
fn cancel (#v:vprop) (c:cinv)
requires inv (iref_of c) (cinv_vp c v) ** active c 1.0R
ensures v
opens add_inv emp_inames (iref_of c)
```

### An increment operation

Our first step is to build an increment operation from an
`atomic_read`

and a `cas`

. Here is its specification:

```
fn incr_atomic
(x: ref int)
(#p:perm)
(#refine #aspec: int -> vprop)
(c:C.cinv)
(f: (v:int -> vq:int -> stt_ghost unit
emp_inames
(refine v ** aspec vq ** pts_to x (v + 1))
(fun _ -> refine (v + 1) ** aspec (vq + 1) ** pts_to x (v + 1))))
requires inv (C.iref_of c) (C.cinv_vp c (exists* v. pts_to x v ** refine v)) ** aspec 'i ** C.active c p
ensures inv (C.iref_of c) (C.cinv_vp c (exists* v. pts_to x v ** refine v)) ** aspec ('i + 1) ** C.active c p
```

The style of specification is similar to the generic style we used
with `incr`

, except now we use cancellable invariant instead of a
lock.

For its implementation, the main idea is to repeatedly read the
current value of `x`

, say `v`

; and then to `cas`

in `v+1`

if
the current value is still `v`

.

The `read`

function is relatively easy:

```
atomic
fn read ()
requires inv (C.iref_of c) (C.cinv_vp c (exists* v. pts_to x v ** refine v)) ** C.active c p
returns v:int
ensures inv (C.iref_of c) (C.cinv_vp c (exists* v. pts_to x v ** refine v)) ** C.active c p
opens (add_inv emp_inames (C.iref_of c))
{
with_invariants (C.iref_of c)
{
C.unpack_cinv_vp #p c;
let v = atomic_read x;
C.pack_cinv_vp #(exists* v. pts_to x v ** refine v) c;
v
}
};
```

We open the invariant

`l`

; then, knowing that the invariant is still active, we can unpack` it; then read the value`v`

; pack it back; and return`v`

.

The main loop of `incr_atomic`

is next, shown below:

```
let mut continue = true;
fold (cond true (aspec 'i) (aspec ('i + 1)));
while (
with _b. _;
let b = !continue;
rewrite each _b as b;
b
)
invariant b.
inv (C.iref_of c) (C.cinv_vp c (exists* v. pts_to x v ** refine v)) **
pts_to continue b **
C.active c p **
cond b (aspec 'i) (aspec ('i + 1))
{
let v = read ();
let next =
with_invariants (C.iref_of c)
returns b1:bool
ensures inv (C.iref_of c) (C.cinv_vp c (exists* v. pts_to x v ** refine v))
** cond b1 (aspec 'i) (aspec ('i + 1))
** pts_to continue true
** C.active c p
{
C.unpack_cinv_vp c;
let b = cas x v (v + 1);
if b
{
elim_cond_true b _ _;
elim_cond_true true _ _;
with vv. assert (refine vv);
f vv _;
intro_cond_false (aspec 'i) (aspec ('i + 1));
C.pack_cinv_vp #(exists* v. pts_to x v ** refine v) c;
false
}
else
{
with p q. rewrite (cond b p q) as q;
C.pack_cinv_vp #(exists* v. pts_to x v ** refine v) c;
true
}
};
continue := next
};
```

The loop invariant says:

the invariant remains active

the local variable

`continue`

determines if the loop iteration continuesand, so long as the loop continues, we still have

`aspec 'i`

, but when the loop ends we have`aspec ('i + 1)`

The body of the loop is also interesting and consists of two atomic
operations. We first `read`

the value of `x`

into `v`

. Then we
open the invariant again try to `cas`

in `v+1`

. If it succeeds, we
return `false`

from the `with_invariants`

block; otherwise
`true`

. And, finally, outside the `with_invariants`

block, we set
the `continue`

variable accordingly. Recall that `with_invariants`

allows at most a single atomic operation, so we having done a `cas`

,
we are not allowed to also set `continue`

inside the
`with_invariants`

block.

`add2_v3`

Finally, we implement our parallel increment again, `add2_v3`

, this
time using invariants, though it has the same specification as before.

```
fn add2_v3 (x: ref int)
requires pts_to x 'i
ensures pts_to x ('i + 2)
{
let left = GR.alloc 0;
let right = GR.alloc 0;
GR.share left;
GR.share right;
fold (contributions left right 'i 'i);
let c = C.new_cancellable_invariant (
exists* (v:int).
pts_to x v **
contributions left right 'i v
);
ghost
fn step
(lr:GR.ref int)
(b:bool { if b then lr == left else lr == right })
(v vq:int)
requires
contributions left right 'i v **
GR.pts_to lr #0.5R vq **
pts_to x (v + 1)
ensures
contributions left right 'i (v + 1) **
GR.pts_to lr #0.5R (vq + 1) **
pts_to x (v + 1)
{
unfold contributions;
if b
{
with _p _v. rewrite (GR.pts_to lr #_p _v) as (GR.pts_to left #_p _v);
GR.gather left;
GR.write left (vq + 1);
GR.share left;
with _p _v. rewrite (GR.pts_to left #_p _v) as (GR.pts_to lr #_p _v);
fold (contributions left right 'i (v + 1));
}
else
{
with _p _v. rewrite (GR.pts_to lr #_p _v) as (GR.pts_to right #_p _v);
GR.gather right;
GR.write right (vq + 1);
GR.share right;
with _p _v. rewrite (GR.pts_to right #_p _v) as (GR.pts_to lr #_p _v);
fold (contributions left right 'i (v + 1));
}
};
C.share2 c;
with pred. assert (inv (C.iref_of c) (C.cinv_vp c (exists* v. pts_to x v ** pred v)));
dup_inv (C.iref_of c) (C.cinv_vp c (exists* v. pts_to x v ** pred v));
par (fun _ -> incr_atomic x c (step left true))
(fun _ -> incr_atomic x c (step right false));
C.gather2 c;
C.cancel c;
unfold contributions;
GR.gather left;
GR.gather right;
GR.free left;
GR.free right;
drop_ (inv _ _)
}
```

The code too is very similar to `add2_v2`

, except instead of
allocating a lock, we allocate a cancellable invariant. And, at the
end, instead of acquiring, and leaking, the lock, we simply cancel the
invariant and we’re done.

## Exercise

Implement `add2`

on a `ref U32.t`

. You’ll need a precondition that
`'i + 2 < pow2 32`

and also to strengthen the invariant to prove
that each increment doesn’t overflow.