Higher-Order Ghost State
Ralf Jung

Robbert Krebbers

Lars Birkedal

Derek Dreyer

MPI-SWS, Germany
jung@mpi-sws.org

Aarhus University, Denmark
mail@robbertkrebbers.nl

Aarhus University, Denmark
birkedal@cs.au.dk

MPI-SWS, Germany
dreyer@mpi-sws.org

Abstract

were tied to a “conditional critical region” construct for synchronization. Since O’Hearn’s pioneering (and Gödel-award-winning)
paper, there has been an avalanche of follow-on work extending
CSL with more sophisticated mechanisms for modular reasoning,which allow shared state to be accessed at a finer granularity (e.g.,
atomic compare-and-swap instructions) and which support the verification of more “daring” (less clearly synchronized) concurrent
programs [40, 17, 16, 13, 18, 38, 35, 27, 11, 24].
In this paper, we focus on two of the most important extensions
to CSL—higher-order quantification and custom ghost state—andobserve that, although several logics support both of these extensions, none of them reap the full potential of their combination. In
particular, none of them provide general support for a feature wedub “higher-order ghost state”.
Higher-order quantification is the ability to quantify logicalassertions (universally and existentially) over other assertions and,in general, over arbitrary higher-order predicates. Several recent
extensions to CSL have incorporated higher-order quantification [36,35, 24, 21, 27], in part because it leads to more generic and reusable
specifications of concurrent data structures (see §4), and in part
because it is seemingly necessary for verifying some higher-orderconcurrency paradigms [35, 38, 31].
Ghost state is “logical state”, i.e., state that is essential tomaintain in the proof of a program but is not part of the physical state
manipulated by the program itself. It is a fixture of Hoare logics since
the work of Owicki and Gries [29] in the 1970s, and is useful fora variety of purposes: for encoding various kinds of “permissions”,
for recording information about the trace of the computation, fordescribing “protocols” on how threads may interact with sharedstate, and more. Traditionally, ghost state was manipulated byinstrumenting a program with updates to “ghost” (or “auxiliary”)
variables. Although this approach is convenient for integration into
automatic verification tools [10], it is unnecessarily low-level: there
is no reason logical state needs to be manipulated in exactly thesame way as physical state, and doing so makes it harder to reason
about updates to shared logical state in a modular fashion.
Recently, a number of researchers have argued that a more highlevel, general, and flexible way to represent ghost state is via partial
commutative monoids (PCMs). Intuitively, PCMs are a natural
fit for ghost state because they impose only the bare minimum
requirements on something that should be “ownable” in a separation
logic, while leaving lots of room for proof-specific customization.
Several newer extensions to CSL [24, 27, 12] thus give users the
freedom to define ghost state on a per-proof basis in terms of anarbitrary PCM of their choosing. Furthermore, the Iris logic [24] hasestablished that PCMs (together with simple invariants) are flexible
enough to derive several advanced reasoning mechanisms that werebuilt in as primitive in prior logics.
Unfortunately, a limitation arises when one uses PCMs to support
custom ghost state in the context of a logic with higher-order
quantification. Specifically, PCMs yield a model of ghost state thatis first-order. By this we mean that there is an inherent stratification:

The development of concurrent separation logic (CSL) has sparked along line of work on modular verification of sophisticated concurrent
programs. Two of the most important features supported by several
existing extensions to CSL are higher-order quantification andcustom ghost state. However, none of the logics that support bothof these features reap the full potential of their combination. In
particular, none of them provide general support for a feature wedub “higher-order ghost state”: the ability to store arbitrary higherorder separation-logic predicates in ghost variables.
In this paper, we propose higher-order ghost state as a interesting
and useful extension to CSL, which we formalize in the frameworkof Jung et al.’s recently developed Iris logic. To justify its soundness,
we develop a novel algebraic structure called CMRAs (“cameras”),
which can be thought of as “step-indexed partial commutative
monoids”. Finally, we show that Iris proofs utilizing higher-orderghost state can be effectively formalized in Coq, and discuss thechallenges we faced in formalizing them.
Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about
Programs
Keywords Separation logic, fine-grained concurrency, higherorder logic, compositional verification, interactive theorem proving

1.

Introduction

Over a decade ago, O’Hearn made a critical observation: separation
logic—developed to simplify the verification of sequential, heapmanipulating programs—can help simplify the verification of concurrent programs as well. In concurrent separation logic (CSL) [28],assertions denote not only facts about the state of the program, butalso ownership of a piece of that state. Concretely, this means that
if a thread t can assert ` 7→ v, then t knows not only that location` currently points to v, but also that it “owns” `, so no other thread
can read or write ` concurrently. Given this ownership assertion, t
can perform local (and essentially sequential) reasoning on accessesto `, completely ignoring concurrently operating threads.
Of course at some point threads have to communicate throughsome kind of shared state (such as a mutable heap or messagepassing channels). To reason modularly about such communication,
the original CSL used a simple form of resource invariants, which

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored.
Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, contact
the Owner/Author(s). Request permissions from permissions@acm.org or Publications Dept., ACM, Inc., fax +1 (212)869-0481.
ICFP ’16, September 18–22, 2016, Nara, Japan.
Copyright c 2016 held by owner/author(s). Publication rights licensed to ACM.
ACM 978-1-4503-4219-3/16/09. . . $15.00.
DOI: http://dx.doi.org/10.1145/2951913.2951943

1

W1

C1

M

C2

P1

P2

P1

P2

term e should be the witness for x, it will set γ to e.1 We will write
γ ,→ e to denote the knowledge that e has been stored in γ. Unlike
normal heap ownership assertions, γ ,→ e can be freely duplicated(i.e., γ ,→ e ⇔ γ ,→ e ∗ γ ,→ e) since γ can only be assigned once.
Furthermore, if we know γ ,→ e1 and γ ,→ e2 , then we also knowthat e1 = e2 because, once set, γ maps to a unique e.
We can now amend the assertions ∃x:T. Pi that are sent between
the threads to ∃x:T. (γ ,→ x ∗ Pi ), thus recording the fact thatthe witness x is precisely the term stored in γ. And the virtue of
this encoding is that now the existential can be split and rejoined:∃x:T. (γ ,→ x ∗ P ) ⇔ ∃x:T. (γ ,→ x ∗ P1 ) ∗ ∃x:T. (γ ,→ x ∗ P2 ).
The ⇒ direction relies on the fact that γ ,→ x is duplicable, and the⇐ direction relies on the fact that γ stores a unique witness.
There is just one catch: in all the existing logics that support
custom ghost state, the witness x stored in γ is restricted to be
first-order (i.e., an “object-level” term), hence restricting all theexistentials in the example to be first-order as well. If x instead is (orcontains) an assertion or higher-order predicate of the logic—as mayvery well be the case if we are working in a higher-order concurrent
separation logic [36, 35, 24, 27]—then the whole approach falls
over. Moreover, this problem is not limited to logics with custom
ghost state: to our knowledge, no existing logic is capable of proving
this example in the general case.
The good news is that restricting custom ghost state to first-orderis unnecessary. To overcome it, we will need the ability to store
terms of arbitrary higher type T (including assertions and higherorder predicates) in ghost variables like γ. In other words, we willneed higher-order ghost state.

W2

P1 ∗ P2
Figure 1. Structure of illustrative example
separation-logic assertions may talk about ownership of ghost state,
but the PCM structure of ghost state may not depend (recursively)on the language of logical assertions. At first glance, this may notseem like a big deal. Why would you want higher-order ghost
state—i.e., ghost state that is mutually recursive with the languageof assertions—anyway? What would that even mean?
To give some intuition for what higher-order ghost state is andwhat it can be good for, let us turn to a simple yet interestingillustrative example of some intuitively sensible reasoning that, as
far as we know, no existing logic can support.
1.1

Illustrative Example: Splitting and Joining Existentials

Imagine we have three threads—a main thread M and two worker
threads W1 and W2 —running concurrently, and that we have two
communication channels C1 and C2 connecting each worker to themain thread (see Figure 1). The idea of the example is that M isgoing to initialize some state, split up ownership of the state, send
the pieces to W1 and W2 via their respective channels, and aftersome computation, they are going to send their pieces back so that
M can join them together and reassert ownership of the whole state.
Formally: Let i range over {1, 2}. Let us suppose that M will
initialize its state so that it satisfies the assertion P , after which M
would like to split up ownership into two “disjoint” pieces P1 andP2 such that P = P1 ∗ P2 and Pi is the assertion to be transferredback and forth with the corresponding Wi over Ci . (The ∗ operator
here is the “separating conjunction” connective of separation logic,
which enforces the disjointness of P1 and P2 .) To make this work,
it is essential that M and Wi agree ahead of time on the fact that Ci
will be used to transfer ownership of Pi .
So far, so good. But now what happens if the assertion P
depends on some information (say, on some x of type T ) that is only
determined dynamically, right before M wants to transfer ownershipof P to the other, already running, threads. (For instance, x might
be some information that depends on the result of I/O or some othersource of nondeterminism.) In this case, we cannot associate thechannels Ci ahead of time with the assertions Pi since, at the point
the channels are created, the identity of x is not known. Instead,all we can really do is to existentially quantify over x—that is, set
up our channels so that instead of transferring Pi to Wi , M willtransfer ∃x:T. Pi , which is well-defined at the point the channels
are created.
In the forward direction (sending from M to Wi ), this works
because P = P1 ∗ P2 implies ∃x:T. P ⇒ ∃x:T. P1 ∗ ∃x:T. P2 .
But when the Wi try to return the state to M , we run into a problem:
although P1 ∗ P2 ⇒ P , it is not true that ∃x:T. P1 ∗ ∃x:T. P2 ⇒∃x:T. P because there is no way to deduce that the existential
witnesses for x in ∃x:T. P1 and ∃x:T. P2 are the same. This is allvery frustrating since we know that, at least when M split up its
original state, the witnesses were indeed the same.
Fortunately, there is another way: custom ghost state! Usingcustom ghost state, we can allocate a oneshot ghost variable γ up
front: initially, γ will be undefined, and once M determines what

1.2

Contributions

In this paper, we make the following contributions:• We propose and formalize higher-order ghost state as an inter-esting and useful extension of concurrent separation logic.
• We give a semantics to justify this extension in terms of a novel

algebraic structure we call a CMRA (“camera”), which can bethought of as a kind of “step-indexed” PCM.
• We demonstrate that separation-logic proofs utilizing higher-

order ghost state can be effectively formalized in Coq.
To be concrete, we will develop our notion of higher-order ghost
state as an extension to the Iris logic of Jung et al. [24]. Iris is ahigher-order variant of CSL that supports custom ghost state throughthe choice of an arbitrary user-supplied PCM. Over the course of
the paper, we will gradually extend Iris from its original version,
numbered 1.0, to the latest version, numbered 2.0, which can handle
higher-order ghost state in a generic manner.
In §2, we give an overview of the key features of Iris andshowcase their use on a simple representative example. Along theway, we introduce Iris 1.1, which makes some improvements to theoriginal Iris 1.0, in particular generalizing its model of resourcesfrom PCMs to resource algebras (RAs), which are more flexible.
In §3, we extend Iris with higher-order ghost state and put theextension on a sound formal footing. This involves revisiting thecategory-theoretic model of Iris 1.x and further generalizing its
model of resources to the aforementioned step-indexed CMRAs.
Furthermore, we discuss how the new semantic structure of ourhigher-order ghost state not only generalizes the original model of
Iris—in certain ways, it also simplifies it.
In §4, we return to our example from §1.1, flesh it out more
carefully, and show how to verify it in Iris 2.0. Our implementationof the example makes use of a “barrier” synchronization primitive
1 This is just one particular form of proof-specific ghost state that can be

encoded as a PCM—we will see in §2.1 how to encode it.

2(drawn from Dodds et al. [15]), whose own proof of correctness
independently involves an interesting use of higher-order ghost state.
In §5, we describe our Coq formalization of Iris 2.0, which
improves significantly on the original Coq formalization of Iris
1.0 in several respects. All proofs backing this paper have beenformalized in Coq [1].
Finally, in §6 and §7, we conclude with related and future work.

2.

mk_oneshot , λ . let x = ref(inl(0)) in{ tryset = λn. CAS(x, inl(0), inr(n)),
check = λ . let y = !x in λ .
match y, !x withinl( ) ,⇒ ()| inr(n), inl( ) ⇒ assert(false)| inr(n), inr(m) ⇒ assert(n = m)end }Iris Primer

Iris is a generic higher-order concurrent separation logic. Generichere refers to the fact that the logic is parameterized by the languageof program expressions that one wishes to reason about, so the same
logic can be used for a large variety of languages. For the purposeof this paper, we instantiate Iris with an ML-like language withhigher-order store, fork, and compare-and-swap (CAS):{True} mk_oneshot(){c. ∀v. {True} c.tryset(v) {w. w ∈ {true, false}} ∗{True} c.check() {f. {True} f () {True} }}e ::= x | rec f(x) = e | e1 (e2 ) | assert(e) | fork {e} || ref(e) | !e | e ← e | CAS(e, e1 , e2 ) | . . .

Figure 2. Example code and specification(We omit the usual operations on pairs and sums.)
The logic includes the usual connectives and rules of higherorder separation assertion logic, some of which are shown in thegrammar below.2 In this section, we will give a brief tour of Iris, anddemonstrate the purpose of these most important logical connectives.

logic, the specification for mk_oneshot actually permits the client
to call tryset and check, as well as the f returned by check,concurrently from multiple threads and in any combination.
High-level proof structure. To perform this proof, we need tosomehow encode the fact that we are only performing a oneshot
update to x. To this end, we will allocate a ghost location γ which
mirrors the current state of x. This may at first sound rather pointless;why should we record a value in the ghost state that is exactly thesame as the value in a particular physical location?
The reason we do this is so that we can control what kindof sharing is possible on the location. For a physical location `,the assertion ` 7→ v expresses full ownership of ` (and hence theabsence of any sharing of it). In contrast, Iris permits us to choose
whatever kind of structure and ownership we want for our ghost
location γ; in particular, we can define it in such a way that, although
the contents of γ mirror the contents of x, we can freely shareownership of γ once it has been initialized (by a call to tryset).
This in turn will allow the closure returned by check to own a pieceof γ witnessing its value after initialization. We will then have aninvariant tying the value of γ to the value of x, so we know which
value that closure is going to see when it reads from x, and we knowthat that value is going to match y.
With this high-level proof structure in mind, we now explain
how exactly ownership and sharing of ghost state can be controlled.

