License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2017.6
URN: urn:nbn:de:0030-drops-72670
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7267/
Go to the corresponding LIPIcs Volume Portal

Castegren, Elias ; Wrigstad, Tobias

Relaxed Linear References for Lock-free Data Structures

pdf-format:
LIPIcs-ECOOP-2017-6.pdf (2 MB)

Abstract

Linear references are guaranteed to be free from aliases. This is a strong property that simplifies reasoning about programs and enables powerful optimisations, but it 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. 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 across 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.

BibTeX - Entry

@InProceedings{castegren_et_al:LIPIcs:2017:7267,
  author =	{Elias Castegren and Tobias Wrigstad},
  title =	{{Relaxed Linear References for Lock-free Data Structures}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{6:1--6:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{Peter M{\"u}ller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7267},
  URN =		{urn:nbn:de:0030-drops-72670},
  doi =		{10.4230/LIPIcs.ECOOP.2017.6},
  annote =	{Keywords: Type systems, Concurrency, Lock-free programming}
}

Keywords: Type systems, Concurrency, Lock-free programming
Collection: 31st European Conference on Object-Oriented Programming (ECOOP 2017)
Issue Date: 2017
Date of publication: 16.06.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI