Strong Logic for Weak Memory
Reasoning About ReleaseAcquire Consistency in Iris
 JanOliver Kaiser
 HoangHai Dang
 Derek Dreyer
 Ori Lahav
 Viktor Vafeiadis
http://plv.mpisws.org/igps/
Weak Memory is
different threads
observing
memory events
in
different orders
Weak Behaviour: Store Buffering Example
x := 0; y := 0 
x := 1
a := y

y := 1 b := x

Is $\;a = b = 0\;$ allowed?
 Forbidden in sequentially consistent (SC) models
 Allowed in (almost) all weak memory models:
the threads have not observed each other's writes.
Weak Memory Is Ubiquitous
 All multicore hardware exhibits weak memory behaviors
 Preserving the fiction of SC requires synchronization barriers
 Languages now expose weak memory accesses to satisfy programmers' demand for performance (C/C++, Java)
Our Focus: The C/C++11 Memory Model
The C11 Memory Model
— Synchronization →

NonAtomics
Relaxed
ReleaseConsume
Sequential Consistency

— Performance →

ReleaseAcquire: Message Passing
x := 0; y := 0 
x_{[na]} := 37
y_{[rel]} := 1

while (y_{[acq]} == 0){} a := x_{[na]}
// a = 37

a  local variable/register 
x_{[na]}  nonatomic access 
y_{[rel]}  atomic release write 
y_{[acq]}  atomic acquire read 
Challenge:
How can we formally reason about programs that use ReleaseAcquire + NonAtomics?
Program Logics for C11 RA+NA
 Relaxed Separation Logic (RSL) OOPSLA'13
 Ghosts, Protocols, and Separation (GPS) OOPSLA'14
Soundness proofs based on axiomatic semantics

Unable to use standard program logic machinery.
 Difficult to add standard features (i.e., ghost state).
 Hard to extend, adapt to other models, compose, etc.
 No support for mechanized proofs of programs.
What About Using Iris?
We would like to use IrisPOPL'15, ICFP'16, POPL'17, ESOP'17:
 a framework for deriving advanced concurrent program logics
 and using them to verify programs in Coq.
However,
 Iris assumes interleaving semantics…
 … whereas C11 provides axiomatic semantics
We develop
interleaving semantics for C11 ReleaseAcquire + NonAtomics
and derive and extend
RSL & GPS in Iris
iRSL & iGPS — RSL & GPS on Top of Iris
 Simpler soundness proofs:
 Proofs in standard concurrent separation logic
 Free advanced features from Iris (e.g., higherorder ghost state)
 Extensible & composable logics:
 Both logics derived from a common base logic.
 Mechanized verification of programs using the Iris Proof Mode
Roadmap
Roadmap
Operational ReleaseAcquire: Message Passing
x := 0; y := 0 
x_{[na]} := 37 y_{[rel]} := 1
 while (y_{[acq]} == 0){} a := x_{[na]} 
$\View \eqdef \Loc \rightarrow \Time$
Roadmap
The Base Logic
Two essential assertions:

Location ownership with write events $\hist$: $\; \lhist\loc\hist$
(Similar in flavor to $\loc \pointsto \val$ in standard separation logic.)
 Thread views: $\seen\thread\view$
Base Logic: Atomic Read
$
%\PSCtx \entails
\hoareV{t}{
\seen\thread\view ∗ \lhist\loc\hist
%∗
%\init\hist\view
}{
a := \eread\acq\loc % \quad {\color{grey} @\;\thread}
}{
\begin{array}{l}%
%\Ret\val.
%\exists \view_1.
%\exists \view' \futv \view \sqcup \view_1.
%\exists \ts \ge \view(\loc).
\exists (\val, \ts, \view_1) \in \hist.
a = \val
∗ \ts \ge \view(\loc)
\\
\quad{}∗
\seen\thread{\view \sqcup \view_1} ∗ \lhist\loc\hist
\end{array}
}{}
$
(where $\thread$ is the thread performing the read.)
Base Logic: Message Passing
x := 0; y := 0 
x_{[na]} := 37 y_{[rel]} := 1
 while (y_{[acq]} == 0) {} a := x_{[na]} 
