Verona is a concurrent object-oriented programming language that organises all the objects in a program into a forest of isolated regions. Memory is managed locally for each region, so programmers can control a program's memory use by adjusting objects' partition into regions, and by setting each region's memory management strategy. A thread can only mutate (allocate, deallocate) objects within one active region---its "window of mutability". Memory management costs are localised to the active region, ensuring overheads can be predicted and controlled. Moving the mutability window between regions is explicit, so code can be executed wherever it is required, yet programs remain in control of memory use. An ownership type system based on reference capabilities enforces region isolation, controlling aliasing within and between regions, yet supporting objects moving between regions and threads. Data accesses never need expensive atomic operations, and are always thread-safe.

The age of multi-core computers is upon us, yet current programming languages, typically designed for single-core computers and adapted post hoc for multi-cores, remain tied to the constraints of a sequential mindset and are thus in many ways inadequate. New programming language designs are required that break away from this old-fashioned mindset. To address this need, we have been developing a new programming language called Encore, in the context of the European Project UpScale. The paper presents a motivation for the Encore language, examples of its main constructs, several larger programs, a formalisation of its core, and a discussion of some future directions our work will take. The work is ongoing and we started more or less from scratch. That means that a lot of work has to be done, but also that we need not be tied to decisions made for sequential language designs. Any design decision can be made in favour of good performance and scalability. For this reason, Encore offers an interesting platform for future exploration into object-oriented parallel programming.

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.

Expressive actor models combine aspects of functional programming into the pure actor model enriched with futures. Such functional features include first-class closures which can be passed between actors and chained on futures. Combined with mutable objects, this opens the door to race conditions. In some situations, closures may not be evaluated by the actor that created them yet may access fields or objects owned by that actor. In other situations, closures may be safely fired off to run as a separate task. This paper discusses the problem of who can safely evaluate a closure to avoid race conditions, and presents the current solution to the problem adopted by the Encore language. The solution integrates with Encore’s capability type system, which influences whether a closure is attached and must be evaluated by the creating actor, or whether it can be detached and evaluated independently of its creator. Encore’s current solution to this problem is not final or optimal. We conclude by discussing a number of open problems related to dealing with closures in the actor model.

Expressive actor models combine aspects of functional programming into the pure actor model enriched with futures. Such functional features include first-class closures which can be passed between actors and chained on futures. Combined with mutable objects, this opens the door to race conditions. In some situations, closures may not be evaluated by the actor that created them yet may access fields or objects owned by that actor. In other situations, closures may be safely fired off to run as a separate task.

This paper discusses the problem of who can safely evaluate a closure to avoid race conditions, and presents the current solution to the problem adopted by the Encore language. The solution integrates with Encore's capability type system, which influences whether a closure is attached and must be evaluated by the creating actor, or whether it can be detached and evaluated independently of its creator.

Encore's current solution to this problem is not final or optimal. We conclude by discussing a number of open problems related to dealing with closures in the actor model.

Functional programming languages are well-suited for developing compilers, and compilers for functional languages are often themselves written in a functional language. Functional abstractions, such as monads, allow abstracting away some of the repetitive structure of a compiler, removing boilerplate code and making extensions simpler. Even so, functional languages are rarely used to implement compilers for languages of other paradigms. This paper reports on the experience of a four-year long project where we developed a compiler for a concurrent, object-oriented language using the functional language Haskell. The focus of the paper is the implementation of the type checker, but the design works well in static analysis tools, such as tracking uniqueness of variables to ensure data-race freedom. The paper starts from a simple type checker to which we add more complex features, such as type state, with minimal changes to the overall initial design.

Functional programming languages are well-suited for developing compilers, and compilers for functional languages are often themselves written in a functional language. Functional abstractions, such as monads, allow abstracting away some of the repetitive structure of a compiler, removing boilerplate code and making extensions simpler. Even so, functional languages are rarely used to implement compilers for languages of other paradigms.

This paper reports on the experience of a four-year long project where we developed a compiler for a concurrent, object-oriented language using the functional language Haskell. The focus of the paper is the implementation of the type checker, but the design works well in static analysis tools, such as tracking uniqueness of variables to ensure data-race freedom. The paper starts from a simple type checker to which we add more complex features, such as type state, with minimal changes to the overall initial design.

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. 

