Write a Blog >>
Fri 23 Jun 2017 10:30 - 10:55 at Auditorium, Vertex Building - Types and Effects Chair(s): Philipp Haller

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

ecoop-2017-papers
10:30 - 12:10: ECOOP Research Papers - Types and Effects at Auditorium, Vertex Building
Chair(s): Philipp HallerKTH Royal Institute of Technology
ecoop-2017-papers10:30 - 10:55
Talk
Elias CastegrenUppsala University, Tobias WrigstadUppsala University
Link to publication Media Attached
ecoop-2017-papers10:55 - 11:20
Talk
Colin GordonDrexel University
Link to publication Pre-print Media Attached
ecoop-2017-papers11:20 - 11:45
Talk
Edlira KuciTU Darmstadt, Germany, Sebastian ErdwegTU Delft, Oliver BračevacTU Darmstadt, Andi BejleriTU Darmstadt, Germany, Mira MeziniTU Darmstadt
Link to publication Media Attached
ecoop-2017-papers11:45 - 12:10
Talk
Alceste ScalasImperial College London, Ornela DardhaUniversity of Glasgow, Raymond HuImperial College London, Nobuko YoshidaImperial College London
Link to publication Media Attached