P, Q, R ::= True | False | P ∧ Q | P ∨ Q | P ⇒ Q| ∀x. P | ∃x. P | P ∗ Q | ` 7→ v | .P | t = u
| P

ι

| a

γ

| V(a) | {P } e {v. Q} | P V Q | . . .

What makes Iris a higher-order separation logic is that universal
and existential quantifiers can range over any type, including that ofassertions and (higher-order) predicates. Furthermore, notice that
Hoare triples {P } e {v. Q} are part of the assertion logic insteadof being a separate entity. As a consequence, triples can be used in
the same way as any logical assertion, and in particular, they can benested to account for specifications of higher-order functions.
We will demonstrate this, and some other core features of Iris,by verifying the safety of the simple higher-order-program given in
Figure 2. This is of course a rather contrived example, but it serves
to showcase the core features of Iris.
The function mk_oneshot allocates a oneshot location at x andreturns a record with two functions. (Formally, records are syntactic
sugar for pairs.) The function tryset(n) tries to set the location ton, which will fail if the location has already been set. We use CAS toensure correctness of the check even if two threads concurrently try
to set the location. The function check() records the current stateof the location and then returns a closure which, if the location has
already been initialized, checks that it does not change.
The specification looks a little funny with most pre- and postconditions being True. The reason for this is that all we are aiming
to show here is that the code is safe, i.e., that the assertions3 succeed:
the branch with assert(false) will never get executed, and in the
final branch, n will always equal m. In Iris, Hoare triples imply
safety, so we do not need to impose any further conditions.
As is common for Hoare triples about functional programs, thepostconditions have a binder to refer to the return value. We will
omit the binder if the result is always unit.
We use nested Hoare triples to express that mk_oneshot returns
closures: Since Hoare triples are just assertions, we can put theminto the postcondition of mk_oneshot to describe what the client
can assume about c. Furthermore, since Iris is a concurrent program

2.1

Ghost State in Iris: Resource Algebras

The key properties of ownership of ghost state in concurrent separation logics are:• Ownership of different threads can be composed.
• Composition of ownership is associative and commutative,

mirroring the associative and commutative semantics of parallel
composition.
• Combinations of ownership that do not make sense are ruled out,e.g., multiple threads claiming to have exclusive ownership of
the same piece of ghost state.
For these reasons, partial commutative monoids (PCMs) havebecome a canonical structure for representing ghost state in separation logics. Iris 1.0 was parameterized by an arbitrary PCM, so thatthe structure of the ghost state was entirely up to the user.
In Iris 1.1, we are deviating slightly from this, using our own
notion of a resource algebra (RA), whose definition is in Figure 3.
As we will see in our example, the additional flexibility afforded by
RAs results in additional logical expressiveness.

2 Actually, many of the connectives given in this grammar are defined as

derived forms in Iris, and this flexibility is an important aspect of the logic.
For more details on this, see [24, 1].
3 Our semantics here is that assert(e) gets stuck if e evaluates to false.

3

A resource algebra (RA) is a tuple(M, V ⊆ M, |−| : M → M ? , (·) : M × M → M ) satisfying:∀a, b, c. (a · b) · c = a · (b · c)

GHOST- OPa·b∀a. |a| ∈ M ⇒ |a| · a = a(RA - CORE - ID)∀a. |a| ∈ M ⇒ ||a|| = |a|(RA - CORE - IDEM)∀a, b. (a · b) ∈ V ⇒ a ∈ V
M , M ] {ε}γ∗bGHOST- ALLOC(RA - COMM)

GHOST- VALID

γ

a

γ

⇒ a

GHOST- UPDATE

V(a)

a

True V ∃γ. aγγ∗ V(a)a(RA - VALID - OP)?

?

|a| = aV bγγ

persistent( a )INV(side conditions on ι and I omitted){I ∗ P } e {v. I ∗ Q}
atomic(e)?

a ·ε,ε·a ,aa 4 b , ∃c ∈ M. b = a · cγ

PERSISTENT- GHOSTbb , ∀a?f ∈ M ? . a · a?f ∈ V ⇒ b · a?f ∈ V

where a∀a, b. |a| ∈ M ∧ a 4 b ⇒ |b| ∈ M ∧ |a| 4 |b|(RA - CORE - MONO)
where

⇔ a

(RA - ASSOC)∀a, b. a · b = b · a?

γINV- ALLOC(RA - INCL)

IV I

ι

ι

I ` {P } e {v. Q}

CSQ

Figure 3. Resource algebras

P V P0{P 0 } e {v. Q0 }∀v. Q0 V Q{P } e {v. Q}

There are two key differences between RAs and PCMs:
1. The composition operation on RAs is total (as opposed tothe partial composition operation of a PCM), but there is a
specific subset V of valid elements that is compatible with thecomposition operation (RA - VALID - OP).
We will see in §3.2 that this take on partiality is necessary whendefining the structure of higher-order ghost state.

PERSISTENT- DUPPERSISTENT- HOARE

persistent(P )P ⇔P ∗P{P ∗ Q} e {v. R}