In concurrent systems, some form of synchronisation is typically needed to achieve data-race freedom, which is important for correctness and safety. In actor-based systems, messages are exchanged concurrently but executed sequentially by the receiving actor. By relying on isolation and non-sharing, an actor can access its own state without fear of data-races, and the internal behavior of an actor can be reasoned about sequentially. However, actor isolation is sometimes too strong to express useful patterns. For example, letting the iterator of a data-collection alias the internal structure of the collection allows a more efficient implementation than if each access requires going through the interface of the collection. With full isolation, in order to maintain sequential reasoning the iterator must be made part of the collection, which bloats the interface of the collection and means that a client must have access to the whole data-collection in order to use the iterator. In this paper, we propose a programming language construct that enables a relaxation of isolation but without sacrificing sequential reasoning. We formalise the mechanism in a simple lambda calculus with actors and passive objects, and show how an actor may leak parts of its internal state while ensuring that any interaction with this data is still synchronised.

Encore is a programming language that was developed between 2014  and 2019. Encore was designed following the principle of  inversion of defaults: computations are concurrent (rather than  sequential) by default; data is isolated (rather than freely  sharable) by default. The language worked as a seedbed for a  large number of research ideas aimed at making programming with  active objects safe, expressive and efficient.

Encore allows active objects to share data but statically  ensures the absence of data races and allows fully concurrent  garbage collection. Active objects can synchronize using  first-class futures, which are also used to delegate and  coalesce computations across active objects. The type system  also supports orchestration of intra-object parallelism,  expressed using composable units of computation. Active objects  which see a lot of traffic can turn themselves into passive  objects protected by lock-free synchronization mechanisms to  avoid performance bottle-necks, while still facilitating safe  sharing and concurrent garbage collection.

This paper gives an overview of these features of Encore,  reflecting on lessons learned from trying to fit all of these  research ideas into a single language.

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. 

A linear reference is a reference guaranteed to be unaliased. Thisis a powerful property that simplifies reasoning about programs,but is also a property that is too strong for certainapplications. For example, lock-free algorithms, which implementprotocols to ensure safe concurrent access to data structures, aregenerally not typable with linear references as they involvesharing of mutable state.

This paper presents a type system with a relaxed notion oflinearity that allows an unbounded number of aliases to an objectas long as at most one alias at a time owns the right to accessthe contents of the object. This ownership can be transferredbetween aliases, but can never be duplicated. The resultinglanguage is flexible enough to express several lock-freealgorithms and at the same time powerful enough to guarantee theabsence of data-races when accessing owned data. The language isformalised and proven sound, and is also available as a prototype implementation.

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 L^AT_EX typesetting (written in Ott), a mechanised version for doing rigorous proofs in Coq, and a prototype interpreter (written in OCaml) for typechecking an running OOlong programs.

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), a mechanised version for doing rigorous proofs in Coq, and a prototype interpreter (written in OCaml) for typechecking an running OOlong programs.

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.

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.

The proliferation of shared mutable state in object-oriented programming complicates software development as two seemingly unrelated operations may interact via an alias and produce unexpected results. In concurrent programming this manifests itself as data-races.

Concurrent object-oriented programming suffers from the fact that code that warrants synchronisation cannot easily be distinguished from code that does not. The burden is placed solely on the programmer to reason about alias freedom, sharing across threads and side-effects to deduce where and when to apply concurrency control, without inadvertently blocking parallelism.

This paper presents a reference capability approach to concurrent and parallel object-oriented programming where all uses of aliases are guaranteed to be data-race free. Locations' static types describe their possible sharing. Type information can express non-interfering deterministic parallelism without dynamic concurrency control, thread-locality, lock-based schemes, and guarded-by relations giving multi-object atomicity to nested data structures. Unification of capabilities and traits allows trait-reuse across multiple concurrency scenarios with minimal code duplication. The resulting system brings together features from a wide range of prior work in a unified way.

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.

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 discusses a prototype implementation which integrates LOLCAT with an object-oriented programming language.

