Ivan Lanese
email: lanese@cs.unibo.it

Michael Lienhardt
email: lienhard@cs.unibo.it

Mario Bravetti
email: bravetti@cs.unibo.it

Einar Broch Johnsen
email: einarj@ifi.uio.no

Rudolf Schlatte

Volker Stolz
email: stolz@ifi.uio.no

Gianluigi Zavattaro
email: zavattar@cs.unibo.it

Fault Model Design Space for Cooperative Concurrency ⋆

This paper critically discusses the different choices that have to be made when defining a fault model for an object-oriented programming language. We consider in particular the ABS language, and analyze the interplay between the fault model and the main features of ABS, namely the cooperative concurrency model, based on asynchronous method invocations whose return results via futures, and its emphasis on static analysis based on invariants.

Introduction

General-purpose modeling languages exploit abstraction to reduce complexity [START_REF] Kramer | Is abstraction the key to computing?[END_REF]: modeling is the act of describing a system succinctly by leaving out some aspects of its behavior or structure. Software models primarily focus on the functional behavior and the logical composition of the software. Modeling formalisms can have varying levels of detail and can express structural properties (for example UML diagrams), interactions (π-calculus), or the effects of functions or methods (pre-and post-conditions), etc.

Concurrent and distributed systems demand flexible communication forms between distributed processes. While object-orientation is a natural paradigm for distributed systems [START_REF]Open Distributed Processing -Reference Model parts 1-4[END_REF], the tight coupling between objects traditionally enforced by method calls may be criticized. Concurrent (or active) objects have been proposed as an approach to concurrency that blends naturally with objectoriented programming [START_REF] Agha | Actors: A conceptual foundation for concurrent objectoriented programming[END_REF][START_REF] Lavender | Active object: an object behavioral pattern for concurrent programming[END_REF][START_REF] Yonezawa | ABCL: An Object-Oriented Concurrent System[END_REF]. Several slightly differently flavored concurrent object systems exist for, e.g., Java [START_REF] Baduel | Grid Computing: Software Environments and Tools, chapter Programming, Composing, Deploying, for the Grid[END_REF][START_REF] Schäfer | JCoBox: Generalizing active objects to concurrent components[END_REF], Eiffel [START_REF] Caromel | Service, Asynchrony, and Wait-By-Necessity[END_REF][START_REF] Nienaltowski | Practical framework for contract-based concurrent object-oriented programming[END_REF], and C++ [START_REF] Morris | CActive and Friends. Symbian Developer Network[END_REF]. Concurrent objects are reminiscent of Actors [START_REF] Agha | Actors: A conceptual foundation for concurrent objectoriented programming[END_REF] and Erlang processes [START_REF] Armstrong | Programming Erlang: Software for a Concurrent World[END_REF]: objects are inherently concurrent, conceptually each object has a dedicated processor, and there is at most one activity in an object at any time. Thus, concurrent objects encapsulate not only their state and methods, but also a single (active) thread of control. In the concurrent object model, asynchronous method calls may be used to better combine object-orientation with distributed programming by reducing the temporal coupling between the caller and callee of a method, compared to the tightly synchronized (remote) method invocation model (of, e.g., Java RMI [START_REF] Pitt | Java.Rmi: The Remote Method Invocation Guide[END_REF]). Intuitively, asynchronous method calls spawn activities in objects without blocking execution in the caller. Return values from asynchronous calls are managed by futures [START_REF] Halstead | Multilisp: A language for concurrent symbolic computation[END_REF][START_REF] Liskov | Promises: Linguistic support for efficient asynchronous procedure calls in distributed systems[END_REF][START_REF] Yonezawa | ABCL: An Object-Oriented Concurrent System[END_REF]. Asynchronous method calls and futures have been integrated with, e.g., Java [START_REF] Goetz | Java Concurrency in Practice[END_REF][START_REF]Concurrency utilities[END_REF] and Scala [START_REF] Haller | Scala actors: Unifying thread-based and event-based programming[END_REF] and offer a large degree of potential concurrency for deployment on multi-core or distributed architectures.

ABS is a modeling language targeting distributed systems [START_REF] Johnsen | ABS: A core language for abstract behavioral specification[END_REF]; the language combines concurrent objects and asynchronous method calls with cooperative scheduling of method invocations. In ABS the basic unit of computation is the concurrent object group (cog): a cog provides to a group of objects a shared processor. Method invocations on an object of a cog instantiate a new task that requires the cog's processor in order to execute. Cooperative scheduling allows tasks to suspend in a controlled way at explicit points in the code, so that other tasks of the object can execute. The suspend and await commands are used to explicitly release the processor: the difference between the two commands is that await has an associated boolean guard expressing under which condition the task should be re-activated by the scheduler. Asynchronous method invocations are used among objects belonging to different cogs; at each asynchronous method invocation a future is instantiated to store the return value. Futures are first class citizens in ABS and are accessed via a get command; get is blocking because a task, executing get on a future of a method invocation which has not yet completed, blocks and keeps the processor until the future is written. To avoid keeping the processor, one can use an await f? to ensure that future f contains a value.

ABS has a formal, executable semantics; ABS models can be run on a variety of backends and can be verified using the KeY proof checker [START_REF] Beckert | Verification of Object-oriented Software: The KeY Approach[END_REF]. In particular, asynchronous method calls and cooperative scheduling allow the verification of distributed and concurrent programs by means of sequential reasoning [START_REF] De Boer | A complete guide to the future[END_REF]. In ABS this is reflected in a proof system for local reasoning about objects where the class invariant must hold at all scheduling points [START_REF] Din | Observable behavior of distributed systems: Component reasoning for concurrent objects[END_REF]. Although ABS targets distributed systems, a notable abstraction of the language design is that faults are currently not considered part of the behavior to be modeled. On the other hand, dealing with faults is an essential and notoriously difficult part of developing a distributed system; this difficulty is exacerbated by the lack of clear structuring concepts [START_REF] Cristian | Understanding fault-tolerant distributed systems[END_REF]. A well-designed model is essential to understand potential faults and reason about robustness, especially in distributed settings. Thus, it is interesting to extend a modeling language such as ABS in order to model faults and how these can be resolved during the system design.

It is common in the literature to distinguish errors due to the software design (sometimes called faults) from random errors due to hardware (sometimes called failures). For software deployed on a single machine, such hardware failures entail a crash of the program. A characteristic of distributed systems is that failures may be partial [START_REF] Waldo | A note on distributed computing[END_REF]; i.e., the failure may cause a node to crash or a link to be broken while the rest of the system continues to operate. In our setting, a strict separation between faults and failures may seem contrived, and we will refer to unintended behavior caused by both the software and hardware as faults. A fault is masked if the fault is not detected by the client of the service in which the fault occurs. In hierarchical fault models, faults can propagate along the path of service requests; i.e., a fault at the server level can result in a (possibly different) fault at the client level. In a synchronous communication model, a client object can only send one method call at the time whereas in an asynchronous communication model, the client may spawn several calls. Thus, it need not be clear for a client object which of the spawned calls resulted in a specific fault in the asynchronous case. However, asynchronous method calls in ABS allow results to be shared before they are returned: futures are firstclass citizens of ABS and may be passed around. First-class futures give rise to very flexible patterns of synchronization, but they further obfuscate the path of service requests and thus of fault propagation.

This paper discusses an extension of the semantics of the ABS modeling language to incorporate a robust fault model that is both amenable to formal analysis and familiar to the working programmer. The paper considers how faults can be introduced into ABS in a way which is faithful to its syntax, semantics, and proof system, and discusses the appropriate introduction of faults along three dimensions: fault representation (Section 2), fault behavior (Section 3), and fault propagation (Section 4).

How Are Faults Represented?

Exceptions are the language entities corresponding to faults in an ABS program's execution. ABS includes two kinds of entities which in principle can be used to represent faults: objects and datatypes (datatypes [START_REF] Jay | Algebraic data types[END_REF] are part of the functional layer of ABS, and abstract simple, common structures like lists and sets).

Exceptions as Objects. Representing exceptions as objects allows for a very flexible management of faults. Indeed, in this setting exceptions would have both a mutable state and a behavior. Also, one could define new kinds of exceptions using the interface hierarchy. Finally, exceptions would have identities allowing to distinguish different instances of the same fault. However, most of these features are not needed for faults: faults are generated and consumed, but they are static and with no behavior. Representing them as objects would allow a programming style not matching the intuition and difficult to understand. Furthermore, in ABS static verification is a main concern, and semantic clarity is more needed than in other languages. For this reason we think that in the setting of ABS exceptions should not be objects.

