Verifiable C is a useful tool for proving correctness of C programs, including lock-based concurrent programs. But surprisingly, the straightforward extension of separation logic to concurrency is not strong enough to prove interesting properties of concurrent programs: we cannot even prove that 1 + 1 = 2! The standard solution to this problem is to add ghost state, which allows threads to remember information about shared state. In this talk, I will explain the general mechanism of ghost state in concurrent separation logic, and show how it turns CSL’s local reasoning into a technique for proving global properties like linearizability. With the recent addition of ghost state to VST, we can now prove the correctness of C implementations of concurrent data structures.

Tue 19 Jun

14:00 - 15:40: DeepSpec 2018 - Concurrency and Concurrent Operating Systems at Columbus Ballroom B
deepspec-2018-papers14:00 - 14:30
Jieung KimYale University, USA
deepspec-2018-papers14:30 - 15:00
Thomas SewellUNSW, Australia
deepspec-2018-papers15:00 - 15:30
William ManskyPrinceton University