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.


Coq formalization

The soundness proof of GPS has been formalized in Coq (latest version 1.7, released 2016-12-20). (Excluding blank lines and standard libraries, the formalization is about 10KLOC.
MD5 hashes for all the downloads can be found here.)


Related projects

Valid XHTML 1.0 Transitional