This extended abstract overviews work on a type system for lock-free programming based on compare-and-swap. The type system prevents atomicity violations in lock-free programs, where insertion and removal of objects from a linked structure would be subject to data-races breaking linearity of ownership. The type system has successfully been applied to a small number of lock-free data structures.

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.

Ownership type systems give a strong notion of separation between aggregates. Objects belonging to different owners cannot be aliased, and thus a mutating operation internal to one object is guaranteed to be invisible to another. This naturally facilitates reasoning about correctness on a local scale, but also proves beneficial for coarse-grained parallelism as noninterference between statements touching different objects is easily established. For fine-grained parallelism, ownership types fall short as owner-based disjointness only allows separation of the innards of different aggregates, which is very coarse-grained. Concretely: ownership types can reason about the disjointness of two different data structures, but cannot reason about the internal structure or disjointness within the data structure, without resorting to static and overly constraining measures. For similar reasons, ownership fails to determine internal disjointness of external pointers to objects that share a common owner. In this paper, we introduce the novel notion of refined ownership which overcomes these limitations by allowing precise local reasoning about a group of objects even though they belong to the same external owner. Using refined ownership, we can statically check determinism of parallel operations on tree-shaped substructures of a data structure, including operations on values external to the structure, without imposing any non-local alias restrictions.

In many actor-based programming models, asynchronous method calls communicate their results using futures, where the fulfilment occurs under-the-hood. Promises play a similar role to futures, except that they must be explicitly created and explicitly fulfilled; this makes promises more flexible than futures, though promises lack fulfilment guarantees: they can be fulfilled once, multiple times or not at all. Unfortunately, futures are too rigid to exploit many available concurrent and parallel patterns. For instance, many computations block on a future to get its result only to return that result immediately (to fulfil their own future). To make futures more flexible, we explore a construct, forward, that delegates the responsibility for fulfilling the current implicit future to another computation. Forward reduces synchronisation and gives futures promise-like capabilities. This paper presents a formalisation of the forward construct, defined in a high-level source language, and a compilation strategy from the high-level language to a low-level, promised-based target language. The translation is shown to preserve semantics. Based on this foundation, we describe the implementation of forward in the parallel, actor-based language Encore, which compiles to C.

When building a new programming language, it can be useful to compose parts of existing languages to avoid repeating implementation work. However, this is problematic already at the syntax level, as composing the grammars of language fragments can easily lead to an ambiguous grammar. State-of-the-art parser tools cannot handle ambiguity truly well: either the grammar cannot be handled at all, or the tools give little help to an end-user who writes an ambiguous program. This composability problem is twofold: (i) how can we detect if the composed grammar is ambiguous, and (ii) if it is ambiguous, how can we help a user resolve an ambiguous program? In this paper, we depart from the traditional view of unambiguous grammar design and enable a language designer to work with an ambiguous grammar, while giving users the tools needed to handle these ambiguities. We introduce the concept of resolvable ambiguity wherein a user can resolve an ambiguous program by editing it, as well as an approach to computing the resolutions of an ambiguous program. Furthermore, we present a method based on property-based testing to identify if a composed grammar is unambiguous, resolvably ambiguous, or unresolvably ambiguous. The method is implemented in Haskell and evaluated on a large set of language fragments selected from different languages. The evaluation shows that (i) the approach can handle significantly more cases of language compositions compared to approaches which ban ambiguity altogether, and (ii) that the approach is fast enough to be used in practice.

Traditionally, a grammar defining the syntax of a programming language is typically both context free and unambiguous. However, recent work suggests that an attractive alternative is to use ambiguous grammars,thus postponing the task of resolving the ambiguity to the end user. If all programs accepted by an ambiguous grammar can be rewritten unambiguously, then the parser for the grammar is said to be resolvably ambiguous. Guaranteeing resolvable ambiguity statically---for all programs---is hard, where previous work only solves it partially using techniques based on property-based testing. In this paper, we present the first efficient, practical, and proven correct solution to the statically resolvable ambiguity problem. Our approach introduces several key ideas, including splittable productions, operator sequences, and the concept of a grouper that works in tandem with a standard parser. We prove static resolvability using a Coq mechanization and demonstrate its efficiency and practical applicability by implementing and integrating resolvable ambiguity into an essential part of the standard OCaml parser.

