In a reversible language, any forward computation can be undone by a finite sequence of backward steps. Reversible computing has been studied in the context of different programming languages and formalisms, where it has been used for testing and verification, among others. In this paper, we consider a subset of Erlang, a functional and concurrent programming language based on the actor model. We present a formal semantics for reversible computation in this language and prove its main properties, including its causal consistency. We also build on top of it a rollback operator that can be used to undo the actions of a process up to a given checkpoint.
Regarding reversibility, the approach presented in this paper is in the line of work on causal-consistent reversibility @cite_9 @cite_3 (see @cite_14 for a survey). In particular, our work is closer to @cite_9 , since we also consider adding a (a history in our terminology) in order to make a computation reversible. Moreover, our proof of causal consistency mostly follows the proof scheme in @cite_9 . In contrast, we consider a different concurrent language with asynchronous communication, while communication in @cite_9 is synchronous. On the other hand, @cite_3 does not introduce a memory but keeps the old actions marked with a key''. As pointed out in @cite_3 , process equivalence is easier to check than in @cite_9 (where one would need to abstract away from the memories). Like @cite_9 , also @cite_3 considers synchronous communication. Formalising the Erlang semantics using a labelled transition relation as in @cite_9 @cite_3 (rather than a reduction semantics, as we do in this paper), and then defining a reversible extension would be an interesting and challenging approach for further research.
@cite_9 @cite_14 @cite_3
1497640022 40444246 2059141487
One obtains in this paper a process algebra RCCS, in the style of CCS, where processes can backtrack. Backtrack, just as plain forward computation, is seen as a synchronization and incurs no additional cost on the communication structure. It is shown that, given a past, a computation step can be taken back if and only if it leads to a causally equivalent past. Reversible debugging provides developers with a way to execute their applications both forward and backward, seeking the cause of an unexpected or undesired event. In a concurrent setting, reversing actions in the exact reverse order in which they have been executed may lead to undo many actions that were not related to the bug under analysis. On the other hand, undoing actions in some order that violates causal dependencies may lead to states that could not be reached in a forward execution. We propose an approach based on causal-consistent reversibility: each action can be reversed if all its consequences have already been reversed. The main feature of the approach is that it allows the programmer to easily individuate and undo exactly the actions that caused a given misbehavior till the corresponding bug is reached. This paper major contribution is the individuation of the appropriate primitives for causal-consistent reversible debugging and their prototype implementation in the CaReDeb tool. We also show how to apply CaReDeb to individuate common real-world concurrent bugs. Abstract Reversible computation has a growing number of promising application areas such as the modelling of biochemical systems, program debugging and testing, and even programming languages for quantum computing. We formulate a procedure for converting operators of standard algebraic process calculi such as CCS into reversible operators, while preserving their operational semantics. We define forward–reverse bisimulation and show that it is preserved by all reversible operators.