基于异步通道编程的细粒度因果可逆性
Fine-grained Causal Reversibility for Asynchronous Channel-based Programming
- Graduate School of Informatics, Nagoya University（名古屋大学情报学研究科）
- Department of Computer Science, University of Oxford（牛津大学计算机科学系）
- University of Bari Aldo Moro（巴里阿尔多·莫罗大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文提出revGo，针对Go语言的无界异步通道，通过重排序队列中无因果关系的独立消息，实现最小性的回滚与重放，用于调试并发系统的并发错误。
AI中文摘要：
因果可逆性已成为调试并发系统的有效技术，特别是，对具有因果一致性的并发程序进行回滚和重放被发现对调试并发错误非常有帮助。在基于通道的通信中，队列排序会创建依赖关系，阻止因果独立的操作被回滚和重放。为了在不受队列依赖关系限制的情况下实现高效的回滚和重放，有必要分析队列中消息之间的因果依赖关系并对独立消息进行重排序。本文提出了revGo，它是假设无界异步通道的Go编程语言的核心。我们的回滚和重放语义允许在正向执行中消息在队列中不存在因果关系时对其进行重排序。结果表明，重排序独立消息不会产生进程不可达的配置。通过重排序独立消息，回滚和重放可通过为通信分配唯一键来以最小性实现。
英文摘要：
Causal reversibility has emerged as an effective technique for debugging concurrent systems. In particular, rolling back and replaying a concurrent program with causal consistency has been found very helpful in debugging concurrency bugs. In channel-based communication, queue ordering creates dependencies that prevent causally independent actions from being rolled back and replayed. To enable efficient rollback and replay without being constrained by queue dependencies, it is necessary to analyse causal dependencies between messages in queues and reorder independent messages. This paper presents revGo, a core of the Go programming language assuming unbounded asynchronous channels. Our rollback-and-replay semantics allows us to reorder messages in the queue if they are not causally related in the forward execution. It is shown that reordering independent messages generates no configuration with non-reachable processes. By reordering independent messages, rollback and replay are implementable with minimality by assigning unique keys to communications.
