DIKU IT-C RUC

COPLAS

Copenhagen Programming Language Seminar


Local Reasoning for Read-Copy-Update

Hongseok Yang
Queen Mary, University of London

Wednesday, October 29, 2008, 11:00-12:00
The IT University, Rued Langgaards Vej 7, DK-2300 Room 3A 08

Abstract:

Read-copy-update (in short, RCU) is a variant of reader/writer lock that allows a very efficient implementation of readers. In RCU, readers are allowed to access a shared data structure even when a writer is modifying the data structure. Furthermore, readers do not invoke any synchronization primitives, incurring almost zero synchronization overhead. Because of this benefit, RCU has gained popularity among Linux kernel developers. For instance, it is used in the System V IPC implementation, the lock-free IPv4 route cache and the lock-free lookup of directory entries in the dcache subsystem.

In this talk, I will describe our logic for RCU, which aims for local reasoning about heap-manipulating concurrent RCU programs. Two main challenges for achieving our aim are that (1) an RCU-protected shared data structure, such as a linked list, can be accessed by a writer and multiple readers at the same time, and (2) RCU implicitly lets a writer know when readers finish reading a part of data structure and it is safe to dispose the part. During my talk, I will explain how the idea of ownership in concurrent separation logic lets us handle these challenges, while avoiding complicated interference checks between readers and writers.

This is joint work with Peter O'Hearn, Matthew Parkinson, Noam Rinetzky, Mooly Sagiv and Viktor Vafeiadis.


Scientific host:Lars Birkedal Administrative host: Annette Enggaard. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org