LOLCAT: Relaxed Linear References for Lock-free Programming

Elias Castegren and Tobias Wrigstad

July 2016

Abstract:

A linear reference is a reference guaranteed to be unaliased. This is a powerful property that simplifies reasoning about programs, but is also a property that is too strong for certain applications. For example, lock-free algorithms, which implement protocols to ensure safe concurrent access to data structures, are generally not typable with linear references as they involve sharing of mutable state.

This paper presents a type system with a relaxed notion of linearity that allows an unbounded number of aliases to an object as long as at most one alias at a time owns the right to access the contents of the object. This ownership can be transferred between aliases, but can never be duplicated.

The resulting language is flexible enough to express several lock-free algorithms and at the same time powerful enough to guarantee the absence of data-races when accessing owned data. The language is formalised and proven sound, and is also available as a prototype implementation.

Available as PDF (1.42 MB, no cover)

Download BibTeX entry.