使用选择性接收在消息传递并发编程中计算种族变体。
摘要：消息传递并发是一种流行的计算模型，它是一些编程语言（如Erlang、Akka和在某种程度上的Go和Rust）的基础。我们特别考虑具有动态进程生成和选择性接收的消息传递并发语言，即只有当消息与特定约束条件匹配时，目标进程才能消费这些消息（例如Erlang的情况）。在这项工作中，我们引入了一种轨迹的概念，可以看作是一类因果等价执行的抽象（即产生相同结果的执行）。然后，我们展示了执行轨迹可以用来识别消息竞争。我们提供了构造性定义来计算消息竞争以及产生所谓的竞争变体，这些变体可以用来驱动与之前的执行在因果关系上不等价的新执行。这是程序验证中状态空间探测技术的一个重要组成部分。
作者：Germ''an Vidal
论文ID：2210.03026
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-10-07