论文标题
与选择性接收的消息传递并发编程中的计算竞赛变体
Computing Race Variants in Message-Passing Concurrent Programming with Selective Receives
论文作者
论文摘要
消息通讯并发是一种流行的计算模型，它是几种编程语言基础的基础，例如Erlang，Akka和（在某种程度上）Go and Rust（在某种程度上）。特别是，我们考虑一种带有动态过程产卵和选择性接收的并发语言，即，在目标过程匹配特定约束时只能被消息消耗的消息（例如，Erlang的情况）。在这项工作中，我们引入了一个痕迹概念，可以看作是一类因果关系执行的抽象（即产生相同结果）。然后，我们证明可以使用执行轨迹来识别消息赛车。我们提供了建设性的定义来计算消息种族以及产生所谓的种族变体，然后可以用来驱动新的执行，而新执行与以前的执行不等同。这是用于程序验证的状态空间探索技术的重要组成部分。
Message-passing concurrency is a popular computation model that underlies several programming languages like, e.g., Erlang, Akka, and (to some extent) Go and Rust. In particular, we consider a message-passing concurrent language with dynamic process spawning and selective receives, i.e., where messages can only be consumed by the target process when they match a specific constraint (e.g., the case of Erlang). In this work, we introduce a notion of trace that can be seen as an abstraction of a class of causally equivalent executions (i.e., which produce the same outcome). We then show that execution traces can be used to identify message races. We provide constructive definitions to compute message races as well as to produce so-called race variants, which can then be used to drive new executions which are not causally equivalent to the previous ones. This is an essential ingredient of state-space exploration techniques for program verification.