Exceptions as Datatypes. Datatypes fit more with the intuition of exceptions as described before: they are simple values with no identity nor behavior. However, in ABS datatypes are closed, meaning that once a datatype has been declared, it is not possible to extend it with new constructors. This is a potential problem in using them to represent exceptions. Indeed, we would like the datatype for exceptions to include system-defined exceptions such as Division by Zero or Array out of Bound, and to be extended to accommodate user-defined exceptions. Also, for modularity reasons, programmers of an ABS module should be able to declare their own exceptions, thus exception declaration cannot be centralized. User-defined exceptions are not only handy for the programmer, but may also help the definition of invariants by tracking the occurrence of specific conditions. We discuss below a few possible design choices related to the definition of user-defined exceptions.

Allow open datatypes in ABS. In this setting exception would be an open datatype [START_REF] Löh | Open data types and open functions[END_REF], and other ABS datatypes could be open as well. The declaration of system-defined exceptions can be done as: However, this is a major modification of datatypes, a key component of ABS, and introducing this additional complexity only to accommodate exceptions may not be a good choice. In fact, handling open datatypes is in contrast with the fact that ABS type system is nominal. One would need to resort to a structural type system (similar to, e.g., OCaml's variants [START_REF] Rémy | Type checking records and variants in a natural extension of ml[END_REF]) to ensure that a pattern matching is complete, which is far less natural.

Allow any datatype to be an exception. In this setting any value of any datatype may be used as an exception (the fact of declaring which datatypes are actually used as exceptions does not change too much the setting). User-defined datatypes can be added by simply defining new datatypes. When the programmer wants to catch an exception, he has to specify which types of exceptions he can catch, and do a pattern matching both on the type and on its constructor to understand which particular fault happened. This produces a syntax like:

Exceptions as a new kind of value. In this setting exceptions are a separate kind of value, at the same level of objects and datatypes. The type Exception is open. New exceptions (both system-and user-defined) can be declared as follows:

exception NullPointerException exception RemoteAccessException ... exception MyUserDefinedException(Int, String)

Pattern matching can be used to distinguish different exceptions:

try { ... } catch(e) { NullPointerException => ... MyUserDefinedException(n,s) => ... e2 => ... ... }
Structural typing can be used if one wants to check that all exceptions possibly raised are caught, as, e.g., in Java.

Discussion. The simplest approach is to model exceptions as a closed datatype.

However, if open exceptions are desired to increase the expressive power, the last solution is the one with minimal impact on the existing ABS language. Allowing any datatype as an exception also seems a viable option, but with a more substantial impact on the existing structure of ABS.

Which is the Behavior of Faults?

Faults interrupt the normal control flow of the program. A first issue concerning faults is how they are generated. Concerning fault management, it is a common agreement that faults are manipulated with a try/catch structure, and we do not see any reason to change this approach in our design for ABS. However, after this choice has been taken, the design space is still vast and many questions still need to be investigated.

Fault Generation. In programming languages, faults can be generated either by an explicit command such as throw f where f is the raised fault, or by a normal command. For instance, when evaluating the expression x/y a Division by Zero exception may be raised if y is 0. In this second case, which exception is raised is not explicit, but defined by the semantics of the command. After having been raised, the two kinds of exceptions are indistinguishable. A third kind of exception may be considered in ABS. Indeed, ABS is currently evolving towards having an explicit distribution, and in this setting localities or links may break. The only remote interaction in ABS is via asynchronous method invocation, and the corresponding await/get on the created future. In principle, network problems could be notified either during invocation, or during the await/get. However, invocation is asynchronous, and will not check for instance whether the callee will receive and/or process the invocation message. For the same reason, it is not reasonable that it checks for network problems. Clearly, the get should raise the fault, since no return value is available.

The behavior of await depends on its intended semantics. If executing the statement await f? means that the process whose result will be stored in f has successfully finished, then the await needs to synchronize with the remote computation and should raise a pre-defined fault upon timeout and network errors. In this setting thus network faults are raised by both await and get. On the other hand, if executing await f? gives only the guarantee that a subsequent f.get will not block, then all faults, including network-and timeout-related faults, can be raised by get exclusively.

Fault Management. As discussed in the beginning of the section, we use the common try/catch structure to manage faults. This structure sometimes also features an additional block finally. The finally block specifies some code that must be executed both if no exception is raised and if it is. A common use of the finally block is to release resources which need to be freed whatever the result of the computation is. For instance, P may close a file used inside the try block. The finally block is very convenient for programming, but may not be needed in the core language. Indeed, in many cases it can be encoded. The encoding instantiated on the example above is as follows: Essentially, one has to catch all the exceptions, do P and rethrow the same exception. P also needs to be replicated at the end, so to be executed if no exception is raised. Note that this encoding relies on always having exactly one return statement per method, at its end (this is the recommended style of programming in ABS), and on the ability to catch all exceptions and to be able to rethrow them identically. Actually, in principle, one can also consider some uncatchable faults, but this seems not particularly relevant in practice.

For resource management, an alternative to the finally block is the autorelease mechanism of Java 7 [START_REF] Ponge | Better resource management with Java SE 7: Beyond syntactic sugar[END_REF], which automatically releases its resource at the end of the block. Encoding such a mechanism in ABS could be done using an approach similar to the one above for the finally block.

Fault Effects. We have discussed how to catch faults. However, it may happen that a fault is not caught inside the method raising it. Then, as already said, the fault should interrupt the normal flow of computation, i.e. killing the running process. However, one may decide to kill a larger entity. Suitable candidates in ABS are the object where the fault has been raised, or its cog. Now, remember that in ABS there is a strong emphasis on correctness proofs based on invariants, and that whenever a process releases the lock of an object the class invariant must hold. An uncaught fault releases the lock by killing the running process. This means that whenever an uncaught fault may be raised, the invariant must hold. Since faults may be raised by many constructs, including expressions and get, ensuring this may be particularly difficult, and may require in practice to manage all the faults inside the method raising them. However, this is undesirable since a method may not have enough information to correctly manage a given fault. One can try to define a weaker invariant, but this may be difficult. A solution is to decide that a fault may not only kill the process, but also the object whose invariant may be no more valid. An even more drastic solution is to kill the whole cog. This may be meaningful if invariants involving different objects (of the same cog) are considered. However, this kind of invariant is currently not considered in ABS, thus the introduction of mechanisms for killing a whole cog seems premature.

Effect Declaration. In classic programming languages, the only effect of an uncaught fault is to kill the running process. However, we just discussed that also killing the whole object (or cog) is a possible effect. One may want to have different effects for different faults. More in general, different faults may have different properties. Another possible property may describe whether a fault can be caught or not. Whatever the set of possible properties is, an important issue is where those properties are associated with the raised fault. One can have a keyword deadly specifying that a given exception will kill the whole object if uncaught, while the behavior of just killing the process can be considered the default behavior. We can see three possibilities here. Properties may be specified: when an exception is declared: for instance, one may write deadly exception NullPointerException A main drawback of this approach is that the same exception will behave the same everywhere. Intuitively, an exception may be deadly for an object where the invariant cannot be restored, and not for another one where the fault has no impact on the invariant. Note also that if any datatype can be an exception, then one has to specify properties for each datatype, e.g. deadly Int. Actually, this second drawback is mitigated by choosing suitable default values for properties. when an exception is raised: for instance, one may write throw deadly NullPointerException or also shorten it into die NullPointerException. Clearly, this approach is only reasonable for exceptions raised by an explicit throw (unless one wants to write something like x=y/0 deadly). The approach is also less compositional, thus less suitable for static analysis. In fact, to understand the behavior of an exception it is not enough to look at declarations. For instance, the same exception may be either deadly or not for the same method, depending on how it has been raised. Note also that this approach would break the encoding of finally above, since there is no way to rethrow an exception with the exact same properties. in the signature of the method raising the exception: for instance, one may write

Int calc(Int x) deadly: NullPointerException {...}
Clearly, this approach is viable only for properties relevant when the exception exits the method, such as deadly. It would not work for instance to specify whether an exception can be caught or not. Notice that this approach integrates well with the declaration of which faults a method may raise, useful to statically verify that all exceptions are caught. In fact, one could write

Int calc(Int x) throws: DivisionByZero, deadly NullPointerException {...} More in general, this approach is suitable for static analysis, since a method declaration also provides the information on the behavior of exceptions raised by the method itself. The same information is useful also for the programmer, in particular when using methods he did not write himself.

Discussion. We think that in the context of ABS, a fault may have two different effects: either killing the process or the whole object, depending on whether the object invariant holds or not. Whether a fault should kill the whole object or not should be declared at the level of method signature to enhance compositionality. Note that in the most used object-oriented languages, objects are never killed as a result of an exception: indeed such a feature is relevant in ABS because of its emphasis on analysis based on invariants, and no widespread object-oriented language has been developed according to this philosophy. A possible alternative to kill the object would be to roll back state changes. A transparent rollback [START_REF] Elnozahy | A survey of rollback-recovery protocols in message-passing systems[END_REF] in our setting could lead to the last release point, where one is sure the invariant holds. However such an approach, discussed in [START_REF] Göri | Erlang-style error recovery for concurrent objects with cooperative scheduling[END_REF], is not always satisfying. Indeed, rolling back only locally may easily lead to inconsistencies between different local states (what corresponds to break invariants concerning multiple objects). On the other hand, global rollback as in [START_REF] Lanese | Controlling reversibility in higher-order pi[END_REF] results in an overly complex semantics. Furthermore, if local rollback is needed in particular cases, it can usually be encoded. Similarly, the finally construct is not strictly needed, since with the choices we advocate it can be encoded.

How Do Faults Propagate?

We have discussed in the previous section the effect of a fault on the process or object where it is raised. However, in case of fault, in particular of uncaught fault, it is reasonable to propagate the exception also to other processes/objects related to it. In particular, possible targets for propagation are processes interested in the result of the computation, processes that have been invoked by the failed one, processes in the same object/cog of the failed one, processes trying to access an object after it died.

Propagation through the Return Future. In a language with synchronous method invocation the only process that can directly access the result of the computation is the caller. However, in languages with asynchronous method invocation any process receiving the future can directly access the result of the computation. The caller may be or may not be one of them, and indeed may even terminate before the result of the computation becomes ready. Thus we discuss here notification of faults to the processes synchronizing with the future. We have two possibilities: processes may synchronize with the future either with a get or with an await statement. The case of get is clear: those processes are interested in the result of the computation, in case of fault no correct result is available and those processes need to be notified so that they can decide how to proceed. The natural way of being notified is that the same exception is raised by get. A process doing an await is just interested in waiting for the computation to terminate, but not in knowing its result. Thus we claim that if the computation terminated, either with a normal value or with an exception, the await should not block and the exception, if any, should not be raised. The exception would be raised only if later on a get on the future is performed. This approach requires to put the fault notification inside the future, and has been explored in the context of ABS in [START_REF] Johnsen | Fault in the future[END_REF]. Indeed, this is also the approach of Java future library (asynchronous computation with futures has been standardized in a Java library since Java SE 5 [START_REF] Goetz | Java Concurrency in Practice[END_REF]). In contrast to ABS, Java's API does not distinguish between waiting for a future to become available, and retrieving the results. In fact, no primitive like await is available in Java. In addition, Java's futures do not faithfully propagate exceptions: the get method on a faulty future always raises the same exception ExecutionException.

An additional problem is related to concurrency. Indeed, in ABS, one may have multiple concurrent get and/or await statements on the same future containing an exception. Let us consider the case of multiple get statements. In this case, one has to decide whether they all raise the fault contained in the future or just one of them does. This second solution is more troublesome since to this end, the first process accessing the future would receive the exception and remove the fault from the future. The only possibility is to replace it with some default value, and this requires locking the future. However, this in turn changes the behavior of futures in a relevant way: Futures are understood as logical variables that change at most once, and this would no longer be true. Additionally, this creates a weak synchronization point between two processes accessing the same future. Indeed, if a process knows that a future originally contains an exception, by accessing it he will know if another process accessed it before. These weak synchronization points between processes that would be independent otherwise make the concurrency model and thus the analysis more difficult. Note that concurrent await statements are not a problem, since they do not locally raise the fault, but just check whether the future is empty or not.

Propagation through Method Invocations. It may be the case that the failed computation has invoked methods in other objects, whose execution is no more necessary after the failure. Indeed, it may even be undesired. For instance, if you are planning a trip and the booking of the airplane fails, you do not want to complete the booking of the hotel. Thus a mechanism to cancel a computation originated by a past method call may be useful. Actually, cancel may have different meanings according to the state of the invocation. If the invocation has not started yet, one can simply remove the invocation message itself. If the invoked process is running, one may raise the exception. If the execution already completed, one may do nothing or execute some code to compensate the terminated execution. This second option has been explored in [START_REF] Johnsen | Fault in the future[END_REF]. The most interesting case is the one where the invoked process is running. Indeed, in this case the fault may be raised in any point of the execution, thus dealing with it using a try-catch would require to have the whole method code, including the return command, inside the try block. A better approach is to define specific points in the code where the running process checks for exceptions from its invoker, and specifying there the code to be executed in this case. A more modular way is to separate the two issues. One may have a statement check to specify when to check for faults, and a statement setHandler H establishing that H is the handler to be used to deal with faults from the invoker from now on. H can be a simple piece of code, or a function associating pieces of code to exceptions. Pieces of code may have a return statement, to communicate the result of the fault management to the invoker. If the execution of the handler terminates successfully, the execution of the method code restarts. One may also decide that the last handler has to be used to compensate the execution if the cancellation occurs after the termination of the invoked process.

We have described the effect of propagation to invoked processes. However, one has to understand which invoked processes to consider. The simplest possibility is to let the programmer decide. We call this approach programmed propagation. This can be done through a statement f1 = f.cancel(e) where f is the future corresponding to the invocation to be canceled, e the exception to be raised and f1 the future storing the result of exception management. Note that the future f is the right entity to individuate the invocation, since each invocation corresponds to a different future. Note also that with programmed cancel one may cancel twice the same invocation, and that cancel can be executed by any process on any future he knows of. Future f1 may contain different values according to the outcome of the cancel. If the exception sent by the cancel is correctly managed, the handler returns a specific value to fill that future (potentially different from the value returned as a result of the method, which is in future f). In all the other cases a system-defined exception is put inside future f1 (one cannot put there a normal value, since this should depend on the type of the future):

an exception notStarted if the cancel arrives before the invocation started (while the future f contains an exception canceled); -an exception terminated if the cancel arrives after method termination, and compensations are not used (future f keeps its value); -an exception noCompensation if the cancel arrives after method termination, compensations are allowed, but no compensation is specified for the target method (future f keeps its value); -an exception CancelNotManaged if the exception arrives when the method is running, but it is not managed since there is no handler for it (while the future f stores the exception e).

In case of multiple cancellations, cancellations behave as above according to the state of the method when they are processed. Note also that the future f is not changed if it already contains the result of the method invocation. An alternative approach is to have an automatic propagation of exceptions to invoked processes. First, one should decide whether to propagate only uncaught faults, or also managed faults. This last solution is not desirable in general, since most managed faults should not affect other processes, and can be dealt with by programmed propagation in case of need. Propagation of uncaught faults, if desired, should be necessarily done automatically. Now, the problem is to understand to which method invocations the fault needs to propagate. An upper bound is given by the futures known by the dying process. One may also consider that futures on which a get has already been performed are no more relevant. However, there is no fast and easy answer to this question. We think that a reasonable solution is to choose the futures which have been created by the current method execution and on which no get has been performed yet by the same method. One may also want to check whether the reference to the future has been passed to another method, and whether this method has performed a get on the future, but this would make the implementation and the analysis much more tricky. Similarly, one may want to consider also futures received as parameters, but again this needs to propagate the information on whether a future has been accessed or not from one method to the other. Note that in case of automatic propagation, no information on the result of the cancellation is needed, since the caller already terminated.

One may want to ensure that children can manage all the faults from their parent. To this end, each child should declare the exceptions that he can manage (at any point, since it may be the case that some exceptions can be managed only at some check due to handler modifications). Then, one can check that these include all the exceptions the parent may send to him. For automatic propagation, these coincide with the exceptions the parent may raise. For programmed propagation, these are the arguments of the various cancel of the corresponding future in the parent or in methods to which the future is passed.

Propagation to Other Processes in the same Object/Cog. We already discussed the fact that it is important for processes to restore the invariant of the object or cog before releasing the lock, and in particular before terminating because of an uncaught exception. In case the invariant cannot be restored, we proposed as a solution the possibility of killing the whole object/cog. An alternative solution is to terminate only the process P that first raised the fault, and notifying the other processes about the uncaught fault, since they may be able to manage it. Note that when process P is terminated, there is no other running process in the same cog. Thus the other processes will get the fault notification when they will be scheduled again. This means that they may get a fault, either when they start, or when they resume execution at an await or suspend statement. The fault may then be managed, or propagated as discussed above. In particular, if not managed, will be propagated to the next process to be scheduled. In this setting objects never die, but method calls may receive an exception as soon as they start. If we raise the same exception that was raised by P , then it may be difficult to track which exceptions may be raised inside any method. A simpler solution is to have a dedicated exception, e.g., InvariantNotRestored. What said above for objects holds similarly for cogs, concerning cog invariants. However, as already said, they are not a main concern in ABS at the moment.

Propagation through Dead Objects/Cogs. Some of the approaches we discussed involve the killing of an object or cog. We have not yet discussed what happens when a dead object is accessed (through method invocation). An exception should be raised. We can follow either the approach discussed above for network errors, or the one for normal faults. In practice the only difference is whether also the await will raise such a fault or not. We do not see any particular advantages or disadvantages for the two approaches: which is the best solution depends on which one better fits the programmer intuition, which may be different from one programmer to the other. In both the cases, using a standard exception such as DeadObject, instead of propagating the exception that caused the death of the object, simplifies the management. Also, it allows the caller to know whether the object is dead because of its invocation or it was already dead before.

Discussion. Among the propagation strategies above, propagation through the return future is nowadays standard, since it is used, e.g., in Java and C#. The possibility of canceling a running process via a future is also available in Java and C#, but the possibility of doing it automatically and/or of defining handlers and compensations for managing cancel requests while the process is running are not considered. Indeed, these strategies are quite complex, and it is not yet clear how useful they are in real programming. Also propagation of the fault to other processes in the same object is not considered in mainstream languages as far as we know, but we think this is a viable strategy in ABS. In fact, when a process is not able to restore the object invariant, there are two possibilities: either destroying the whole object or leave to another method call the task of restoring it. This second strategy seems also less extreme.

Conclusion

We have discussed the design space for fault models to be included in the ABS modeling language. As future work, we will extend the formal semantics of ABS with appropriate datatypes for the representation of faults, primitives to raise and catch faults, and mechanisms to distribute faults to other objects and cogs.

We complete the paper with a review of related fault models (the comparison with Java has been already discussed throughout the paper).

Functional programming languages, like OCaml or Haskell, also include primitives for faults modeled as exceptions. Both languages allow user-defined exceptions, but they implement them in different manners. OCaml uses a special type (called exn) to type exceptions, and new exceptions can be declared using the syntax exception e of data. In [START_REF] Löh | Open data types and open functions[END_REF], the introduction of open datatypes in Haskell to encode exceptions is discussed. However, the current implementation of GHC uses typeclass [START_REF] Chen | Parametric type classes[END_REF], which allow one to register new datatypes as being exceptions.

Message-Passing Interface (MPI) is a cross-language standard, used, e.g., for C and Fortran, to program distributed applications. MPI expresses communication via so-called MPI functions, the basic ones being SEND and a blocking RECV. The SEND can work with three modalities: (buffered send) buffering the data to be sent, thus returning immediately as we assumed in this paper; (synchronous send) waiting for a corresponding RECV to be posted by the destination before terminating; or (ready send) failing in the case a corresponding RECV has not yet been posted by the destination. Dealing with the network, MPI functions represent communication at a lower level than we do: in MPI also the process of data delivering is taken into account. SEND (in all its modalities) and RECV have asynchronous variants, called ISEND and IRECV (where the "I" stands for "initiation"), which indicate a buffer where to fetch/put data and return immediately. For each such asynchronous send/receive, functionalities similar to some of the ones considered in this paper can be used: WAIT makes it possible to wait for the completion of data sending/receiving (in addition in MPI there is also a function TEST which returns immediately the status of the data sending/receiving without waiting); failures (e.g., in the communication while sending/receiving data) are detected by calling WAIT or TEST; and it is possible to cancel a send/receive by a call to CANCEL. The semantics of the latter, however, is the removal of the send/receive, supposing that it has not completed yet, as if it never occurred (a matching receive/send would perceive, as well, the canceled send/receive as if it never occurred). By combining the mechanisms above it is possible to obtain the waiting and canceling mechanisms considered in this paper. For example an asynchronous method invocation can be modeled by executing both ISEND and IRECV, and cancellation by executing CANCEL both on the send and the receive in the case the data is still under transmission or just on the receive in the case the send has completed. In the latter case, if the invoked method performs a ready send at the end of method execution, it will be notified of the matching IRECV having been canceled.

In web applications the HTTP protocol is used to realize service invocations by means of request/response pairs over a TCP/IP connection, as happens in the popular approaches of Java and Javascript, i.e. Asynchronous Javascript and XML (AJAX) invocations. In Java a method is used to initiate the HTTP request/response, which differently from the approach considered in this paper, may yield an error in the case the connection with the HTTP server cannot be established (timeout based). Then the client goes through a two phase process, where he first sends data over an output-stream and then, similarly, receives data. At the server side a symmetric process is followed. Java methods for reading pieces of response data are blocking as for the waiting function used in MPI and considered in this paper. Similarly, failures are notified via exceptions when reading response data (or while sending request data). Finally concerning cancellation, the HTTP request/response can be aborted as a whole by the client and this causes the server to detect the failure (an exception is raised) when it is in the phase of inserting data in the response, i.e. when returning data (or while reading request data). In Javascript (AJAX) request data are preliminarily put into memory (as in MPI) and then the request/response is initiated (again this can fail if connection cannot be established). Such an initiation function also installs a user-defined function which is expected to manage the data received once the response is completed (including also managing the case of failure). This mechanism is an alternative to the waiting function used in MPI and considered in this paper. Concerning cancellation, it is possible, as in Java, to abort the HTTP request/response (with the same effect at server side).

  open data Exception = NullPointerException | RemoteAccessException where the keyword open specifies that the datatype is open (in principle open and closed datatypes may coexist). Then one can add user-defined exceptions as: open data Exception = ... | MyUserDefinedException

  try { ... } catch(MyFirstException e) { ... } catch(MySecondeException e) {... } finally { P }

try { ... } catch(List e) { case(e) { | Empty => ... | Cons(v,e2) => ... } } catch(NullPointerException e) { ... } catch(_ e) { ... / * capture all exceptions * / }where a special syntax _ is needed to catch exceptions of any type, since there is no hierarchy for datatypes in ABS. Note that in case the exception has type List a case is done to analyze its structure. A difficulty in applying this approach to ABS is due to the fact that in ABS values do not carry their type at runtime, but adding such an information seems not to have relevant drawbacks.

⋆ Partly funded by the EU project FP7-610582 ENVISAGE


Ivan Lanese
email: ivan.lanese@gmail.com

Claudio Antares Mezzina
email: mezzina@fbk.eu

Francesco Tiezzi
email: francesco.tiezzi@imtlucca.it

Causal-Consistent Reversibility *

Reversible computing allows one to execute programs both in the standard, forward direction, and backward, going back to past states. In a concurrent scenario, the correct notion of reversibility is causal-consistent reversibility: any action can be undone, provided that all its consequences (if any) are undone beforehand. In this paper we present an overview of the main approaches, results, and applications of causal-consistent reversibility.

Introduction

Reversibility in computer science refers to the possibility of executing a program both in forward and backward directions. The former is the standard kind of execution, while the latter enables programs to go back to past states by undoing the effects of forward computations previously performed. Reversibility has been studied for different motivations. A first motivation dates back to the observation by Landauer [START_REF] Landauer | Irreversibility and heat generation in the computing process[END_REF] that only irreversible computations need to consume energy, thus reversible computations are interesting in a scenario of low-energy computing. Reversibility has also been studied for modeling systems which are naturally ' 3 e 7 f 8 g 9 g 9 h @ i A i A (b)

Figure 1: Example of causal-consistent executions reversible. This is the case of biological or chemical systems, where the direction of computation depends on environment conditions such as temperature or pressure, but also of quantum computations [START_REF] Altenkirch | A functional quantum programming language[END_REF], where most operations are naturally reversible. Another motivation comes from the desire to better explore a computation, analyzing different possibilities, as in debugging [START_REF] Feldman | Igor: A system for program debugging via reversible execution[END_REF] or in statespace exploration, e.g., in Prolog. Recently [START_REF] Danos | Transactions in RCCS[END_REF][START_REF] Lanese | Concurrent flexible reversibility[END_REF], reversibility has also been put forward as a common framework to study constructs for system reliability, such as transactions or checkpoints, with the idea that in case of error a system can automatically go backward to a more stable state. Reversibility in a sequential setting is well understood (see, e.g., [START_REF] Leeman | A formal approach to undo operations in programming languages[END_REF]). To reverse the execution of a sequential program one has simply to recursively undo the last action performed by the program. The definition of reversibility in a concurrent setting (including also distributed systems) is trickier, since there is no concept of "last action". Indeed, many actions are performed concurrently.

A suitable definition of reversibility in a concurrent scenario has been proposed by Danos and Krivine in their seminal paper [START_REF] Danos | Reversible communicating systems[END_REF]. Intuitively, the definition says that any action can be undone provided that all its consequences, if any, are undone beforehand. For instance, two threads that run without interactions can be reversed independently, while if a thread T 1 sends a message to thread T 2 , the receipt from T 2 , as well as all the consequent interactions, should be undone before the send from T 1 can be undone. This definition highlights the link between reversibility in a concurrent setting and causality, and is then called causalconsistent.

To better understand this crucial concept, consider the example in Figure 1. In Figure 1a, from state M there are two possible paths leading to state N, one executing first a and then b (on the left), and the other executing first b and then a (on the right). If the two actions a and b are concurrent, possibly executed by physically remote components, it may be difficult to distinguish the two computations. Thus one should be able to reverse any of the two executions by reversing the other, i.e. if the forward computation proceeds by executing first a and then b (double-pointed arrow in Figure 1b), not only undoing first b and then a, but also undoing first a and then b (wave arrow in Figure 1b) is a valid reverse computation.

Given this definition of reversibility, a first line of research considered how to define reversible extensions of a given concurrent language. Actually, the research done so far on this topic concentrated mainly on process calculi such as CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF]. We discuss the different approaches in Section 2.

