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. Ownership can, however, be transferred via certain atomic accesses. For SC-atomic accesses, arbitrary ownership transfer can occur; for acquire/release atomic accesses, ownership transfer can occur only in one direction; while for relaxed atomic accesses, no ownership transfer is possible.

- 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] (Earlier version working with Coq 8.4: [rsl-1.0.zip])