Mon 15 Jun 2015 15:15 - 15:40 at PLDI Main BLUE (Portland 254-255) - Verification Chair(s): Zachary Tatlock

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 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.

Mon 15 Jun

pldi2015-papers
14:00 - 15:40: Research Papers - Verification at PLDI Main BLUE (Portland 254-255)
Chair(s): Zachary Tatlock
pldi2015-papers14:00 - 14:25
Talk
Ilya SergeyIMDEA Software Institute, Aleksandar NanevskiIMDEA Software Institute, Anindya BanerjeeIMDEA Software Institute
Link to publication Media Attached
pldi2015-papers14:25 - 14:50
Talk
Rahul SharmaStanford University, Michael BauerNVIDIA Research, Alex AikenStanford University
Media Attached
pldi2015-papers14:50 - 15:15
Talk
Peter GammieNICTA, Tony HoskingAustralian National University, Data61, and Purdue University, Kai EngelhardtUNSW and NICTA
Link to publication Media Attached
pldi2015-papers15:15 - 15:40
Talk
Joseph TassarottiCarnegie Mellon University, Derek DreyerMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Media Attached