Those works focussed on defining backward transitions and computations, and on proving some relevant properties. They however provided no insight on when backward transitions should be preferred over forward ones and vice versa. A second line of research then considered different mechanisms to control reversibility. This research line is described in Section 3.

The descriptions above concentrated on the operational semantics of reversible processes. Later on, other aspects have been explored, such as the behavioral theory, the related logics, abstract representations as event structures or categories, the relations between different reversible and irreversible calculi, the cost of reversibility in terms of space, and the complexity of analyzing reversible systems. We discuss those aspects in Section 4.

With all these tools in place, causal-consistent reversibility was mature enough to be applied to various programming problems. Most of the applications have been found in the field of biological systems, of state-space exploration, of reliability and of debugging. Those applications are discussed in Section 5.

In Section 6 we summarize the state of research on causal-consistent reversibility and describe a few open challenges.

Uncontrolled Reversibility

In order to make a concurrent language reversible, two main issues have to be considered. First, as in sequential reversibility, history information has to be kept. This avoids that transitions cause loss of information, which would forbid to go back in a sound way. Second, information on causality has to be kept. This permits knowing which actions can be immediately reversed and which cannot according to the definition of causal-consistent reversibility. The first issue is clearly understood already in any sequential imperative language 1 . For instance, the assignment x := 5 deletes the old value of x, which needs to be stored if this assignment should be reversed. Note that this is not the case for any assignment: for instance, the assignment x := x + 1 causes no loss of information and can be reverted by executing x := x -1 without the need for keeping history information. Actually, some approaches to reversibility restrict the language to actions of this second kind (called reversible updates [START_REF] Yokoyama | Principles of a reversible programming language[END_REF]), although this is not the typical approach for causal-consistent reversibility. In process calculi the situation is even worst. For example, let us consider CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF]: a transition of the form a.P + Q a -→ P, executing action a and discarding alternative Q, will lose both the information on a and on Q, thus this information needs to be saved to enable reversibility.

