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

Displayed time zone: Tijuana, Baja California change

14:00 - 15:40
VerificationResearch Papers at PLDI Main BLUE (Portland 254-255)
Chair(s): Zachary Tatlock University of Washington, Seattle
14:00
25m
Talk
Mechanized Verification of Fine-grained Concurrent Programs
Research Papers
Ilya Sergey IMDEA Software Institute, Aleksandar Nanevski IMDEA Software Institute, Anindya Banerjee IMDEA Software Institute
Link to publication Media Attached
14:25
25m
Talk
Verification of Producer-Consumer Synchronization in GPU Programs
Research Papers
Rahul Sharma Stanford University, Michael Bauer NVIDIA Research, Alex Aiken Stanford University
Media Attached
14:50
25m
Talk
Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO
Research Papers
Peter Gammie NICTA, Tony Hosking Australian National University, Data61, and Purdue University, Kai Engelhardt UNSW and NICTA
Link to publication Media Attached
15:15
25m
Talk
Verifying Read-Copy-Update in a Logic for Weak Memory
Research Papers
Joseph Tassarotti Carnegie Mellon University, Derek Dreyer MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany
Media Attached