Q ` {P } e {v. R}
persistent(Q)Figure 4. Some Iris 1.1 proof rules

2. Instead of a single unit that is an identity to every element,
we allow for an arbitrary number of units, via a function |−|assigning to an element a its (duplicable) core |a|, as demanded
by RA - CORE - ID. We further demand that |−| is idempotent (RA CORE - IDEM ) and monotone ( RA - CORE - MONO) with respect to theextension order, defined similarly to that for PCMs (RA - INCL).
Notice that the domain of the core is M ? , a set that adds adummy element ε to M . Thus, the core can be partial: not allelements need to have a unit. We use the metavariable a? toindicate elements of M ? . We also lift the composition (·) to M ? .
As we will see in §2.5, partial cores help us to build interesting
composite RAs from smaller primitives.
Notice also that the core of an RA is a strict generalization of
the unit that any PCM must provide, since |−| can always be
picked as a constant function.

As a result of this definition, if we own pending, we knowthat no other thread can own anything about this location, since
the composition with that other piece of ownership would beinvalid (i.e., ⊥). Furthermore, if we own shot(n), we know thatthe only ownership any other thread can have is also shot(n), since
everything else is incompatible with our own ownership. However,since shot(n)·shot(n) = shot(n), we can also duplicate ownershipof the location as much as we want, once it has been set to some n.
This gives rise to the sharing that we need.
In defining the duplicable core, we make sure that we keep asmuch ownership as possible while satisfying RA - CORE - ID:|pending| , ε|shot(n)| , shot(n)|⊥| , ⊥

Note that, since ownership of pending is exclusive, it has nosuitable unit element, so we assign it the “dummy core” ε. It is
now straightforward to verify that the RA for our example satisfies
the RA axioms.

A resource algebra for our example. We will now define the RA
that can be used to verify our example, which we call the oneshot RA.
This RA appropriately mirrors the state of the physical location x.
The carrier is defined using a datatype-like notation as follows:

Proof rules for ghost state. Resource algebras are embedded intoγ
the logic using the assertion a , which asserts ownership of a piece
a of the ghost location γ.4 The proof rule GHOST- ALLOC in Figure 4
can be used to allocate a new ghost location, with an arbitrary but
valid initial state a. The assertion V(a) reflects validity of a into
the logic, i.e., it corresponds to a ∈ V on the meta-level. The V in
GHOST- ALLOC is a view shift, also known as a ghost move: P V Q
says that, starting in a (ghost and physical) state satisfying P , wecan do updates to the ghost state only and arrive in a state satisfying
Q. The rule of consequence (CSQ) says that we can apply view shifts
in the pre- and postconditions of Hoare triples.
The rule GHOST- OP says that ghost state can be separated (in thesense of separation logic) following the composition operation (·)
defined for the RA. And GHOST- VALID encodes the fact that only
valid RA elements can ever be owned.
Finally, we need a way to update ghost locations. Updates toghost locations are called frame-preserving updates and can be

M , pending | shot(n : Z) | ⊥V , {pending} ∪ {shot(n) | n ∈ Z}
The two important states of the ghost location are: pending, torepresent the fact that the single update has not yet happened, andshot(n), saying that the location has been set to n. We need an
additional element ⊥ to account for partiality.
The most interesting piece of data of an RA is of course its
composition: What happens when ownership of two threads is
combined? For our example, we are most interested in the behaviorof pending and shot:
pending · pending , ⊥pending · shot(n) , shot(n) · pending , ⊥shot(n) if n = mshot(n) · shot(m) ,⊥otherwise

4 The notation γ ,→ e used in §1.1 is defined in terms of the more generalγa4(see §4.2).

Since x is initialized with inl(0), the invariant I initially holds.

performed using the rule GHOST- UPDATE. We can perform a framepreserving update ab on a ghost location γ, if the update ensuresthat no matter what assumptions the rest of the program is making
about the state of γ, if these assumptions were compatible with a,they should also be compatible with b. Or in other words, we haveto make sure that the assumptions the rest of the program is making
about γ will not be invalidated by the update.
We only need one frame-preserving update for our example:
pendingshot(n)Proof of tryset. How exactly can invariants be used? This is
described by INV, which allows us to open the invariant for theverification of e. That is, we can assume that the invariant holds inthe precondition, and then we have to reestablish that it holds inthe postcondition. Crucially, we require that e is physically atomic,
meaning that it is guaranteed to evaluate to a value in a single step ofcomputation. This side condition is essential for soundness: within
the verification of e the invariant I might be temporarily broken, but
by restricting e’s execution to a single instruction we ensure that noother thread can observe that I has been broken. In our language,
reading from memory (!e), assigning to memory (e1 ← e2 ), andCAS are all physically atomic operations.
In the case of tryset, we have to open the invariant to justify
safety of the CAS. The invariant always provides x 7→ , so safety ofthe memory operation is justified. In case the CAS fails, no change
is made to x, so reestablishing the invariant is immediate.
The case in which the CAS succeeds is more subtle. Here, weknow that x originally had value inl(0), so we obtain the invariant
in its left disjunct. Thus, after the CAS, we have the following:(ONESHOT- SHOOT)

This property follows from the fact that no frames are compatible
with pending. That is, by the definition of (·), we know that
pending · a?f ∈ V can only hold for the dummy frame a?f = ε.
2.2

Invariants

Now that we have set up the structure of our ghost location γ, we
have to connect the state of γ to x. This is done using an invariant.
ι
In Iris, invariants are provided in the form of the assertion P ,which asserts that P is maintained as an invariant on the global(ghost and physical) state. In order to identify invariants, every
invariant has a name ι. We need to do some bookkeeping with thesenames to avoid reentrancy, which in the case of invariants means
avoiding “opening” the same invariant twice in a nested fashion.
However, we omit the bookkeeping for this paper, as it is orthogonal
to our focus; see the original Iris paper for details [24].
ιNotice that P is just another kind of assertion, and can be usedanywhere that normal assertions can be used—including the preand postconditions of Hoare triples, and invariants themselves. The
latter property is sometimes referred to as impredicativity.
Invariants are created using the INV- ALLOC rule (Figure 4):
Whenever an assertion P has been established, it can be turned
into an invariant. Allocating an invariant is another example of aview shift, since only ghost state is changed to record that thisinvariant will henceforth be maintained.
2.3

x 7→ inr(n) ∗ pending

How can we reestablish the invariant I after this CAS? Clearly,
we must pick the right disjunct, since x 7→ inr(n). Hence we haveto update the ghost state to match the physical state. To this end,
we apply GHOST- UPDATE with the frame-preserving update ONESHOTSHOOT , which allows us to update the ghost location to shot(n) if
we own pending. We then have I again and can finish the proof.
Notice that we could not complete the proof if tryset would
ever change x again, since ONESHOT- SHOOT can only ever be used
once on a particular ghost location. We have to be in the pending
state if we want to pick the n in shot(n). This is exactly what wewould expect, since check indeed relies on x not being modified
once it has been set to inr(n).

Persistent Assertions

Proof of check. What remains is to prove correctness of check.
We open our invariant I to justify safety of !x, which is immediate
since I always provides x 7→ , but we will not immediately close I
again. Instead, we will have to acquire some piece of ghost state thatshows that if we read an inr(n), then x will not change its value.
At this point in the proof, we have the following assertion:

Before we come to the actual proof of Figure 2, we have to talk about
the notion of a persistent assertion. These are assertions that, once established, will remain valid for the rest of the verification. Examples
ιof persistent assertions are invariants P , validity V(a), equalityt = u, Hoare triples {P } e {v. Q} and view shifts P V Q. Persistent assertions can be freely duplicated (PERSISTENT- DUP) and can be
moved in and out of the precondition of Hoare triples (PERSISTENTHOARE ). This differentiates them from ephemeral assertions likeγ
` 7→ v and a , which could be invalidated in the future by actionsof the program or the proof, and for which the above properties thus
do not hold.
Another example of a persistent assertion is ghost ownership ofγa core: |a| is persistent (PERSISTENT- GHOST). This possibility of
having persistent ghost ownership is a novel concept of Iris 1.1 thatcannot be expressed in a PCM-based logic. In the proof of check,we will see this concept in action.
A closely related concept is the notion of duplicable assertions,
i.e., assertions P for which one has P ⇔ P ∗ P . This is a strictly
weaker notion, however: not all duplicable assertions are persistent.
q
For example, ∃q. ` 7−
→ v is duplicable (which follows from halving
the fractional permission q), but is not persistent.
2.4γ

x 7→ y ∗ ((y = inl(0) ∗ pending ) ∨γ(∃n. y = inr(n) ∗ shot(n) ))We use the identity shot(n) = shot(n) · shot(n) with GHOST- OP
to show that this logically implies:γ

x 7→ y ∗ ((y = inl(0) ∗ pending ) ∨(∃n. y = inr(n) ∗ shot(n)γγ∗ shot(n) ))which in turn implies:γ

I ∗ (y = inl(0) ∨ (∃n. y = inr(n) ∗ shot(n) ))
|
{z
}
P

We can then reestablish the invariant, but we keep P , the information
we gathered about y. The plan is to use this in the proof of the closurethat we return to justify that the assertion will hold.
To do so, we have to show that P is persistent. Technically,
this is mandated by PERSISTENT- HOARE; intuitively, it is needed
because the client could call the closure returned by check in anarbitrary future state of the program, and we have to make surethat it is always safe to do so. The reason P is persistent is that,γ
thanks to shot(n) = |shot(n)| and PERSISTENT- GHOST, shot(n)is persistent. This matches the intuition that, once we observe that x
has been set, we can then forever assume it will not change again.

Proof of the Example

Proof of mk_oneshot. In order to verify mk_oneshot, we will
first allocate a new ghost location γ with the structure of the oneshot
RA defined above, picking the initial state pending. Then, we will
establish and allocate the following invariant:γγγI , (x 7→ inl(0) ∗ pending ) ∨ (∃n. x 7→ inr(n) ∗ shot(n) )5

To finish this proof, let us look at the closure returned by checkin more detail: Again, we will open our invariant to justify safety of!x. Our assertion then is I ∗ P , which unfolds to:γ

a·b ⇔ a ∗ bb

Figure 5. Primitive rules for ghost stateγ(y = inl(0) ∨ (∃n. y = inr(n) ∗ shot(n) ))In order to proceed, we do 4-way case distinction over the valuesof x and y. Our goal is to prove that the assertions do not fail, so wehave to show the following:

Agreement. Given a set X, the task of the agreement RA AG(X)
is to make sure multiple parties can agree upon which value x ∈ X
has been picked. We define AG by essentially dropping pending
from the oneshot RA and generalizing the carrier:

1. Goal: It cannot be the case that y = inr(n) and x 7→ inl( ).
γγIn this case, we would have pending · shot(n) and hence ⊥ ,which according to GHOST- VALID is a contradiction.

AG(X) , ag(x : X) | ⊥V , {ag(x) | x ∈ X}ag(x) if x = yag(x) · ag(y) ,⊥otherwise

2. Goal: In the case that y = inr(n) and x 7→ inr(m), weγ
have shot(n) · shot(m) . The following lemma shows that theassertion cannot fail:γ⇒n=m(ONESHOT- AGREE)|ag(x)| , ag(x)The lemma holds by GHOST- VALID, which yields V(shot(n) ·shot(m)), implying shot(n) · shot(m) 6= ⊥, and thus n = m.
2.5

a

a V b

γ

((x 7→ inl(0) ∗ pending ) ∨ (∃m. x 7→ inr(m) ∗ shot(m) )) ∗shot(n) · shot(m)a ⇒ V(a)Oneshot. We can now define the general idea of the oneshot RA
as O NE S HOT(M ) , E X(1) +⊥ M , and recover the RA for theexample as O NE S HOT(AG(Z)). Notice that the decomposition of
O NE S HOT into a sum relies crucially on the fact that one summand,
namely E X(1), has a partial core. The following generalization of
ONESHOT- SHOOT can be shown in general for O NE S HOT :RA Constructions

One of the key features of Iris is that it leaves the structure of ghost
state entirely up to the user of the logic, so if there is the need forsome special-purpose RA, the user has the freedom to directly use
it. However, it turns out that many frequently needed RAs can beconstructed by composing smaller, reusable pieces—so while wehave the entire space of RAs available when needed, we do not haveto construct custom RAs for every new proof.
For example, looking at the oneshot RA from §2.1, it really does
three things:

inl(ex())

inr(a)

This update relies on the fact that ex() has no frame. If there was aunit |ex()| for ex(), then inl(|ex()|) would be a frame compatible
with inl(ex()), and the frame-preserving update would not hold.
Obtaining usable frame-preserving updates for sums is one of our
key motivations for making the core a partial function.

1. It separates the allocation of an element of the RA from thedecision about what value to store there (ONESHOT- SHOOT).

Joining existentials. The general construction O NE S HOT(−)
comes in handy, because it is exactly the RA that we need forthe challenge of splitting and joining existentials as described in§1.1. Remember that there, too, we want to allocate ghost state
before it is known what will be stored there.
Now, it may seem that we are already equipped to solve thechallenge posed in §1.1, but that is not the case. To prove thatexample, we need the ghost state to be M , O NE S HOT(AG(T )),where T may depend on iProp (the type of Iris assertions). However,the structure of the ghost state is a parameter of Iris, so iProp is
actually defined in terms of M —which means we cannot define M
in terms of iProp. We have to do some interesting work in the modelof Iris to resolve this cycle, as we will describe in §3.

2. While the oneshot location is uninitialized, ownership is exclusive, i.e., at most one thread can own the location.
3. Once the value has been decided on, it makes sure everybody
agrees on that value (ONESHOT- AGREE).
We can thus decompose the oneshot RA into the sum, exclusive
and agreement RAs as described below. (In the definitions of all theRAs, the omitted cases of the composition and core are all ⊥.)Sum. The sum RA M1 +⊥ M2 for any RAs M1 and M2 is:M1 +⊥ M2 , inl(a1 : M1 ) | inr(a2 : M2 ) | ⊥V , inl(a1 ) a1 ∈ V 0 ∪ inr(a2 ) a2 ∈ V 00

2.6

inl(a1 ) · inl(b1 ) , inl(a1 · b1 )εif |a1 | = ε|inl(a1 )| ,inl(|a |) otherwise
1

Derived Forms and the Global Ghost StateIn Iris, there is a strong emphasis on only providing a minimal core
logic, and deriving as much as possible within the logic rather thanbaking it in as a primitive [24]. For example, both Hoare triples andassertions of the form l 7→ v are actually derived forms. This has
the advantage that the model can be kept simpler, since it only has
to justify soundness of a minimal core logic.
γ
In this section we discuss the encoding of the assertion a forghost ownership, which is not a baked-in notion. Instead, the idea of
having a heap of ghost variables, which can be individually allocatedand updated, is derived within the logic. Although this construction
did not fundamentally change since Iris 1.0 [24], it is important forunderstanding the model construction in §3.
As a primitive, Iris provides the construct a , which asserts
ownership of a piece a of the entire global ghost state, rather thanownership of a piece of an individual ghost variable. The structureof the global ghost state is a single RA picked by the user, and therules governing global ghost state are given in Figure 5.

The composition and core for inr are defined symmetrically. Above,
V 0 refers to the validity of M1 , and V 00 to the validity of M2 .
Exclusive. Given a set X, the task of the exclusive RA E X(X) is
to make sure that one party exclusively owns a value x ∈ X. We
define E X by essentially dropping shot from the oneshot RA, andgeneralizing the carrier:
E X(X) , ex(x : X) | ⊥V , {ex(x) | x ∈ X}
|ex(x)| , εComposition is always ⊥ to ensure that ownership is exclusive.

6

n

Objects: tuples (T, (= ⊆ T × T )n∈N ) satisfying:n∀n. (=) is an equivalence relationnm∀n, m. n ≥ m ⇒ (=) ⊆ (=)
n∀x, y. x = y ⇔ (∀n. x = y)(Completeness axiom omitted)

Step-indexed Assertions:(COFE - EQUIV)SProp , {X ∈ ℘(N) | ∀n ≥ m. n ∈ X ⇒ m ∈ X}

(COFE - MONO)

X = Y , ∀m ≤ n. m ∈ X ⇔ m ∈ YnDiscrete:(COFE - LIMIT)∆X , Xnx=y,x=yne→ U satisfying:
Arrows: non-expansive functions f : T −nn∀x, y. x = y ⇒ f (x) = f (y)Later:(COFE - NONEXP)n

IT , {next(x) | x ∈ T }n−1

next(x) = next(y) , n = 0 ∨ x = y

Figure 6. Objects and arrows of the category COFE of COFEs

Figure 7. The COFEs used as part of the Iris model

In practice, however, the end-user typically wants to use multiple
ghost variables of multiple RAs, in particular when combining
different proofs. We apply a general construction facilitating this:We assume a family of RAs (Mi )i∈I for some index set I, andthen define the RA M of the global ghost state to be the indexed(dependent) product over “heaps of Mi ” as follows:
Y fin
M,
N−
* Mi

the exclusive RA structure defined in §2.5, so that Res becomes theRA of resources (logical and physical) that can be owned. Prop is
the domain of meta-level propositions (e.g., Coq’s Prop).
monRes −−→ Prop is a predicate over resources, the usual modelof assertions in separation logic. Iris is an intuitionistic separation
logic, which gives rise to the monotonicity requirement—owning
more resources makes more assertions true.5 We can easily model
ghost ownership a in this domain of resource predicates.
The World keeps track of the invariants that have been created.
We index the resource predicate over “possible worlds”. The invariι
ant assertion P is thus modeled as asserting the existence of aninvariant named ι in the current world. Worlds are ordered by theextension order, i.e., allocating new invariants “grows” the world.
It is crucial to demand monotonicity of assertions with respect tothat order, so that assertions cannot be invalidated by new invariants
being added.
Notice that the above equations are circular: World depends on
iProp, which depends contravariantly on World.

i∈I

In this construction, we use the natural point-wise lifting of the
RA operations from each Mi through the finite maps and products
all the way to M , so that M is an RA itself.
This allows us (a) to use all the Mi in our proofs, and (b) to treat
ghost state as a heap, where we can allocate new instances of anyof the Mi at any time. We define local ghost ownership of a single
location as:[γ 7→ a] if i = jγ
a : Mi , λj.
∅otherwiseγ

In other words, a : Mi asserts ownership of the singleton heap
[γ 7→ a] at position i in the product. We typically leave the concreteγ
Mi implicit and write just a . The rules given in Figure 4 can thenbe derived from those shown in Figure 5.

3.

Step-indexing to the rescue. To solve the circularity in the proposed definition of iProp, we use step-indexing [3] to stratify therecursive domain equation. Following Birkedal et al. [7], we do thisin an abstract way by working in the category COFE of Complete
Ordered Family of Equivalences (COFEs), as defined in Figure 6.
The key intuition behind COFEs is that elements x and y arenn-equivalent, written x = y, if they are equivalent for n stepsof computation, i.e., if they cannot be distinguished by a programnrunning for no more than n steps. It follows that, as n increases, =becomes more and more refined (COFE - MONO). In the limit, it agrees
with plain equality (COFE - LIMIT). In order to solve the recursive
domain equation it is essential that COFEs are complete, i.e., thatany chain has a limit. See [7, 1] for more details.
ne
An arrow f : T −→ U between two COFEs is a non-expansivenfunction. Such functions preserve the structure defined by (=) (COFE NONEXP). In other words, applying such a function to some data will
not suddenly introduce differences between seemingly equal data.
Elements that cannot be distinguished by programs within n steps
remain indistinguishable after applying f .
The COFEs that are essential to the Iris model are defined in
Figure 7. The COFE of step-indexed assertions SProp represents
assertions that are true for some number of steps, or forever. (SProp
corresponds to the set of ordinals up to ω.) The discrete COFE
∆X turns any set X into a COFE by assigning the degenerate
step-indexed equivalence. Finally, the later COFE IT moves the
step-indexed equivalence of a COFE T up by one, thus making
everything “one level more equal” than in T .

A Model for Higher-Order Ghost StateIn this section, we explain how to solve the problem outlined at theend of §2.5 by changing the semantic model of Iris assertions toaccount for higher-order ghost state. We start by giving a modelfor Iris 1.1. This is essentially a review of how the model of Iris
1.0 was built; the differences are minuscule. Next we show why
the agreement construction AG as defined in §2.5 does not scale tohigher-order ghost state, and give a refined version that does scale.
Finally, we show how to evolve the model to Iris 2.0 in order tosolve the challenge posed in §1.1 in a generic and foundational way.
3.1

The Iris Model

Proving soundness of Iris involves giving a model to all its primitive
assertions in an appropriate semantic domain, and then verifying
correctness of every primitive rule with respect to that model.
The main difficulty here is to come up with a semantic domainthat is sufficient to model Iris’s assertions. This domain, which wecall iProp, should satisfy (roughly) the following equations:
mon

mon

iProp = World −−→ Res −−→ Prop

(IRIS -1.0)

finwhere World , N −* iPropRes , M × E X(PhyState)

5 In other words, the function has to be monotone with respect to the

Let us look at the individual pieces: M is the RA of ghost stateas picked by the user. Physical states PhyState are equipped withextension order 4 (defined in Figure 3) and implication on Prop.

7

A CMRA is a tuple (M : COFE, (Vn ⊆ M )n∈N ,nene|−| : M −→ M ? , (·) : M × M −→ M ) satisfying:

It turns out that, within the category COFE, the following
recursive domain equation can be solved up to isomorphism using
America and Rutten’s theorem [2]:
mon

mon

iProp ≈ World −−→ ∆Res −−→ SPropn∀n, a, b. a = b ∧ a ∈ Vn ⇒ b ∈ Vn

(IRIS -1.1)

finwhere World , N −* IiProp
Res , M × E X(PhyState)

3.2∀n, m. n ≥ m ⇒ Vn ⊆ Vm

(CMRA - VALID - MONO)∀a, b, c. (a · b) · c = a · (b · c)

(CMRA - ASSOC)∀a, b. a · b = b · a

An Iris assertion is hence indexed by a world w ∈ World, by aresource r ∈ Res, and by a step-index n ∈ N.
Compared to IRIS -1.0, the key differences are the use of SProp
instead of Prop, and the I in front of the recursive occurrence ofiProp. The I serves as a guard that introduces a stratification step.
This is needed to ensure that the recursive domain equation reaches
a fixed point. It is also the reason that the proof rule INV needs a sidecondition about I: Due to World actually containing IiProp rather
than iProp, INV only holds for assertions that do not depend on theγ
step-index, such as ghost ownership a . We call such assertions
timeless. There is a stronger version of INV [1] that works for any
assertion, but it needs more care because we have to deal with thefact that I only holds at the next step-index (which is written as .I).
Since the equation IRIS -1.1 only holds up to isomorphism, we
have to be careful not to perform operations that are not preservedby the isomorphism. Basically, we have to make sure that we stayinside the category COFE, which in particular means that every
function must be non-expansive.
However, the end user of Iris 1.1 does not have to bother muchabout this: Since we use the discrete COFE ∆ for Res, all functions
on Res—and in particular the RA operations for composition andcore—are trivially non-expansive.

(CMRA - CORE - ID)∀a. |a| ∈ M ⇒ ||a|| = |a|(CMRA - CORE - IDEM)∀n, a, b. (a · b) ∈ Vn ⇒ a ∈ Vn

(CMRA - VALID - OP)n∀n, a, b1 , b2 . a ∈ Vn ∧ a = b1 · b2 ⇒nn

∃c1 , c2 . a = c1 · c2 ∧ c1 = b1 ∧ c2 = b2
(CMRA - EXTEND)
where
a 4 b , ∃c. b = a · c(CMRA - INCL)

Figure 8. CMRA operations and axioms
Elements a ∈ AG(T ) now consist of an a.x ∈ T (the actual
data represented by a) and a set a.V defining how valid a is. The
set contains those n such that a is valid for n steps of computation.
Finally, the quotient by ∼ ensures that elements of AG(T ) are only
equated for the number of steps for which they are valid.
In this construction, validity of a is generalized from a “plain”
assertion a ∈ V to a step-indexed assertion a ∈ Vn . Recall thatvalidity in RAs corresponds to partiality in PCMs—we obtain anotion of two elements being composable or not. With step-indexed
validity, we have a notion of elements being n-composable. You canthink of this as “step-indexed partiality”.
The step-indexed equality on AG(T ) propagates the one on T .
nThis makes composition a non-expansive operation: For a1 = a2 , itn
is easy to see that a1 · b = a2 · b (and likewise if b changes).
In order to explain how we use AG, we first define an injection
ag : T → AG(T ) as follows:

Higher-Order Agreementag(x) , (x, N)

n6=(CMRA - COMM)∀a. |a| ∈ M ⇒ |a| · a = a∀a, b. |a| ∈ M ∧ a 4 b ⇒ |b| ∈ M ∧ |a| 4 |b|(CMRA - CORE - MONO)

With the framework of the model—in particular the category
COFE—set up, let us now look again at the agreement RA defined in §2.5. Remember that ultimately we would like to obtain
AG(T ) for some T that may depend on iProp.
Ignoring the circularity that came up in §2.5, there is anotherproblem with the definition of AG in that section: when the AG(T )construction is generalized to range over a non-discrete COFE T ,such as iProp, the composition operator (·) is not non-expansive.
That is, given P and Q that are equal up to n steps, but not equalnfor all steps, i.e., P = Q for some n while P 6= Q, we have:ag(P ) · ag(Q) = ⊥(CMRA - VALID - NE)ag(P ) = ag(P ) · ag(P )Now imagine we start with two elements x, y ∈ T . You can see thatnag(x) · ag(y) is n-valid if and only if x = y—in other words, thecomposition of two elements is as valid as the elements are equal.
This gives rise to the following property:n

For (·) to be non-expansive, we should have ag(P ) · ag(P ) =ag(P ) · ag(Q), which is clearly not the case. This is not entirely
surprising: agreement composition was defined in terms of equality
rather than step-indexed equality.
In order to make sense of the idea of agreement over COFEs,
we have to drop absolute terms like the elements being (exactly)
equal and composition being (completely) defined, and instead use
step-indexed versions of those terms. This is achieved by keeping
track of how valid an RA element is, which we can then relate to
how equal the operands of the composition were. So, we re-defineAG(T ) for any COFE T :V(ag(x) · ag(y)) ⇒ x = y(AG - VALID)

Note that this is a statement in Iris, not in the meta-logic. Bothvalidity and equality are actually step-indexed assertions, namely,n
Vn and (=). This implication has to be shown once and for all whendefining AG; it can then be used in Iris proofs.
There is one last technical step that we have to take: AG(T ) as
defined in this section does not satisfy the completeness axiom of
COFEs (see Figure 6). To turn AG(T ) into an actual COFE, weperform a Cauchy completeness construction (by considering chainsof elements). This technical step is detailed in the appendix [1] andfully formalized in Coq, as are all the constructions in this paper.

AG(T ) , {(x, V ) ∈ T × SProp} / ∼nwhere a ∼ b , a.V = b.V ∧ ∀n ∈ a.V . a.x = b.xna = b , (∀m ≤ n. m ∈ a.V ⇔ m ∈ b.V ) ∧m(∀m ≤ n. m ∈ a.V ⇒ a.x = b.x)

3.3

Vn , {a ∈ AG(T ) | n ∈ a.V }nona · b , a.x, n n ∈ a.V ∧ n ∈ b.V ∧ a = b

CMRAs

The AG(T ) construction as defined in the previous section is nolonger just an RA—we had to define Vn , and we had to prove nonexpansiveness of the operations. In this section we introduce the8F (_) = M for any CMRA or RA M . In this case, there are nofurther proof obligations; F trivially satisfies all the functor laws.
So, to sum this up: Iris 2.0 is parameterized over a user-selected
locally contractive bifunctor F . Within the logic, the user then has
F (iProp) available for the ghost state, which gives rise to arbitrary
higher-order ghost state in a canonical and principled way.

algebraic structure of CMRAs (“cameras”) to abstractly characterizesuch “step-indexed RAs”. You can find its definition in Figure 8.
The differences from RAs are as follows:• The carrier needs to be a COFE, and the core and composition

operations have to be non-expansive.
• The set of valid elements Vn is step-indexed. The rule CMRA VALID - OP expresses that we need decomposition to preserve
validity at every step-index. The rule CMRA - VALID - NE demands

Unifying worlds and resources. There is one final change inthe model of Iris 2.0, compared to IRIS -1.1. Looking at IRIS - PRE 2.0, we see that World and Res are recursively referring to iProp.
By equipping worlds with an appropriate CMRA structure, we
can merge worlds into the resources, which means we can makeresources comprise physical state, ghost state, and worlds.
What we need for this is a CMRA structure on World—but itturns out that we have already defined the right CMRA, namely,
AG. One important property of invariants is that everybody involved
agrees on what the invariant with a particular name is; the agreement
CMRA ensures that this is the case.
This leads us to the following equation for defining the semantic
model of Iris:

that Vn must not make a distinction between n-equal elements(this is a form of non-expansiveness), and CMRA - VALID - MONO
declares that at smaller step-indices, more elements are valid.
As discussed in the previous section, Vn encodes “step-indexed
partiality”, which is more general than using a partial function forcomposition. For consistency, we decided that partiality should
be handled the same for RAs and CMRAs, which is why RAs
use a validity predicate as well.
• The extension axiom CMRA - EXTEND roughly states that decom-

position must commute with step-indexed equivalence. This isdiscussed in more depth in our technical appendix [1].

mon

iProp ≈ Res −−→ SProp

Notice that every RA can be trivially turned into a CMRA byequipping it with the discrete COFE ∆ and making Vn just ignore
the step-index, so that validity is the same at every n.
We can easily generalize existing RA constructions to CMRA
constructions by lifting the step-indexed validity. For example, for+⊥ from §2.5, this is done as follows:Vn , inl(a1 ) a1 ∈ Vn0 ∪ inr(a2 ) a2 ∈ Vn00
3.4

where Res , World × F (iProp) × ∆E X(PhyState)finWorld , N −* AG(IiProp)
Ignoring the AG, this is just the uncurried form of IRIS - PRE -2.0.
However, as a consequence of this, iProp is now just a predicate overa CMRA. Practically speaking, this means that most Iris connectives
can be modeled independently of worlds. Almost all connectives canmonbe interpreted in M −−→ SProp, completely generic in the choiceof the CMRA M . This kind of abstraction and unification simplifies
proving soundness of the logical rules.
Note that IRIS -2.0 brings us very close to the canonical model of
traditional separation logic—using a predicate over PCMs—the coredifference being step-indexing. This goes to show that even the mostcomplicated of concurrent impredicative higher-order separation
logics can be semantically reduced to the same fundamental idea.
In that sense, equipping Iris with generic higher-order ghost state
actually simplifies its model.

The Model of Iris 2.0

We now have everything set up to generalize Iris to higher-orderghost state. Instead of the user picking a fixed RA R, they can pickan arbitrary CMRA M that can depend on iProp. Formally, thisdependency is expressed by a function F : COFE → CMRA:
mon

mon

iProp ≈ World −−→ Res −−→ SProp(IRIS -2.0)(IRIS - PRE -2.0)

finwhere World , N −* IiProp
Res , F (iProp) × ∆E X(PhyState)4.

Notice that this is very similar to IRIS -1.1. The only differenceis that Res is no longer discrete, but rather defined in terms of F .
Similar to the case of the I in World, every recursive occurrence ofiProp in F needs to be guarded by a I to ensure the existence of a
fixed point of the recursive domain equation. (Formally that means
F should be locally contractive [2, 7].)
In order to solve the challenge outlined in §1.1, recall that wewish to obtain an instantiation of Iris where the ghost state is a heapof oneshots of type T , where T may depend on iProp. Let us rewrite
it as T = G(iProp) to factor out the dependency on iProp. We canthen choose the following function for the ghost state:

Case Study: Barrier

In this section, we will show how to implement and verify theexample from §1.1 using a synchronization primitive called a barrier(which one can also think of as a “oneshot channel”). We follow
the implementation and specification of this primitive as presented
in Dodds et al. [15]. As we will see, higher-order ghost state is
crucially useful both in our use of the barrier and in verifying thecorrectness of the barrier itself.
A barrier is a synchronization primitive offering two actions:• Clients can wait on the barrier, which will block these processes

until the barrier is triggered.
• A client can signal the barrier, which will cause all waitingfin

F (X) , N −* O NE S HOT(AG(IG(X)))

clients to resume execution.

We will see in §4.2 that this suffices to prove the correctness of theclient from §1.1.
Since F is a function between types in a category, we require it
to be a bifunctor from COFE to CMRA.6 This is typically easy
to show. Using bifunctors, we can handle both co- and contravariant
occurrences of F ’s argument, e.g., if the type T is iProp → iProp,nein which case G(X) , X −→ X. Of course, if all you need isfirst-order ghost state, you can easily pick the constant functor

You can find the code implementing a barrier in Figure 9. This
implementation is fairly straightforward: A waiting client is in abusy loop until it sees the location x updated to 1. So, all that signal
has to do is set the location to 1, and all current and future waitingclients will leave their busy loop.
The example client in Figure 11 shows how a barrier can beused to implement the pattern described in §1.1. Notice that we are
actually using the same barrier to communicate with both worker
threads, which is possible because a barrier can trigger multiple
threads when signaled. In fact, the client given here is even moregeneral than the one sketched in §1.1, since the worker threads

6 The arrows of CMRA are monotone, non-expansive functions—forfurther details, see our technical appendix [1].

9Here and below, the assertions P , Pi , Qi and Q range over avariable x of type T = G(iProp) for some bifunctor G (cf. §3.4).
We furthermore assume that resources can be split and merged.

newbarrier , λ . ref(0)signal , λx. x ← 1∀x:T. P ⇒ P1 ∗ P2

wait , rec wait(x) = if !x = 1 then () else wait(x)Oneshot ghost variables. The functor that we need to implement
oneshot ghost variables is F (X) , O NE S HOT(AG(IG(X))), so
the ghost state is of type F (iProp) = O NE S HOT(AG(IT )). We
encode oneshot ghost locations as follows:

Figure 9. Implementation of a barrier
NEWBARRIER{True} newbarrier() {`. send(`, P ) ∗ recv(`, P )}γ ,→ pending , inl()

