GPS: Navigating Weak Memory with
Ghosts, Protocols, and Separation

Introduction

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.

Papers

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...]