Relaxed Linear References for Lock-free Programming
Linear references are guaranteed to be free from aliases. This is a strong property that simplifies reasoning about programs and enables powerful optimisation, but is also a property that is too strong for many applications. Notably, lock-free algorithms, which implement protocols that ensure safe, non-blocking concurrent access to data structures, are generally not typable with linear references because they rely on aliasing to achieve lock-freedom.
This paper presents LOLCAT, 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. LOLCAT types are powerful enough to type several lock-free data structures and give a compile-time guarantee of absence of data-races when accessing owned data.
In particular, LOLCAT is able to assign types to the CAS (compare and swap) primitive that precisely describe how ownership is transferred between aliases, possibly across different threads. The paper introduces LOLCAT through a sound core procedural calculus, and shows how LOLCAT can be applied to three fundamental lock-free data structures. It also discusses a prototype implementation which integrates LOLCAT with an object-oriented programming language.
Fri 23 Jun
|10:30 - 10:55|
|Link to publication Media Attached File Attached|
|10:55 - 11:20|
Colin GordonDrexel UniversityLink to publication Pre-print Media Attached
|11:20 - 11:45|
Edlira KuciTU Darmstadt, Germany, Sebastian ErdwegTU Delft, Oliver BračevacTU Darmstadt, Andi BejleriTU Darmstadt, Germany, Mira MeziniTU DarmstadtLink to publication Media Attached File Attached
|11:45 - 12:10|
Alceste ScalasImperial College London, Ornela DardhaUniversity of Glasgow, Raymond HuImperial College London, Nobuko YoshidaImperial College LondonLink to publication Media Attached File Attached