具有选择接收的消息传递并发程序设计中竞争变量的计算
Computing Race Variants in Message-Passing Concurrent Programming with Selective Receives
摘要：
消息传递并发性是一种流行的计算模型，它是几种程序设计语言的基础，Erlang、Akka，以及（在某种程度上）Go和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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
