Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic

TL;DR

Actris 2.0 introduces an advanced logic combining session types with asynchronous message passing and subprotocols, enabling formal reasoning about complex concurrent programs with multiple paradigms.

Contribution

It extends previous work by adding subprotocols and asynchronous semantics, with formal proofs and mechanization in Coq for verifying concurrent programs.

Findings

Proved functional correctness of channel-based algorithms

Extended Actris with subprotocols for flexible composition

Mechanized the entire theory and examples in Coq

Abstract

Message passing is a useful abstraction for implementing concurrent programs. For real-world systems, however, it is often combined with other programming and concurrency paradigms, such as higher-order functions, mutable state, shared-memory concurrency, and locks. We present Actris: a logic for proving functional correctness of programs that use a combination of the aforementioned features. Actris combines the power of modern concurrent separation logics with a first-class protocol mechanism -- based on session types -- for reasoning about message passing in the presence of other concurrency paradigms. We show that Actris provides a suitable level of abstraction by proving functional correctness of a variety of examples, including a channel-based merge sort, a channel-based load-balancing mapper, and a variant of the map-reduce model, using concise specifications. While Actris was already presented in a conference paper (POPL'20), this paper expands the prior presentation significantly. Moreover, it extends Actris to Actris 2.0 with a notion of subprotocols -- based on session-type subtyping -- that permits additional flexibility when composing channel endpoints, and that takes full advantage of the asynchronous semantics of message passing in Actris. Soundness of Actris 2.0 is proven using a model of its protocol mechanism in the Iris framework. We have mechanised the theory of Actris, together with custom tactics, as well as all examples in the paper, in the Coq proof assistant.