Reversible CSP Computations
| Autor: | Josep Silva, Carlos Galindo, Naoki Nishida, Salvador Tamarit |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Source code
Semantics (computer science) Computer science media_common.quotation_subject 02 engineering and technology Code inspections and walkthroughs computer.software_genre Concurrent programming Tracing Debugging aids CIENCIAS DE LA COMPUTACION E INTELIGENCIA ARTIFICIAL 0202 electrical engineering electronic engineering information engineering Concurrent computing media_common computer.programming_language 020203 distributed computing Programming language Communicating sequential processes Data structure Computational Theory and Mathematics Debugging Promela Hardware and Architecture Signal Processing State (computer science) LENGUAJES Y SISTEMAS INFORMATICOS computer |
| Zdroj: | IEEE Transactions on Parallel and Distributed Systems RiuNet. Repositorio Institucional de la Universitat Politécnica de Valéncia instname |
| ISSN: | 2161-9883 1045-9219 |
| Popis: | [EN] 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. A preliminary version of this work was presented at the 12th Conference on Reversible Computation [31]. The authors would like to thank the anonymous reviewers for their useful comments and constructive feedback that helped them to improve this work. This work was supported in part by the EU (FEDER) and the Spanish MCI/AEI under Grant TIN2016-76843-C4-1-R and Grant PID2019-104735RB-C41, in part by the Generalitat Valenciana under Grant Prometeo/2019/098 (DeepTrust), in part by JSPS KAKENHI under Grant JP17H01722, and in part by TAILOR, a project funded by EU Horizon 2020 research and innovation programme under GA 952215. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|