Actor Capabilities for Message Ordering (Extended Version)

TL;DR

This paper introduces actor capabilities, a protocol-based approach to restrict message ordering in actor systems, enhancing reasoning about message sequences and improving concurrency safety.

Contribution

It proposes a novel static capability system for actor references that enforces message order restrictions and integrates with effect systems for better behavior guarantees.

Findings

Actor capabilities restrict message sequences effectively.

The approach enables static reasoning about message order.

Layered effect systems ensure actors handle all possible messages.

Abstract

Actor systems are a flexible model of concurrent and distributed programming, which are efficiently implementable, and avoid many classic concurrency bugs by construction. However actor systems must still deal with the challenge of messages arriving in unexpected orderings. We describe an approach to restricting the orders in which actors send messages to each other, by equipping actor references -- the handle used to address another actor -- with a protocol restricting which message types can be sent to another actor and in which order using that particular actor reference. This endows the actor references with the properties of static (flow-sensitive) capabilities, which we call actor capabilities. By sending other actors only restricted actor references, they may control which messages are sent in which orders by other actors. Rules for duplicating (splitting) actor references ensure that these restrictions apply even in the presence of delegation. The capabilities themselves restrict message ordering, which may form the foundation for stronger forms of reasoning. We demonstrate this by layering an effect system over the base type system, where the relationships enforced between the actor capabilities and the effects of an actor's behaviour ensure that an actor's behaviour is always prepared to handle any message that may arrive.