Bestow and Atomic: Concurrent Programming using Isolation, Delegation and Grouping

TL;DR

This paper introduces new programming constructs to improve concurrent programming by decoupling isolation and synchronization, enabling higher-level atomicity guarantees, with a focus on actor-based systems like Encore.

Contribution

It extends previous work by adding constructs for decoupling isolation and synchronization, and building atomicity guarantees, applicable to both actor and lock-based concurrency.

Findings

Proposed constructs facilitate decoupling isolation and synchronization.

Formal semantics and properties of the constructs are discussed.

Implementation in the Encore language is underway.

Abstract

Any non-trivial concurrent system warrants synchronisation, regardless of the concurrency model. Actor-based concurrency serialises all computations in an actor through asynchronous message passing. In contrast, lock-based concurrency serialises some computations 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 type 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.