@inproceedings{fff59696d4f247e88d15a212255ca8b1,
title = "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 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.",
keywords = "C/C++, Concurrency, Program logic, RCU, Separation logic, Weak memory models",
author = "Joseph Tassarotti and Derek Dreyer and Viktor Vafeiadis",
year = "2015",
month = jun,
day = "3",
doi = "10.1145/2737924.2737992",
language = "English (US)",
series = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",
publisher = "Association for Computing Machinery",
pages = "110--120",
editor = "Steve Blackburn and David Grove",
booktitle = "PLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation",
note = "36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015 ; Conference date: 13-06-2015 Through 17-06-2015",
}