Persistently

Introduction

In separation logic, propositions are generally not duplicable. This is because resources are generally exclusive. However, resources do not have to be exclusive. A great example of this is `read-only memory'. There is no danger in letting many threads access the same location simultaneously if they can only read from it. Hence, it would not make sense to require that ownership of those locations be exclusive. Motivated by this, we introduce a new modality denoted the persistently modality, written □ P, for propositions P. The proposition □ P describes the same resources as P, except it does not claim that the resources are exclusive – hence □ P can be duplicated. Persistent propositions hence act like propositions in an intuitionistic logic, which is why they are also sometimes referred to as intuitionistic. A proposition is persistent when P ⊢ □ P. That is, assuming P, we need to show that P does not rely on any exclusive resources. Persistency is preserved by most connectives, so proving that a proposition is persistent is usually a matter of showing that the mentioned resources are shareable. Which resources are shareable depends on the specific notions of resources being used. For the resource of heaps, a location can be marked as read-only, making it shareable. The associated points-to predicate hence becomes persistent. We will see an example of this later. Propositions that do not rely on resources altogether are trivially persistent. We have already given those types of propositions a name: pure. This is also why we do not have to split the non-spatial context when using iSplitL/iSplitR; all pure propositions are persistent, hence duplicable. Of course, not all persistent propositions are pure (e.g. persistent points-to predicates). Thus, the Iris Proof Mode provides a third context just for persistent propositions, called the persistent context. Pure propositions can go in all three contexts. Persistent propositions can go in the spatial context or the persistent context. And all other propositions are limited to the spatial context only. Iris uses the typeclass Persistent to identify persistent propositions.

The introduction pattern "#_" allows us to place a persistent hypothesis into the persistent context.

Notice that after splitting, both the non-spatial and persistent contexts are duplicated. In particular, HP is available in both subgoals.

Note that all propositions in the spatial context are treated as non-persistent, regardless of whether they are persistent.

We introduce HP to the spatial context.

HP is no longer duplicated.

Exercise: prove that persistent propositions are duplicable.

Persistent propositions satisfy a lot of nice properties simply by being duplicable P ⊢ P ∗ P. For example, P ∧ Q and P ∗ Q coincide when either P or Q is persistent. Likewise, P → Q and P -∗ Q coincide when P is persistent.

The Iris Proof Mode knows these facts and allows iSplit to introduce ∗ when one of its arguments is persistent.

Proving Persistency

To prove a proposition □ P, we must prove P without assuming any exclusive resources. In other words, we have to throw away the spatial context when proving P.

The iModIntro tactic introduces a modality in the goal. In this case, since the modality is a □, it throws away the spatial context.

Since the only difference between □ P and P is that the former does not claim the resources are exclusive, it follows that the persistently modality is idempotent.

Iris already knows that □ is idempotent, so it automatically removes all persistently modalities from a proposition when adding it to the persistent context. One may think of all propositions in the persistent context as having an implicit □ in front.

Similarly, we do not have to introduce □ before proving it.

Only propositions that are instances of the Persistent typeclass can be added to the persistent context. As with the typeclasses for pure, the Persistent typeclass can automatically identify most persistent propositions.

The Persistent typeclass detects that □ P ∗ □ Q is persistent.

By default, iFrame will not frame propositions from the persistent context. To make it do so, we must give it the argument "#".

Persistency is preserved by quantifications.

For simple predicates, such as myPredicate below, the Persistent typeclass can automatically infer that it is persistent. However, we can still manually make propositions instances of Persistent.

As mentioned in the beginning of the chapter, a proposition P is persistent when P ⊢ □ P. This is almost what Persistent requires us to prove.

Our actual goal is of the form P ⊢ <pers> P. Technically, there is a small discrepancy between □ and <pers>, but we will ignore that here. As pure propositions are persistent, we quite easily prove this.

Iris is quite smart, so we do not have to spell out the proof.

For more complicated predicates, such as ones defined as a fixpoint, Persistent cannot automatically infer its persistence. The following predicate asserts that all values in a given list are equal to 5.

This predicate only consists of pure propositions, so it should of course be persistent, but when we try to add it to the persistent context, Iris complains that it is not `intuitionistic' (i.e. persistent).

