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
Bestow and Atomic: Concurrent Programming using Isolation, Delegation and Grouping
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]

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.

Place, publisher, year, edition, pages
2017.
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:uu:diva-336020OAI: oai:DiVA.org:uu-336020DiVA: diva2:1164765
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. 106 p.
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1611
Keyword
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-01-13

Open Access in DiVA

No full text

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: 28 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