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.