Before discussing how the approaches in the literature deal with history information, let us discuss the issue of causality. As already said, concurrent actions as in a | b can be reversed independently. Vice versa, dependent actions as in a.b + b.a should be undone in reverse order of completion; e.g., if the left branch is chosen by executing first a and then b, action b should be undone before a. These two simple examples already provide many intuitions. First, reversibility distinguishes concurrency from non-determinism. Second, different instances of the same action may need to be distinguished, e.g., the two a actions in a.b + b.a are different because they have different causal dependences. This explains why many approaches to reversibility [START_REF] Phillips | Reversing algebraic process calculi[END_REF][START_REF] Lanese | Reversing higher-order pi[END_REF][START_REF] Cristescu | A compositional semantics for the reversible pi-calculus[END_REF] rely on unique indexes for processes. Last, actions in a thread are undone in reverse order of execution, while concurrent threads are reversed independently (unless there are synchronizations). This explains why in many approaches history information is attached to threads. Let us now discuss synchronization. Consider for instance the process νb (a.b | b.c).

Here the only possible forward computation is given by an input on a, followed by a synchronization between b and b, and by an input on c. Here, a and c are in different threads, and do not interact directly, however c blocks the undo of a via the synchronization on b.

Even in this simple setting, a few subtleties emerge, and one can ask whether there are correctness criteria for causal-consistent reversibility. In other words, given a language equipped with its reversible semantics, how can one check whether this is indeed a correct causal-consistent reversible semantics? Two properties have been put forward in the literature since [START_REF] Danos | Reversible communicating systems[END_REF].

