一句话：基于并发行为提出统一的消息传递通信模型层级，并证明其均可用一元二阶逻辑公理化。
消息传递通信模型多种多样，既包括同步 rendez-vous，也包括完全异步/乱序通信。大规模分布式系统常由传输层决定通信模型，并以 FIFO、因果序等逻辑公理刻画；本地消息传递应用则常由消息缓冲区实现及 FIFO 队列使用方式的操作语义定义。本文连接这两种方法，以并发行为为出发点，提出一个涵盖大规模与本地尺度模型的统一通信模型层级。作者进一步证明，所考虑的所有通信模型都可用一元二阶逻辑（MSO）公理化，因此可受益于基于有界特殊树宽的多种有界验证技术。
There is a wide variety of message-passing communication models, ranging from synchronous "rendez-vous" communications to fully asynchronous/out-of-order communications. For large-scale distributed systems, the communication model is determined by the transport layer of the network, and a few classes of orders of message delivery (FIFO, causally ordered) have been identified in the early days of distributed computing. For local-scale message-passing applications, e.g., running on a single machine, the communication model may be determined by the actual implementation of message buffers and by how FIFO queues are used. While large-scale communication models, such as causal ordering, are defined by logical axioms, local-scale models are often defined by an operational semantics. In this work, we connect these two approaches, and we present a unified hierarchy of communication models encompassing both large-scale and local-scale models, based on their concurrent behaviors. We also show that all the communication models we consider can be axiomatized in the monadic second order logic, and may therefore benefit from several bounded verification techniques based on bounded special treewidth.
@article{paperbot2079,
title = {A Partial Order View of Message-Passing Communication Models},
author = {Cinzia Di Giusto and Davide Ferré and Laetitia Laversa and Etienne Lozes},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571248}
}