SIGNALP `Q
recv(`, P ) ` recv(`, Q)

RECV- SPLIT

recv(`, P1 ∗ P2 ) V recv(`, P1 ) ∗ recv(`, P2 )γ ,→ x ∗ γ ,→ y ⇒ .(x = y)inr(ag(next(x)) · ag(next(y)))γ

By GHOST- VALID we know that we can only own valid ghost CMRA
elements. In combination with AG - VALID, we thus obtain

Barrier Specification

The behavior of the barrier is specified in Figure 10. When initializing a barrier using newbarrier(), the resources recv(`, P ) andsend(`, P ) are created, which can then be used by the waiting thread
and signaling thread, respectively. The assertion P describes theresources the barrier has to transfer, so when calling signal(`), theresource P has to be given up and is transferred to the waiting client.
Conversely, when wait(`) returns, the waiting client receives P .
Notice that newbarrier works for any assertion P , without thecaller having to establish P or give up any resources on initializationof the barrier. In the example shown in Figure 11, the assertion P isin fact only established by the “expensive computation”, long after
the barrier has been created.
The predicates recv(`, P ) and send(`, P ) are impredicative
higher-order abstract predicates. This means that they are predicates describing any assertion P (higher-order), which can include
occurrences of recv and send itself (impredicative), as well as e.g.,
Hoare triples. It is thus for example possible to send the permission
for code pointers through the barrier. Finally, these predicates aredefined by the implementation of the barrier, but their details are notexposed to the client (abstract).
The rule RECV- SPLIT plays an important role in proving thecorrectness of the client in Figure 11. The client has two threads
that both call wait, and thus both need a recv resource, whereas
after initialization of the barrier we have just one such resource. If
we can split P into two pieces P1 and P2 , then we can use RECVSPLIT to split recv(`, P ) into recv(`, P1 ) and recv(`, P2 ). Splitting
makes it possible to move the resources recv(`, P1 ) and recv(`, P2 )to different threads, which then can both call wait to obtain theirpiece of the resource transmitted through the barrier.

