Verifying read-copy-update in a logic for weak memory
Abstract
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jun 03, 2015
- Source ID
- 10.1145/2813885.2737992
Entities
People
- Derek Dreyer
- Joseph Tassarotti
- Viktor Vafeiadis
Organizations
- Air Force Office of Scientific Research
- Carnegie Mellon University
- Max Planck Institute for Software Systems
- United States Department of Defense