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
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. },
}