Actor Capabilities for Message Ordering

Gordon, Colin S.

Concurrent Programming, Open Systems and Formal Methods: Essays Dedicated to Gul Agha to Celebrate his Scientific Career, October 2025, doi: 10.1007/978-3-032-05291-9_3

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 they must still deal with the challenge of messages arriving in unexpected orders. 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 (flow-sensitive) static capabilities, which we call actor capabilities. By sending other actors only restricted actor references, actors 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 send 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.

Bibtex

@incollection{gulfest,
	bibtex_show = {true},
	abbr = {GulFest},
	author = {Gordon, Colin S.},
	title = {Actor Capabilities for Message Ordering},
	booktitle = {{Concurrent Programming, Open Systems and Formal Methods:
	             Essays Dedicated to Gul Agha to Celebrate his Scientific Career}
	             },
	editors = {Meseguer, Jos\'e and Varela, Carlos A. and Venkatasubramanian,
	           Nalini},
	year = {2025},
	note = "Invited Contribution..",
	month = {October},
	arxiv = {2502.07958},
	doi = {10.1007/978-3-032-05291-9_3},
	springer = {https://link.springer.com/chapter/10.1007/978-3-032-05291-9_3},
	address = {{Chicago, IL, USA}},
	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 they
	            must still deal with the challenge of messages arriving in
	            unexpected orders. 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 (flow-sensitive) static capabilities, which we call actor
	            capabilities. By sending other actors only restricted actor
	            references, actors 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 send 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. },
}