The choice of how to represent an abstract type can have a major impact on the performance of a program, yet mainstream compilers cannot perform optimizations at such a high level. When dealing with optimizations of data type representations, an important feature is having extensible representation-flexible data types; the ability for a programmer to add new abstract types and operations, as well as concrete implementations of these, without modifying the compiler or a previously defined library. Many research projects support high-level optimizations through static analysis, instrumentation, or benchmarking, but they are all restricted in at least one aspect of extensibility.

This paper presents a new approach to representation-flexible data types without such restrictions and which still finds efficient optimizations. Our approach centers around a single built-in type repr and function overloading with cost annotations for operation implementations. We evaluate our approach (i) by defining a universal collection type as a library, a single type for all conventional collections, and (ii) by designing and implementing a representation-flexible graph library. Programs using repr types are typically faster than programs with idiomatic representation choices---sometimes dramatically so---as long as the compiler finds good implementations for all operations. Our compiler performs the analysis efficiently by finding optimized solutions quickly and by reusing previous results to avoid recomputations.

The array is a fundamental data structure that provides an efficient way to store and retrieve non-sparse data contiguous in memory. Arrays are important for the performance of many memory-intensive applications due to the design of modern memory hierarchies: contiguous storage facilitates spatial locality and predictive access patterns which enables prefetching. Operations on large arrays often lend themselves well to parallelisation, such as a fork-join style divideand-conquer algorithm for sorting. For parallel operations on arrays to be deterministic, data-race freedom must be guaranteed. For operations on arrays of primitive data, data-race freedom is obtained by coordinating accesses so that no two threads operate on the same array indices. This is however not enough for arrays of non-primitives due to aliasing: accesses of separate array elements may return pointers to the same object, or overlapping structures. Reference capabilities have been used successfully in the past to statically guarantee the absence of dataraces in object-oriented programs by combining concepts such as uniqueness, read-only access, immutability, and borrowing. This paper presents the first extension of reference capabilities—called array capabilities— that support concurrent and parallel operations on arrays of both primitive and non-primitive values. We define a small language of operators on array capabilities. In addition to element access, these operations support the abstract manipulation of arrays: logical splitting of arrays into subarrays; merging subarrays; and in-place alignment of the physical elements of an array with the logical order defined through splitting and merging. The interplay of these operations with uniqueness, borrowing and read-only access allows expressing a wide range of array use cases. By formalising our type system and the dynamic semantics of the key operations on array capabilities in a simple calculus, we give a precise description of the array capabilities. We when prove type soundness and array disjointness—that two capabilities that allow mutation can never give access to overlapping sets of elements. Data-race freedom is stated as a corollary to these theorems, as data races require two array capabilities in different threads. In addition to the formal approach, we experiment with array capabilities on a small number of parallel array algorithms and report our preliminary findings. Array capabilities extend the safety of reference capabilities to arrays in a way that build cleanly on existing reference capability concepts and constructs. This allows programmers to express parallel array algorithms on a higher level than individual indices, and with absences of data races guaranteed statically.

In on-going work, we are exploring reference capabilities for arrays, with the intention of carrying over previous results on statically guaranteed data-race freedom to parallel array algorithms. Reference capabilities typically restrict incoming pointers to an object to one (uniqueness), or restrict operations via multiple pointer to a single object (e.g., to only read). Extending such a design to arrays involve operations such as logically partitioning an array so that even though there are multiple pointers to a single array, these pointers cannot access the same elements. In this paper, we report on the on-going work of a prototype implementation of array capabilities, focusing in particular on the “array capability API design”, meaning the native operations on capabilities such as splitting and merging arrays. Using our prototype implementation, we translate several existing array algorithms into using array capabilities and qualitatively study the result. In addition to identifying the need for additional operations, we study what features are commonly exercised, what are the recurring patterns, and how reliance on direct element addressing using indexes can be reduced. We end by discussing a possible design for a more performant implementation once the API is fixed.