The first property, called Loop Lemma, says that each transition has an inverse. Formally, for each forward transition t :

P α - → f Q there is a backward transition t -1 : Q α -1
--→ b P and vice versa, where α -1 is the inverse label of α and subscripts f and b are used to distinguish f orward transitions from backward ones. An obvious consequence of the Loop Lemma is that any (non trivial) program in a language with uncontrolled reversibility can diverge by doing and undoing the same action forever.

The second property, called causal-consistency, relates reversibility and concurrency. Indeed, it is based on a notion of concurrent transitions. If two transitions t 1 : Another interesting property is the so-called Parabolic Lemma, which states that each reversible computation can be decomposed into a backward computation followed by a forward one. Intuitively, this means that, up to causal equivalence, the process first goes backward to enable as many choices as possible, and only then goes forward. Consider, for instance, the CCS process a+b | c.d. Assume that we are in a state in which the process has performed the action a, that is the process has now the form c.d (where, for the sake of simplicity, we omit the history information about the execution of action a). Assume also that the process c.d

P α 1 -→ R
proceeds with the computation c - → f d - → f a -1 --→ b .
According to the Parabolic Lemma, we can decompose the above trace into a backward one followed by a forward one, that is

a -1 --→ b c - → f d - → f . Notably, after the backward transition a -1
--→ b , the process goes back to its initial state, where all possible forward computations are enabled.

Finally, since the reversible language is normally a reversible extension of an existing language, a correspondence theorem shows that the forward semantics of the reversible language indeed coincides with the standard semantics of the underlying language.

Given these premises, the works in the literature can be mainly classified according to which underlying language they consider, and whether they deal with a reduction semantics or a LTS one. Other differences lie in the technical means used for storing history and causality information. The approaches in the literature are summarized in Table 1.

Reversible CCS (RCCS) [START_REF] Danos | Reversible communicating systems[END_REF] is the first proposal of a causal-consistent reversible calculus. It introduces the notion of memories attached to threads to keep history information. In RCCS memories are also used as thread identifiers. [START_REF] Danos | Reversible communicating systems[END_REF] CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF] stacks memories as ids fork numbers labeled CCS-R [START_REF] Danos | Formal molecular biology done in CCS-R. In BioConcur[END_REF] CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF] stacks thread ids empty memories labeled CCSK [START_REF] Phillips | Reversing algebraic process calculi[END_REF] CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF] communication -labeled (static rules) keys ρπ [START_REF] Lanese | Reversing higher-order pi[END_REF] HOπ [START_REF] Sangiorgi | Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms[END_REF] non-structured thread ids structured tags reduction Rπ [START_REF] Cristescu | A compositional semantics for the reversible pi-calculus[END_REF] π-calculus [START_REF] Milner | A Calculus of Mobile Processes, I and II[END_REF] stacks event ids fork symbol labeled Reversible DSD [START_REF] Phillips | A programming language for composable DNA circuits[END_REF] signal ids -reduction structures [START_REF] Cardelli | Reversible structures[END_REF] (pointers to next operations) RµOz [START_REF] Lienhardt | A reversible abstract machine and its space overhead[END_REF] µOz [START_REF] Lienhardt | A reversible abstract machine and its space overhead[END_REF] stacks thread ids -reduction CCS-R [START_REF] Danos | Formal molecular biology done in CCS-R. In BioConcur[END_REF] extends RCCS to deal with recursion, and uses unique names to identify threads.

