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

Keyword
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
2017 (English)In: Article in journal (Other academic) Submitted
Abstract [en]

Concurrency warrants synchronisation, regardless of concurrency model. Actor-based concurrency serialises all computation in an actor through asynchronous message passing. In contrast, lock-based concurrency serialises some computation by following a lock-unlock protocol for accessing certain data.

Both systems require sound reasoning about pointers and aliasing to exclude data-races. If actor isolation is broken, so is the single thread of control-abstraction. Similarly for locks, if a datum is accessible outside of the scope of the lock, the datum is not governed by the lock.

In this paper we discuss how to balance aliasing and synchronisation. In previous work, we defined a reference capability system that guarantees data-race freedom of actor-based concurrency and lock-based concurrency. This paper extends this work by the introduction of two programming constructs; one for decoupling isolation and synchronisation and one for constructing higher-level atomicity guarantees from lower-level synchronisation. We focus predominantly on actors, and in particular the Encore programming language, but our ultimate goal is to define our constructs in such a way that they can be used both with locks and actors, given that combinations of both models occur frequently in actual systems.

We discuss the design space, provide several formalisations of different semantics and discuss their properties, and connect them to case studies showing how our proposed constructs can be useful. We also report on an on-going implementation of our proposed constructs in Encore.

National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-336020 (URN)
Available from: 2017-12-11 Created: 2017-12-11 Last updated: 2018-01-13
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.

Keyword
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)2306 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: 2306 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: 67890 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