next(x) = next(y)Finally, we use the following general property of the later construction IT to complete the proof of ONESHOT- AGREE - LATER:
next(x) = next(y) ⇔ .(x = y)Remember that .(x = y) means that x and y are equal at thenext step-index. This is not a problem, since we can get rid of the .
when the program performs a physical step of execution.
Verification of the worker threads. We decorated Figure 11 withverification conditions to document resources available at any
particular point in the code. To obtain the resources needed for theworker threads, we want to split the recv using RECV- SPLIT, which
first requires us to weaken the barrier assertion with RECV- MONO:(∃x:T. γ ,→ x ∗ P ) ⇒ (∃x:T. γ ,→ x ∗ P1 ) ∗ (∃x:T. γ ,→ x ∗ P2 )It is straightforward to verify correctness of the worker threads.
Joining the existentials. What is left to justify is the last line of
Figure 11: How can the two existentials be joined together? The corelemma for this step of the proof is ONESHOT- AGREE - LATER. From
there, we easily obtain:(∃x:T.γ ,→ x∗Q1 )∗(∃x:T.γ ,→ x∗Q1 ) ⇒ .(∃x:T.γ ,→ x∗Q)
The . on the right hand side is then consumed by the parallel
composition, when it performs a physical step of computation tojoin the threads back together.
This completes the verification: We demonstrated that, using thehigher-order ghost state as defined in §3, we can solve the challenge
posed in §1.1 for existential quantification over arbitrary types.

