Strong Logic for Weak Memory

Reasoning About Release-Acquire Consistency in Iris

Jan-Oliver Kaiser
Hoang-Hai Dang
Derek Dreyer
Ori Lahav
Viktor Vafeiadis

http://plv.mpi-sws.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.

let me make this more concrete with an example. we are looking at two threads using locations x and y which are both initially zero. thread 1 will write to x and reading the value of y into local variable a. Conversely, thread 2 will write to y and read x into b. If were to imagine the possible interleavings, you would come to the conclusion that the outcome a equal to b equal to 0 is impossible. so this behaviour is forbidden in sequential consistent memory models. In almost all weak memory models, however, the behaviour is allowed. The two threads might simply not see each others writes quickly enough.

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 →

Non-Atomics

Relaxed

Release-Consume

Sequential Consistency

— Performance →

The C11 memory model offers two different kinds of accesses. The first kind are the so called non-atomic accesses, which you can think of as "normal" data accesses. this is the default memory access you get when you access memory and they are *not* threadsafe. Racing on these accesses leads to undefined behavior. Secndonly, C11 offers four different modes of atomic accesses. These are threadsafe and can safely be raced on. They range from the very performant but barely synchronizing relaxed accesses to the strongly synchronizing but very expensive sequentially consistent ones. We target the release-acquire fragment, which sits firmly in the middle between the two extremes. Release-Acquire is an important part of the model because it is much more performant than the SC fragment and still allows useful synchronization patterns to be implemented, like the so called message passing idiom which I will show you now.

Release-Acquire: 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]	non-atomic access
y_[rel]	atomic release write
y_[acq]	atomic acquire read

In the message passing example, we want to pass a message, specifically the value 37, from thread 1 to thread 2. naive attempt at; 2 problems: no guarantee to find 37; no guarantee at all because racy. to fix this, we make use of the release-acquire fragment of C11. first introduce synchronization variable y. after writing to x, the first thread will set y to 1 with a so called release write to signal the second thread that it is now okay to read from x. the second thread waits for the signal by repeatdly performing so called acq reads until it sees a value of 1. when the acquire read reads from the release write, the second thread synchronizes with the first thread. this guarantees that the non-atomic read from x in the second happens after the non-atomic write in the first thread. this means that the accesses do not race AND that the read will return 37. Now that we have an intuition for release-acquire it is natural to ask how go from that to a systematic, formal method for reasoning about..

Challenge:
How can we formally reason about programs that use Release-Acquire + Non-Atomics?

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.

there have been two program logics that target these kind of programs and these logics have been useful in verifying a variety of programs. *But* both logics are based on the original C11 memory model which is defined by axiomatic semantics. This means that non-standard proof techniques were necessary to establish soundness. As a result, the logics suffer from several drawbacks: - standard features like ghost state are missing or were extremely hard to proof sound, for example, ghost state - a major feature of standard separation logic was missing in RSL and it was a major advance in GPS that it supported ghost state at all. - the soundness proofs are hard to understand, extend, adapt to other memory models - the soundness proofs are very non-standard and it's not obvious that you can compose proofs done in one logic with proofs done in the other or whether you can compose these proofs with proofs done in future logics. - while the soundness of the lgoics themselves was mechanized in coq, there was no support for somebody who wnats to use this logics to mechanize proofs done in these logics. (— a feature supported by some modern program logics.) transition: our solution to all these drawbacks is to use iris.

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 Release-Acquire + Non-Atomics

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., higher-order ghost state)
Extensible & composable logics:
- Both logics derived from a common base logic.
Mechanized verification of programs using the Iris Proof Mode

in particular, we show that we can derive logics which we call iRSL and IGPS which have all the befenits of the original RLS and GPS but additionally they fix the four problems i mentioned on the prvious slide. (1) the soundness proofs are considerably simpler - they are just proofs in separation logic. by virtue of working in the iris framework these logics inherit useful features from iris, like higher-ghost state, for free. our approach also yields extensible logics that can safely be combined. we do this by introducing a common base logic from which both higher-level logics are derived. Finally, for the first time we can now support mechanized verfication of programs by using the iris proof mode. Pause and Drink now that I've told you about the advantages of this approach, let me show you how we did it.

