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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Types and EffectsECOOP Research Papers at Auditorium, Vertex Building
Chair(s): Philipp Haller KTH Royal Institute of Technology
10:30
25m
Talk
Relaxed Linear References for Lock-free Programming
ECOOP Research Papers
Elias Castegren Uppsala University, Tobias Wrigstad Uppsala University
Link to publication Media Attached
10:55
25m
Talk
A Generic Approach to Flow-Sensitive Polymorphic Effects
ECOOP Research Papers
Colin Gordon Drexel University
Link to publication Pre-print Media Attached
11:20
25m
Talk
A Co-contextual Type Checker for Featherweight Java
ECOOP Research Papers
Edlira Kuci TU Darmstadt, Germany, Sebastian Erdweg TU Delft, Oliver Bračevac TU Darmstadt, Andi Bejleri TU Darmstadt, Germany, Mira Mezini TU Darmstadt
Link to publication Media Attached
11:45
25m
Talk
A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming
ECOOP Research Papers
Alceste Scalas Imperial College London, Ornela Dardha University of Glasgow, Raymond Hu Imperial College London, Nobuko Yoshida Imperial College London
Link to publication Media Attached