Bestow and Atomic: Concurrent Programming using Isolation, Delegation and Grouping
Elias Castegren Joel Wallin Tobias Wrigstad





[funding]This work is sponsored by the UPMARC center
  of excellence, the FP7 project “UPSCALE” and the project
  “Structured Aliasing” financed by the Swedish Research
  Council.


elias.castegren@it.uu.se

joel.wallin.3149@student.uu.se

tobias.wrigstad@it.uu.se
Uppsala University, Sweden
[mycorrespondingauthor]Corresponding author


  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.






§ INTRODUCTION


Concurrency can be defined as coordinating access to shared
resources. Synchronisation is naturally a key aspect of concurrent
programs and different concurrency models handle synchronisation
differently. Pessimistic models, like locks or the actor model
<cit.> serialise computation within certain
  encapsulated units, allowing sequential reasoning about
internal behaviour at the cost of sometimes pruning possible
parallel performance gains. In contrast, optimistic models, like
lock-free programming <cit.> or software transactional memory
<cit.> allow concurrent operations on the same data, but
require that all operations follow some protocol to exclude
unwanted behaviour, or avoid side-effects that cannot be
rolled-back in the event of conflicts between threads. In this
paper, we focus on pessimistic models.





In the case of the actor model, if a reference to an actor A's
internal state is accessible outside of A, operations inside of
A are subject to data-races and sequential reasoning is lost.
The same holds true for operations on an aggregate object behind a
lock, if a sub-object is leaked and becomes accessible where the
appropriate lock is not held.

In previous work, we designed Kappa <cit.>, a type
system in which the boundary of a unit of encapsulation can be
statically identified. An entire encapsulated unit can be wrapped
inside some synchronisation mechanism,  a lock or an
asynchronous actor interface, and consequently all operations
inside the boundary are guaranteed to be data-race free. An
important goal of this work is facilitating object-oriented reuse
in concurrent programming: internal objects are oblivious to how
their data-race freedom is guaranteed, and the building blocks can
be reused without change regardless of their external
synchronisation. Further, making synchronisation tractable
simplifies concurrent programming as the
portions of a system that are accessed concurrently will be identified,
and compilers can verify that the program behaves in accordance with
the programmer's intention, with respect to concurrent accesses.

This paper explores two extensions to the Kappa system, which we
explain in the context of the actor model (although they are
equally applicable to a system using locks). The first extension,
bestow, allows references to an object to escape its
unit of encapsulation without escaping its unit of
  synchronisation; all external operations on private state will
be implicitly delegated to the owner of that state, either via
message passing, or by acquiring a lock specific to the owner of
the private state.

This enables several useful programming
patterns without relaxing Kappa's static data-race freedom
guarantee. For example, in the context of an actor system, actors
may safely leak references to state, effectively allowing many
objects to cooperate in constructing the actor's interface.
Similarly, in the context of a lock, it will be possible to hold
on to references deep inside a structure, even when the lock is
not held, with a guarantee from the type system that these will not be used until the
lock is re-acquired.

When encapsulation and synchronisation are decoupled, another
extension becomes necessary to group operations together,
enabling atomicity of multiple operations on a data structure that potentially has several
different entry-points. To this end, we
introduce an atomic block scoped construct. In the context
of an actor system, this allows  grouping several messages to
prune unwanted interleavings. In the context of a lock-based
system, it allows performing several distinct operations without releasing the lock in-between.

This paper makes the following contributions:



  * We discuss (DRF) the difference between actor
  systems where data-races are avoided through isolation of
  an actor's passive objects and actor systems where data-races are
  avoided through delegation of operations on passive
  objects to the actors that own them, and show how both are
  supported in the Encore programming language <cit.>.
  Encore supports delegation through bestowed references,
  which were introduced in Encore as part of this work. In
  contrast to systems like E <cit.> and
  AmbientTalk <cit.>, Encore's delegation is
  purposely not transparent, allowing programmers to reason
  about the performance and latency of operations and distinguish
  between operations on local and remote objects (bestow).


  * We extend the delegation concept with a notion of movement
  of objects between actors,  implicit and/or automated
  transfer of ownership. This enables a form of load-balancing of
  passive objects between actors (load-balancing,
  formalised in formal2).


  * We introduce a block-scoped construct for grouping
  operations to be performed as an atomic unit that can be applied
  to both actor-based systems and lock-based systems, as well as
  systems that combine the two models (atomic).


  * We explore and formalise three variations of the semantics of bestowed
  references and atomic blocks, and show that the resulting systems are free from data-races. For simplicity, our formalisations
  are based on simple λ-calculus models with actors. We provide
  mechanised versions in Coq for others to build on. (Sections
  <ref>–<ref>).


  * We report on a number of small case studies using our
  proposed constructs (case-studies) and on the on-going
  implementation of bestowed references and atomic blocks in
  Encore (implementation).



This paper extends earlier work <cit.> by adding the
two variations of the semantics (formal2), mechanising
the semantics and their proofs <cit.>, providing case
studies (case-studies), reporting on the current state of
implementation (implementation), and adding more in-depth
discussions about the work throughout all sections of the paper.




§ BACKGROUND: KAPPA AND ENCORE

background

This section covers the background needed to understand the
context of this work. It explains the basics of Kappa, a type
system which guarantees data-race freedom in concurrent programs,
and Encore, an actor-based language which uses Kappa to facilitate
safe sharing between actors.



Kappa is a type system for concurrent object-oriented
programming <cit.>. Its most important guarantee is
that no two concurrent operations will access the same memory
address, unless both operations only use this address for reading.
Kappa achieves this by preventing the creation of aliases which
could be used to cause data-races. A reference can only be shared
between threads if all accesses are synchronised ( by using
locks) or if all operations available through the reference are
non-mutating.

The sharing properties of a reference are specified by its
mode, which is tracked by the type system. For example, a
reference with the locked mode is implicitly protected by a
lock, similar to a Java object whose methods are all
şy̧ņçḩŗo̧ņi̧z̧ȩḑ. It may be safely shared between threads, as any
concurrent accesses will be synchronised. In contrast, a reference
with the subordinate mode may not be shared between
threads. In fact, it may not even leak outside of the object that
created it (similar to ownership types <cit.>). This means that
a locked object (whose aliases all have the locked mode) may
encapsulate additional subordinate objects. Since these objects
may only be accessed via the locked object (thus grabbing its
lock), they can be operated on without additional synchronisation.



Kappa has been implemented as the type system for Encore, an
object-oriented language developed in the context of the UPSCALE
project <cit.>. Encore uses actors to achieve
concurrency, and Kappa ensures that objects shared between actors
are always accessed without data-races. Encore's actors are
implemented by extending Kappa with an actor mode.
References with this mode point to actors and may only be used to
send messages. Since all interaction with an actor go via its
message queue, operations on it will be synchronised, similar to
the operations on a locked object. Just like locked objects,
actors can use subordinate references to ensure that their own
private state is never accessed by other actors. Additionally,
Encore allows sharing of immutable or read-only data, and supports
ownership transfer of objects.

The interface of an actor is defined by its class, and the
messages in an actor's message queue are processed in sequence
(there is no selective receieving of messages, as in 
Erlang <cit.>). This means that Encore's actors behave as
active objects <cit.>. The work relating to actors
in this paper was done with Encore's actors in mind, but is
applicable to any actor language with active object semantics.

The constructs presented in this paper rely both on the
encapsulation guarantees given by the subordinate mode, as well as
the synchronisation guarantees given by locks and actors. They are
however orthogonal to which synchronisation technique is used (and
can be used in a system that uses both).

Encore does not yet support Kappa's locked mode because of
the complexity of integrating locks with Orca
<cit.>—Encore's garbage collection protocol (which
is shared with the Pony programming language <cit.>).
Besides implementation, garbage collection is orthogonal to the
matters discussed in this paper.



§ DATA-RACE FREEDOM: DELEGATION AND ISOLATION

DRF

Actors simplify concurrent programming by enabling sequential
reasoning inside each actor. The majority of actor-based
programming languages and frameworks— Akka <cit.>,
ProActive <cit.>, ABS <cit.>, Orleans
<cit.>, Encore <cit.>, Pony
<cit.> and Joelle <cit.> rely on
isolation, enforced manually by programmer diligence or
through compiler support to do so: by preventing references to an
actor's state to leak outside of the actor, the only way to
manipulate an actor's state is by sending it a message. (Compilers
and run-time systems may either reject references which would
violate encapsulation, or insert instructions to deep-copy message
payloads.) illustrate (left) shows the key situation to
be prevented to avoid data-races. The brown circles denote actors,
each with a (logical) thread of control. If the external reference
to f̧o̧o̧ is possible, accesses to foo could be subject to data
races.

An alternative model to isolation is found in some actor systems,
such as E <cit.> and AmbientTalk
<cit.> which allows an actor's state to be
arbitrarily referenced, but requires that operations on the state of some other
actor is implicitly delegated to that actor. In the isolation
model, data-race freedom is achieved through enforcing that all
external access go via an asynchronous interface. In the
delegation model, an actor can be thought of having just one
method in its interface: perform, and each operation is
translated into a perform call with some appropriate lambda.
Internal calls to perform can be carried out synchronously.
illustrate (right) shows how operations on a passive
object belonging to another actor can be enabled by making the
operations asynchronous and asking the actor that owns the passive
object to carry them out. Thus, only the actor owning the object
o pointed to by f̧o̧o̧ will ever operate on o.

The isolation model ties into existing theory on abstraction,
modularisation, and encapsulation. In most languages, it serves to
simplify reasoning: operations on passive objects are synchronous
and efficient whereas operations on actors are asynchronous and
introduce latency, but also make concurrency and parallelism
possible. The isolation model also helps clearly delimiting actor
interfaces. In contrast, the delegation model is much less
restrictive on the object graph of a system, but (in E and
AmbientTalk) complicates reasoning about the performance and
latency, and makes an actor's interface less clearly
delimited and defined.

