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:

Other relaxed program logics