Atomic accessors and atomic updates

Our theories for atomic accessors and updates have a lot in common (where AU ∈ {aacc,aupd}, M ∈ {fupd,wand}):

  AU_proper	[Proper] for [≡] (in [atomic_udpate.v])
  AU_update	"strong monotonicity" lemmas for changing all components

  AU_mask_{weaken,strengthen}	change masks
  AU_{apre,apost,ppost}_M	change individual components
  aacc_ppre_M

  fupd_aacc, AU_fupd		compatibility with fancy updates

  AU_{apre,apost,ppost}_frame_{l,r}	frame affine, persistent resources
  aacc_ppre_frame_{l,r}

  AU_{apre,apost,ppost}_mono	monotonicity
  aacc_ppost_mono
  AU_{,flip_}mono'		[Proper] for [⊢], [⊣]

We also provide a few proof mode instances for atomic accessors, and a few higher-level lemmas for atomic updates. These are described below. NOTE: any uses of Laterable and make_laterable are no longer necessary, thanks to later credits. Some of the sections below are kept as documentation. This is an introduction. If you want the theory, skip down. An atomic accessor

  Definition atomic_acc Eo Ei α P β Φ : PROP :=
    (|={Eo, Ei}=> ∃.. x, α x ∗	(** OPEN *)
          ((α x ={Ei, Eo}=∗ P) ∧	(** ABORT *)
           (∀.. y, β x y ={Ei, Eo}=∗ Φ x y))	(** COMMIT *)
    )%I.

is a fancy update (call it OPEN) enabling a callee to access a caller's atomic precondition α x (for some x) and then take one of two fancy updates:

• ABORT lets the callee give α x back to the caller in exchange for the public precondition P
• COMMIT lets the callee, if she can change α x to the atomic postcondition β x y (for some y), return β x y to the callee in exchange for the public postcondition Φ x y.

An atomic update is (roughly) an atomic accessor whose public precondition is the atomic update itself:

  atomic_update Eo Ei α β Φ ≈	(** [†] *)
    atomic_accessor Eo ei α (atomic_update Eo Ei α β Φ) β Φ

In fact, atomic updates satisfy the following recursive equation, which adds a make_laterable to †.

Laterable assertions

The point of baking make_laterable into the definition of atomic updates is to ensure that atomic updates are themselves Laterable. Because Laterable propositions are relevant to the introduction of atomic updates, we go into some detail. If you run Print Instances Laterable, you'll see that the class of Laterable propositions includes timeless propositions, ▷ P, make_laterable P, and is closed under separating conjuction:

  timeless_laterable       P : Timeless P → Laterable P
  later_laterable          P : Laterable (▷ P)
  sep_laterable          P Q : Laterable P → Laterable Q → Laterable (P ∗ Q)
  make_laterable_laterable P : Laterable (make_laterable P)

  (* so that *)
  aupd_laterable Eo Ei α β Φ : Laterable (atomic_update Eo Ei α β Φ)

A Laterable P satisfies

  laterable_fupd E : P ⊢ ∃ Q, ▷ Q ∗ □ (▷ Q ={E}=∗ P)

We can thus decompose a laterable P into ▷ Q for some Q as well as knowledge of a fancy update sending ▷ Q back to P (with any mask).

Except at zero

The preceding characterization laterable_fupd of Laterable assertions is just a lemma (proved below). Laterable P is defined in terms of the modality ◇ P, read "except at zero, P":

  laterable : P ⊢ ∃ Q, ▷ Q ∗ □ (▷ Q -∗ ◇ P)

The except at zero modality ◇ P usually remains hidden during verification efforts. In practice, you can read it as "P up to updates". In the model of Iris' base logic, ◇ P means precisely the same thing as P except at step-index zero (when all bets are off). Perhaps a more familiar place where the except at zero modality arises is in the definition of timelessness. A Timeless P satisfies

  timeless : ▷ P -∗ ◇ P

Because both concepts build on except at zero, we can easily relate Timeless and Laterable propositions to fancy updates (something the Iris proof mode usually takes care of). See the following lemmas timeless_fupd and laterable_fupd.

Atomic accessors

Workhorse for rewriting parts of an atomic accessor.

Easy corollaries of aacc_update

Atomic accessors and the outer mask Attribution: The following are inspired by Iris' interface for weakestpre.

We can frame knowledge into any component of an atomic accessor. We can't frame arbitrary resources, as in fupd_frame_r, but some of the rules could be strengthened to framing any Affine R (dropping the Persistent assumption). Consider framing R into a public postcondition Φ. We get both R and a conjunction of updates ABORT //\\ COMMIT and we have to prove ABORT //\\ COMMIT' (where COMMIT' mentions R). To handle the ABORT case, we need Affine R, but we don't care if it's persistent.

Monotonicity

We prove no Frame instances. Atomic preconditions and atomic postconditions seem incompatible with Frame. Framing in the public precondition seems useless, and an instance would slow down IPM framing. We want a Frame instance for public postconditions. PDS: Proving various Frame instances for public postconditions is easy. Writing them so they work, or debugging the typeclass resolution problems that arise is not (at least for me). We don't need an IsExecpt0 instance for atomic_acc, which lets the IPM strip laters from, e.g., timeless propositions when the goal is an atomic accessor. It's covered by the forwarding instance elim_modal_acc, the IsExcept0 instance for fancy updates, and the fact that the proof mode strips laters using ElimModal.

Using iMod to eliminate an atomic_acc when the goal can be transformed into a fancy update at Eo.

Let the proof mode specialization pattern [> H1 ... Hn] add fancy updates when the goal is an atomic accessor.

Atomic updates

Workhorse for rewriting parts of an atomic update.

Easy corollaries of aupd_update

The analog fupd_aupd to fupd_aacc is unsound because fancy updates aren't Laterable.

Monotonicity

Properties relevant to automation

Learn from an atomic precondition. (To use the bound variables x, pick P := ∃ x, P' x.)

PDS: This is intended to help with zeta390. Our aim is to change an atomic precondition based on knowledge gleaned from it. A common place where this can be used is to manifest pointers outside of atomic updates, e.g. [[ AU << this ., _foo |-> ... >> ... ]] becomes [[ valid_ptr (this ., _foo) ** AU << this ., _foo |-> ... >> ...]].