For such predicates, we have to prove that it is persistent manually, as we did for myPredicate above.

We prove it by induction in xs.

True is persistent

By IH, myPredFix xs' is persistent. As ⌜x = 5⌝ is also persistent, it follows that [myPredFix (x :: xs')] is persistent.

Iris now recognises myPredFix as persistent.

iPoseProof is similar to iDestruct, but it does not throw away the hypothesis being destructed, if it is persistent.

Examples of Persistent Propositions

Thus far, the only basic persistent propositions we have seen are pure propositions, such as equalities. In this section, we introduce two additional examples of persistent propositions: Hoare triples and persistent points-to predicates.

Hoare Triples

All Hoare triples are persistent. This probably does not come as a surprise if the reader recalls how we defined Hoare triples in the specifications chapter. As a reminder, here is the definition again. □( ∀ Φ, P -∗ ▷ (∀ r0 .. rn, Q -∗ Φ v) -∗ WP e {{v, Φ v }}) The outermost part of the definition is the persistently modality! As such, Hoare triples can be duplicated and reused. Intuitively, we should also expect Hoare triples to be persistent. A Hoare triple {{{ P }}} e {{{ Φ }}} does not actually claim ownership of any resources; it merely states that if we own the resources described by P, then we can safely run e, and we get the resources described by Φ in case of termination. Of course, if we can get ownership of the resources described by P multiple times, we should be able to run e multiple times. As an example, consider a function counter, which is parametrised by an increment function.

If inc is a function which adds 1 to the contents of a given location, we would expect the above program to return 2. We express this by describing the specification for inc in the precondition of the specification for counter.

Persistent Points-to

The resource of heaps is more sophisticated than what we have been letting on. The general shape of a points-to predicate is actually l ↦ dq v, where dq is a `discarded fraction'. We return to the `discarded' part momentarily, but for now, we assume that dq is a fraction in the interval (0; 1]. The predicate l ↦ v is a special case where the fraction dq is 1. The basic idea is that points-to predicates can be split up and recombined, allowing ownership of points-to predicates to be shared.

Crucially, a store operation can only take place if the entire fraction is owned, i.e. dq = 1. However, load operations can occur for any fraction.

Throw away half of the points-to predicate.

We can still load.

But we can no longer update the pointer.

Fractional points-to predicates are especially useful in scenarios where a location is read by multiple threads in parallel but later only used by a single thread.

The idea is to give each thread half of the points-to predicate and assert that both will return their halves afterwards.

Each thread has a fraction of the points-to predicate, so both can perform the load.

The threads return their fractions.

We combine them, allowing us to perform the store.

Let us now turn to the `discarded' part. If one owns a fraction of a points-to predicate, one can decide to discard the fraction. This means that it is no longer possible to recombine points-to predicates to get the full fraction. As such, the value in the points-to predicate can never be changed again – the location has become read-only. We write l ↦□ v for a points-to predicate whose fraction has been discarded. As the □ suggests, this predicate is persistent. Persistent points-to predicates are great if your program has a read-only location, as it becomes trivial to give all threads access to the associated points-to predicate, and it ensures that no thread can sneakily update the location. The pointsto_persist lemma asserts that we can update any points-to predicate l ↦{dq} v into a persistent one l ↦□ v.

There are some caveats as to when we can discard fractions; the proposition P ==∗ Q is equivalent to P -∗ (|==> Q), where |==> is the update modality, the details of which we defer to later. For now, we remark that the iMod tactic can remove the update modality in many cases. For instance, if the goal is a weakest precondition.

Make the points-to predicate persistent.

Exercise: finish the proof of the par_read_spec specification.

Both threads have the same postcondition, t_post.