Atomic Operations and Invariants

Creating an invariant

Let’s start by looking at how to create an invariant.

First, let’s define a predicate owns x, to mean that we hold full-permission on x.

let owns (x:ref U32.t) : timeless_slprop = exists* v. pts_to x v

Now, if we can currently prove pts_to r x then we can turn it into an invariant inv i (owns r), as shown below.

ghost
fn create_invariant (r:ref U32.t) (v:erased U32.t)
requires pts_to r v
returns i:iname
ensures inv i (owns r)
{
    fold owns;
    new_invariant (owns r)
}

Importantly, when we turn pts_to r x into inv i (owns r), we lose ownership of pts_to r x. Remember, once we have inv i (owns r), Pulse’s logic aims to prove that owns r remains true always. If we were allowed to retain pts_to r x, while also creating an inv i (owns r), we can clearly break the invariant, e.g., by freeing r.

Impredicativity and the later modality

Pulse allows any predicate p:slprop to be turned into an invariant inv i p : slprop. Importantly, inv i p is itself an slprop, so one can even turn an invariant into another invariant, inv i (inv j p), etc. This ability to turn any predicate into an invariant, including invariants themselves, makes Pulse an impredicative separation logic.

Impredicativity turns out to be useful for a number of reasons, e.g., one could create a lock to protect access to a data structure that may itself contain further locks. However, soundly implementing impredicativity in a separation logic is challenging, since it involves resolving a kind of circularity in the definitions of heaps and heap predicates. PulseCore resolves this circularity using something called indirection theory, using it to provide a foundational model for impredicative invariants, together with all the constructs of Pulse. The details of this construction is out of scope here, but one doesn’t really need to know how the construction of the model works to use the resulting logic.

We provide a bit of intuition about the model below, but for now, just keep in mind that Pulse includes the following abstract predicates:

val later (p:slprop) : slprop
val later_credit (i:nat) : slprop

with the following forms to introduce and eliminate them:

ghost fn later_intro (p: slprop)
requires p
ensures later p

ghost fn later_elim (p: slprop)
requires later p ** later_credit 1
ensures p

fn later_credit_buy (amt:nat)
requires emp
ensures later_credit n

Opening Invariants

Once we’ve allocated an invariant, inv i (owns r), what can we do with it? As we said earlier, one can make use of the owns r in an atomic computation, so long as we restore it at the end of the atomic step.

The with_invariants construct gives us access to the invariant within the scope of at most one atomic step, preceded or succeeded by as many ghost or unobservable steps as needed.

The general form of with_invariants is as follows, to “open” invariants i_1 to i_k in the scope of e.

with_invariants i_1 ... i_k
returns x:t
ensures post
{ e }

In many cases, the returns and ensures annotations are omitted, since it can be inferred.

This is syntactic sugar for the following nest:

with_invariants i_1 {
 ...
  with_invariants i_k
  returns x:t
  ensures post
  { e }
 ...
}

Here’s the rule for opening a single invariant inv i p using with_invariant i { e } is as follows:

• i must have type iref and inv i p must be provable in the current context, for some p:slprop

• e must have the type stt_atomic t j (later p ** r) (fun x -> later p ** s x). [1] That is, e requires and restores later p, while also transforming r to s x, all in at most one atomic step. Further, the name_of_inv i must not be in the set j.

• with_invariants i { e } has type stt_atomic t (add_inv i j) (inv i p ** r) (fun x -> inv i p ** s x). That is, e gets to use p for a step, and from the caller’s perspective, the context was transformed from r to s, while the use of p is hidden.

• Pay attention to the add_inv i j index on with_invariants: stt_atomic (or stt_ghost) computation is indexed by the names of all the invariants that it may open.

Let’s look at a few examples to see how with_invariants works.

[@@expect_failure]
atomic
fn update_ref_atomic (r:ref U32.t) (i:iname) (v:U32.t)
requires inv i (owns r)
ensures inv i (owns r)
{
  with_invariants i {    //later (owns r)
     unfold owns;        //cannot prove owns; only later (owns r)
  }
}

atomic
fn update_ref_atomic (r:ref U32.t) (i:iname) (v:U32.t)
requires inv i (owns r) ** later_credit 1
ensures inv i (owns r)
opens [i]
{
  with_invariants i {    //later (owns r) ** later_credit 1
     later_elim _;       //ghost step: owns r
     unfold owns;        //ghost step;  exists* u. pts_to r u
     write_atomic r v;   //atomic step; pts_to r v
     fold owns;          //ghost step;  owns r
     later_intro (owns r) //ghost step: later (owns r)
  } // inv i (owns r)
}

fn update_ref (r:ref U32.t) (i:iname) (v:U32.t)
requires inv i (owns r)
ensures inv i (owns r)
{                    
  later_credit_buy 1;
  update_ref_atomic r i v;
}

The later modality and later credits

Having seen an example with later modality at work, we provide a bit of intuition for the underlying model.

The semantics of PulseCore is defined with respect to memory with an abstract notion of a “ticker”, a natural number counter, initialized at the start of a program’s execution. In other logics, this is sometimes called a “step index”, but in PulseCore, the ticker is unrelated to the number of actual steps a computation takes. Instead, at specific points in the program, the programmer can issue a specific ghost instruction to “tick” the ticker, decreasing its value by one unit. The decreasing counter provides a way to define an approximate fixed point between the otherwise-circular heaps and heap predicates. The logic is defined in such a way that it is always possible to pick a high enough initial value for the ticker so that any finite number of programs steps can be executed before the ticker is exhausted.

