Detail

Reversing execution in higher order pi-calculus

Reversible computing has a long history. Nowadays, reversible
computing is attracting increasing interest because of its potential
applications in diverse fields, including hardware design, biological
modelling, program debugging and testing and quantum computing. Of
particular interest is the application of notions of reversible
computing to the study of programming abstractions for dependable
systems, because several techniques used to build dependable systems
rely on some forms of undo or rollback.

In this talk I will present recent results on defining reversible
computing from a process calculi perspective.
More precisely, I will present the reversible, higher-order pi-calculus (rhopi).
Our work has continued the study undertaken on reversible CCS by
Vincent Danos and Jean Krivine.

We prove that reversibility in our calculus is causally consistent.
Moreover, we design a fine-grained rollback primitive able to control
the rollback of a concurrent execution. We give a formal specification
of this primitive and show that it enjoys good properties, even in
presence of concurrent conflicting rollbacks. We then devise a
concurrent algorithm implementing such primitive and show that the
algorithm respects the defined semantics.

The talk will be based on joint work with Ivan Lanese and J.B. Stefani.