AmbientTalk actors are data race and deadlock free

We recently published a new article on AmbientTalk, an actor language I co-designed with a focus on developing mobile applications for ad hoc wireless networks.

The main novelty of the article is what we believe to be the first formal account of the communicating event loops model, which is the concurrency model underlying the family of actor languages upon which AmbientTalk is based. Interestingly, this model is also closest to the concurrency model you get in JavaScript, if you think of a WebWorker as an actor.

The article gives a comprehensive overview of AmbientTalk’s roots, the language itself, and introduces a “featherweight AmbientTalk” calculus with an operational semantics. We use it to establish data race freedom (actors have isolated memory) and deadlock freedom (assuming all event loop turns are finite, all asynchronous messages sent between actors will eventually be processed).

The article is published in the journal "Computer Languages, Systems & Structures". A preprint copy of the paper is available here. Quoting the abstract:

The rise of mobile computing platforms has given rise to a new class of applications: mobile applications that interact with peer applications running on neighbouring phones. Developing such applications is challenging because of problems inherent to concurrent and distributed programming, and because of problems inherent to mobile networks, such as the fact that wireless network connectivity is often intermittent, and the lack of centralized infrastructure to coordinate the peers.

We present AmbientTalk, a distributed programming language designed specifically to develop mobile peer-to-peer applications. AmbientTalk aims to make it easy to develop mobile applications that are resilient to network failures by design. We describe the language's concurrency and distribution model in detail, as it lies at the heart of AmbientTalk's support for responsive, resilient application development. The model is based on communicating event loops, itself a descendant of the actor model. We contribute a small-step operational semantics for this model and use it to establish data race and deadlock freedom.