一句话：提出 Actris，将基于会话类型的一等协议机制融入并发分离逻辑，用 Coq 机器化验证消息传递程序的功能正确性。
消息传递是编写并发程序的重要抽象，但实际系统常将其与高阶函数、可变状态、共享内存并发、锁等范式混合使用。论文提出 Actris：一种用于证明混合使用上述特性的程序功能正确性的逻辑。Actris 将现代并发分离逻辑的能力与基于会话类型的一等协议机制结合起来，从而在其他并发范式共存的情况下推理消息传递。作者通过分布式归并排序、分布式负载均衡 mapper 以及 map-reduce 变体等实例，用相对简单的规约证明了功能正确性，说明 Actris 提供了合适的抽象层次。其协议的可靠性在 Iris 框架中通过模型证明，理论、符号执行策略及全部示例均已在 Coq 证明助手中机器化。
Message passing is a useful abstraction to implement 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 distributed merge sort, a distributed load-balancing mapper, and a variant of the map-reduce model, using relatively simple specifications. Soundness of Actris is proved using a model of its protocol mechanism in the Iris framework. We mechanised the theory of Actris, together with tactics for symbolic execution of programs, as well as all examples in the paper, in the Coq proof assistant.
@article{paperbot543,
title = {Actris: session-type based reasoning in separation logic},
author = {Jonas Kastberg Hinrichsen and Jesper Bengtson and Robbert Krebbers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371074}
}