Reversible CSP Computations
Reversible CSP Computations
复制标题
可逆 CSP 计算
DOI：
10.1109/tpds.2021.3051747
复制
发表时间：
2021
影响因子：
5.3
通讯作者：
Tamarit Salvador
中科院分区：
文献类型：
--
作者：
Galindo Carlos;Nishida Naoki;Silva Josep;Tamarit Salvador
可逆性使程序能够向前和向后执行。这种能力允许程序员将执行回溯到以前的状态。如果计算不是确定性的，这是必不可少的，因为重新向前运行程序可能不会导致感兴趣的状态。顺序程序的可逆性已经得到了很好的研究，并有很强的理论基础。首先，并发程序的可逆性研究还很不成熟，特别是在实用方面。例如，在通信顺序进程（CSP）语言的特定情况下，可逆性实际上是缺失的。在这篇文章中，我们提出了一种新的技术，包括其形式化的定义和实现，逆向CSP计算。本文提出的大部分思想可以直接应用于其他并发规范语言，如Promela或CCS，但我们的讨论和实现集中在CSP上。该技术提出了不同形式的可逆性，包括严格可逆性和因果一致可逆性。在实践方面，我们提供了一个实现的系统，以扭转CSP计算，能够突出的源代码，正在执行的每个向前/向后计算步骤，并已被优化为可扩展到真实的系统。
Reversibility enables a program to be executed both forwards and backwards. This ability allows programmers to backtrack the execution to a previous state. This is essential if the computation is not deterministic because re-running the program forwards may not lead to that state of interest. Reversibility of sequential programs has been well studied and a strong theoretical basis exists. Contrarily, reversibility of concurrent programs is still very young, especially in the practical side. For instance, in the particular case of the Communicating Sequential Processes (CSP) language, reversibility is practically missing. In this article, we present a new technique, including its formal definition and its implementation, to reverse CSP computations. Most of the ideas presented can be directly applied to other concurrent specification languages such as Promela or CCS, but we center the discussion and the implementation on CSP. The technique proposes different forms of reversibility, including strict reversibility and causal-consistent reversibility. On the practical side, we provide an implementation of a system to reverse CSP computations that is able to highlight the source code that is being executed in each forwards/backwards computation step, and that has been optimized to be scalable to real systems.