Verifying Read-Copy-Update in a Logic for Weak Memory

Joseph Tassarotti, Derek Dreyer, and Viktor Vafeiadis

Read-Copy-Update (RCU) is a technique for letting multiple readers safely access a data structure while a writer concurrently modifies it. It is used heavily in the Linux kernel in situations where fast reads are important and writes are infrequent. Optimized implementations rely only on the weaker memory orderings provided by modern hardware, avoiding the need for expensive synchronization instructions (such as memory barriers) as much as possible.

Using GPS, a recently developed program logic for the C/C++11 memory model, we verify an implementation of RCU for a singly-linked list assuming "release-acquire" semantics. Although release-acquire synchronization is stronger than what is required by real RCU implementations, it is nonetheless significantly weaker than the assumption of sequential consistency made in prior work on RCU verification. Ours is the first formal proof of correctness for an implementation of RCU under a weak memory model.

More information can be found in the following paper:

• 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 paper with the appendix] [Video abstract]

The Coq formalization of GPS with exchanges can be found at the GPS page.