Roadmap

Operational Release-Acquire: Message Passing

x := 0; y := 0
x_[na] := 37 y_[rel] := 1	while (y_[acq] == 0){} a := x_[na]

Write Event
Thread #1 View
Thread #2 View

$\View \eqdef \Loc \rightarrow \Time$

The operational semantics has two key ingredients: (1) a set of write events for each location we keep all write events to all locations as they could still potentially be read by some thread. (2) one so-called "view" for each thread, which records the most recent message of every location observed by the thread. this view indicates which write events are "available" to be read from: the thread can read everyting to the right of the view, including the most recent message the thread has seen. everyting to the left is off-limits. initially, both threads views agree on the most recent write to x and y. The 2nd thread will not be able to make any progress on its own so we focus on thread number 1 first. thread 1 performs its non-atomic write with value 37 to x, which is promptly recorded as a new message. thread 1 then performs the release write, which demonstrates a key feature of the semantics: the view of thread 1 is recorded in the message. we call this view the release view of the write event. at this point, thread 2 can make progress. as soon as it reads a value of 1 from y, it will acquire the release view and incorporate into its own view, thereby achieving synchronization. thread 2 now has only one write event to x to read from and thus, a will have value 37. Now that I've introduced the operational semantics, let's look at our roadmap.

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 Release-Acquire with a
single-location 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)}{}$$

What is RSL? RSL is a program logic for the message passion idiom in release-acquire. It makes uses of single-location invariants. Its key ingredients are the release and the acquire assertions, indexed by location l and by a predicate Q which restricts the values written to l. The Release assertion signifies the permission to perform writes to the location. And we can see here in the rule for atomic writes that we have to provide both the release assertion as well as the precidate Q for the value v which we want to write. Conversely, Acquire is the permission to read and we see in the read rule that we are provided with the predicate Q for a, which is the result of our read. This way, the ownership flows from the release write to the acquire read. Let's revisit our message passing example again to see what the proof looks like in RSL.

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!

Here's the example again, with some convenient extra space. We start by defining our predicate Q. It has three cases: initially, the predicate is trivially satisfied. once we write 1 to it, the predicate will get ownership of the non-atomic location with value 37. in all other cases the predicate is unsatisfiable — those cases will never happen in our program. And here's the proof: We give the permission to perform writes on location y to the first thread, and the permission to read to the second. the first thread also gets ownership of location x. it writes non-atomically and then uses the Rel assertion to perform a write to y. to do this, it moves ownership of x into the invariant. when the second thread reads non-zero value from y, it will receive ownership of location x with value 37. the subsequent read from x is now guaranteed to return that value and that completes the proof. This is a beatufiul proof why? no views. Let's change gears and look at the encoding of RSL.

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

Originally RSL is a stand-alone logic. We encode it on top of the base logic. To do that, we model the original RSL assertions as monotone view predicates. why? because they should be stable under taking any step in the opsem. Most of the encoding is defined in straight-forward structural way, for example the encoding of the separating conjunction. The encoding of hoare triples demonstrates how we make use of the Seen assertion I introduced earlier to give meaning to these RSL triples in our base logic. I don't have a lot of time to talk about this so if you want to know more I recommend to look into the paper. in addition to RSL this encoding also works for, its successor GPS.

GPSOOPSLA'14

We also encode GPS — with very useful extensions.

Highlight

Very strong write rule for programs without write-write races:
the single-writer rule.

Write-write 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, Michael-Scott queue, …
- Read-Copy-Update algorithm (used in linux kernel)

All verified in Coq

Backup Slides

Difference to C11

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

GPS Write Rule

GPS-Write

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

iGPS-SW-Write

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