Local Reasoning for Read-Copy-Update

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.

Short bio

Resources

• talk slide