Restricting object graph topologies means limiting aliasing in a
system. This is unsurprising since aliasing is a prerequisite of
data-races—but far from all aliasing is bad. Aliasing is
commonly used to provide shortcuts through a data structure, such
as a last pointer in a linked list implementation to allow
constant-time append operations. Staying with the linked list
example, we now demonstrate how delegation can be useful in an
actor setting. While the example is a little contrived, it
demonstrates the importance of allowing the creation of—and
sharing of—aliases.






 §.§ Delegation: Motivating Example

example

We motivate breaking isolation in the context of an
object-oriented actor language, with actors serving as the units
of encapsulation, encapsulating zero or more passive objects.
list shows an Encore program[We deviate from
  Encore syntax for brevity and omit end keywords in
  favour of using indentation to show block scoping.] with a
linked list in the style of an actor with an asynchronous external
interface. For simplicity we allow asynchronous calls to return
values and omit the details of how this is accomplished ( by
using futures, promises, or by passing continuations).

We use the .̧ operator to denote synchronous method calls or
field lookups, and the !̧ operator to denote asynchronous
method calls.

Clients can interact with the list for example by sending the
message ģȩţ with a specified index. With this implementation,
each time ģȩţ is called, the corresponding element is
calculated from the head of the list, giving linear time
complexity for each access. Iterating over all the elements
of the list has quadratic time complexity, which is clearly undesirable.















To allow more efficient element access, lists commonly
provide an iterator which holds a
pointer to the current node (iterator). This allows
constant-time access to the current element, and linear
iteration, but also breaks encapsulation by providing direct
access to nodes and elements without going through the list
interface ( <cit.> for a related discussion of
internal vs. external iterators). Since a list is its own actor,
with this design, list operations are now subject to data-races,
which breaks the single-thread-of-control abstraction.















A middle ground providing linear time iteration without data-races can be implemented by




moving the iterator logic into the list actor, so that
the calls to ģȩţŅȩx̧ţ and ḩa̧şŅȩx̧ţ are synchronised in the
message queue of the actor. This




requires a more advanced scheme to map different
clients to different concurrent iterators, clutters the
list interface, 


creates unnecessary coupling
between Ļi̧şţ and I̧ţȩŗa̧ţo̧ŗ, and complicates support of
 several kinds of iterators.

The next section shows how external accesses to an internal object
can be synchronised to preclude data-races, while still avoiding
all of the complications mentioned above.






§ BESTOW: ADDING DELEGATION TO ENCORE

bestow










Encapsulating state behind a synchronisation mechanism allows
reasoning sequentially about operations on that state. The Kappa
type system in Encore will not allow calls to
ģȩţI̧ţȩŗa̧ţo̧ŗ(̧)̧ from outside the list actor itself,
defeating the purpose of creating the iterator in the first place.
In Encore, the I̧ţȩŗa̧ţo̧ŗ return type of ģȩţI̧ţȩŗa̧ţo̧ŗ(̧)̧ has a
subordinate mode ( background), which is a requirement for allowing the direct
reference to the actor's links. Similar to ownership types
<cit.>, calls to methods that return subordinate objects are
only allowed on other subordinate objects,  navigation is
permitted inside each isolation domain, but not across. Notably,
the ţḩi̧ş reference of an actor has a subordinate mode, meaning
that an actor's internal type differs from its external.

A call on a non-subordinate receiver thus always denotes a call
that crosses from one synchronisation domain into another. To
support delegation-based synchronisation in Encore, we extend
Kappa with a bestowed mode, written as B̧(̧Ţ)̧ when
applied to the type Ţ. B̧(̧Ţ)̧ denotes an external reference
to an object of type Ţ which is part of the internal state of
an actor. All of Ţ's operations are available through a
reference of type B̧(̧Ţ)̧, but they will be performed
asynchronously by implicitly delegating the operations to the
actor that owns the object.




For clarity, we introduce a bestow operation, which lifts a
type with subordinate mode to an equivalent type whose mode is
instead bestowed. This operation allows a programmer to create
a “safe remote reference” to a local passive object, which can be
freely shared—and safely, since it adheres to the delegation model.

We use the term bestowed reference to mean a reference to a
bestowed object, which in turn denotes an object to which
there are bestowed references. We call the actor encapsulating the
bestowed object its owner.



















bestow shows the changes needed to the code in
iterator, as well as the code for a client using the
iterator, to go from isolation-based to delegation-based data-race
freedom. In the list, ģȩţI̧ţȩŗa̧ţo̧ŗ(̧)̧ now returns a bestowed
iterator which is tractable through the B̧(̧.̧.̧.̧)̧
type[If desired, this type change can be implicit through
  view-point adaptation <cit.>; Kappa lets us statically
detect when an internal object is crossing its encapsulation boundary.
For clarity, we explicitly annotate bestowed return types here.], and not
a passive iterator. In the client code, synchronous calls to
ḩa̧şŅȩx̧ţ(̧)̧ and ģȩţŅȩx̧ţ(̧)̧ become asynchronous message sends
which is reflected by the change from .̧ to !̧. Notably,
messages to the iterator are handled by the list actor and are
and are executed in a serialised fashion, interleaved with normal
messages sent to the list actor.

The granularity of the delegated operations, and thereby the
amount of interleaving allowed, is related to the reach of the
objects which are bestowed. Creating an iterator inside the
list and returning a bestowed reference to it allows it to access
multiple nodes of the list atomically. In contrast, creating an
iterator outside the list holding bestowed references to
links in the list only gives atomic access to a single link at a
time.

In the case of returning a bestowed reference to an iterator,
entire ģȩţŅȩx̧ţ(̧)̧ operations are performed without interleaved
activities in the list actor. In the case of returning bestowed
references to individual links, getting the element out of a link,
and obtaining a bestowed reference to its next link are two
separate operations which may be interleaved with other operations
on the list ( fine-grained-iterator).




 §.§ Bestowed References and Lock-Based Synchronisation


Encore actors are typed by Kappa's actor mode, which is visible in
the code examples so far. There, the actor mode is applied to
class declarations to denote that instances of these classes are
data-race free because of their asynchronous interface and
encapsulated single thread of control. Replacing “actor” with
“locked” in the code examples up to this point is sound and
preserves data-race freedom of all instances of locked classes by
forcing all method calls to first acquire a per-instance lock.

Notably, the bestowed type and bestow operations in
bestow are still meaningful if actor is changed
for locked. At the type-level, a bestowed reference is
oblivious to how an isolated object's data-race freedom is
guaranteed. Dynamically, though, a bestowed reference into a
capsule protected by a lock will implicitly acquire the lock
associated with that capsule.




 §.§ Differences Between Locks and Actors

LocksVsActors

The small changes needed in Kappa to switch between using locks
and actors as a means of protecting access to a group of objects
does not reflect the differences between the two concepts. In
lock-based programs, data is “dead” and only lives when visited
by a thread of control. In actor-based programs, actors are alive,
only act upon themselves, and only upon so choosing. The
difference is push vs. pull—whether activity is pushed upon an
object by a thread, or whether activity happens as a result of the
actor pulling a message from its message queue. In lock-based
programs, a thread can be denied entrance into an object by
another thread holding the appropriate lock. In actor-based
programs, an actor may never ask for the next message (for example
because it is stuck in an infinite loop) causing another actor's
request to be effectively ignored.

In an actor-based setting, the owner of a bestowed object will
perform all operations on that object. Thus, while the owner will
technically never block on an access to an object that it owns, it
may instead end up performing operations on behalf of other
actors. In some scenarios, this may make the owner of a bestowed
object an unintentional bottleneck in a system, especially if
delegated operations are long-running, the owner has
unproportionally many bestowed objects, or it performs critical
operations unrelated to the bestowed object which are now
interleaved with delegated tasks. In a lock-based setting, all
threads operating on a shared resource take part in performing
those operations. Thus, if operations are spread out in time, it
is possible that contention is never witnessed in the system and
that operations unrelated to the bestowed object are never
delayed.




 §.§ Towards Actor-Style Delegation-Locks


We note that it is possible to make a bestow-based interpretation
of locks by replacing delegation with transfer of ownership:
instead of an actor lifting an operation into a closure and
passing it to the owner to be performed, the actor simply
transfers ownership of the bestowed object to itself and
subsequently performs the operation without any delegation.

Because there are no topological restrictions on bestowed
references, transfer of ownership of a bestowed object o is
possible unless o is currently being used (equivalent to another
thread holding a lock).

For example, if an actor which owns some collection data structure
is currently inactive, another actor with a bestowed reference to
this collection could transfer ownership of the collection to
itself and operate on it, rather than waking the owning actor to
delegate the operation.

If transfer is not possible, the actor
attempting the transfer could block (making accesses to bestowed
references equivalent to accessing references with locked mode) or
fall-back to delegation to avoid blocking. This is similar to
queue delegation locks <cit.> which handle contention by
delegating blocking operations to the thread currently holding the
lock. This allows operations that would otherwise block to return
immediately with a future value which will eventually be fulfilled
by some other thread.

Allowing objects' owners to change prevents giving the owner
special access, and thus forces all references to a bestowed
object to be bestowed. Accesses must then branch on whether the
object is local, and if not, whether or not its ownership can be
transferred. For the example above, whoever is accessing the
collection must first check if they are the current owner of the
collection, in which case the operation can proceed, and otherwise
decide if ownership transfer is possible or if the operation
should be delegated.

transfer gives the details on the semantics of
transferable bestowed objects.

load-balancing
Encore uses a work-stealing based load-balancing scheme that moves
actors across cores. In many ways, allowing transfer of ownership
of bestowed objects is a form of load-balancing for passive
objects. Just like load-balancing of actors is governed by
carefully tuned heuristics, how and when to transfer ownership of
a bestowed object is not clear-cut. In many cases, keeping objects
local to a core may have locality benefits which favours ownership
transfer for actors on the same core, but delegation
otherwise 


Also, the cost of creating and passing
closures may be non-negligible, which may favour keeping ownership
among frequent accessors, etc. Run-time optimisation of ownership
transfer for bestowed references is an interesting direction for
future work.





§ ATOMIC: ATOMICITY AND GROUPING OF OPERATIONS ON BESTOWED REFERENCES

atomic