CCS with communication Keys (CCSK) [START_REF] Phillips | Reversing algebraic process calculi[END_REF] is the instance on CCS of a general procedure to make calculi, specified in a simple path format, reversible. The main novelty of the approach is that the structure of processes is not consumed, but simply annotated as executed. This is obtained by making all the rules defining the semantics static. Thus, no memories are needed. The approach can be applied to other calculi without name passing, such as ACP [START_REF] Bergstra | Process Algebra for Synchronous Communication[END_REF] or CSP [START_REF] Brookes | A Theory of Communicating Sequential Processes[END_REF], but it is not suitable for name-passing calculi, as the π-calculus.

The reversible higher-order π-calculus (ρπ) [START_REF] Lanese | Reversing higher-order pi[END_REF] is a reversible extension of the higher-order π-calculus [START_REF] Sangiorgi | Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms[END_REF]. Notably, differently from the approaches mentioned before, the semantics of ρπ is only given in a reduction style.

A reversible extension of π-calculus is Rπ [START_REF] Cristescu | A compositional semantics for the reversible pi-calculus[END_REF]. Rπ at the moment is the only reversible calculus with name passing that provides a labeled semantics. A main feature of Rπ is that two transitions are concurrent only if there is a context where the reductions generated by those two transitions are actually concurrent.

Reversible structures [START_REF] Cardelli | Reversible structures[END_REF] are a simple computational calculus for modeling chemical systems composed by signals and gates. The gate structure is not consumed, and a cursor reminds which part of the gate already interacted. The novelty of this setting is that signal identifiers are not necessarily unique, following the idea that two instances of the same molecule are indistinguishable.

Finally, RµOz [START_REF] Lienhardt | A reversible abstract machine and its space overhead[END_REF] is a reversible abstract machine for a functional language with threads and asynchronous communication via ports. The works discussed above specify how a system can reverse a forward computation and what kind of information it should exploit, but they give no hint about when forward execution should be preferred over backward one and vice versa. At most, one can non-deterministically choose whether to go forward or backward, obtaining a system that may well diverge by doing and undoing the same action again and again. Those works have been useful to understand the basics of causalconsistent reversibility, but they are not directly suitable for most applications.

Indeed, in practice, the direction of computation is determined by various conditions, related to the application area. For instance, in biology, temperature and pressure conditions determine the chosen direction of computation. In state space exploration, normal computation is forward and backtracking is used when the forward computation gets stuck since no solution can be found from the reached state. Similarly, when programming reliable systems, backtracking is used when an error state is reached.

Those strategies can be implemented using different mechanisms. We describe below the main mechanisms that have been considered, following the categorization in [START_REF] Lanese | Controlled reversibility and compensations[END_REF].

Internal control: specific commands inside processes specify whether the process itself should go forward or backward. A possibility along this line has been explored in [START_REF] Danos | Transactions in RCCS[END_REF], where irreversible actions, i.e. actions that once performed cannot be undone, have been integrated in RCCS. The idea underlying irreversible actions is that, when the exploration reaches a desirable result, backtracking is disallowed by executing an irreversible action.

In other words, an irreversible action acts as a sort of commit. A dual approach has been proposed in roll-π [START_REF] Lanese | Controlling reversibility in higher-order pi[END_REF], an extension of ρπ. There, normal computation is forward, and an explicit rollback primitive is used to trigger backward execution. In this way, when an error state is reached, the rollback primitive can be used to go back to a past consistent state. To specify how far back to go, the rollback primitive takes as parameter a reference to a past action, and it undoes all (and only) the actions causally dependent on it. Note that, in a concurrent scenario, a (possibly more intuitive) behavior such as "go back n steps" is not meaningful, since there may not be a unique choice about which the last n actions have been. Irreversible actions and explicit rollback are dual, the former specifying when it is forbidden to go back, and the latter specifying when it is required to go back. The roll-π approach is satisfactory to deal with transient errors, but not with permanent errors. In this second case, rollback leads back to a past state, where the same computation can restart, leading again to the same error state. To solve this problem, a construct, called alternative, is introduced in [START_REF] Lanese | Concurrent flexible reversibility[END_REF] to specify a (slightly) different behavior to be chosen after a rollback.

External control: this approach follows the separation of concerns principle: a process is potentially able to go both backward and forward, while another process is in charge of controlling it by deciding when it has to go backward and when it has to go forward. Such an approach is suitable, e.g., for hierarchical component-based systems, where the father component may decide when and how to roll-back its children, and the children notify the father in case of errors. Such a hierarchical structure for failure handling is typically the one advocated for Erlang systems [START_REF] Armstrong | Making reliable distributed systems in the presence of software errors[END_REF]. External control naturally emerges in a reversible debugger such as the one proposed in [START_REF] Giachino | Causal-consistent reversible debugging[END_REF] for µOz [START_REF] Lienhardt | A reversible abstract machine and its space overhead[END_REF]: the user, through the debugger interface, decides whether the program under debugging should execute forward or should get back to a previous state. One can either go back step-by-step, and the debugger ensures that only actions with no causal dependences can be undone, or can choose a past action and undo it and all its consequences in a causalconsistent way, as done by the rollback primitive of roll-π described above. This is in contrast, e.g., to [START_REF] Cook | Reverse execution of java bytecode[END_REF], where the user has to decide which actions to undo and in which order. External control has been applied also to biological reversible systems in [START_REF] Phillips | A reversible process calculus and the modelling of the ERK signalling pathway[END_REF]. There, a reversible CCS process P is controlled by a controller process C, which is again a CCS process. The controller C always computes forward, and it constrains the possible actions of P, thus decreasing the non-determinism due to reversibility and to concurrency. Together with a generalized form of prefix, this allows one to model different forms of reversibility, including reversibility that is not (always) causally consistent.

Semantic control: in this approach the semantics of the language is extended with guidelines on whether to go forward or to go backward. Consider the following scenario: a reversible program is used to perform a state-space exploration looking for some solution of a given problem. In this case reversibility is needed to backtrack in case a branch with no solution has been taken. One can imagine to add to the history information about whether and how many times a particular path has been taken and favor paths (and directions of execution) leading to less explored areas. For instance, one can label each action with the number of times it has been tried, and choose among the enabled actions (both forward and backward) one with the minimal value. It is clear that in such a way a finite state space is completely explored, allowing to find a solution if at least one exists. A refined approach has been explored in [START_REF] Bacci | On the statistical thermodynamics of reversible communicating processes[END_REF]. There RCCS is equipped with a probabilistic [START_REF] Danos | Transactions in RCCS[END_REF] RCCS [START_REF] Danos | Reversible communicating systems[END_REF] Internal Roll [START_REF] Lanese | Controlling reversibility in higher-order pi[END_REF] ρπ [START_REF] Lanese | Reversing higher-order pi[END_REF] Internal Roll+alternatives [START_REF] Lanese | Concurrent flexible reversibility[END_REF] ρπ [START_REF] Lanese | Reversing higher-order pi[END_REF] Internal Debugger [START_REF] Giachino | Causal-consistent reversible debugging[END_REF] RµOz [START_REF] Lienhardt | A reversible abstract machine and its space overhead[END_REF] External Controller [START_REF] Phillips | A reversible process calculus and the modelling of the ERK signalling pathway[END_REF] CCSK [START_REF] Phillips | Reversing algebraic process calculi[END_REF] External Potential [START_REF] Bacci | On the statistical thermodynamics of reversible communicating processes[END_REF] RCCS [START_REF] Danos | Reversible communicating systems[END_REF] Semantic semantics, where the rate of forward and backward steps is determined by energy potential. The paper shows that if the potential satisfies suitable conditions then a solution, if it exists, is reached in a finite amount of time even in an infinite state space. The main point is to avoid that the computation diverges in an infinite branch without solutions.

We conclude the section by summarizing the main approaches described above in Table 2.

Theoretical Results

