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 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 singlylinked list assuming “release-acquire” semantics. Although releaseacquire 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. Categories and Subject Descriptors...

• Type: Journal
• Year: 2015
• Where: PLDI
• Authors: Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis
• Keywords: PLDI 2015, Programming Languages