So far, we have discussed data-race freedom. Data-race freedom is
important, but not always enough achieve atomicity,  the
ability to make a set of changes appear atomic in a system. For
example, a data-race free counter in Kappa will correctly handle
concurrent increments and decrements, but is not enough to support
swapping the values of two counters in the presence of concurrent
operations. The root cause is that Kappa's protection is per-object
(notably including its transitive closure of sub-objects), and
exchanging values involves more than one object where neither
object is nested inside the other.

Additionally, the protection from data-races offered by Kappa only
applies to a single top-level operation[Kappa can
  overcome this limitation through explicit lock-taking, which is
  only supported on locked objects, not actors <cit.>.]. For
example, operating on a ļo̧çķȩḑ file to first open and
subsequently read, one cannot exclude the possibility of a
separate thread closing the file in-between. The same holds
if the file is an actor: messages are serialised but any messages
may be interleaved, meaning that [o̧p̧ȩņ, çļo̧şȩ, ŗȩa̧ḑ]
is a valid mailbox. This problem is exacerbated by more
fine-grained operations being added to an interface through
bestowed references.

To support atomicity of groups of operations over one or more
objects we extend Encore with an atomic block construct. In
its simplest form, it supports operations on a single reference
whose mode is actor, locked, or bestowed and coalesces operations
on the reference making them atomic in the system.



As a concrete, simple example, coarse-grained-iterator
shows an iterator with a bestowed reference to its current node,
and which wraps its operations in an atomic block, preventing
any interleaving between the two message sends, thus regaining the
same interleaving guarantees as the iterator in bestow.
The atomic block thereby allows a client to define new operations by
composing smaller ones and giving a use-site definition of
where atomicity is useful, as opposed to declaration-site. For
example, merging ȩļȩm̧ and ņȩx̧ţ into a single operation in the Ņo̧ḑȩ class
voids the need for an atomic block in
coarse-grained-iterator, but in the general case, it is
unreasonable to expect declarations to cater to all possible use
cases.

The simplest case, a single atomic block of messages whose results
are ignored (or v̧o̧i̧ḑ), can be implemented efficiently through
coalescing messages to the receiver and delivering them as
a single “big message”[In Encore, this may additionally
  have garbage collection benefits if messages contain overlapping
  state.]. atomic-semantics (left) shows how an atomic
block containing two message sends is translated into a single
message, containing instructions for performing the two operations
in sequence. This avoids interleaving from other actors, but does
not support multi-actor atomicity.

Similarly, for the case of operations on an object guarded by a
lock, an atomic block acts as an explicit locking
operation—similar to a şy̧ņçḩŗo̧ņi̧z̧ȩḑ block in Java—voiding
the need for an individual lock–release for each operation in the
block ( <cit.>).




 §.§ Grouping Semantics and Atomicity

grouping-semantics

Coalescing messages to avoid interleaving is simple and efficient,
but also limited. For example, a client of the iterator from bestow
may want to atomically perform operations on all the elements of
list until a certain element is found. However, a coalescing
semantics prevents the client from reacting to results from the
iterator except between discrete atomic blocks. Furthermore, it
imposes some upper limit on the messages from the client to the
list. Last, it will delay the time when the client can start
operating on the elements until the right element is found, making
it impossible to implement parallel pipelines. Moreover,
coalescing semantics is not strong enough to support a notion of
atomicity across multiple actors.

Atomicity across actors can be made possible by delaying the
processing of messages not originating from within the atomic
block until after a particular point. In its simplest form, the
actor executing the atomic block will be able to reason about the
receiving actor throughout the atomic block enabling  pre-
and post condition reasoning. By wrapping several atomic blocks,
this extends to multiple actors.

To this end, we explore a richer semantics for atomic blocks which
involves the creation of a private mailbox, which is only
known by the actor running the atomic block and the receiving
actor. Private channels can be found  in Pi calculus
<cit.> and CSP
<cit.>, but in our implementation we restrict them to follow
a block-scoped, structured programming approach. Under the private
mailbox semantics, at the start of an atomic block, the current
actor creates a new mailbox, technically a FIFO queue, and passes
one end (for receiving) to the target actor in a normal message
and keeps the other for sending. Upon receipt of this message, the
target actor replaces its normal, public mailbox with the private
mailbox, and from this point continues to process only messages
from the latter. Since the private mailbox is only known by the
sender and receiver, no other messages may interleave their
communication. At the end of the atomic block, the target actor is
sent a new message to restore its original mailbox, where any other communication
has been buffered, and will now be processed in FIFO order. (See
money-transfer for an example that can be encoded with
private mailboxes, but not with coalescing.)

In languages which allow actors to use pattern matching to
selectively pick messages from its message queue ( Erlang
<cit.>), this kind of “private conversation” between two
actors can be encoded. However, this requires that the receiving
actor is implemented with support for atomically processing
exactly the messages that the client wanted to send. By using a
private queue created by the client, the client can create new
atomic operations by composing the operations that a receiving
actor provides, without explicit support for this in the receiving
actor.

The atomic block notably turns actor-based programs into more
structured programs, because the atomic blocks are unidirectional:
the only way for the list actor to communicate with a client during the execution of
an atomic block in the client is through futures—not message sends, as
they will not be processed before the atomic block is finished.
Furthermore, only tree-shaped communication is possible inside
atomic blocks. If a client of the list has entered an atomic block
targeting the iterator, and then enters a nested block targeting some
other actor A, there is no way for A and the list actor to communicate
directly[However, the list actor may return a value to the client which the client
  subsequently passes to A, and similar for A.].







 §.§ Tractability of Atomic Operations


One reason why lock-based programming is hard in mainstream
programming is because there is no way to express what a lock
governs in a program. Kappa addresses this by keeping track of
synchronisation and encapsulation through modes in types. Imagine
an actor A holding a reference the list actor in its field f. In
its method m_1, A enters into an atomic block targeting the list actor.
A subsequently calls its method m_2 which performs ţḩi̧ş.̧f̧ ̧!̧
̧ ̧ ̧ģȩţF̧i̧ŗşţ(̧)̧. There is nothing in f's type that expresses the
current situation where communication with the list actor is uninterruptible.
Should ţḩi̧ş.̧f̧ ̧!̧ ̧ģȩţF̧i̧ŗşţ(̧)̧ be considered part of the atomic block
or not,  is atomicity actor-wide? If yes, then the
tractability of Kappa is significantly weakened. If no, we deviate
from the standard behaviour of locks and must additionally solve a
problem with tracking bestowing references. A simple approach in
the latter case is to tie operations to the lexical scope
of the atomic block. This means that ţḩi̧ş.̧f̧ ̧!̧ ̧ģȩţF̧i̧ŗşţ(̧)̧ will not
be processed by its receiver until after the atomic block is
finished. A hybrid approach is to introduce an additional
handle to the subject of an atomic block, whose type
reflects its “atomic status”. This handle can be passed to where
atomic operations should be performed, allowing ḩa̧ņḑļȩ ̧!̧ ̧ģȩţF̧i̧ŗşţ(̧)̧ to
take part in the atomic block. This is the route Encore follows;
inside the block a̧ţo̧m̧i̧ç ̧x̧ ̧ḑo̧ ̧.̧.̧.̧ the type Ţ of x̧ is
changed to A̧(̧Ţ)̧, where the new qualifier A̧(̧)̧ expresses
that:


  * Operations will not be interleaved with operations from other
  actors.

  * The reference is stack-bound (or borrowed) meaning that for
  any given scope where the reference occurs, no aliases can be
  created that survives that scope.

  * The reference is local to the current actor meaning it may
  not be passed to another actor, either as an element or by
  returning it.


In Encore, for the message ģȩţF̧i̧ŗşţ(̧)̧ in m_2 to be be part of
the atomic block in m_1, m_2 must be passed the correct
A̧(̧)̧ handle and ţḩi̧ş.̧f̧ ̧!̧ ̧ģȩţF̧i̧ŗşţ(̧)̧ replaced by ḩa̧ņḑļȩ ̧!̧
̧ ̧ ̧ģȩţF̧i̧ŗşţ(̧)̧.




































§ FORMALISING “VANILLA” BESTOW AND ATOMIC

formalism
formal1

To explain bestow and atomic we use a simple lambda
calculus with actors and passive objects. For brevity, we only
discuss bestow and atomic under one concurrency model, namely
actors. We chose actors for two reasons: they have the most
compelling design space, and it more closely matches our
implementation in Encore. In this section, we formalise the bestow
as presented in bestow together with the coalescing
atomic operations from atomic.

In subsequent sections, we also formalise two variants of the
actor-based semantics for bestow and atomic: passive
objects with transferable ownership and private mailboxes.

The purpose of these formalisations is to flesh out the details of
bestow and atomic,

and we abstract away most details that are unimportant for describing
the behavior of these constructs. For example, we leave out
classes and actor interfaces and simply allow arbitrary operations
on values. This makes the formalisation simple and fairly unsurprising.

By disallowing sharing of (non-bestowed) passive
objects, we show that our language is free from data-races
(meta). The calculus has been mechanised and proven sound in
Coq (coq).

The syntax of our calculus is shown in syntax. An
expression e is a variable x, a function application e e'
or a message send e!̧v. Messages are sent as anonymous
functions, which are executed by the receiving actor.

We abstract updates to passive objects as e.m̧u̧ţa̧ţȩ(̧)̧, which
has no actual effect in the formalism, but is reasoned about in
meta. A new object or actor is created with ņȩw̧
τ and a passive object can be bestowed by the current actor
with b̧ȩşţo̧w̧ e.

Since this version of the semantics uses coalescing semantics
for atomic blocks, we don't yet need a special a̧ţo̧m̧i̧ç
construct in the formalism. Instead we model atomic interactions by
composing operations as in atomic-semantics (left).




Statically, values are anonymous functions or the unit value ().
Dynamically, 𝑖𝑑 is the identifier of an actor, ι is the
memory location of a passive object, and ι_𝑖𝑑 is
a passive object ι bestowed by the actor 𝑖𝑑.

A type is an active type α, a passive type 𝗉, a function
type τ→τ, or the  type. An active type
is either an actor type 𝖼 or a bestowed type 𝐁(𝗉). Note that for simplicity,
𝗉 and 𝖼 are not meta-syntactic variables; every passive object
has type 𝗉, every actor has type 𝖼, and every bestowed
object has type 𝐁(𝗉).





 §.§ Static Semantics