RSL: Relaxed Separation Logic
RSLOOPSLA'13: Message passing in ReleaseAcquire with a
singlelocation invariant
${\color{alert}\pred : \Val \rightarrow \textrm{Prop}}$
.
$\color{notgreen}\Rel\loc\pred$: permission to write to $\loc$ by releasing $\pred(\val)$
$\color{hred}\Acq\loc\pred$: permission to read from $\loc$ and acquire $\pred(\val)$
$$\hoare{}{\top}{\ealloc}{\Ret\loc. {\color{notgreen}\Rel\loc\pred} ∗ {\color{hred}\Acq\loc\pred}}{}$$
$$\hoare{}{{\color{notgreen}\Rel\loc\pred} ∗ \color{alert}\pred(\val)}{\ewrite\rel\loc\val}{{\color{notgreen}\Rel\loc\pred}}{}$$
$$\hoare{}{{\color{hred}\Acq\loc\pred}}{a := \eread\acq\loc}{{{\color{hred}\Acq\loc{{\Fupd\pred[a\! >\!\top]}}}} ∗ \color{alert}\pred(a)}{}$$
Message Passing in RSL
x := 0; y := 0 
$\left\{
{\color{notgreen}\Rel{y}\pred} ∗ x \pointsto 0
\right\}$
x_{[na]} := 37
$\left\{
{\color{notgreen}\Rel{y}\pred} ∗ x \pointsto {\color{hblue}37}
\right\}$
y_{[rel]} := 1
$\left\{
%\Rel{y}\pred
\top
\right\}$

$\left\{
{\color{hred}\Acq{y}\pred}
\right\}$
while (y_{[acq]} == 0) {}
$\left\{
%\Acq{y}{{\Fupd\pred[1 > \top]}} ∗
x \pointsto 37
\right\}$
a := x_{[na]}
$\left\{a = 37
% ∗
%\Acq{y}\top ∗ x \pointsto 37
%\ldots
\right\}$

$$\hoare{}{{\color{notgreen}\Rel\loc\pred} ∗ \color{alert}\pred(\val)}{\ewrite\rel\loc\val}{{\color{notgreen}\Rel\loc\pred}}{}$$
$$\hoare{}{{\color{hred}\Acq\loc\pred}}{a := \eread\acq\loc}{{{\color{hred}\Acq\loc{{\Fupd\pred[a\! >\!\top]}}}} ∗ \color{alert}\pred(a)}{}$$
$
{\color{alert}\pred(\val)} = \begin{cases}
\top & \mbox{ if } \val = 0 \\
x \pointsto 37 & \mbox{ if } \val = 1 \\
\bot & \mbox{ otherwise }
\end{cases}$
Look, no views!
Encoding RSL Assertions
We encode RSL assertions as
monotone view predicates in Iris.
 $\interp{\cdot}({\color{hred}\cdot}) :$ $\textrm{RSLAssertion} \rightarrow {\color{hred}\View} \stackrel{\textrm{mon}}{\rightarrow} \textrm{IrisAssertion}$
 $\interp{P ∗ Q}({\color{hred}\view_0}) \eqdef \interp{P}({\color{hred}\view_0}) ∗ \interp{Q}({\color{hred}\view_0)}$
 …

$\interp{\hoare{}{\pre}{\expr}{\post}{}}({\color{hred}\view_0}) \eqdef\\
\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')}{}$
GPSOOPSLA'14
We also encode GPS — with very useful extensions.
Highlight
Very strong write rule for programs without writewrite races:
the singlewriter rule.
 Writewrite races are very rare in examples.
 Our rule simplifies proofs dramatically.
 Iris makes prototyping such rules very easy.
What Else is in the Paper?
 Model of iRSL/iGPS assertions as monotone view predicates
 Allocation and Deallocation
 Additional useful extensions to both RSL and GPS
 Examples from previous work
 Circular Buffer, Bounded Ticket Lock, MichaelScott queue, …
 ReadCopyUpdate algorithm (used in linux kernel)
All verified in Coq
© Lilia Anisimova
Difference to C11
x := 0 
$\ecas\var{0}{1}$

$\ewrite\rel\var{2}$;
$\eread\na\var$

GPS Write Rule
GPSWrite
$\forall \prtst' \futst \prtst. \pre ∗ \prot(\prtst', \_) \implies \prtst'' \futst \prtst'$
$\pre \implies \prot(\prtst'', \val) ∗ \post$

$\{$$\loc$:$\prtst$$\prot$${} ∗ \pre \}
\; \ewrite\rel\loc\val
\; \{$$\loc$:$\prtst''$$\prot$${} ∗ \post\}$

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

$\{$$\loc$:$\prtst$$\prot$_{${}_W$}${} ∗ \pre \}
\; \ewrite\rel\loc\val
\; \{$$\loc$:$\prtst''$$\prot$_{${}_R$}${} ∗ \post\}$
