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

Read-Copy-Update (RCU) is a technique for letting multiple readers safely access a data structure while a writer concur-rently modifies it. It is used heavily in the Linux kernel in situations where fast reads are important and writes are infre-quent. 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 C11 weak memory model, we verify an implementation of RCU for a singly-linked list assuming “release-acquire” semantics. This is, to our knowledge, the first formal proof of an RCU implementation in a weak-memory setting. 1