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.



Coq proofs

Related projects

Valid XHTML 1.0 Strict