What is Iris?

Language-independent higher-order separation logic framework
with simple foundations for modular reasoning
about fine-grained concurrency in Coq

What is it Good for?

• The Rust Type System (Jung, Jourdan, Dreyer, Krebbers)
• Logical Relations (Krogh-Jespersen, Svendsen, Timany, Birkedal, Tassarotti, Jung, Krebbers)
• Object Capabilities (Swasey, Dreyer, Garg)
• Logical Atomicity (Krogh-Jespersen, Zhang, Jung)

Common theme: SC languages

Iris is very general — but it needs interleaving semantics

No support for weak memory?

We develop interleaving semantics for C11 Release-Acquire

and derive two major Release-Acquire program logics in Iris

Benefits of Using Iris for Weak Memory

• For free: separation, higher-order ghost state, impredicative invariants
• Mechanized soundness proofs at very high level of abstraction
• Mechanized examples: all examples of encoded logics, including RCU (PLDI' 2015)
• Mixing reasoning principles from different weak program logics

Operational Release-Acquire: Message Passing

Support for Non-Atomic Accesses

• Built-in race detection for non-atomic accesses
• Allow mixing atomic and non-atomic accesses to same location
• (Almost) equivalent to C11

Roadmap

Iris: Fictional Separation

0. Have a monolithic, non-splittable resource $\res$ to be shared
1. Make a splittable ghost copy
   (by designing a PCM with the right separation structure)
2. Keep copy in sync with $\res$ using the $\Auth$ construction
   
   • unique authoritative copy marked with ●
   • splittable fragments marked with ◯
   • all ◯'s combine into ●
3. Use invariant to tie ● to original resource $\res$
4. Derive rules to update ◯ in conjuction with ● and $\res$

Iris: Heap with Fictional Separation

0. Monolithic resource: $\ownPhys\sigma$ — the physical state (heap)
1. We want exclusive, per-location fragments: $\Loc \stackrel{\mathrel{{}_\text{fin}}}{\rightharpoonup}_{\uplus} \Val$
2. Wrap it in $\Auth$.
   $\loc \pointsto \val \eqdef{}$◯ $[\loc := \val]$
3. Establish invariant: $\exists \sigma. \ownPhys\sigma ∗{}$● $\sigma$
4. Derive all rules from these two:
   
   • ● $\sigma$${}∗{}$◯ $[\loc := \val]$ ${}\implies{} \always(\sigma(\loc) = \val)$
   • ● $\sigma$${}∗{}$◯ $[\loc := \val]$ ${}\Rrightarrow{}$ ● $\Fupd\sigma[\loc -> \valB]$${}∗{}$◯ $[\loc := \valB]$

The Base Logic: Fictional Separation of $\ownPhys\sigma$

• $\sigma : \left\{\msgs : \Msgs;\; \views : \Thread \stackrel{\mathrel{{}_\text{fin}}}{\rightharpoonup} \View;\; \ldots \right\}$
• Excl. history: ${\color{alert}\lhist\loc\hist} \eqdef{}$ ◯ $[\loc := \hist]$
  ($\hist : \mathcal{P}(\Val \times \Time \times \View)$)
• Excl. views: ${\color{alert}\seen\thread\view} \eqdef{}$ ◯ $[\thread := \view]$
• One big invariant:
  $\exists \sigma. \ownPhys\sigma ∗{}$● $\sigma{.}\msgs$ ${}∗{}$● $\sigma{.}\views$ ${}∗{}\ldots$
• Relating thread views and history:
  • ${\color{alert}\init\hist\view} \eqdef{} \exists (\val, \_, \view_0) \in \hist. \view \futv \view_0 \wedge \val \in \Val$
  • $\color{alert}\alloc\hist\view$
  • $\color{alert}\lna\hist\view$

Base Logic: Atomic Read

Base-AT-Read

Base Logic: Atomic Write

Base-AT-Write

Base Logic: Message Passing

• ${\color{alert}\textrm{Inv}_y(\view_0)} \eqdef{} \\ \exists \hist. \lhist{y}\hist \ast (0,\_,\view_0) \in \hist \\\;\;\ast \forall \view_1, \val_1 \neq 0. (\val_1, \_, \view_1) \in \hist \implies \exists \view_{37} \pastv \view_1.$ $\textrm{Inv}_x(\view_{37})$
• ${\color{alert}\textrm{Inv}_x(\view_{37})} \eqdef{}$◇${}∗ \lhist{x}{\{(37,\_,\view_{37})\}}$

What is RSL?

$$\hoare{}{\top}{\ealloc}{\Ret\loc. \Rel\loc\pred ∗ \Acq\loc\pred}{}$$
$$\hoare{}{\Rel\loc\pred ∗ \pred(\val)}{\ewrite\at\loc\val}{\Rel\loc\pred ∗ \Init\loc}{}$$
$$\hoare{}{\Acq\loc\pred ∗ \Init\loc}{\eread\at\loc}{\Ret\val. {\Acq\loc{{\color{alert}\Fupd\pred[v\! ->\!\top]}}} ∗ \pred(\val)}{}$$

Message Passing in RSL

$ \pred(\val) = \begin{cases} x \pointsto 37 & \mbox{ if } \val = 1 \\ \top & \mbox{ ow. } \end{cases}$

Challenge: How to Deal With Views?

Truth is relative to a thread's view.

Idea: Encode RSL assertions as predicates on views.

Frame

$\interp\propC({\color{hred}\view}) \stackrel{?}{\implies} \interp\propC({\color{hred}\view'})$

Use monotone predicates on views.

View-monotone predicates

Backup Slides

Difference to C11

Iris: The Elevator Pitch

• Key idea of Iris: Ghosts & Invariants are all you need
• Ghosts represent ownership of resources
  $m : M$ $≈$ "I own element $m$ in PCM $M$"
• Invariants are shared resources
  $P$ $≈$ "I know of an invariant that owns $P$"
• A special resource: the physical state
  $\ownPhys{\state} ≈$ "I own the physical state $\state$, exclusively"