*Relaxed separation logic* (RSL) is a program logic for reasoning about
concurrent programs running under the C11 relaxed memory model. From a
user's perspective, RSL is an extension of *concurrent separation logic*
(CSL) with proof rules for the various kinds of C11 atomic accesses. As in CSL,
individual threads are allowed to access *non-atomically* only the memory that
they own, thus preventing data races.
Similar to CSL, however, ownership can be transferred via certain atomic accesses.
The difference is that RSL restricts the direction in which ownership can be transfered.
Ownership can be transfered away using *release* atomic accesses
and gained using *acquire* atomic accesses.
In contrast, no ownership transfer is possible with *relaxed* atomic accesses.

- Viktor Vafeiadis and Chinmay Narayan.

Relaxed separation logic: A program logic for C11 concurrency.

In OOPSLA 2013. ACM, 2013.

[Slides]

**Erratum:**In Section 6, we claim that the program in Figure 13 can print an arbitrary value less than 20 in C11. This is true for the Batty et al. (2011) formalization of C11, but not according to paragraphs 29.3p9-10 of the C standard. (Thanks to Brian Demsky for alerting us of this issue.)

- At POPL'14, 20 January 2014

[Slides (90min)] - At the UPMARC Summer School 2014, 28-29 July 2014

[Slides (1st lecture, Monday 2014-07-28, 90min)]

[Slides (2nd lecture, Tuesday 2014-07-29, 90min)]

- Browse the online documentation [proofs hidden] [proofs visible]
- Download the Coq 8.5 proofs: [rsl-1.1.zip]