Now, rather than explicitly working with the ticker, PulseCore encapsulates all reasoning about the ticker using two logical constructs: the later modality and later credits, features found in Iris and other separation logics that feature impredicativity.

The predicate later p states that the p:slprop is true after one tick.

val later (p: slprop) : slprop

All predicates p:slprop are “hereditary”, meaning that if they are true in a given memory, then they are also true after that memory is ticked. The ghost function later_intro embodies this principle: from p one can prove later p.

ghost fn later_intro (p: slprop)
requires p
ensures later p

Given a later p, one can prove p by using later_elim. This ghost function effectively “ticks” the memory (since later p says that p is true after a tick), but in order to do so, it needs a precondition that the ticker has not already reached zero: later_credit 1 says just that, i.e., that the memory can be ticked at least once.

ghost fn later_elim (p: slprop)
requires later p ** later_credit 1
ensures p

The only way to get a later_credit 1 is to buy a credit with the operation below—this is a concrete operation that ensures that the memory can be ticked at least n times.

fn later_credit_buy (amt:nat)
requires emp
ensures later_credit n

At an abstract level, if the ticker cannot be ticked further, the program loops indefinitely—programs that use later credits (and more generally in step indexed logics) are inherently proven only partially correct and are allowed to loop infinitely. At a meta-level, we show that one can always set the initial ticker value high enough that later_credit_buy will never actually loop indefinitely. In fact, when compiling a program, Pulse extracts later_credit_buy n to a noop ().

Note, later credits can also be split and combined additively:

val later_credit_zero ()
: Lemma (later_credit 0 == emp)

val later_credit_add (a b: nat)
: Lemma (later_credit (a + b) == later_credit a ** later_credit b)

All predicates p:slprop are hereditary, meaning that p implies later p. Some predicates, including many common predicates like pts_to are also timeless, meaning that later p implies p. Combining timeless predicates with ** or exisentially quantifying over timeless predicates yields a timeless predicate.

All of the following are available in Pulse.Lib.Core:

val timeless (p: slprop) : prop
let timeless_slprop = v:slprop { timeless v }
val timeless_emp : squash (timeless emp)
val timeless_pure  (p:prop) : Lemma (timeless (pure p))
val timeless_star (p q : slprop) : Lemma
   (requires timeless p /\ timeless q)
   (ensures timeless (p ** q))
val timeless_exists (#a:Type u#a) (p: a -> slprop) : Lemma
 (requires forall x. timeless (p x))
 (ensures timeless (op_exists_Star p))

And in Pulse.Lib.Reference, we have:

val pts_to_timeless (#a:Type) (r:ref a) (p:perm) (x:a)
: Lemma (timeless (pts_to r #p x))
        [SMTPat (timeless (pts_to r #p x))]

For timeless predicates, the later modality can be eliminated trivially without requiring a credit.

ghost fn later_elim_timeless (p: timeless_slprop)
requires later p
ensures p

let owns_timeless (x:ref U32.t)
: squash (timeless (owns x))
by T.(norm [delta_only [`%owns; `%auto_squash]]; 
      mapply (`FStar.Squash.return_squash);
      mapply (`timeless_exists))
= ()

let owns (x:ref U32.t) : timeless_slprop = exists* v. pts_to x v

atomic
fn update_ref_atomic_alt (r:ref U32.t) (i:iname) (v:U32.t)
requires inv i (owns r)
ensures inv i (owns r)
opens [i]
{
  with_invariants i {    //later (owns r) ** later_credit 1
     later_elim_timeless _;       //owns r
     unfold owns;        //ghost step;  exists* u. pts_to r u
     write_atomic r v;   //atomic step; pts_to r v
     fold owns;          //ghost step;  owns r
     later_intro (owns r) //later (owns r)
  } // inv i (owns r)
}

Double opening is unsound

To see why we have to track the names of the opened invariants, consider the example below. If we opened the same invariant twice within the same scope, then it’s easy to prove False:

[@@expect_failure]
fn double_open_bad (r:ref U32.t) (i:inv (owns r))
requires emp
ensures pure False
{
    with_invariants i {
      with_invariants i {
        unfold owns;
        unfold owns;
        pts_to_dup_impossible r;
        fold owns;
        fold owns
      }
    }
}

Here, we open the invariants i twice and get owns r ** owns r, or more than full permission to r—from this, it is easy to build a contradiction.

Subsuming atomic computations

Atomic computations can be silently converted to regular, stt computations, while forgetting which invariants they opened. For example, update_ref below is not marked atomic, so its type doesn’t record which invariants were opened internally.

fn update_ref (r:ref U32.t) (i:iname) (v:U32.t)
requires inv i (owns r)
ensures inv i (owns r)
{                    
  later_credit_buy 1;
  update_ref_atomic r i v;
}

This is okay, since a non-atomic computation can never appear within a with_invariants block—so, there’s no fear of an stt computation causing an unsound double opening. Attempting to use a non-atomic computation in a with_invariants block produces an error, as shown below.

[@@expect_failure] 
fn update_ref_fail (r:ref U32.t) (i:iname) (v:U32.t)
requires inv i (owns r)
ensures inv i (owns r)
{
  with_invariants i {
    unfold owns;
    r := v; //not atomic
    fold owns;
  }
}

- This computation is not atomic nor ghost. `with_invariants`
  blocks can only contain atomic computations.