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 non-sequential behaviors. We also show that all the communication models we consider can be axiomatised in the monadic second order logic, and may therefore benefit from several bounded verification techniques based on bounded special treewidth. CCS Concepts: $\bullet$ Theory of computation $\rightarrow$ Verification by model checking; Modal and temporal logics; Distributed computing models.
翻译:信息传递通信模式种类繁多, 从同步的“ endez- vous ” 通信到完全的不同步/ 异常的通信。 对于大规模分布式通信系统,通信模式由网络的运输层决定,并且在分布式计算初期就确定了几类信息发送命令( FIFO, 因果订购) 。对于本地规模的信息传递应用程序,例如运行在一台机器上,通信模式可能由信息缓冲的实际实施和FIFO队列的使用来确定。对于大规模通信模式,如因果排序,则由逻辑的轴轴线界定,而本地规模模式则往往由操作的语义界定。在这项工作中,我们将这两种方法连接起来,我们根据它们非相继行为,提出一个统一的通信模式等级,包括大型和地方规模模式。 我们还表明,我们所考虑的所有通信模式都可以在模式二阶值第二阶线中被固定化,例如因果排序,而导致的因果排序等大型通信模式,而导致的本地规模模式的逻辑。 因此,通过若干条框框化的核查技术, 将获得若干个固定的计算。