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.



Coq proofs

Related projects

Imprint | Data protection