Seminar 2017-09-20

Date: 2017-09-20
Time: 11:00-12:00
Speaker: Elias Castegren

Title: Relaxed Linear References for Lock-Free Data Structures

Abstract

The increasing importance of parallel and concurrent programming has rejuvenated interest in systems that statically control the use of shared mutable state in order to guarantee properties such as data-race freedom. This control is commonly achieved by banning concurrent access to mutable state altogether, either through isolation
(e.g., ownership types), synchronisation (e.g., by enforcing correct usage of locks), immutability (e.g., read-only references), or uniqueness (e.g., linear references).

Banning shared mutable state simplifies reasoning about concurrent programs—for programmers as well as for optimizing compilers—but it is too strong a restriction for many applications. Notably, lock-free algorithms, which implement protocols that ensure safe, non-blocking concurrent access to data structures, generally rely on shared mutable state to achieve lock-freedom.

This presentation details the work on LOLCAT, a type system that allows an unbounded number of aliases to a shared mutable resource, as long as at most one alias at a time owns the right to access the contents of the resource. This ownership can be transferred between aliases, but can never be duplicated. LOLCAT types are flexible enough to type several lock-free data structures, but also powerful enough to give a compile-time guarantee of absence of data-races when accessing owned data. In articular, LOLCAT is able to assign meaningful types to the CAS (compare and swap) primitive that precisely describe how ownership is transferred across aliases, possibly across different threads.

Bio

Elias Castegren is currently finishing his PhD with Tobias Wrigstad at Uppsala University. His research interests are type systems for concurrent and parallel programming, as well as the implementation of languages using these type systems. When he isn’t statically preventing data-races, Elias conducts and composes music for choirs. He is urrently looking for a postdoc position! More info: https://eliasc.github.io/