We described till now the calculi that have been proposed to model reversible systems. The formalization enabled further studies, concerning in particular the behavioral theory, the related logics, abstract representations as event structures or categories, the relations between different reversible and irreversible calculi, the cost of reversibility in terms of space, and the complexity of analyzing reversible systems.

Concerning behavioral theory, the seminal paper [START_REF] De Nicola | Back and forth bisimulations[END_REF] considers back and forth bisimulation, a variation of bisimulation where processes should match not only in the forward direction, but also in the backward one. It shows that in principle this allows one to distinguish concurrency from non-determinism. In fact, in a | b one can do a, then b and then either undo a and then b or b and then a. Instead, in a.b+b.a, if one does a and then b, it is obliged to undo first b and then a. However, [START_REF] De Nicola | Back and forth bisimulations[END_REF] quickly dismissed this setting by obliging processes to go back following the same path they were coming from. With this restriction, back and forth strong bisimilarity is as expressive as standard strong bisimilarity. This is not the case for other equivalences.

In causal-consistent reversible calculi, processes can go back along causalequivalent paths. In this setting, the natural notion of bisimilarity allows forward (resp. backward) moves to match only forward (resp. backward) ones. This relation is more discriminating than standard strong bisimilarity for the reason above.

Indeed, [START_REF] Phillips | A hierarchy of reverse bisimulations on stable configuration structures[END_REF] has shown that (in the context of stable configuration structures) this notion of reversible bisimilarity is as strong as hereditary history-preserving bisimilarity [START_REF] Joyal | Bisimulation from open maps[END_REF] (in the absence of auto-concurrency, i.e. when concurrent events do not have the same label).

Similar results are obtained also for logics. An extension of Hennessy-Milner Logic [START_REF] Hennessy | Algebraic laws for nondeterminism and concurrency[END_REF] with backward modalities has been studied in [START_REF] Nielsen | Bisimulation for models in concurrency[END_REF], which shows that, in the absence of auto-concurrency, the extended logic characterizes the hereditary history-preserving bisimulation [START_REF] Joyal | Bisimulation from open maps[END_REF]. In [START_REF] Phillips | A logic with reverse modalities for history-preserving bisimulations[END_REF], an extension of Hennessy-Milner Logic with reverse modalities and event identifiers, used to distinguish the undo of different events with the same label, is proved to characterize hereditary history-preserving bisimulation even in presence of auto-concurrency. Sublogics of this logic are proved to characterize history-preserving bisimulation, weak history-preserving bisimulation and hereditary weak history-preserving bisimulation (see [START_REF] Van Glabbeek | Refinement of actions and equivalence notions for concurrent systems[END_REF] for a description of these logics).

The above results about logics are obtained by defining backward moves inside standard stable event structures. A first notion of reversible event structure has been proposed in [START_REF] Phillips | Modelling of bonding with processes and events[END_REF], by adding reversing events to Winskel event structures [START_REF] Winskel | Event structures[END_REF]. The approach is refined in [START_REF] Phillips | Reversibility and asymmetric conflict in event structures[END_REF][START_REF] Ulidowski | Concurrency and reversibility[END_REF] by describing backward steps as the removal of an event from the current configuration. The approach is applied to define both reversible prime event structures and reversible asymmetric event structures. The expressive power of the two kinds of structures is studied. A main point of the approach is the possibility of specifying both causal-consistent and non causalconsistent reversibility.

An abstract model of reversibility based on category theory has been studied in [START_REF] Danos | General reversibility[END_REF]. The results therein essentially generalize the ones in [START_REF] Danos | Transactions in RCCS[END_REF], showing how given a category of computations including both reversible and irreversible actions one can define in a unique way (up-to isomorphisms) a category of histories allowing to correctly define causal-consistent reversible computations. Furthermore, it shows that the computations of systems with histories are essentially the same as the causal computations of the original system, i.e. the computations where only those reversible actions needed to execute irreversible actions are performed.

Given that many reversible languages exist in the literature, a natural question is the relationship between them, and with the non reversible languages. A main result in this setting has been presented in [START_REF] Lanese | Reversing higher-order pi[END_REF], where ρπ has been encoded into the higher-order π-calculus. The correctness of the encoding has only been proved up-to weak barbed equivalence (mixing forward and backward reductions), but the actual correspondence is tighter. This is the only encoding of a causal-consistent reversible calculus into a non reversible one we are aware of. Concerning encodings of reversible calculi into other reversible calculi, in [START_REF] Cardelli | Reversible structures[END_REF] an encoding of asynchronous RCCS [START_REF] Danos | Reversible communicating systems[END_REF] into reversible structures is provided. An operational correspondence result shows that RCCS steps are correctly matched.

A separation result has been proved in [START_REF] Lanese | Concurrent flexible reversibility[END_REF], showing that the introduction of alternatives strictly increases the expressive power of the rollback operator of roll-π [START_REF] Lanese | Controlling reversibility in higher-order pi[END_REF]. The separation result shows that no encoding can preserve both the possibility of performing a backward step, and termination.

The cost of irreversibility in terms of space has been studied in [START_REF] Lienhardt | A reversible abstract machine and its space overhead[END_REF]. Indeed, this paper proves that reversible µOz stores history information which is linear in the number of steps for any given program. More importantly, it shows that in order to enable causal-consistent reversibility an amount of history information which is linear in the number of steps is actually needed in the worst case. The main point is that with less information one is not able to distinguish different pasts leading to the same state which are not causally equivalent.

Reversibility has been proved useful for specifying and proving correct systems based on state-space exploration. Indeed, classically one has to specify both the exploration strategy and how to escape from states from where no solution can be found. In a reversible system, only the exploration strategy needs to be specified, since the reversibility mechanism can be used to escape undesired states. This leads to smaller specifications, which are easier both to understand and to verify correct as shown in [START_REF] Danos | Self-assembling trees[END_REF][START_REF] Krivine | A verification technique for reversible process algebra[END_REF].

The cost of deciding reachability has been studied in reversible structures [START_REF] Cardelli | Reversible structures[END_REF], and proved quadratic in the number of gates for coherent reversible structures (where atoms have unique identifiers). Only an EXPSPACE bound is known for weak coherent reversible structures (where identifiers are not unique).

Applications

Causal-consistent reversibility is quite young. Nevertheless the first applications are emerging in different areas, in particular in the fields of biological systems, state-space exploration, reliability and debugging.

The modeling of systems and reactions from biology and biochemistry has been highlighted as an interesting application area for causal-consistent reversibility since the seminal work presented in [START_REF] Danos | Reversible communicating systems[END_REF]. The first real application has been presented in [START_REF] Danos | Formal molecular biology done in CCS-R. In BioConcur[END_REF], where CCS-R is used to model a system in which the transcription of a protein is controlled by a competition between different reactants. The modeling of the beginning of the RTK-MAPK cascade [START_REF] Regev | Representation and simulation of biochemical processes using the pi-calculus process algebra[END_REF] is also discussed. The Ras/Raf-1/MEK/ERK signaling pathway [START_REF] Cho | Mathematical modeling of the influence of RKIP on the ERK signaling pathway[END_REF], which delivers mitogenic and differentiation signals from the membrane of a cell to its nucleus, has been modeled in CCSK with a control operator in [START_REF] Phillips | A reversible process calculus and the modelling of the ERK signalling pathway[END_REF]. A main point here is that reversibility is not causal-consistent. For instance, in a reaction it happens that an event a causes b, b causes c and c causes d. Now, according to causal-consistent reversibility, undoing the event a would cause the undoing of the other three events, but this is not what happens in practice. The same application is also considered in [START_REF] Phillips | Modelling of bonding with processes and events[END_REF], and modeled with a calculus relying on an explicit notion of bonding. In [START_REF] Phillips | Reversibility and asymmetric conflict in event structures[END_REF] the basic catalytic cycle for protein substrate phosphorylation by a kinase [START_REF] Jeffrey | Mechanisms of specificity in protein phosphorylation[END_REF] is described using reversible event structures.

