Case Study: Counter

Implementation

Let us define a simple counter module. Our counter consists of three functions:

• a constructor, mk_counter, which creates a new counter starting at 0.
• an increment function, incr, which increments the counter and returns the old value of the counter.
• a read function, read, which reads the current value of the counter.

Furthermore, we want the counter to be shareable across multiple threads, so we will implement incr with CAS as the synchronisation mechanism.

Defining a Representation Predicate for the Counter

We are going to keep the fact that our counter is built on a pointer as an implementation detail. Instead, we will define a predicate describing when a value is a counter. Note that #n uses an implicit coercion from nat to Z called Z.of_nat. So if you have trouble applying lemmas that should work, it is likely because there is a hidden coercion in the way.

This predicate is, however, not persistent, so our value would not be shareable across threads. To fix this, we can put the knowledge into an invariant.

However, with this definition, we have locked the value of the pointer to always be n. To fix this, we could abstract the value and instead only specify its lower bound.

We can now change what the pointer maps to, but we still cannot refine the lower bound. The final step is to use ghost state. The idea is to link n and m to pieces of ghost state in such a way that the validity of their composite is n ≤ m. To achieve this, we will use the authoritative resource algebra, auth. This resource algebra is parametrised by a CMRA, A. There are two types of elements in the carrier of the authoritative RA:

• ● x called an authoritative element
• ◯ y called a fragment

where x, y ∈ A. The idea of the authoritative RA is as follows. The authoritative element represents the whole of the resource, while the fragments act as the pieces. To achieve this, the authoritative element acts like the exclusive RA, while the fragment inherits all the operations of A. Furthermore, validity of ● x ⋅ ◯ y is defined as ✓ x ∧ y ≼ x. In our case, we will use the authoritative RA over the max_nat resource algebra. The carrier of max_nat is the natural numbers, and the operation is the maximum.

As such, ● (MaxNat m) will represent the true value of the counter m, and ◯ (MaxNat n) will represent a fragment of the counter – a lower bound n.

Properties of the Authoritative RA with MaxNat

Before we start proving the specification, let us prove some useful lemmas about our ghost state. For starters, we need to know that we can allocate the initial state we need.

Ownership of multiple fragments of state amounts to ownership of their composite. So we can simplify the goal a little.

Now the goal is on the form expected by own_alloc.

However, we are only allowed to allocate valid states. So we must prove that our desired state is a valid one. The validity of auth says that the fragment must be included in the authoritative element and the authoritative element must be valid.

Inclusion for max_nat turns out to be the natural ordering.

All elements of max_nat are valid.

As we saw in the Resource Algebra chapter, to update a resource, we must show that we can perform a frame preserving update to the updated resource.

auth has its own special version of these called local updates, as we know what the whole of the state is.

Proving the Counter Specification

We are finally ready to give and prove specifications for the three counter functions. We begin with mk_counter.

A Simple Counter Client

To illustrate how this counter specification works, let us consider a simple concurrent client of our counter module, which increments a counter twice in parallel. Our specification will simply be that the value of the counter will be at least 1 afterwards.

A Stronger Counter Specification

Our first specification only allowed us to find a lower bound for the value in par_incr. Any solution to this problem has to be non-persistent, as we need to aggregate the knowledge to conclude the total value. To this end, we will use fractions. The frac resource algebra is similar to dfrac but without the capability of discarding fractions. As such, frac consists of non-negative rationals with addition as composition, and a fraction is only valid if it is less than or equal to 1. This means that all the fractions can add up to at most 1. Combining frac with other resource algebras allows us to keep track of how much of the resource we own, meaning we can do the exact kind of aggregation we need. So this time, we will use the resource algebra authR (optionUR (prodR fracR natR)). Here, natR is the natural numbers with addition.

With this definition, we can now decompose access to the counter by splitting the fraction, as well as splitting the knowledge of how much the counter has been incremented.

When allocating a new state, there will be one fragment, which contains the entire fraction. Using the above lemma, we can then split up the fragment and supply these fragments to participating threads.

The fragments of natural numbers add up to the full value, meaning that, in particular, they must all be less than or equal to the authoritative element.

However, when a fragment has the entire fraction, there can't be any other fragments – intuitively, we have collected all contributions from all threads. So the count stored in the fragment must be equal to the one in the authoritative element.

Finally, when we have both the authoritative element and a fragment, we can increment both.

Let us prove the specifications for the counter functions again. This time, however, we will have two specifications for read – one with an arbitrary fraction and one with the whole fraction.