GPS: Navigating Weak Memory with
Ghosts, Protocols, and Separation
Weak memory models formalize the inconsistent behaviors that one can expect to observe in multithreaded programs running on modern hardware. In so doing, however, they complicate the already-difficult task of reasoning about correctness of concurrent code. Worse, they render impotent the sophisticated formal methods that have been developed to tame concurrency, which almost universally assume a strong (i.e., sequentially consistent) memory model.
We introduce GPS, a program logic that provides a full-fledged suite of modern verification techniques—including ghost state, protocols, and separation logic—for high-level, structured reasoning about weak memory. We demonstrate the effectiveness of GPS by applying it to challenging examples drawn from the Linux kernel as well as lock-free data structures. We also define the semantics of GPS and prove in Coq that it is sound with respect to the axiomatic C11 weak memory model.
Aaron Turon, Viktor Vafeiadis, and Derek Dreyer.
GPS: Navigating weak memory with ghosts, protocols, and separation.
In OOPSLA 2014: ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, Portland, USA. ACM, 2014.
Joseph Tassarotti, Derek Dreyer, and Viktor Vafeiadis.
Verifying read-copy-update in a logic for weak memory.
In PLDI 2015: ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, USA. ACM, 2015.
[Full version] [More...]
Coq formalizationThe soundness proof of GPS has been formalized in Coq (latest version 1.7, released 2016-12-20).
- Download the formalization [gps-1.7.zip] [README.txt] [CHANGELOG.txt] [older versions]
- Browse the formalization online [proofs visible] [proofs hidden]
MD5 hashes for all the downloads can be found here.)
- OGRA: An Owicki-Gries proof system for release-acquire consistency.