The typing rules for our formal language can be found in
static. The typing context Γ maps variables to types.

The “normal” lambda calculus rules e-var and e-apply
are straightforward. The ņȩw̧ keyword can create new passive
objects or actors e-new-*. Passive objects may be mutated
e-mutate, and may be bestowed activity e-bestow.

Message sends are modelled by sending anonymous functions which are
run by the receiver e-send. The receiver must be of active
type ( be an actor or a bestowed object), and the argument of
the anonymous function must be of passive type 𝗉 (this can be
thought of as the ţḩi̧ş of the receiver). Finally, all free
variables in the body of the message must have active type to make
sure that passive objects are not leaked from their owning actors.
This is captured by Γ_α which contains only the
active mappings _ : α of Γ. Dynamically, the body may
not contain passive objects ι.

Typing values is straightforward.






 §.§ Dynamic Semantics

dyn-semantics



dynamic shows the small-step operational semantics
for our language.

A running program is a heap H, which maps actor identifiers id
to actors (ι, L, Q, e), where ι is the ţḩi̧ş of the
actor, L is the local heap of the actor (a set containing the
passive objects created by the actor), Q is the message queue (a
list of lambdas to be run), and e is the current expression
being evaluated.

The step relation id↪ is indexed by
the actor id that is currently scheduled.

An actor whose current expression is a value may pop a message
from its message queue and apply it to its ţḩi̧ş
eval-actor-msg. Any actor in H may step its current
expression, possibly also causing some effect on the heap
eval-actor-run. The relation
𝑖𝑑⊢⟨ H, e ⟩↪⟨
H', e' ⟩ denotes actor 𝑖𝑑 evaluating expression
e one step in heap H, resulting in a new heap and expression
e' and H'.

Sending a lambda to an actor prepends this lambda to the
receiver's message queue and results in the unit value
eval-send-actor. Sending a lambda v to a bestowed value
instead prepends a new lambda to the queue of the actor that
bestowed it, which simply applies v to the underlying passive
object eval-send-bestowed.

Function application replaces all occurrences of the parameter x
in its body by the argument v eval-apply. Mutation is a
no-op in practice eval-mutate. Bestowing a passive value
ι in actor 𝑖𝑑 creates the bestowed value
ι_id eval-bestow.

Creating a new object in actor 𝑖𝑑 adds a fresh location
ι' to the set of the actors passive objects L and results
in this value eval-new-passive. Creating a new actor adds a
new actor with a fresh identifier to the heap. Its local heap
contains only the fresh ţḩi̧ş, its queue is empty, and its
current expression is the unit value eval-new-actor.

We handle evaluation order by using an evaluation context E
eval-context.





 §.§ Well-formedness


wf shows our well-formedness rules. A heap H is well-formed if all its actors are well-formed with
respect to H, and the local heaps L_i and L_j of any two
different actors are disjoint wf-heap. We use
ℒℋ(H(id)) to denote the local heap of actor id.

An actor is well-formed if its ţḩi̧ş is in its local heap L
and its message queue Q is well-formed. The current expression
e must be typable in the empty environment, and all passive
objects ι that are subexpressions of e must be in the
local heap L. Similarly, all actor identifiers in e must be
actors in the system, and all bestowed objects must belong to the
local heap of the actor that bestowed it wf-actor.

A message queue is well-formed if all its messages are well-formed
wf-queue-*. A message is well-formed if it is a well-formed
anonymous function taking a passive argument, and has a body e
with the same restrictions on values as the current expression in
an actor.



 §.§ Meta Theory

meta

We prove soundness of our language by proving progress and
preservation in the standard fashion:


  Progress: In a well-formed heap H, each actor can
  either be evaluated one step, or has an empty message queue and
  a fully reduced expression:

    ∀ id ∈𝐝𝐨𝐦(H).
      ⊢ H 
        (∃ H'  .  H id↪ H')
          
        (H(id) = (ι, L, ϵ, v))




  Preservation: Evaluation preserves well-formedness of heaps:
⊢ H    H id↪ H' ⊢ H'


Both properties can be proven to hold with straightforward
induction.

