uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • 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
Types for CAS: Relaxed Linearity with Ownership Transfer
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: Article in journal (Other academic) Submitted
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 shows how LOLCAT can be used to implement synchronisation primitives like locks, and discusses a prototype implementation which integrates LOLCAT with an object-oriented programming language.

Place, publisher, year, edition, pages
2017.
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:uu:diva-336019OAI: oai:DiVA.org:uu-336019DiVA, id: diva2:1164764
Available from: 2017-12-11 Created: 2017-12-11 Last updated: 2018-01-13
In thesis
1. Capability-Based Type Systems for Concurrency Control
Open this publication in new window or tab >>Capability-Based Type Systems for Concurrency Control
2018 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Since the early 2000s, in order to keep up with the performance predictions of Moore's law, hardware vendors have had to turn to multi-core computers. Today, parallel hardware is everywhere, from massive server halls to the phones in our pockets. However, this parallelism does not come for free. Programs must explicitly be written to allow for concurrent execution, which adds complexity that is not present in sequential programs. In particular, if two concurrent processes share the same memory, care must be taken so that they do not overwrite each other's data. This issue of data-races is exacerbated in object-oriented languages, where shared memory in the form of aliasing is ubiquitous. Unfortunately, most mainstream programming languages were designed with sequential programming in mind, and therefore provide little or no support for handling this complexity. Even though programming abstractions like locks can be used to synchronise accesses to shared memory, the burden of using these abstractions correctly and efficiently is left to the programmer.

The contribution of this thesis is programming language technology for controlling concurrency in the presence of shared memory. It is based on the concept of reference capabilities, which facilitate safe concurrent programming by restricting how memory may be accessed and shared. Reference capabilities can be used to enforce correct synchronisation when accessing shared memory, as well as to prevent unsafe sharing when using more fine-grained concurrency control, such as lock-free programming. This thesis presents the design of a capability-based type system with low annotation overhead, that can statically guarantee the absence of data-races without giving up object-oriented features like aliasing, subtyping and code reuse. The type system is formally proven safe, and has been implemented for the highly concurrent object-oriented programming language Encore.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2018. p. 106
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1611
Keywords
Programming languages, Type Systems, Capabilities, Concurrency, Parallelism, Data-Race Freedom, Lock-Free Data Structures, Object-Oriented Programming, Actors, Active Objects, Object Calculi, Semantics
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-336021 (URN)978-91-513-0187-7 (ISBN)
Public defence
2018-02-09, sal 2446, ITC, Lägerhyddsvägen 2, hus 2, Uppsala, 13:15 (English)
Opponent
Supervisors
Available from: 2018-01-10 Created: 2017-12-12 Last updated: 2018-03-07

Open Access in DiVA

No full text in DiVA

Authority records BETA

Castegren, EliasWrigstad, Tobias

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 43 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • 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