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
Capability-Based Type Systems for Concurrency Control
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computing Science. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.ORCID iD: 0000-0003-4918-6582
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 [en]
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: urn:nbn:se:uu:diva-336021ISBN: 978-91-513-0187-7 (print)OAI: oai:DiVA.org:uu-336021DiVA, id: diva2:1164769
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
List of papers
1. Reference Capabilities for Trait Based Reuse and Concurrency Control
Open this publication in new window or tab >>Reference Capabilities for Trait Based Reuse and Concurrency Control
2016 (English)Report (Other academic)
Abstract [en]

The proliferation of shared mutable state in object-orientedprogramming complicates software development as two seeminglyunrelated operations may interact via an alias and produceunexpected results. In concurrent programming this manifestsitself as data-races.

Concurrent object-oriented programming further suffers from thefact that code that warrants synchronisation cannot easily bedistinguished from code that does not. The burden is placed solelyon the programmer to reason about alias freedom, sharing acrossthreads and side-effects to deduce where and when to applyconcurrency control, without inadvertently blocking parallelism.

This paper presents a reference capability approach to concurrentand parallel object-oriented programming where all uses of aliasesare guaranteed to be data-race free. The static type of an aliasdescribes its possible sharing without using explicit ownership oreffect annotations. Type information can express non-interferingdeterministic parallelism without dynamic concurrency control,thread-locality, lock-based schemes, and guarded-by relationsgiving multi-object atomicity to nested data structures.Unification of capabilities and traits allows trait-based reuseacross multiple concurrency scenarios with minimal codeduplication. The resulting system brings together features from awide range of prior work in a unified way.

Series
Technical report / Department of Information Technology, Uppsala University, ISSN 1404-3203 ; 2016-007
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-309774 (URN)
Projects
Structured AliasingUpscaleUPMARC
Available from: 2016-12-07 Created: 2016-12-07 Last updated: 2018-01-13Bibliographically approved
2. Kappa: Insights, Current Status and Future Work
Open this publication in new window or tab >>Kappa: Insights, Current Status and Future Work
2016 (English)Conference paper, Oral presentation with published abstract (Refereed)
Abstract [en]

KAPPA is a type system for safe concurrent object-oriented program- ming using reference capabilities. It uses a combination of static and dynamic techniques to guarantee data-race freedom, and, for a certain subset of the system, non-interference (and thereby determin- istic parallelism). It combines many features from previous work on alias management, such as substructural types, regions, ownership types, and fractional permissions, and brings them together using a unified set of primitives.

In this extended abstract we show how KAPPA’s capabilities express variations of the aforementioned concepts, discuss the main insights from working with KAPPA, present the current status of the implementation of KAPPA in the context of the actor language Encore, and discuss ongoing and future work. 

Keywords
Type systems, Language Implementation, Capabilities, Traits, Concurrency, Object-Oriented
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-307137 (URN)
Conference
IWACO
Projects
Structured AliasingUpscaleUPMARC
Funder
EU, FP7, Seventh Framework Programme, FP7-612985
Available from: 2016-12-07 Created: 2016-11-09 Last updated: 2018-01-13Bibliographically approved
3. Types for CAS: Relaxed Linearity with Ownership Transfer
Open this publication in new window or tab >>Types for CAS: Relaxed Linearity with Ownership Transfer
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.

National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-336019 (URN)
Available from: 2017-12-11 Created: 2017-12-11 Last updated: 2018-01-13
4. Bestow and Atomic: Concurrent programming using isolation, delegation and grouping
Open this publication in new window or tab >>Bestow and Atomic: Concurrent programming using isolation, delegation and grouping
2018 (English)In: The Journal of logical and algebraic methods in programming, ISSN 2352-2208, E-ISSN 2352-2216, Vol. 100, p. 130-151Article in journal (Refereed) Published
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-336020 (URN)10.1016/j.jlamp.2018.06.007 (DOI)
Projects
UPMARC
Available from: 2018-06-30 Created: 2017-12-11 Last updated: 2018-08-19Bibliographically approved
5. OOlong: An Extensible Concurrent Object Calculus
Open this publication in new window or tab >>OOlong: An Extensible Concurrent Object Calculus
2018 (English)Conference paper, Published paper (Refereed)
Abstract [en]

We present OOlong, an object calculus with interface inheritance, structured concurrency and locks. The goal of the calculus is extensibility and reuse. The semantics are therefore available in a version for LaTeX typesetting (written in Ott), and a mechanised version for doing rigorous proofs in Coq.

Keywords
Object Calculi, Semantics, Mechanisation, Concurrency
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-335174 (URN)10.1145/3167132.3167243 (DOI)
Conference
Proceedings of SAC 2018: Symposium on Applied Computing , Pau, France, April 9–13, 2018 (SAC 2018)
Available from: 2017-12-01 Created: 2017-12-01 Last updated: 2018-01-13

Open Access in DiVA

fulltext(807 kB)2818 downloads
File information
File name FULLTEXT01.pdfFile size 807 kBChecksum SHA-512
3817b2ab46f0667aae164cda7679a09cea4fba6f050fac4ea550c0c6cb260a617960b7fe79b4b67f69eb88bf0f6cfdc7b14128533ebd68596cd1836b4c7c8d64
Type fulltextMimetype application/pdf
Buy this publication >>

Search in DiVA

By author/editor
Castegren, Elias
By organisation
Division of Computing ScienceComputing Science
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 2818 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

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 68172 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