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.
翻译:传递信息是执行并行程序的一个有用的抽象信息。 但是,对于现实世界系统来说,它往往与其他编程和货币范式相结合,例如高阶功能、变异状态、共模调调调和锁。 我们介绍Actris:证明使用上述特征组合的程序功能正确性的逻辑。 Actris将现代同时分离逻辑的力量与一流协议机制(以届会类型为基础)结合起来,用以推理在其他同类货币范式面前传递的信息。我们表明,Actris提供了适当的抽象程度,通过证明各种实例的功能正确性,包括基于频道的合并类型、基于频道的负载平衡映像仪和地图-调色模型的变体,使用简洁的规格。Actris在一份会议文件(PPPL'20)中已经介绍了现代同时同时存在的分离逻辑的力量,但本文大大扩展了先前的表述。此外,Actorris 2.0 和子协议概念 -- 以届会类型的子缩写为基础 -- 提供了一种适当的抽象性概念,这在将频道端端端端端的策略中具有额外的进一步证据,在Sholy Actortical 框架中具有充分的优势。