Another area where reversibility has been applied is state-space exploration. Indeed, one of the first languages with rollback capabilities is Prolog, which explores the state-space of SLD-derivations looking for a solution for a given goal. A first application of causal-consistent reversibility for state-space exploration has been presented in [START_REF] Danos | Self-assembling trees[END_REF], where an algorithm for creating a set of trees from nodes equipped with their arities is specified in RCCS. In [START_REF] Krivine | A verification technique for reversible process algebra[END_REF] a RCCS model of the classic dining philosophers problem is used as a benchmark for the efficiency of checking the conformance to a given specification. Finally, in [START_REF] Lanese | Concurrent flexible reversibility[END_REF] a concurrent solution of the 8-queens problem is presented, and then implemented in Maude [START_REF] Clavel | Maude: specification and programming in rewriting logic[END_REF]. These examples are noteworthy not for their performances (the ones in RCCS may even not terminate), but for their concise and clear definition, which takes advantage of the fact that backtracking is available in the language semantics. Also, they all refer to highly distributed algorithms, where a global solution is obtained by a set of peers through binary synchronizations. Indeed, this is the setting where reversibility shines, since the peers may easily reach states from where no solution can be found, and backtracking is needed to avoid deadlocks.

The first contribution on reversibility concerning constructs for programming reliable systems is in [START_REF] Danos | Transactions in RCCS[END_REF]. There, irreversible actions are introduced in RCCS. This gives rise in a natural way to a very simple notion of transaction. Indeed, while executing only reversible actions a process is conceptually executing inside a transaction, which can be aborted at any time simply by undoing the performed actions. Irreversible actions act as a commit, since they make the performed actions permanent (durability of transactions). In particular, all the actions on which the irreversible action depends are committed in this way.

This first attempt at modeling transactions is quite basic, since, e.g., it only considers non-nested transactions. A more refined approach is presented in [START_REF] Lanese | Concurrent flexible reversibility[END_REF]. There, CommTrans [START_REF] Vries | Communicating transactions[END_REF], a calculus featuring a notion of interacting transactions with compensation, is encoded in roll-π with alternatives. These transactions allow the transactional process to interact with the environment. In case of abort, the changes performed on the environment are undone, while the body of the transaction is replaced by a compensation. The same behavior can be obtained in roll-π with alternatives by rolling back the initial action of the transaction, and using alternatives to encode compensations. The correctness and completeness of the encoding is proved resorting to an ad hoc notion of bisimulation. Interestingly, roll-π has a more precise management of causality information than CommTrans, and this allows it to undo only those actions which are causally related to the transaction body, while CommTrans also features some spurious undo of unre-lated actions.

Reversible debugging has been studied in the sequential setting since a long time [START_REF] Grishman | The debugging system AIDS[END_REF][START_REF] Zelkowitz | Reversible execution[END_REF], and today various sequential reversible debuggers exist. Even GDB [START_REF] Gdb | The GNU Project Debugger[END_REF] provides support for reversible debugging since version 7. However, most of the available reversible debuggers do not support concurrency. A few of them do, and they can be divided in two classes:

Log-based: [START_REF]Commercial reversible debugger[END_REF][START_REF] King | Debugging operating systems with time-traveling virtual machines[END_REF] record the exact order of execution of actions, and they undo them exactly in reverse order of execution;

Without log: [START_REF] Visan | Temporal debugging using URDB[END_REF][START_REF] Arya | FReD: Automated debugging via binary search through a process lifetime[END_REF][START_REF]Commercial reversible debugger[END_REF] replay the program till the desired point, but may use a different scheduling each time, thus potentially generating a different behavior, which may not highlight the same bugs.

According to the causal-consistent approach, actions should be undone in any order which is compatible with the causal dependencies. Such an approach has been explored in [START_REF] Giachino | Causal-consistent reversible debugging[END_REF]. The main primitives considered there are the undo of a single action in a given thread, which is enabled only if the action has no dependences, and a primitive for undoing a given action including all its dependences. The semantics of this primitive essentially coincides with the one of the rollback primitive of roll-π. The primitive comes with different interfaces, which allow one to choose the action to be undone according to the kind of wrong behavior that is observed. For instance, if an unexpected message is seen, the interface allowing one to undo the send of a given message can be used. Similar interfaces allow one to undo the creation of a variable, the receipt of a message and the creation of a thread. Equipped with these primitives, the debugging strategy consists in finding a misbehavior and recursively undo the actions that may have caused it. Interestingly, the debugger autonomously finds which thread these actions belong to, and which are the dependencies. The only other work considering causality information for debugging is CauseWay [START_REF] Stanley | Causeway: a message-oriented distributed debugger[END_REF], which is only a post-mortem trace analyzer, with no execution capabilities.

Conclusion

Causal-consistent reversibility, introduced in [START_REF] Danos | Reversible communicating systems[END_REF], is arguably the correct notion of reversibility in a concurrent scenario. Since its definition, different approaches and applications of causal-consistent reversibility have been considered. Nonetheless, the field is still at an initial stage, and while interesting ideas have been proposed, a systematic study of the related problems and of the possible application areas is still missing. Concerning the definition of uncontrolled reversibility, different approaches exist and have been outlined in Section 2, but the relationships among them are not clear. The only approach trying to deal with multiple calculi in a uniform way [START_REF] Phillips | Reversing algebraic process calculi[END_REF] poses quite strict constraints on them. Furthermore, all these approaches deal with toy languages, with [START_REF] Lienhardt | A reversible abstract machine and its space overhead[END_REF] probably being the one more in the direction of real languages. Indeed, the interplay between reversibility and various language features, with dynamic data structures, objects, error handling and type systems2 being probably the most relevant, is still not understood. This would be useful, e.g., to write causal-consistent debuggers for real languages.

For controlled reversibility, different control mechanisms have been proposed. However, how they relate and compose and whether they are enough to specify all the needed control policies, or even which the needed control policies are, is not clear.

Coming to the theoretical treatment, different interesting aspects have been studied, but most of the approaches are tailored to one specific calculus, and it is not clear whether they can be applied in more general cases. A main open point is understanding which is the good notion (or, possibly, which are the good notions) of behavioral equivalence to reason about reversible systems. In the strong case, back and forth bisimilarity, allowing to undo actions according to any causalconsistent path, is a reasonable candidate. In the weak case, many more possibilities exist, since, e.g., it is not clear if backward (resp. forward) τ actions should be allowed when matching forward (resp. backward) actions. Also, reversible processes are equipped with history information, and it is not clear how to deal with this information when doing axiomatic reasoning on reversible programs.

Coming to applications, the preliminary results described in Section 5 are encouraging, but a deeper exploration is needed. For instance, in the field of constructs for reliable systems, the relation between causal-consistent reversibility and distributed checkpointing is still unclear. Also, it seems reasonable that reversibility can be handy to deal with software transactional memories, but a precise relationship has not been found yet. In the biological field, it seems that causal-consistent reversibility is not enough to capture all the observed behaviors, but how to generalize it to cope with them deserves further investigation.

  1 and t 2 : P where ǫ is an empty trace and ; the sequential composition of traces. Causalconsistency says that two coinitial traces are cofinal iff they are causal equivalent. While quite obscure at first sight, this definition captures the essence of causalconsistent reversibility. Indeed, two computations starting from the same state (coinitial) that are causal equivalent should end in the same state (cofinal), since exchanging the order of concurrent actions and doing and undoing the same action

	closing the square. One can define causal equivalence, written ∼, as the minimal
	equivalence on traces closed under composition and satisfying:
	t 1 ; t 2 /t 1 ∼ t 2 ; t 1 /t 2	t; t -1 ∼ ǫ	t -1 ; t ∼ ǫ
	α 2 -→ R 2 starting from the same process P are concurrent then there exist two transitions t 1 /t 2 : R 2 α 1 -→ Q and t 2 /t 1 : R 1 α 2 -→ Q

should not change the final state. Vice versa, computations that differ for any other reason should not lead to the same state, i.e. should not be confused since they have different pasts. For instance, the two computations leading from a.b + b.a to 0 should not be confused, since they have different pasts, and indeed history information should be added to the final state 0 to disambiguate the two possible histories.

Table 1 :

 1 Process calculi with uncontrolled reversibility

	Language	Memories	Identifiers	Fork handling Semantics
	RCCS

Table 2 :

 2 Process calculi with controlled reversibility

	Mechanism	Calculus Category
	Irreversible actions

The first example of a reversible sequential programming model is the reversible Turing machine[START_REF] Bennett | Logical Reversibility of Computation[END_REF].

A preliminary exploration of the interplay between reversibility and session types is presented in[START_REF] Tiezzi | Towards reversible sessions[END_REF].

* This work has been partially supported by the MIUR PRIN project CINA n. 2010LHT4KM. † This author has been also partially supported by the French National Research Agency (ANR), project REVER n. ANR 11 INSE 007.