Concurrent Program Logics

Program logics are formal systems for reasoning about the correctness of software. In the context of the ADVENT project, we have developed a number of program logics for concurrent programs.

• CaReSL is a logic that can reason about the refinement of concurrent higher-order programs. It has been used to manually verify a number of intricate concurrent algorithms, including a flat-combining stack.


• Relaxed Separation Logic (RSL) was the first program logic that could reason about concurrent programs interfacing the C/C++11 weak memory model. Formally, it is an adaptation of concurrent separation logic to this setting with appropriate rules enabling ownership transfer along release-acquire synchronization. (The soundness of the logic is proved in Coq and is available at the previous link.)


• GPS is a more advanced program logic for the release-acquire fragment of the C/C++ weak memory model that incorporates some important ideas from CaReSL, namely ghost state and protocols. It has been used to verify a number of algorithms under the release-acquire model, including a version of the read-copy-update (RCU) synchronization mechanism. (The soundness proof in Coq and details of the RCU verification are available at the previous link.)


• Fenced Separation Logic (FSL) in a conservative extension of RSL that can also handle synchronization arising because of C/C++ fence instructions. (The soundness of FSL is also proved in Coq and is available at the previous link.)


• OGRA is an adaptation of the Owicki-Gries proof system to release-acquire consistency. Unlike the previous logics, it does not support separate conjunction, but is nevertheless useful for verification. It has also been used to verify a different variant of the RCU synchronization mechanism.


• LogicCAL is a stylized form of rely/guarantee logic aimed at verifying concurrency-aware linearizability. The logic was use to provide the first modular proof of an elimination-based concurrent stack.


• Finally, we have also developed a protocol-based logic for concurrent programs running under the x86-TSO memory model and have implemented it in the Verifast verification tool. [Read more]