CITI has stopped operations in 2014, to co-launch NOVA LINCS THIS SITE IS NOT BEING UPDATED SINCE 2013
citi banner
Home Page FCT/UNL UNL
  Home  \  Seminars @ CITI  \  Seminar Page Login  
   
banner bottom
File Top
Reversing execution in higher order pi-calculus
{ Wed, 7 Dec 2011, 14h00 }

By: Claudio Mezzina  [ show info ]

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.


Hosted by: Software Systems

Location: DI seminars room

File Bottom