Splitting and Joining the Existentials

For the verification of the example client in Figure 11, we assume
that we have the following Hoare triples for the main thread M andthe workers Wi for i ∈ {1, 2}:{P 0 } e {∃x:T. P }(ONESHOT- INIT)(ONESHOT- AGREE - LATER)

We will now prove the latter rule (ONESHOT- AGREE - LATER) to showthat it is indeed a derived rule. First of all, observe that owning
γ ,→ x ∗ γ ,→ y is logically equivalent to (using GHOST- OP):are transforming their Pi into Qi , and the main thread later joinsthese two together to obtain Q. Before we go into details about theverification of the client, let us have a closer look at specifying theinterface provided by the barrier library.

4.2

for x : T

γ ,→ pending V γ ,→ x

Figure 10. Barrier specification

4.1

γ

Notice that γ ,→ x is a persistent assertion stating that the oneshot
location has been initialized. The state of location γ is obtained byinjecting x into O NE S HOT(AG(IT )).
From generic properties of the oneshot and agreement CMRA
we obtain the following proof rules to initialize a previously uninitialized location, and to encode that a location, once initialized, will
not change its value:

RECV- MONO
WAIT

γγ ,→ x , inr(ag(next(x))){send(`, P ) ∗ P } signal(`) {True}{recv(`, P )} wait(`) {P }∀x:T. Q1 ∗ Q2 ⇒ Q

4.3

Verifying the Barrier Specification: Saved Propositions

As has been discussed in [15], it is very difficult to prove a specification for a barrier that includes the splitting axiom. Intuitively, thereason for this is as follows: When a thread calls send to give up∀x:T. {Pi } ei {Qi }10let b = newbarrier() in0γ ,→ pending ∗ P ∗ send(b, ∃x : T. γ ,→ x ∗ P ) ∗ recv(b, ∃x : T. γ ,→ x ∗ P )

γ ,→ pending ∗ P 0 ∗ send(b, ∃x : T. γ ,→ x ∗ P ) ∗ recv(b, ∃x : T. γ ,→ x ∗ P1 ) ∗ recv(b, ∃x : T. γ ,→ x ∗ P2 )[W1 ]{recv(b, ∃x : T. γ ,→ x ∗ P1 )}wait(b);{∃x : T. γ ,→ x ∗ P1 }[work on P1 ] e1{∃x : T. γ ,→ x ∗ Q1 }[M ]γ ,→ pending ∗ P 0 ∗ send(b, ∃x : T. γ ,→ x ∗ P )[W2 ]{recv(b, ∃x : T. γ ,→ x ∗ P2 )}[expensive computation] e;{∃x : T. γ ,→ x ∗ P ∗ send(b, ∃x : T. γ ,→ x ∗ P )}signal(b)wait(b);{∃x : T. γ ,→ x ∗ P2 }[work on P2 ] e2{∃x : T. γ ,→ x ∗ Q2 }

[After joining] {∃x : T. γ ,→ x ∗ Q}
Figure 11. Example client of a barrier• In Iris we use large nested COFE constructions composed fromsmaller COFEs (see for example the construction IRIS -2.0).

resources P , it has to prove that P matches the separating conjunction of the resources that all waiting clients are expecting to receive.
But how should signal know how the resources should be split
among the waiting clients? The splitting may have happened after
the call to newbarrier, and yet it must be somehow communicatedto signal.
To our knowledge, the only way to do this is to record the desired
splitting in the global ghost state, which is accessible to both thethread that performs the splitting and to signal. This immediatelymeans that we need to be able to have ghost state that depends on
propositions—that is, arbitrary propositions of the logic (iProp), notjust meta-level propositions (Prop).
One convenient way of actually going about this proof is to apply
saved propositions [15]. In Iris, the interface of saved propositions
is as follows:∀P. True V ∃γ. γ ⇒ P∀γ, P, Q. (γ ⇒ P ∗ γ ⇒ Q) ⇒ .(P ⇔ Q)

Coq should be able infer the COFE structure on these nested
constructions automatically without considerable overhead.
• Defining non-expansive functions should be lightweight. Most

importantly, just to write down a ∀x:T. P x or ∃x:T. P x
nequantification in the logic (where P : T −→ iProp), there should
be no proof obligations.
n• Rewriting with the equivalence relations = of COFEs shouldnwork fast and reliably. Note that rewriting with = is only possible
in the context of non-expansive functions, and thus requires Coq
to derive facts about non-expansiveness. In Coq, rewriting withuser-defined equivalence relations is called setoid rewriting.
The Coq formalization of Iris 1.0, which used the ModuRes
library [32], did not meet any of these challenges. Dealing with large
COFE constructions made Coq very slow, setoid rewriting worked
unreliably, and proofs of non-expansiveness cluttered definitions.
The Coq formalization of Iris 2.0 has been implemented fromscratch, and we have improved on all of these points.
In order to emphasize the difficulties involved, let us describe
the two most commonly used patterns of representing algebraic
structure (like COFEs and CMRAs in our case) in Coq.

(SPROP - ALLOC)(SPROP - AGREE)

The first rule says that we can allocate a new saved proposition P ata fresh ghost location γ. Notice that to establish a saved proposition,
we do not actually have to establish that assertion. The allocatedassertion γ ⇒ P is persistent. The second rule then allows us toderive, given two assertions about the same location, that they must
be about the same proposition.
It is not coincidental that these rules look very similar to GHOSTALLOC and ONESHOT- AGREE: the oneshot locations described in §4.2
are strictly more general than saved propositions. However, it iseasy enough to directly encode saved propositions by defining
F (X) , AG(IX) to obtain ghost state of the form AG(IiProp).
The full proof of the barrier specification in Iris is carried out inour technical appendix [1] and is formalized in Coq.

5.

• The bundled approach consists of representing algebraic struc-tures as dependently typed records containing the carrier, theoperations, and proofs. COFEs would thus be formalized as:
Record cofeT := {cofe_car :> Type;
cofe_dist : nat → relation cofe_car;
cofe_dist_equivalence : ∀ n,
Equivalence (cofe_dist n);(* ... *)}.

Coq Formalization

Adequacy and soundness for Iris 2.0, many derived constructions,and all specifications and proofs in this paper have been fully formalized using Coq. We discuss important aspects of the formalization,
features of Coq that were essential, and the key differences between
the formalization of Iris 1.0 and Iris 2.0.
5.1

• The unbundled approach consists of representing algebraic

structures as predicates over the carrier, the operations, andproofs. COFEs would thus be formalized as:

Algebraic Structures

Record cofeT {A} (d : nat → relation A) := {cofe_dist_equivalence : ∀ n,
Equivalence (cofe_dist n);(* ... *)}.

The main challenge of formalizing the Iris logic is that it lives
in the category of COFEs instead of the conventional category of
Coq Types. So, instead of using plain Coq Types, we use types
equipped with an ordered family of equivalences, and instead ofplain Coq functions, we use non-expansive functions. This posessome interesting challenges:

11In order to automatically infer algebraic structures given theType of the carrier, Coq supports two similar mechanisms: canonicalstructures and type classes. Canonical structure search is guided by
the fields of a record, and is thus commonly used in combination
with the bundled approach [19]. Type class search, on the other hand,is guided by the parameters of a record, and is thus commonly usedin combination with the unbundled approach [34].
Iris 1.0 used the unbundled approach to represent COFEs, which
is known to suffer from an exponential blow-up in term size whennesting instances of algebraic structures. In order to remedy thisshortcoming, Iris 2.0 uses a bundled approach using canonicalstructures inspired by Ssreflect’s [19].
Iris 1.0 demanded proofs of non-expansiveness of functions apriori pretty much everywhere. We changed this in Iris 2.0 such thatfor example the predicates in universal and existential quantification,and the post-condition of Hoare triples, do not a priori have to
be non-expansive. This allows us to reuse Coq’s functions andnotation when writing down formulas in the Iris logic. Proofs of nonexpansiveness are only needed for setoid-rewriting and constructing
recursive definitions, but not for validity of the proof rules, andcan thus be established a posteriori. This approach matches wellwith Coq’s setoid machinery, which uses type classes to registercompatibility with equivalence relations a posteriori [33].
Although Iris 2.0 made considerable progress on the formalization challenges we posed, we do not consider these challenges
to be solved. Since we need the combination of bundled algebraic
structures and setoid rewriting, we are using a mixture of canonicalstructures and type classes, whose interaction is somewhat fragile.
Most notably, many Coq tactics, including the rewrite tactic andthe type class machinery, are very sensitive to terms that are only
equal up to conversion (e.g., unfolding of canonical structure projections), and they often fail to infer type class arguments. In order
to work around these problems, we are using the Ssreflect rewrite
tactic, which deals better with these issues.
We thus welcome some machinery that unifies type classes andcanonical structures in a streamlined way. Unification hints may be
a step in this direction [5].
5.2Class VarBound (x : string) (X : list string) :=var_bound : if decide (x∈X) then True else False.
Inductive expr (X : list string) : Type :=| Var x : VarBound x X → expr X| App: expr X → expr X → expr X| Lam x : expr (x :: X) → expr X.
Coercion App : expr >-> Funclass.
Notation "’ x" := (Var x _).
Notation "λ: x .. y , e" := (Lam x .. (Lam y e) ..).
The type expr X represents expressions whose free variables
are a subset of X, and as such, expressions of type expr [ ] areguaranteed to be closed. An important part of this definition isthat the condition x ∈ X for variables is decidable, and can thus beinferred by computation while type checking concrete programs.
This is achieved by instrumenting the type class mechanism with ahint to solve VarBound constraints by computation:
Hint Extern 0 (VarBound _ _) =>vm_compute; exact I : typeclass_instances.
Notice that we can use a named approach to variable binding
without having to worry about variable capture because our language
has weak reduction—i.e., we do not reduce under λs.
Example. The Coq version of the code of the barrier implementation is as follows:7
Definition newbarrier : val := λ: <>, ref #0.
Definition signal : val := λ: "x", ’"x" <- #1.
Definition wait : val :=rec: "wait" "x" :=if: !’"x" = #1 then #() else ’"wait" ’"x".
5.3

Notable Formalization Aspects

Weakest precondition. The Hoare triples of Iris are defined interms of a more primitive weakest precondition judgment. Since theweakest preconditions are better suited for interactive proving, we
use them in our Coq proofs. Hoare-triple-based specifications—suchas those in §2 and §4.1—are only established at the end.

Programming Language

Similar to Iris 1.0, the Coq formalization of Iris 2.0 is parameterized
by the programming language that one wishes to reason about.
For the purpose of this paper, we have instantiated Iris with adeeply embedded untyped ML-like language with higher-order store
and the concurrency primitives fork and CAS (compare-and-swap).
This improves on the Iris 1.0 formalization, which has not been
instantiated with an actual programming language.
The main goal of the Iris 2.0 Coq formalization is verificationof actual code, and as such, readability of programs written in the
deeply embedded language becomes important. In particular:

Non-expansive functions. We have implemented a tactic to provethat functions are non-expansive by repeatedly applying congruence
properties. Contrary to Coq’s solve_proper, our tactic is more
efficient and handles match constructs.
Combining functors. A core feature of Iris is that the structureof the ghost state can be chosen by the user. This is achieved byparameterizing the logic by a functor F (§3.4). However, whenverifying programs that consist of multiple program modules, it
is likely that different program modules are in need of different
functors Gi . We have used Coq’s type class machinery to implement
infrastructure that automatically combines these Gi to form theglobal functor F , so the modules can be combined in one proof.

1. We want to be able to write programs in a syntax that resembles
ML, and we want programs to be pretty printed similarly to how
they appear when being interactively verified.

5.4

2. Variable binding should be human-readable, hence a “machineoriented” approach like De Bruijn indexes does not suffice.

Overview

The Coq development, which is entirely constructive and axiomfree, consists of the parts described in Figure 12. Line counts
exclude whitespace and comments. We used a support library by
Krebbers [25] that contains many definitions and theorems aboutdata structures such as lists, finite sets, and finite maps.
The compilation times of Iris 2.0 have improved by an order ofmagnitude: Compilation of the components ‘Algebra’ and ‘Programlogic’ takes less than 2 minutes for Iris 2.0 vs. 23 minutes for Iris
1.0 (using an Intel Core i5-2450M, 4 threads, 2 cores).

3. All programs should be closed, i.e., they should not contain freevariables. The language formalization should ensure closednessof programs automatically.
We make use of Coq’s expressive notation mechanism to obtain an ML-like notation for our language, we make use of named
variables to make binding human-readable, and we make use of dependent types to ensure closedness of programs. Our representationof programming language expressions is roughly as follows:

7 In this code, <> denotes an anonymous binder.

12

Component

What elsefrom the axioms of our RAs. Some common properties appear
consistently (either as axioms, or as admissible rules): The core
must produce a unit (RA - CORE - ID), be idempotent (RA - CORE - IDEM),
and be a homomorphism, i.e., be compatible with composition:|a · b| = |a| · |b|. The last property is stronger than our monotonicity
axiom (RA - CORE - MONO), and as such, the axioms of RAs are weaker
than those demanded by prior work. In fact, RAs are strictly weaker.
One of our most important RA constructions, the state-transition
system (STS),8 has a core that is not a homomorphism. This showsthat demanding the core to be a homomorphism, as prior work has
done, rules out useful instances.
Another difference is the fact that our core may be partial,
whereas in prior work it was always a total function. As discussedin §2.5, partial cores make it easier to compose RAs out of simpler
constructions like sums.

LOC

AlgebraSolver for domain equations
5.444
Program logic Model, adequacy, derived notions 2.385
1.591
Heap language Derived rules, automation
Barrier
Higher-order client (see [1])433
Examples from §2 and §4.2
239
ExamplesTotal
10.092
Figure 12. Overview of the Coq development

6.

Related Work

User-defined higher-order ghost state. Several prior logics support custom (user-defined) ghost state, via Concurroids [27] orPCMs [24, 39]. However, these logics are all restricted to first-orderghost state, since the structure of the ghost state is defined and fixed
before the logic is instantiated.
Some logics do have a model that can be considered to involve
second-order ghost state, e.g., to justify their use of dynamicallyallocated locks [20, 21, 8], regions [35], or invariants [24]. However,this ghost state has a fixed structure, rather than being an instanceof a generic algebraic structure like CMRAs.
In some of these prior logics, even though the structure of ghost
state is fixed, it can sometimes be adapted cleverly to support a
range of proof patterns. For example, Dodds et al. [15] showedthat the built-in “protocol” mechanism of the iCAP logic [35] canbe repurposed to encode saved propositions (§4.3), a functionality
for which it was not originally intended. However, the encoding issomewhat artificial, must be verified by direct appeal to the modelof iCAP, and does not scale to support general higher-order ghost
state (such as we relied on in proving the example from §1.1).
The Verified Software Toolchain (VST) of Appel et al. [4]provides a general framework for defining higher-order logics via“indirection theory” [22]. Although VST has been demonstrated tosupport particular forms of second-order ghost state, it is not yet
clear how precisely indirection theory compares with the categorical
COFE-based approach. We believe that VST can potentially begeneralized to support more general higher-order ghost state in
the manner of Iris 2.0. Notably, VST has a notion of PCM-likestructures that are compatible with aging (step-indexing) and seemto loosely correspond to CMRAs. However, logics built using the
VST typically fix a particular ghost state for their purpose andprovide primitive rules for this particular ghost state, whereas Iris isdesigned for such proof rules to be derived inside a single logic froma few fundamental proof rules. As a result, Iris proofs using different
CMRAs can be safely composed (§2.6), whereas proofs carried out
in different VST logics do not necessarily interoperate. Furthermore,
VST has so far only been applied to sequential and coarse-grained
concurrent code, not to fine-grained concurrent algorithms.

Coq formalizations. Over the past decade, there has been tremendous progress on formalization of program logics in proof assistants, with focus on supporting strong proof automation, as well as
the ability to deal with realistic programming languages (see, e.g.,[4, 31, 6, 23, 9, 25, 39, 37]).
However, with the exception of the aforementioned VST, theseformalized program logics do not support impredicative invariants(§2.2), let alone higher-order ghost state.

7.

Conclusion

We have introduced higher-order ghost state and have shown that
it is a useful extension of higher-order concurrent separation logic.
Moreover, we have presented Iris 2.0, an extension of the originalIris program logic with support for higher-order ghost state.
Soundness of Iris 2.0 is proven using a new model construction,
which, in addition to supporting higher-order ghost state, also unifies
two of the core model concepts, worlds and resources, that weredistinct before. This simplifies the meta-theory, which is important
not only conceptually, but also when formalizing the meta-theoryof Iris in a proof assistant. We have formalized Iris 2.0 in Coq, andthe formalization itself is a strong improvement over the earlier
formalization of Iris 1.0.
In ongoing work, we are using the new Iris 2.0 formalization to
conduct larger experiments with Iris. To support such experiments,
we are in the process of developing tactic support for reasoning
about concurrent higher-order programs.
In order to facilitate interactive reasoning in Iris using Coq, we
have extended Coq with support for the linear context of separation
logic. This extension provides named assumptions and tactical support for introduction and case analysis of these linear assumptions.
Initial experiments are promising and show a significant improvement in ergonomics compared to using the rules of Iris manually.
In addition, we plan to develop tactics to reason fully automatically about client code. This will probably be done using Malecha
and Bengtson’s recent reflective tactics [26].

Acknowledgments

PCMs with a (duplicable) core. There have been several presentations of variants of PCMs that have “multiple units” or include a
notion of a “duplicable core”.
Dockins et al. introduced multi-unit separation algebras [14],which, unlike PCMs, only demand the existence of a possibly
different unit ua with ua · a = a for any element a. A crucial
difference between multi-unit separation algebras and RAs is that
we present the monoidal operation and core as a function, whereas
they represent these as relations.
The terminology of a (duplicable) core has been adapted from
Pottier, who introduced it in the context of monotonic separation
algebras [30]. However, the axioms of Pottier’s cores, as well as
those of related notions in other work [39, 4], are somewhat different

We wish to thank Jacques-Henri Jourdan for suggesting the notionof a partial core, and Kasper Svendsen for his help with clarifying
details concerning COFEs and saved propositions in iCAP.
This research was supported in part by a European ResearchCouncil (ERC) Consolidator Grant for the project “RustBelt”,
funded under the European Union’s Horizon 2020 Framework Programme (grant agreement no. 683289); and by the ModuRes Sapere
Aude Advanced Grant from The Danish Council for Independent
Research for the Natural Sciences (FNU).
8 The RA of STSs, as well as the example demonstrating that the core is nota homomorphism, is described in our technical appendix [1].

13

References[20] A. Gotsman, J. Berdine, B. Cook, N. Rinetzky, and M. Sagiv. Local
reasoning for storable locks and threads. In APLAS, pages 19–37,
2007.

[1] Higher-Order Ghost State: Appendix and Coq development. Available
on the Iris project website at http://plv.mpi-sws.org/iris/.
[2] P. America and J. Rutten. Solving reflexive domain equations in a
category of complete metric spaces. JCSS, 39(3):343–375, 1989.

[21] A. Hobor, A. Appel, and F. Zappa Nardelli. Oracle semantics forconcurrent separation logic. In ESOP, pages 353–367, 2008.

[3] A. Appel and D. McAllester. An indexed model of recursive types forfoundational proof-carrying code. TOPLAS, 23(5):657–683, 2001.

[22] A. Hobor, R. Dockins, and A. Appel. A theory of indirection via
approximation. In POPL, 2010.

[4] A. W. Appel, editor. Program Logics for Certified Compilers. Cambridge University Press, 2014.

[23] J. B. Jensen, N. Benton, and A. Kennedy. High-level separation logic
for low-level code. In POPL, pages 301–314, 2013.

[5] A. Asperti, W. Ricciotti, C. S. Coen, and E. Tassi. Hints in unification.
In TPHOLs, volume 5674 of LNCS, pages 84–98, 2009.

[24] R. Jung, D. Swasey, F. Sieczkowski, K. Svendsen, A. Turon, L. Birkedal,and D. Dreyer. Iris: Monoids and invariants as an orthogonal basis forconcurrent reasoning. In POPL, pages 637–650, 2015.

[6] J. Bengtson, J. B. Jensen, and L. Birkedal. Charge! - A Framework forHigher-Order Separation Logic in Coq. In ITP, volume 7406 of LNCS,
pages 315–331, 2012.

[25] R. Krebbers. The C standard formalized in Coq. PhD thesis, Radboud
University, 2015.
[26] G. Malecha and J. Bengtson. Easy and efficient automation throughreflective tactics. In ESOP, 2016.

[7] L. Birkedal, K. Støvring, and J. Thamsborg. The category-theoretic
solution of recursive metric-space equations. TCS, 411(47):4102–4122,
2010.

[27] A. Nanevski, R. Ley-Wild, I. Sergey, and G. A. Delbianco. Communicating state transition systems for fine-grained concurrent resources.
In ESOP, pages 290–310, 2014.

[8] A. Buisse, L. Birkedal, and K. Støvring. Step-indexed Kripke modelof separation logic for storable locks. ENTCS, 276:121–143, 2011.

[28] P. O’Hearn. Resources, concurrency, and local reasoning. TCS,
375(1):271–307, 2007.

[9] A. Chlipala. The Bedrock structured programming system: combining
generative metaprogramming and Hoare logic in an extensible program
verifier. In ICFP, pages 391–402, 2013.

[29] S. Owicki and D. Gries. Verifying properties of parallel programs: An
axiomatic approach. CACM, 19(5):279–285, 1976.

[10] E. Cohen, E. Alkassar, V. Boyarinov, M. Dahlweid, U. Degenbaev,
M. Hillebrand, B. Langenstein, D. Leinenbach, M. Moskal, S. Obua,
W. Paul, H. Pentchev, E. Petrova, T. Santen, N. Schirmer, S. Schmaltz,
W. Schulte, A. Shadrin, S. Tobies, A. Tsyban, and S. Tverdyshev.
Invariants, modularity, and rights. In PSI, volume 5947 of LNCS,
pages 43–55, 2009.

[30] F. Pottier. Syntactic soundness proof of a type-and-capability systemwith hidden state. JFP, 23(1):38–144, 2013.
[31] I. Sergey, A. Nanevski, and A. Banerjee. Mechanized verification offine-grained concurrent programs. In PLDI, pages 77–87, 2015.
[32] F. Sieczkowski, A. Bizjak, and L. Birkedal. ModuRes: A Coq
library for modular reasoning about concurrent higher-order imperative
programming languages. In ITP, volume 9236 of LNCS, pages 375–
390, 2015.

[11] P. da Rocha Pinto, T. Dinsdale-Young, and P. Gardner. TaDA: A logic
for time and data abstraction. In ECOOP, pages 207–231, 2014.
[12] T. Dinsdale-Young, L. Birkedal, P. Gardner, M. J. Parkinson, andH. Yang. Views: Compositional reasoning for concurrent programs.
In POPL, 2013.

[33] M. Sozeau. A new look at generalized rewriting in type theory. JFR,
2(1):41–62, 2009.

[13] T. Dinsdale-Young, M. Dodds, P. Gardner, M. Parkinson, andV. Vafeiadis. Concurrent abstract predicates. In ECOOP, pages
504–528, 2010.

[34] B. Spitters and E. van der Weegen. Type classes for mathematics intype theory. MSCS, 21(4):795–825, 2011.
[35] K. Svendsen and L. Birkedal. Impredicative concurrent abstract
predicates. In ESOP, pages 149–168, 2014.

[14] R. Dockins, A. Hobor, and A. W. Appel. A fresh look at separation
algebras and share accounting. In APLAS, pages 161–177, 2009.

[36] K. Svendsen, L. Birkedal, and M. J. Parkinson. Modular reasoning
about separation of concurrent data structures. In ESOP, pages 169–
188, 2013.

[15] M. Dodds, S. Jagannathan, M. J. Parkinson, K. Svendsen, and
L. Birkedal. Verifying custom synchronization constructs using
higher-order separation logic. TOPLAS, 38(2):4, 2016.

[37] H. Tuch, G. Klein, and M. Norrish. Types, bytes, and separation logic.
In POPL, pages 97–108, 2007.

[16] X. Feng. Local rely-guarantee reasoning. In POPL, pages 315–327,
2009.

[38] A. Turon, D. Dreyer, and L. Birkedal. Unifying refinement and Hoarestyle reasoning in a logic for higher-order concurrency. In ICFP, pages
377–390, 2013.

[17] X. Feng, R. Ferreira, and Z. Shao. On the relationship between
concurrent separation logic and assume-guarantee reasoning. In ESOP,
pages 173–188, 2007.

[39] A. Turon, V. Vafeiadis, and D. Dreyer. GPS: navigating weak memory
with ghosts, protocols, and separation. In OOPSLA, pages 691–707,
2014.

[18] M. Fu, Y. Li, X. Feng, Z. Shao, and Y. Zhang. Reasoning about
optimistic concurrency using a program logic for history. In CONCUR,
pages 388–402, 2010.

[40] V. Vafeiadis and M. Parkinson. A marriage of rely/guarantee andseparation logic. In CONCUR, pages 256–271, 2007.

[19] F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau. Packaging
mathematical structures. In TPHOLs, volume 5674 of LNCS, pages
327–342, 2009.

14