Actor Capabilities for Controlled Actor Interactions (Keynote)

Colin S. Gordon

doi:10.1145/3830434.3839001

A fundamental challenge in developing concurrent systems is dealing with event orderings: both ensuring that intended and unavoidable event orderings are supported, and ensuring that no avoidable and unintended orderings are introduced by mistake. As a community, we’ve explored many approaches in language design and analysis tools to manage this problem when developing concurrent and distributed systems. It remains difficult to balance providing the guarantees we want, remaining flexible enough to allow real application code, and supporting a manageable path to retro- fit existing applications. We are using capabilities — an old idea that still holds some surprises — to reason about actor communications. The basic idea behind capabilities is to designate some special values as capabilities, and define operations we would like to reason about such that they require the capabilities to run. If we design the rest of the language or analysis to constrain or track how capabilities may propagate through a program, we gain a powerful reasoning principle: any part of the code that does not receive a particular capability necessarily does not trigger the associated operation(s). In other words: the set of capabilities that enter part of the program establish an upper bound on its behaviour. Substructural reference capabilities are a newer twist on this idea, where a static analysis (such as a type system) refines the capability values, such that different copies of the same value impose different restrictions. We take actor references or process IDs — the handles used to send messages to an actor — to be flow-sensitive reference capabilities. This allows us to attach policies for how clients (other actors) may communicate with an actor by refining the type of the actor reference: a capability’s type specifies the allowable orders in which messages may be sent to the recipient. Existing techniques for working with reference capabilities extend to this setting, allowing capabilities to be split and distributed among actors, delegating specific communication to other parties. An under-appreciated aspect of capabilities is that by constraining their evolution, it is possible to enforce global invariants through only local checks. While this often manifests as creating a fixed set of capabilities and ensuring no individual capability becomes more permissive, every time an actor retrieves its self-reference for a new purpose is effectively creation of a new capability. By augmenting our capability view with a sequential (flow-sensitive) effect system, we gain enough information statically to connect existing capabilities for messaging an actor with information about which messages the actor is prepared to receive — and in what order. This talk goes beyond an earlier version of this work presented at Gul Agha’s Festschrift (for a core actor calculus), describing efforts to apply these ideas to Elixir, Erlang’s prominent younger sibling. Extending to Elixir brings new challenges in dealing with system messages, supervision, and restarts; and reinforces classic challenges in coordination and state-dependent behaviour. We also revisit the code migration challenge, where reference capabilities’ natural support for an incremental migration path from simple types to richer capabilities complements Elixir’s ongoing incorporation of gradual typing.

Actor Capabilities for Controlled Actor Interactions (Keynote)

Files and links (1)

Abstract

Metrics

Details

Actor Capabilities for Controlled Actor Interactions (Keynote)

Files and links (1)

Abstract

Metrics

Details

Drexel University Social media