\( \def\sc#1{\dosc#1\csod} \def\dosc#1#2\csod{{\rm #1{\small #2}}} \definecolor{hred}{RGB}{208,28,139} \definecolor{hblue}{RGB}{77,172,38} \definecolor{alert}{RGB}{235,129,27} \def\Ret#1.{#1.\;} \def\hoareV#1#2#3#4#5{ {\begin{aligned}[#1] &\left\{{#2}\right\} \\ &\quad{#3} \\ &\left\{{#4}\right\}_{#5} \end{aligned}}% }% \def\hoare#1#2#3#4#5{% \left\{{#2}\right\} \;{#3}\; \left\{{#4}\right\}_{#5} } \newcommand{\fpfnupd}[3]{#1\!\left[#2 \mapsto #3\right]} \def\Fupd#1[#2->#3]{\fpfnupd{#1}{#2}{#3}} \newcommand{\protAt}[3]{\mbox{$ \renewcommand{\arraystretch}{0.8} \begin{array}{|@{}l@{}|@{}l@{}|} %\firsthline% \hline% \;#1 : #2\;\; & \;#3\;\; \\ %\lasthline% \hline% \end{array}$}} \def\Proto[#1:#2|#3]{\protAt{#1}{#2}{#3}}% \newcommand\eqdef{\mathrel{\triangleq}} \newcommand{\always}{\Box{}} \def\implies{\Rightarrow} \)

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
  5. Viktor Vafeiadis




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

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

x := 0; y := 0
x[na] := 37
y[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

Roadmap

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:
    • ● $\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

$\PSCtx \entails \hoareV{t}{ \seen\thread\view ∗ \lhist\loc\hist ∗ \init\hist\view}{ \eread\at\loc, \thread }{ \begin{array}{l}% \Ret\val.\exists \view_1, \view' \futv \view \sqcup \view_1, \ts \ge \view(\loc). \\ \quad\seen\thread{\view'} ∗ \lhist\loc\hist ∗ (\val, \ts, \view_1) \in \hist \end{array} }{} $

Base Logic: Atomic Write

Base-AT-Write

$\PSCtx \entails \hoareV{t}{ \seen\thread\view ∗ \lhist\loc\hist ∗ \alloc\hist\view}{ \ewrite\at\loc\val, \thread }{ \begin{array}{l}% \exists \view \futv \view, \ts \ge \view(\loc), \hist' = h \uplus \{(\val, \ts, \view')\}. \\ \quad\seen\thread{\view'} ∗ \lhist\loc{\hist'} ∗ \init{\hist'}{\view'} \end{array} }{} $

Base Logic: Message Passing

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

Invariants:
  • ${\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?

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')}{}$

Backup Slides

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"