Owicki-Gries Reasoning for Weak Memory Models
Ori Lahav and Viktor Vafeiadis
Max Planck Institute for Software Systems (MPI-SWS)
We show that even in the absence of auxiliary variables, the well-known Owicki-Gries method for verifying concurrent programs is unsound for weak memory models. By strengthening its non-interference check, however, we obtain a sound program logic for reasoning about programs in the release-acquire fragment of the C11 memory model, which we call OGRA (Owicki-Gries for Release-Acquire). We demonstrate the usefulness of our logic by applying it to several challenging examples, ranging from small litmus tests to an implementation of the RCU synchronization primitives.
More information can be found in the following paper:
-
Ori Lahav and Viktor Vafeiadis.
Owicki-Gries Reasoning for Weak Memory Models.
In ICALP 2015: 41st International Colloquium on Automata, Languages, and Programming, Track B.
[Full paper] [Slide showing OG unsoundness]