The main property that we are interested in for our language is
data-race freedom. As we don't have any actual effects on passive
objects, we show this by proving that if an actor is about to
execute ι.m̧u̧ţa̧ţȩ(̧)̧, no other actor will be about to
execute m̧u̧ţa̧ţȩ on the same object:


  Data-race freedom: In a well-formed system, for any two
  possible reductions that involve two different actors each
  mutating a passive object, the respective passive objects can
  never be the same.

    (
    [                      id_1 ≠ id_2;  H(id_1) = (ι_1, L_1, Q_1, ι.()); H(id_2) = (ι_2, L_2, Q_2, ι'.()) ])
    ι≠ι'


This property is simple to prove using two observations on what
makes a well-formed heap:



  * An actor will only ever access passive objects that are in
  its local heap wf-actor.

  * The local heaps of all actors are disjoint wf-heap.



The key to showing preservation of the first property is in the
premise of rule e-send which states that all free variables
and values must have an active type
(Γ_α, x : 𝗉⊢ e' : τ' and ∄ι . ι∈ e'). This prevents
sending passive objects between actors without bestowing them
first. Sending a message to a bestowed object will always relay
it to the actor that owns the underlying passive object
(by the premise of wf-actor: ∀ι_id∈ e  . ι∈ℒℋ(H(id))).

Preservation of the second property is simple to show since
local heaps grow monotonically, and are only ever extended with
fresh locations eval-new-passive.

Having made these observations, it is trivial to see that an actor
in a well-formed heap H that is about to execute
ι.m̧u̧ţa̧ţȩ(̧)̧ must have ι in its own local heap. If
another actor is about to execute ι'.m̧u̧ţa̧ţȩ(̧)̧, ι'
must be in the local heap of this actor. As the local heaps are
disjoint, ι and ι' must be different. Since
well-formedness of heaps are preserved by evaluation, all programs
are free from data-races.

Finally, we show that atomic blocks indeed provide atomicity. For
this version of the semantics, we do not state this property
formally;

since atomic blocks are implemented as “big messages”, and
messages are always run to completion before another message is
handled, it follows trivially that atomic operations run without
any interleaving in this semantics.




 §.§ Mechanisation

coq

The formalism presented in this section has been fully mechanised
in Coq, including proofs of progress and preservation
<cit.>. The mechanised version is true to the paper
version, modulo uninteresting differences in representation (for
example, the heap is a list of actors indexed by actor ids,
rather than a map from ids to actors as in
dyn-semantics). It also includes machinery for generating
fresh values.

The whole definition of the semantics is ≈450 lines of Coq. The
proofs are ≈2100 lines, including ≈340 lines of auxiliary lemmas
about list operations and ≈250 lines of tactics specific to this
formalism, including automated case analysis for heap operations.
The proofs also make use of the LibTactics library
<cit.>, as well as the çŗu̧şḩ tactic <cit.>.
There is still some repetition between similar cases in some of
the proofs, which could be broken out to further reduce the size
of the proof.



§ FORMALISING PRIVATE MAILBOXES AND BESTOW WITH OWNERSHIP TRANSFER

formal2

This section explores two variations on the semantics presented in
formalism; bestowed objects that may change owner, and
atomic message passing using private message queues. Both of these
variations have also been fully mechanised and proven sound in
Coq <cit.>.



 §.§ Transferring Ownership of Bestowed Objects

transfer









So far, bestowed objects have always been passive objects owned by
some actor, and the owner of these objects never changes. This
means that once an object has been bestowed and shared between
actors, messages to it will always be relayed to the same actor.
If an actor bestows many objects, the (implicit) contention on
this actor will be high. If ownership of a bestowed object could
be transferred, some of this contention could be alleviated.

transfer-syntax shows the syntax of this language
variation. A transferable object has type
𝐓(𝗉). Since such an object may move between
actors, we cannot allow this object to have aliases of the
non-transferable type 𝗉. Here, we solve this by
requiring the object to be created as transferable with ņȩw̧
𝐓(𝗉), which voids the need for a b̧ȩşţo̧w̧
operation. Dynamically, a transferable object has the value
ι_*. An actor which evaluates ι_*!̧v when it is the
owner of ι_* will perform v ι synchronously. Other
actors will relay to the current owner.

Note that transferring ownership of an object does not prevent the
previous owner from retaining a reference to the transferred
object. The only difference is that messages sent to the
transferred object will now be relayed to the new owner instead.

transfer-static shows the new and changed rules of the
static semantics. There are two new rules for typing transferable
objects (e-new-trans, e-trans). A subtle change is also
needed in the send rule: the body of the message sent must have
type U̧ņi̧ţ to preserve the type of the expression when the
message is run synchronously e-send-trans. This is without
loss of generality since actors cannot do anything with the result
of a message send.

transfer-dynamic shows the new and changed rules of the
dynamic semantics. To track the current owner of a transferable
object, we extend the configuration with a map 𝒪 from
locations ι to actors ι. Creating a new transferable
object adds its creator to the owner map eval-new-trans. When
evaluating ι_*!̧v, the owner of ι_* will be looked
up in 𝒪 and the message will either be run
synchronously eval-send-trans-run or be relayed to the
current owner eval-send-trans-delegate. In
formalism, the “unpacking” of the bestowed object
happens upon delegation ( eval-send-bestowed in
dynamic). Here, the owner may have changed when the
message arrives, so the message we send contains the original
message send ι_*!̧v to allow further delegation if
needed.

We allow ownership transfer when the current owner is not running
a message eval-actor-trans. If ownership could be transferred
in the middle of an actor's behavior, there could be data-races.
When ownership of an object is transferred, its location ι
is also moved between the local heaps of the actors involved in
the transfer. Note that there may still be delegated messages in
the queue of the old owner, and that these will be forwarded to
the new owner when they reach the head of the queue. Ownership
transfer is non-deterministic to simulate a run-time or scheduler
that does load-balancing between actor behaviors.

Finally, trans-wf shows the new and changed
well-formedness rules. An owner map 𝒪 is well-formed
if for all mappings ι↦ id, id is an actor which has
ι in its local heap wf-owners. For a well-formed actor,
its ţḩi̧ş must not be in 𝒪 ( not be
transferable, since ţḩi̧ş of an actor never changes owner), and
for all transferable values in its current expression, there must
be some mapping for that location in 𝒪
wf-actor-trans. Similar rules hold for messages, but
additionally their locations ι may not have transferable
ownership , as this would mean
that their ownership could be transferred before the message has
reached the head of the queue.

The adaptation of the meta-theoretic properties is
straightforward, and the same soundness properties hold for this
variation of the formalism. The mechanised version of the
semantics are ≈470 lines of Coq, and the proofs are ≈2600 lines
with the same ≈600 lines of list lemmas and tactics as for the
core calculus <cit.>.



  §.§.§ Design Considerations for Transferable Objects


For simplicity, this variation does not include the bestowed
references from the formalism in formalism. It is
possible to combine both flavors of bestowed references in the
same system as long as care is taken to ensure that an object is
never both bestowed and transferable. The only place where such an
object could be created is when a transferable object is being
operated on synchronously ( eval-send-trans-run in transfer-dynamic). This
could for example be achieved by introducing a type annotation
which disallows bestowing, and requiring that the parameter of a
message has this annotation when sending to a transferable object.

Another simplification in these formalisms is the absence of
fields in passive objects. If objects could refer to other
objects, a transferable object would not be allowed to refer to
actor-local passive objects, as these references would violate
actor isolation if the object was transferred. In Kappa, the type
system tracks if an object is (thread- or) actor-local, so
preventing transferable objects from referring to such objects is
straightforward.

Transferable objects may safely refer to
objects of active type (actors or transferable/bestowed objects)
or passive objects that are encapsulated by the transferable
object itself. Notably, with bestowed objects no such restriction
is necessary; as a bestowed object is only ever operated on by its
owner, it may only ever get passive references to objects with the
same owner.




 §.§ Private Message Queues












The calculus presented in formalism encodes atomic
operations by batching several operations in a single message.
While this gives some control over the interleaving of messages,
it does not allow the sending actor to react to intermediate
results of the atomic operation. 


For example, an actor interacting with a list may want to
atomically iterate over the list, operating on each element along
the way, without allowing interleaved operations on the list in
the meantime.

This section extends our core calculus with support for
private message queues. An actor can start a private
“conversation” with another actor by creating a new queue and
passing it as a message. When an actor receives a new queue it
will read messages from this queue until it receives a message to
end the conversation. Messages sent by other actors will still be
enqueued in the actor's public queue.

On the surface level, two dual operations are added:
a̧ţo̧m̧i̧çe begins a new atomic operation, and ŗȩļȩa̧şȩe
finishes it ( private-syntax). The target of
a̧ţo̧m̧i̧ç or ŗȩļȩa̧şȩ can be actors or bestowed objects (
private-static). In the latter case, the owner of the
bestowed object gets sent the private queue. The two operations do
not have to appear in the same procedure body, and the language
does not enforce that an a̧ţo̧m̧i̧ç expression has a matching
ŗȩļȩa̧şȩ. In a real programming language, using a blocked
construct is probably more practical—this is how a̧ţo̧m̧i̧ç is implemented in Encore.

Dynamically, we need three extensions to the configuration. First,
each actor is extended with a map C of its ongoing
conversations. C maps actors id to queue identifiers q.
Second, a global map ℳ maps queue identifiers q to
queues and the owner of the queue (the actor who is reading from
it). Third, a message can now be a request for starting a private
conversation using queue q (𝐀𝐭(q)), a request for
ending a conversation (𝐄𝐧𝐝), or a normal message
modelled as anonymous function as before.

private-dynamic1 shows the two new rules for how actors
react to atomic messages. If the head of the actor's public queue
is 𝐀𝐭(q), the private queue corresponding to q is
looked up in ℳ and the first message from this queue
is run, leaving the public queue intact eval-actor-priv-run.
If the head of the private queue is 𝐄𝐧𝐝, the private
queue is dropped from ℳ and the 𝐀𝐭(q)
message is popped from the public queue, allowing the actor to
continue reading messages normally eval-actor-priv-end.

private-dynamic2 shows the rest of the new dynamic rules.
Since we handle starting and finishing of atomic operations, on
both actor and bestowed objects, and these operations can succeed
or fail, there is a large number of new rules. The rules in the
left column all handle actor targets, and the rules in the left
column all handle bestowed targets.

Initiating an atomic operation with actor id' creates a fresh
queue identifier q and updates the current actor so that its
conversation map C maps id' to q. The global map is updated
so that q maps to an empty queue belonging to id', and an
atomic request 𝐀𝐭(q) is enqueued to the public queue of
id' eval-atomic-actor. If the current actor already has a
private conversation with id'—that is, id' is already in
C—the expression is a no-op eval-atomic-actor-fail. The
rules for a bestowed target is symmetric eval-atomic-bestowed-*.

Finishing an atomic operation with actor id' looks up the queue
identifier of the conversation with that actor in C and appends
an 𝐄𝐧𝐝 message to the end of the corresponding private
queue. Since this denotes the end of the conversation, the mapping
from id' is dropped from C eval-release-actor. If there
is no ongoing conversation with id'—that is, id' is not in
C—the expression is a no-op eval-release-actor-fail.
Again, the rules for a bestowed target is symmetric
eval-release-bestowed-*.

Finally, sending a message to an actor id' with whom the current
actor has a private conversation looks up the queue identifier of
this conversation in C (extracted from the actor using the helper function 𝒞) and adds the message to the corresponding
private queue in M eval-send-actor-atomic. The case for a
bestowed target is symmetric eval-send-bestowed-atomic. The
rules for normal message sends (not shown here) are extended with
a premise that there is no ongoing private conversation with the
receiving actor.

private-wf shows the new and changed well-formedness
rules. The queue map ℳ is well-formed if for each
mapping q ↦ (Q, id), the private queue Q is well-formed
with respect to actor id and does not contain any requests for
new private conversations (any such new requests would arrive in
the public queue of the actor). Additionally, if there is an
𝐄𝐧𝐝 in the queue, there can be no actor in the heap
that has a private conversation through the queue identified by
q, since this actor has just ended the conversation
wf-queue-map.

The rule for well-formed heaps is extended with a premise stating
that the ranges of all actors' private conversations must be disjoint, meaning that no
two actors may send messages to the same private queue
wf-heap-priv. The rule for well-formed actors states that
each entry in the conversation map has a corresponding entry in
the global queue map. The public queue of an actor must not
contain 𝐞𝐧𝐝 messages (since these are necessarily sent
to the private queue), and all requests for atomic operations must
use distinct queue identifiers wf-actor-priv. There are two
new well-formedness rules for queues. A request for an atomic
operation must have a corresponding private queue waiting in the
global queue map wf-queue-atomic. 𝐄𝐧𝐝 messages are
always well-formed wf-queue-end.

To show that our private mailboxes are sound we define an informal
property:


  Atomicity: Once a private conversation between actors
  A and B has been initiated, actor B will only read
  messages sent by actor A, up until and including the
  𝐄𝐧𝐝 message.


The key rules for showing that atomic operations run without
interleaving are wf-heap-priv, which states that two
different actors cannot have a private conversation with the same
actor (preventing other actors from “hijacking” the private
queue that A is writing to), and wf-actor-priv, which
states that an ongoing private conversation with actor id' has a
corresponding queue belonging to id' in the global queue map
(guaranteeing that messages sent from A to B will indeed end
up in the mailbox that B is reading from). From the dynamic
rules eval-actor-priv-* it is easy to see that an actor will
keep reading from the same private message queue until it contains
an 𝐄𝐧𝐝 message.

The formulation of the remaining meta-theoretic properties requires adapting
the statement of progress to include the state when an actor is
waiting for a message to arrive to its current private queue.
After this adaptation, the same soundness properties hold for this
variation of the formalism as well. The mechanised version of the
semantics are ≈670 lines of Coq, and the proofs are
≈4000 lines with the same ≈600 lines of list
lemmas and tactics as for the other calculi <cit.>.
The increase in size compared to the other mechanisations is
explained by the large number of cases for evaluation as seen in
private-dynamic2. There is room for reducing the code
size by applying more automation to similar cases of the proofs.



  §.§.§ Design Considerations for Private Queues


The way private mailboxes are formalised here purposely have them
behave similar to locks in mainstream programming languages. The
a̧ţo̧m̧i̧ç and ŗȩļȩa̧şȩ keywords work like acquire and release
on a lock, and all operations carried out by an actor between
calls to a̧ţo̧m̧i̧ç and ŗȩļȩa̧şȩ enjoy absence of interleaving.

This is different from the implementation of a̧ţo̧m̧i̧ç in Encore,
where a new handle to the target actor is created whose type
expresses that messages sent to this actor will not be interleaved
with messages from other actors. This handle is statically
restricted from being passed to other actors and cannot survive
its corresponding atomic block (it is effectively borrowed (
<cit.>)). This forces code to explicitly
propagate this handle to everywhere where the handle is needed.

Allowing such a handle to be shared with other actors is possible,
as is bounding the duration of the sharing to the static scope of
the atomic block. This would extend the number of sources of
messages in a private conversation, and re-introduce interleaving
in a controlled fashion. We have yet to find compelling enough
reasons to support this in real programs.




§ EXPLORING BESTOW AND ATOMIC—CASE STUDIES

case-studies

In this section, we report on three case studies using bestow
and atomic to implement distributed hash tables, distributed
graphs, and atomic money transfer. These case studies highlight
the usefulness of bestow and atomic and some of their
properties, and also serve as more compelling motivating examples
(although less pedagogic) than the list example of
example.





 §.§ Case Study: Distributed Hash Tables


The Encore programming language was recently extended with support
for “locally distributed” arrays and hash tables. These data
structures are backed by several actors to enable true parallel
operations on disjoint parts. Distributing a hash table T over
N different actors allows up to N operations on T to be
carried out in parallel, provided that there are at least N
cores where the actors are scheduled in parallel[This is
  ultimately a decision made by the run-time system, and depends
  on the available cores, system load, etc.].

Encore's distributed hash tables are implemented purely as a
library construct. Each client of a hash table holds a single passive object which acts as a proxy for the
hash table and to this end keeps a map from hash ranges to actors
that it uses to delegate operations to the correct actor.
Distributing this ranges-to-actors map across all proxies is key
to the parallel performance.

Given the aforementioned map, puts and gets are straightforward to
implement. A more complex operation is rehashing, 
updating the map, possibly involving changing the number of actors
backing the data structure in the process. Rehashing involves
stopping all operations in all actors backing the data structure,
reconfiguring the map, and resume operations with the new map.
Since clients may continue to send messages using an outdated map
during rehashing, requests must be buffered until the new map
is in place, and possibly rerouted to another actor. The top right
of rehash shows excerpts of a p̧u̧ţ method that
buffers messages during rehashing.

rehash (left) shows a high-level implementation of the
rehashing function. The important lines with respect to bestow are
16 and 17, iterating over all hash-table proxies and updating
their ranges-to-actors maps. The type of each p̧ is
B̧(̧Ḩa̧şḩM̧a̧p̧)̧ meaning each call to update is wrapped in a closure
which is sent to the containing actor. This design requires that
all proxies are known by the distributed hash table, which is
easily handled  in a constructor and/or factory method. For
simplicity, we omit a versioning scheme checking that the map used
by a proxy is up to date (for example, checking that the
identity of the client's map was the same as the actor's current
map). This handles the case when calls are made on an outdated
proxy after rehashing is finished.

Without the ability to create bestowed references, we are
left with two—problematic—possibilities to implement rehashing:



  Polling for changes to the ranges-to-actors map

  In this scenario, proxies would continuously poll for changes to
  the map. Since polls cross actor boundaries, they would be
  asynchronous increasing the latency of hash table operations,
  possibly causing client actors to block waiting for polling
  responses.


  Forcing actors using hash-tables to implement support methods

  In this scenario, actors using hash-tables would be required to
  implement a special support method for updating client proxies.
  This has the downsides of pushing internal implementation detail
  out into the interface, not just for the actors themselves, but
  any library used inside the actor must somehow be interfaced with
  by the top-level to support updating ranges-to-actors maps.



As rehash shows, it is possible to avoid these problems
through bestowed references as these allow us to push
changes directly to the hash table proxies—without any special
requirements on the clients holding them.



An obvious extension to the atomic construct is the ability to
atomically operate on a number of subjects (actors in the current
example). In the case of a statically known number of subjects, it
is easy to implement a̧ţo̧m̧i̧ç ̧(̧a̧,̧ ̧b̧)̧ ̧.̧.̧.̧ as syntactic sugar
for nested atomic blocks. In the case of a dynamic number,
something similar can be done manually through recursion. If we
imagine a powerful atomic block able to suspend a number of
actors before performing its operations on all of them, and
then releasing them, the ŗȩḩa̧şḩ(̧)̧ function of
rehash could be greatly simplified:


def rehash() unit
  val new_map = this.create_new_map()
  atomic this.actors do – operate atomically on all actors in this set
    for a <- this.actors do
      a ! update(new_map)
  for p <- this.proxies do
    p ! update(new_map)


Notably this implicitly takes care of any buffering of messages
sent to actors backing the hash table while rehashing is taking
place. Furthermore, the aforementioned versioning scheme dealing
with messages sent via proxies whose maps are out of date could be
eliminated if lines 6 and 7 could be made part of the atomic block,
but would only be advisable if the number of proxies was very
small.




 §.§ Case Study: Distributed Graphs


Just like distributing a hash table over a collection of actors,
there are many cases where it is appropriate to distribute a graph
over a collection of actors. A simple representation of a graph is
an object structure where objects representing nodes model edges
using references, keeping a separate list of weights for edges.
When distributing such a model over several actors, different
actors own different nodes in the graph, and thus edges must
sometimes connect nodes across different actors. Here, bestowed
references can be used to abstract whether an edge is inter-actor
(meaning it points to a node inside the same actor) or
intra-actor.



A straightforward implementation of Dijkstra's shortest path
algorithm can be applied with bestowed edges, but will suffer from
added latency due to many lookups of edges or weights changing to
asynchronous message sends. This highlights the importance of
syntactically highlighting asynchronous sends with !̧, and
requiring the act of bestowing to be explicit. Consider for
example the following code, which (possibly) updates the shortest
paths to the nodes reachable from the current node:


for (n, dist) <- src ! edges() do
  unless visited.contains(n) then
    val new_distance = distances(src) + dist
    if new_distance < distances(n) then
      distances(n) = new_distance
      predecessors(n) = src


On Line 1, we obtain the edges and weights for the neighbours of
node şŗç. If şŗç points to another actor o, this lookup
will involve an asynchronous call to o to obtain the result. If
şŗç is local to the current actor, this operation can be
converted to a fast synchronous lookup. In this code, we only use
the identity of ņ, which is a fast operation regardless
whether ņ is a bestowed reference or not.

load-balancing depicts a graph distributed over two
actors. The thick path denotes a “hot path” in the system,
meaning a path that is traversed often. In a system that is able to
load-balance passive objects as discussed in
load-balancing and formalised in formal2,
traversing the hot path could lead to moving the green objects on
the hot path from actor B to actor A, allowing A to operate
synchronously on all the objects in the path, without any latency added
by crossing a dashed edge. The figure also illustrates how
load-balancing might lead to increasing inter-actor references.
The performance impact of increased number of inter-actor
references naturally depends on how frequently they are
dereferenced.




 §.§ Case Study: Money Transfer



Money transfer across bank accounts is a classic example of
atomicity. Imagine actors acting as banks, and each bank holding
passive objects as bank accounts. Foregoing whether unrestricted
external access to a bank account is advisable from a security
perspective, bestowed references allows exposing the interfaces of
individual bank accounts outside of the banks, and also the
construction of an atomic transfer operation even if the banks
themselves do not support it. The following function uses a
combination of bestowed pointers and atomic blocks to implement
transfer in a straightforward fashion:


def transfer(amount : int, from : B(Account), to : B(Account)) : unit
  atomic from do
    atomic to do
      if from ! withdraw(amount) then
        to ! deposit(amount)


Notably, providing syntactic sugar for the nested atomic
blocks is straightforward. When this block is executed, if the
accounts are owned by the same actor, the
whole content of the atomic block can be sent to the owning actor
to be performed there in a synchronous fashion. Outside of this
special case, because we are nesting atomic blocks, external messages to
the actors referenced by f̧ŗo̧m̧ and ţo̧ will not be received
until after Line 4. Thus, no other actor will be able to
witness that a̧m̧o̧u̧ņţ money is “missing” in the system,
between Lines 3 and 4.

Notably, a single atomic block can be strong enough to
support a limited form of inter-actor atomicity for two actors, if
the current actor is one of them, with a small modicum of extra
work for the programmer:


def transfer(amount : int, from : Account, to : B(Account)) : unit
  atomic to do
    if from.withdraw(amount) then
      val done = to ! deposit(amount)
      done.get()


On Line 3, w̧i̧ţḩḑŗa̧w̧(̧)̧ can be called synchronously because
f̧ŗo̧m̧'s type captures that it is a local object. Thus, external
actors' inability to witness the change before the end of the
ţŗa̧ņşf̧ȩŗ(̧)̧ method arises naturally from the
single-thread-of-control invariant of actors. On Line 4, we
capture the future return value of ḑȩp̧o̧şi̧ţ(̧)̧ and block on its
return on Line 5. Thus, the transfer method will not finish until
the money has been deposited in the target account.

Note that because the type of f̧ŗo̧m̧ is not bestowed, this
version of ţŗa̧ņşf̧ȩŗ(̧)̧ cannot be called externally by other
actors. For that to be possible, there needs to be some way for
external actors to identify a particular account, such as a unique
account number.




§ IMPLEMENTATION IN ENCORE

implementation

A prototypical implementation of bestow and atomic exists
in Encore, and is currently being hardened to become part of the
main branch. The prototype has been instrumental in understanding
the performance implications of the two constructs, especially in
relation to Encore's support for fully concurrent garbage
collection <cit.>. A more comprehensive account of the
implementation aspects can be found in <cit.>.

We extend each actor class with an implicit method p̧ȩŗf̧o̧ŗm̧
which takes a function, applies it to the ţḩi̧ş of the
receiver, and returns the result wrapped in a future. A bestowed
reference is logically implemented as a pair of values,
o̧w̧ņȩŗ and o̧b̧j̧ȩçţ. A message send x̧ ̧!̧ ̧m̧(̧)̧ on a
bestowed reference is translated into the message send x̧.̧o̧w̧ņȩŗ ̧!̧
̧ ̧ ̧p̧ȩŗf̧o̧ŗm̧(̧(̧λ _̧ ̧.̧ ̧x̧.̧o̧b̧j̧ȩçţ.̧m̧(̧)̧)̧)̧.

The atomic block is implemented using the private mailbox
semantics sketched in atomic and formalised in formal2. An
atomic block is turned into a pair of matching a̧çq̧u̧i̧ŗȩ and
ŗȩļȩa̧şȩ operations, where the former creates and installs the
private mailbox and returns an atomic reference, and the latter
sends the termination message that reinstates the mailbox at the
start of the atomic block. Similar to a bestowed reference, an
atomic reference is logically implemented as a pair of values
ţa̧ŗģȩţ and m̧a̧i̧ļb̧o̧x̧, and a message send x̧ ̧!̧ ̧m̧(̧)̧ on an
atomic reference uses a special message sending primitive that
directs the message to m̧a̧i̧ļb̧o̧x̧ instead of the normal mailbox.

.2

atomic x do
  x ! foo(42)
  x ! bar(-42)



.7

let x' = acquire x in
  x' ! foo(42)
  x' ! bar(-42)
  release x'









































In previous work <cit.>, we explored an
implementation of atomic with coalescing semantics. While this is
less general than the private mailbox semantics, our original
assumption was that it might serve as an optimisation in simple
uses of atomic. However, an implementation of bestow close to the
formal semantics of coalescing ( formalism) involves
creation of closures passed from the operating actor to the owner
of the passive object. Without special optimisation, the overhead
of closure creation, and garbage collection of the closure value
is significant. We illustrate this in ping-overhead
(left) through a modified version of the Ping benchmark
from the Computer Language Benchmark Game <cit.> where two actors are
involved in a ping–pong exchange of messages. The figure shows a
fairly constant slowdown for the bestowed version of
11–16× over the non-bestowed counterpart. The main source
of this overhead is fully concurrent garbage collection—the
closure is being created on the local heap of one actor and then
sent to another, which must eventually inform the creating actor
when the closure is no longer needed. Passing closures by copy is
likely to reduce this overhead. This benchmark clearly
demonstrates that programs mostly operating on bestowed pointers
might see a noticeable slowdown.

In contrast, the right-hand-side of ping-overhead shows
that the combination of bestow and atomic can outperform
the actor-only solution. By wrapping the loop containing the
message sends in an atomic, the entire loop can be transferred
to the receiver where it can be run synchronously. This reduces
the number of asynchronous message sends, which involve expensive
ÇA̧Ş operations on mailboxes, and enables compile-time
optimisations such as inlining.




In grouping-semantics, we noted that atomic blocks
add structure to actor-programs. If desired, this can be leveraged
in scheduling. When executing a̧ţo̧m̧i̧ç ̧a̧ ̧ḑo̧ ̧.̧.̧.̧, if the actor
denoted by a̧ is idle, meaning its mailbox is empty, it
is possible to turn the asynchronous operations inside .̧.̧.̧
synchronous,  turning  a̧ ̧!̧ ̧p̧i̧ņģ(̧)̧ into a̧.̧p̧i̧ņģ(̧)̧.
This avoids context switching, enables inlining as well as other
optimisations such as removing future indirection which are costly
in Encore. Static analysis can be used to determine whether
removing asynchrony may also remove possible parallel
gains. Making asynchronous operations synchronous allows mixing
the methods of several actors on the same stack frame because
control flow is guaranteed to match the order that frames are
pushed onto and popped from the stack.



§ RELATED WORK

related

An important property of many actor-based systems is that a single
actor can be reasoned about sequentially; messages are exchanged
concurrently but executed sequentially by the receiving actor. For
this property to hold, actors often rely on actor isolation
<cit.>,  that the state of one actor cannot be accessed
by another. If this was the not the case, concurrent updates to
shared state could lead to data-races, breaking sequential
reasoning.

Existing techniques for achieving actor isolation are often based
on restricting aliasing, for example copying all data passed
between actors <cit.>, or relying on linear types to
transfer ownership of data <cit.>. Bestowed objects offer an alternative technique
which relaxes actor isolation and allows sharing of data without
sacrificing sequential reasoning. Combining bestowed objects with
linear types is straightforward and allows for both ownership
transfer and bestowed sharing between actors in the same system.

Miller  propose a programming model based on function
passing, where rather than passing data between concurrent actors,
functions are sent to collections of stationary and immutable data
called silos <cit.>. Bestowed objects are related in
the sense that sharing them doesn't actually move data between
actors. In the function passing model, they could be used to
provide an interface to some internal part of a silo, but
implicitly relay all functions passed to it to its owning silo.

While the formalism in formalism also works by passing
functions around, this is to abstract away from unimportant
details, and not a proposed programming model.

References to bestowed objects are close in spirit to remote
references in distributed programming or eventual references in E
<cit.>. In the latter case, the unit of
encapsulation,  an actor or an aggregate object protected by
a lock, acts similar to a Vat in E, but with an identifiable
boundary and an identity with an associated interface.

By bestowing and exposing sub-objects, a unit of encapsulation can
safely delegate parts of its interface to its inner objects, which
in turn need not be internally aware of the kind of concurrency
control offered by their bestower.

The Emerald language <cit.> has an entire
“locatics” system for expressing object placement and mobility
combined with an object-based language. Very early, Emerald
introduced call-by-move which allowed parameters of a call
to a remote object to be moved to the target's location
<cit.>.

Any actor system which supports sharing of mutable state could
implement individual bestowed objects by using a wrapper with the
same interface as the bestowed object, but where all operations
are delegated to some actor. Similarly, in a language with locks,
a wrapper object could grab a specified lock before calling the
underlying methods.

In both cases, this comes at the cost of explicitly creating
wrapper objects for all bestowed objects, and requires that the
programmer never directly accesses the object inside the wrapper.

For actor systems, bestowed references make the most sense when
messages are handled in sequence. In languages where messages are
explicitly and selectively received by each actor, the owning
actor would have to regularly check for incoming delegated
operations.

X10 introduces a language construct that is called atomic for
executing multiple operations in sequence without interleaving
<cit.>, but with different semantics and notably no
support for side effects or blocking operations.

Ibrahim  introduce the concept of Remote Batch Invocation
for combining operations to be run remotely in a distributed
system (in Java) <cit.>. This is similar to the coalescing
semantics of atomic blocks, but more advanced since parts of a batch
may consist of local computations, allowing the client to react to
the results of the remote operations inside the batch, while still
only making a single round-trip to the server. The private mailbox
semantics of atomic blocks is more flexible than Remote Batch
Invocation, but would be more expensive in a distributed setting
where each remote call is costly.

The coalescing semantics of atomic blocks can be implemented in
any actor language with closures by sending a closure performing
the desired operations in a message. This requires that the
receiving actor has support for running arbitrary closures, which
complicates reasoning about the behaviour of that actor (in our
Encore implementation, the p̧ȩŗf̧o̧ŗm̧ method is only ever called
implicitly as an effect of an atomic block).

Languages with selectively receives can encode the kind of
“private conversation” between two actors, offered by the
private mailbox semantics of atomic blocks, but requires that the
receiving actor is implemented with support for atomically
processing exactly the messages that the client wanted to send.

To the best of our knowledge, there are no other systems which
implicitly delegates locking based on ownership, as when bestowing
the internal state of a locked object.

Ownership types have been used to enforce strong encapsulation and
to allow a single lock to safely govern access to an entire object
aggregate,  in Universes for Race Safety <cit.> or
Parameterized Race Free Java (PRFJ) <cit.>.
PRFJ additionally allows the programmer to specify a lock-order
and enforces that locks are taken in this order, preventing
deadlocks. Kappa does not attempt to prevent deadlocks, and
bestowed references to the private state of locked objects may be
subject to deadlocks.

Universes for Race Safety allow references with unknown owners,
possibly crossing encapsulation boundaries, but require explicitly
locking these objects before they are accessed. In contrast,
accessing a bestowed object only requires locking the owner
object (which is done implicitly).

When using locks, the atomic block behaves like Java's
şy̧ņçḩŗo̧ņi̧z̧ȩḑ blocks, but Kappa additionally precludes
accidentally bypassing the lock of a locked object.

Locked objects in Kappa are protected by a readers-writer lock,
which allows a single writer, but multiple concurrent readers
(statically enforcing that readers will not cause mutation). A
bestowed reference into a locked aggregate which only exposes
reading operations can therefore acquire a reading lock, allowing
multiple concurrent readers through bestowed references to the
same aggregate.



§ DISCUSSION AND CONCLUSION

discussion

Although our formal description and all our examples focus on
actors, bestow also works with threads and locks. An object
protected by a lock can share one of its internal objects while
requiring that any interaction with this object also goes via this
lock.

We believe there is also a straightforward extension to software
transactional memory. In the future, we would like to study
combinations of these.

Bestowed objects let an actor expose internal details about its
implementation. Breaking encapsulation should always be done with
care as leaking abstractions leads to increased coupling between
modules and can lead to clients observing internal data in an
inconsistent state. The latter is not a problem for bestowed
objects however; interactions with bestowed objects will be
synchronised in the owning actor's message queue, so as long as
data is always consistent between messages, we can never
access data in an inconsistent state (if your data is inconsistent
between messages, you have a problem with or without bestowed
objects).

Sharing bestowed objects may increase contention on the owner's
message queue as messages to a bestowed object are sent to its
owner. Similarly, since a bestowed object is protected by the same
lock as its owner, sharing bestowed objects may lead to this lock
being polled more often.

As always when using locks there is a risk of introducing
deadlocks, but we do not believe that bestowed objects exacerbate
this problem. Deadlocks caused by passing a bestowed object back
to its owner can be easily avoided by using reentrant locks (as
accessing them both would require taking the same lock twice).

When using locks, atomic blocks are very similar to Java's
şy̧ņçḩŗo̧ņi̧z̧ȩḑ-blocks. With actors, an atomic block groups
messages into a single message. For fairness, it may make sense to
only allow atomic blocks that send a limited number of
messages.

It is possible to synchronise on several locked objects by simply
grabbing several locks. Synchronising on several actors is more
involved, as it requires actors to wait for each other and
communicate their progress so that no actor starts or finishes
before the others. The canonical example of this is atomically
withdrawing and depositing the same amount from the accounts of
two different actors. Interestingly, if the accounts are bestowed
objects from the same actor ( some bank actor), this atomic
transaction can be implemented with the message batching approach
suggested in this paper. We leave this for future work.

Actor isolation is important to maintain sequential reasoning
about actors' behavior. By bestowing activity on its internal
objects, an actor can share its representation without losing
sequential reasoning and without bloating its own interface. With
atomic blocks, a client can create new behavior by composing
smaller operations. While bestowed references may not be very
efficient, due to their asynchronous nature, they can be used in
concert with atomic blocks to move entire operations closer to
data operated on, which can not only avoid the negative
performance implications of bestowed references, but lead to
performance improvements over pure actor-based solutions.

An earlier version <cit.> of this work quipped “actors
without borders”, in the sense of relaxing isolation-based
data-race freedom using our bestowed references. The same is true
for lock-based synchronisation—bestowed references allows
several objects to sit at the boundary of synchronisation, and
share a common lock. In some ways, this is similar to multiple
ownership <cit.>, but extended to a concurrent
setting. By tracking bestowed-ness through types, operations on
resources owned by others are clearly visible at the use-site, but
need no forethought at the declaration-site: the bestowed objects
themselves do not need to know why access to them is safe, nor
even be aware of their sharing. They can simply trust the safety
of living in a world where borders are a means to an end, not an
end.


10
url<#>1urlprefixURL href#1#2#2 #1#1

hewitt1973session
C. Hewitt, P. Bishop, R. Steiger, Session 8 formalisms for artificial
  intelligence a universal modular actor formalism for artificial intelligence,
  in: Advance Papers of the Conference, Vol. 3, Stanford Research Institute,
  1973.

baker1977laws
H. Baker, C. Hewitt, http://hdl.handle.net/1721.1/41973Laws for
  communicating parallel processes, MIT Artificial Intelligence Laboratory
  Working Papers.
<http://hdl.handle.net/1721.1/41973>

ArtOfMultiProg
M. Herlihy, N. Shavit, The Art of Multiprocessor Programming, Morgan Kaufmann
  Publishers Inc., San Francisco, CA, USA, 2008.

Art:STM
M. Herlihy, J. Eliot B. Moss, Transactional memory: Architectural support for
  lock-free data structures, International Symposium on Computer
  Architecturehttp://dx.doi.org/10.1145/165123.165164
  doi:10.1145/165123.165164.

castegren16
E. Castegren, T. Wrigstad, Reference Capabilities for Concurrency Control,
  in: ECOOP, 2016.
http://dx.doi.org/10.4230/LIPIcs.ECOOP.2016.5
  doi:10.4230/LIPIcs.ECOOP.2016.5.

encoreSFM
S. Brandauer, et al., Parallel Objects for Multicores: A Glimpse at
  the Parallel Language Encore, in: Formal Methods for Multicore
  Programming, 2015.
http://dx.doi.org/10.1007/978-3-319-18941-3_1
  doi:10.1007/978-3-319-18941-3_1.

RobustComposition
M. Miller, Robust composition: Towards a unified approach to access control and
  concurrency control, Ph.D. thesis, Johns Hopkins University, USA (May 2006).

AmbientTalk
T. Van Cutsem, E. G. Boix, C. Scholliers, A. L. Carreton, D. Harnie, K. Pinte,
  W. De Meuter, Ambienttalk: programming responsive mobile peer-to-peer
  applications with actors, Computer Languages, Systems & Structures 40 (3).

Art:Bestow
E. Castegren and T. Wrigstad, Actors without borders: Amnesty for imprisoned
  state, PLACEShttp://dx.doi.org/10.4204/EPTCS.246.4
  doi:10.4204/EPTCS.246.4.

bestow-repo
E. Castegren, Bestowed objects and atomic message passing,
  <https://github.com/EliasC/bestow-atomic> (2017).

OT
D. G. Clarke, J. M. Potter, J. Noble, Ownership types for flexible alias
  protection, in: ACM SIGPLAN Notices, Vol. 33, ACM, 1998.

erlang
J. Armstrong, A History of Erlang, in: HOPL III, 2007.
http://dx.doi.org/10.1145/1238844.1238850
  doi:10.1145/1238844.1238850.

activeObjects
R. G. Lavender, D. C. Schmidt, Active object–an object behavioral pattern for
  concurrent programming.

Art:ORCAOOPSLA
S. Clebsch, J. Franco, S. Drossopoulou, A. M. Yang, T. Wrigstad, J. Vitek,
  Orca: GC and Type System Co-Design for Actor Languages,
  Proceedings of the ACM on Programming Languages 1 (OOPSLA).

ponyAgere
S. Clebsch, S. Drossopoulou, S. Blessing, A. McNeil, Deny Capabilities for
  Safe, Fast Actors, in: AGERE, 2015.
http://dx.doi.org/10.1145/b2824815.2824816
  doi:10.1145/b2824815.2824816.

Akka
Akka – Scala actor library, <http://akka.io/> (Retrieved July 2017).

ProActive
D. Caromel, L. Henrio, A Theory of Distributed Objects, Springer-Verlag, 2004.

ABS
E. B. Johnsen, R. Hähnle, J. Schäfer, R. Schlatte, M. Steffen, Abs: A
  core language for abstract behavioral specification, in: Formal Methods for
  Components and Objects, Springer, 2011.

bernstein2014orleans
P. A. Bernstein, S. Bykov, A. Geller, G. Kliot, J. Thelin, Orleans: Distributed
  virtual actors for programmability and scalability, MSR-TR-2014–41.

Joelle
D. Clarke, T. Wrigstad, J. Östlund, E. B. Johnsen,
  http://www.springerlink.com/content/d502311675h73147/Minimal
  Ownership for Active Objects, in: Programming Languages and Systems
  (Procedings of the 6th Asian Symposium on Programming Languages and Systems),
  Vol. 5356/2008 of Lecture Notes in Computer Science, Springer, 2008.
http://dx.doi.org/10.1007/978-3-540-89330-1_11
  doi:10.1007/978-3-540-89330-1_11.
<http://www.springerlink.com/content/d502311675h73147/>

theoestlund
J. Östlund, Language Constructs for Safe Parallel Programming on
  Multi-cores, Ph.D. thesis, Department of Information Technology,
  Uppsala University (Jan 2016).

potanin2013your
A. Potanin, M. Damitio, J. Noble, Are your incoming aliases really necessary?
  counting the cost of object ownership, in: Proceedings of the 2013
  International Conference on Software Engineering, IEEE Press, 2013.

the-mueller
P. Müller, Modular Specification and Verification of Object-oriented
  Programs, Springer-Verlag, Berlin, Heidelberg, 2002.
http://dx.doi.org/10.1007/3-540-45651-1
  doi:10.1007/3-540-45651-1.

QDL
D. Klaftenegger, K. Sagonas, K. Winblad,
  http://doi.acm.org/10.1145/2612669.2612714Brief announcement: Queue
  delegation locking, in: Proceedings of the 26th ACM Symposium on Parallelism
  in Algorithms and Architectures, SPAA '14, ACM, New York, NY, USA, 2014.
http://dx.doi.org/10.1145/2612669.2612714
  doi:10.1145/2612669.2612714.
<http://doi.acm.org/10.1145/2612669.2612714>

milner1999communicating
R. Milner, Communicating and mobile systems: the pi calculus, Cambridge
  university press, 1999.

hoare1978communicating
C. A. R. Hoare, Communicating sequential processes, in: The origin of
  concurrent programming, Springer, 1978.

libtactics
B. C. Pierce, A. A. de Amorim, C. Casinghino, M. Gaboardi, M. Greenberg,
  C. Hritcu, V. Sjöberg, B. Yorgey, Software Foundations, Electronic
  textbook, 2017, version 5.0.

cpdt
A. Chlipala, Certified Programming with Dependent Types: A Pragmatic
  Introduction to the Coq Proof Assistant, The MIT Press, 2013.

Boyland
J. Boyland, J. Noble, W. Retert,
  https://doi.org/10.1007/3-540-45337-7_2Capabilities for sharing: A
  generalisation of uniqueness and read-only, in: ECOOP 2001 -
  Object-Oriented Programming, 15th European Conference, Budapest, Hungary,
  June 18-22, 2001, Proceedings, 2001.
http://dx.doi.org/10.1007/3-540-45337-7_2
  doi:10.1007/3-540-45337-7_2.
<https://doi.org/10.1007/3-540-45337-7_2>

TheWrigstad
T. Wrigstad, Ownership-based alias management, Ph.D. thesis, Royal Institute of
  Technology, Kista, Stockholm (May 2006).

JoelBSC
J. Wallin, Implementing Safe Sharing Features for Encore, Bachelor Thesis
  IT 17 039 (July 2017).

bench_game
The computer language benchmarks game,
  <http://benchmarksgame.alioth.debian.org> (Retrieved July 2017).

kilim
S. Srinivasan, A. Mycroft, Kilim: Isolation-Typed Actors for Java, in: ECOOP,
  2008.
http://dx.doi.org/10.1007/978-3-540-70592-5_6
  doi:10.1007/978-3-540-70592-5_6.

haller2010
P. Haller, M. Odersky, Capabilities for Uniqueness and Borrowing, in: ECOOP,
  2010.
http://dx.doi.org/10.1007/978-3-642-14107-2_17
  doi:10.1007/978-3-642-14107-2_17.

miller
H. Miller, P. Haller, N. Müller, J. Boullier, Function passing: A model for
  typed, distributed functional programming, in: Onward!, 2016.
http://dx.doi.org/10.1145/2986012.2986014
  doi:10.1145/2986012.2986014.

black2007development
A. P. Black, N. C. Hutchinson, E. Jul, H. M. Levy, The development of the
  emerald programming language, in: Proceedings of the third ACM SIGPLAN
  conference on History of programming languages, ACM, 2007.

jul1988fine
E. Jul, H. Levy, N. Hutchinson, A. Black, Fine-grained mobility in the emerald
  system, ACM Transactions on Computer Systems (TOCS) 6 (1).

Art:X10
V. A. Saraswat, V. Sarkar, C. von Praun, X10: Concurrent programming for
  modern architectures, Principles and Practice of Parallel Programminghttp://dx.doi.org/10.1145/1229428.1229483
  doi:10.1145/1229428.1229483.

batching
A. Ibrahim, Y. Jiao, E. Tilevich, W. R. Cook, Remote batch invocation for
  compositional object services, in: European Conference on Object-Oriented
  Programming, Springer, 2009.

universes
D. Cunningham, S. Drossopoulou, S. Eisenbach, Universes for race safety,
  Verification and Analysis of Multi-threaded Java-like Programs (VAMP).

boyapati2002ownership
C. Boyapati, R. Lee, M. Rinard, Ownership types for safe programming:
  Preventing data races and deadlocks, in: ACM Sigplan Notices, Vol. 37, ACM,
  2002.

MOJO
N. R. Cameron, S. Drossopoulou, J. Noble, M. J. Smith,
  http://doi.acm.org/10.1145/1297105.1297060Multiple ownership,
  SIGPLAN Not. 42 (10).
http://dx.doi.org/10.1145/1297105.1297060
  doi:10.1145/1297105.1297060.
<http://doi.acm.org/10.1145/1297105.1297060>

ombudsmen
J. Östlund, T. Wrigstad,
  https://doi.org/10.1007/978-3-642-31057-7_8Multiple Aggregate Entry
  Points for Ownership Types, Springer Berlin Heidelberg, Berlin, Heidelberg,
  2012.
http://dx.doi.org/10.1007/978-3-642-31057-7_8
  doi:10.1007/978-3-642-31057-7_8.
<https://doi.org/10.1007/978-3-642-31057-7_8>



