Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Relaxed Linear References for Lock-free Data Structures
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.ORCID iD: 0000-0003-4918-6582
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
2017 (English)In: / [ed] Peter Müller, 2017, p. 47:1-47:31, article id 47Conference paper, Published paper (Refereed)
Abstract [en]

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. 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 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.

Place, publisher, year, edition, pages
2017. p. 47:1-47:31, article id 47
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-333668DOI: 10.4230/LIPIcs.ECOOP.2017.47OAI: oai:DiVA.org:uu-333668DiVA, id: diva2:1157340
Conference
European Conference on Object-Oriented Programming (ECOOP)
Projects
Structured AliasingUPSCALEUPMARC
Funder
Swedish Research CouncilEU, FP7, Seventh Framework Programme
Available from: 2017-11-15 Created: 2017-11-15 Last updated: 2018-01-13Bibliographically approved

Open Access in DiVA

fulltext(3551 kB)19 downloads
File information
File name FULLTEXT01.pdfFile size 3551 kBChecksum SHA-512
8f2459f9eb87ece90d91b408929a974b947f1f1c1daac6add97a603aa2186c7b9a072e05f28c530ec47575560497a4a4f4ada0f8f45eefef924450bfe0288c4b
Type fulltextMimetype application/pdf

Other links

Publisher's full texthttps://2017.ecoop.org/event/ecoop-2017-papers-relaxed-linear-references-for-lock-free-programming

Search in DiVA

By author/editor
Castegren, EliasWrigstad, Tobias
By organisation
Computing Science
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 19 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 40 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf