# Strong Logic for Weak Memory

## Reasoning About Release-Acquire Consistency in Iris

1. Jan-Oliver Kaiser
2. Hoang-Hai Dang
3. Derek Dreyer
4. Ori Lahav

http://plv.mpi-sws.org/igps/

# What is Iris?

Language-independent higher-order separation logic framework
with simple foundations for modular reasoning

# 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

• 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

 x := 0; y := 0 x[na] := 37y[at] := 1 repeat (!y[at])!x[na]

# 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

# Iris: Fictional Separation

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

# Iris: Heap with Fictional Separation

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

# What is RSL?

RSL is a logic for message passing in Release-Acquire.

Main Ingredients: $\color{alert}\Rel\loc\pred$ and $\color{alert}\Acq\loc\pred$

$$\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}$

 x := 0; y := 0 $\left\{ x \pointsto 0 ∗ \Rel{y}\pred \right\}$ x[na] := 37 $\left\{ x \pointsto {\color{hblue}37} ∗ \Rel{y}\pred \right\}$ y[at] := 1  $\left\{ \Rel{y}\pred \right\}$ $\left\{ \Acq{y}\pred \right\}$ repeat (!y[at]) $\left\{ \Acq{y}{{\color{hblue}\top}} ∗ x \pointsto 37 \right\}$ !x[na] $\left\{\Ret{z}. z = 37 ∗ %\Acq{y}\top ∗ x \pointsto 37 \ldots \right\}$

# Challenge: How to Deal With Views?

## Truth is relative to a thread's view.

Idea: Encode RSL assertions as predicates on views.

$\interp{\hoare{}{\pre}{\expr}{\post}{}}(\view) \eqdef\\ \qquad\qquad\qquad\forall \thread. \hoareV{t}{{\color{alert}\seen\thread\view} ∗ \interp\pre(\view)}{\expr, \thread}{{\color{alert}\exists \view' \futv \view. \seen\thread{\view'}} ∗ \interp\post(\view')}{}$

## Frame

 $\hoare{t}{\seen\thread\view ∗ \interp\pre(V)}{\expr, \thread}{\exists \view' \futv \view. \seen\thread{\view'} ∗ \interp\post(\view')}{}$ $\hoare{t}{\color{hblue}\seen\thread\view ∗ \interp\pre(V)}{\expr, \thread}{\color{hblue}\exists \view' \futv \view. \seen\thread{\view'} ∗ \interp\post(\view')}{}$ $\hoare{t}{\color{hblue}\seen\thread\view ∗ \interp\pre(V)}{\expr, \thread}{\color{hblue}\exists \view' \futv \view. \seen\thread{\view'} ∗ \interp\post(\view')}{}$ $\interp{\hoare{}{\pre}{\expr}{\post}{}}(\view)$ $\interp{\hoare{t}{\propC ∗ \pre}{\expr}{\post ∗ \propC}{}}(\view)$ $\hoare{t}{\interp\propC(\view) ∗ \seen\thread\view ∗ \interp\pre(V)}{\expr, \thread}{ \exists \view' \futv \view. \seen\thread{\view'} ∗ \interp\post(\view') ∗ \interp\propC(\view') }{}$ $\hoare{t}{ \interp\propC({\color{hred} \view}) ∗ {\color{hblue}\seen\thread\view ∗ \interp\pre(V)}}{\expr, \thread}{ {\color{hblue}\exists \view' \futv \view. \seen\thread{\view'} ∗ \interp\post(\view')} ∗ \interp\propC({\color{hred}\view'}) }{}$

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

Use monotone predicates on views.

# View-monotone predicates

$\interp{\hoare{}{\pre}{\expr}{\post}{}}({\color{hred}\view_0}) \eqdef\\ \qquad\qquad\forall \thread, {\color{hred}\view \futv \view_0}. \hoareV{t}{{\seen\thread\view} ∗ \interp\pre(\view)}{\expr, \thread}{{\exists \view' \futv \view. \seen\thread{\view'}} ∗ \interp\post(\view')}{}$

# Difference to C11

 x := 0 $\ecas\var{0}{1}$ $\ewrite\at\var{2}$; $\eread\na\var$

## GPS-Write

$\forall \prtst' \futst \prtst. \pre ∗ \prot(\prtst', \_) \implies \prtst'' \futst \prtst'$
$\pre \implies \prot(\prtst'', \val) ∗ \post$
$\{$$\loc:\prtst$$\prot$${} ∗ \pre \} \; \ewrite\at\loc\val \; \{$$\loc$:$\prtst''$$\prot$${} ∗ \post\}$

## iGPS-SW-Write

$\pre ∗{}$$\loc:\prtst''$$\prot$${}_W$${}∗ \prot(\prtst, \_) \implies \prtst'' \futst \prtst ∗ \prot(\prtst'', \val) ∗ \post$
$\{$$\loc:\prtst$$\prot$${}_W$${} ∗ \pre \} \; \ewrite\at\loc\val \; \{$$\loc:\prtst''$$\prot$${}_R$${} ∗ \post\}$

# 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"