Sciweavers

Share
PLDI
2015
ACM

Verifying read-copy-update in a logic for weak memory

4 years 12 months ago
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...
Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where PLDI
Authors Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis
Comments (0)
books