Reversibility in Concurrency
Ivan Lanese
Computer Science Department
Focus research group
University of Bologna/INRIA
Bologna, Italy
Joint work with Michael Lienhardt (PPS),
Claudio Antares Mezzina (Trento),
Jean-Bernard Stefani (INRIA) and
Alan Schmitt (INRIA)
1
Roadmap

Reversibility

Uncontrolled reversibility

Controlled reversibility

Compensations

Conclusions
What is reversibility?
The possibility of executing a (concurrent) computation
both in the standard, forward direction, and in the
backward direction, going back to a past state


In some areas systems are naturally reversible: biology,
quantum computing, …
In concurrent systems reversibility allows for
recoverability
– In case of error I go back to a past state which is safe
– We want to use reversibility as a general framework for
programming reliable applications
Concurrent reversibility

In concurrent systems one cannot simply undo “the last
action”
– It is not clear which is the last action


Independent threads are reversed independently
Causal dependencies should be respected
– First reverse the consequences, then the causes
a
b
b
a
Causal Consistent Reversibility

In concurrent systems one cannot simply undo “the last
action”
– It is not clear which is the last action


Independent threads are reversed independently
Causal dependencies should be respected
– First reverse the consequences, then the causes
a
b
b
a
Research questions




How do I reverse a concurrent computation?
How do I control reversibility?
How do I avoid redoing the same errors?
Can I recover existing dependability patterns and devise
new ones?
How do I reverse a concurrent computation?

A few approaches in the literature
–
–
–
–
–

These works define the semantics of uncontrolled
reversibility
–


RCCS by Danos and Krivine [CONCUR 2004]
CCSk by Phillips and Ulidovski [FoSSaCS 2006]
Rhopi by Lanese et al. [CONCUR 2010]
Reversible structures by Laneve and Cardelli [CMSB 2011]
Reversible µOz by Lanese et al. [FMOODS/FORTE 2012]
No hint on when to go backward and up to where
Useful to understand the possible behaviors
More useful as models than as programming languages
Main idea

I keep track of past communication actions and of
causal dependencies
–
–
–
Communication should cause no loss of information
Substitutions normally causes loss of information
Different technical solutions
Power is nothing without control

Programs based on uncontrolled
reversibility are not very useful
– They always diverge
– No way to make a result persistent

We want to go back only when needed
–

In particular, in case of errors
We want to specify how far back to go
Reversibility control

Different approaches in the literature
– Irreversible actions by Danos and Krivine
[CONCUR 2005]
– Rollback operator by Lanese et al [CONCUR 2011]
– Energy parameters by Bacci et al [CALCO 2011]
– Monitors by Phillips et al [RC 2012]
Roll-π idea



Normal computation goes forward
There is an explicit primitive, roll γ, to trigger a rollback
γ refers to a specific action done in the past
–
–
–
–
We specify which action to undo
As a result we undo all the actions depending on it
Independent actions are not undone
In a concurrent world one cannot say “undo the last 10
actions”
Is roll-π enough?

Roll-π allows to control reversibility
– Backtracking only in case of need
– Otherwise the computation proceeds forward

In case of rollback
–
–
–
–


We go back to a past consistent state
And we execute forward again from it
We may take the same path, obtaining the same error again
Good for transient errors, not for permanent ones
Each roll-π program is divergent
We want to remember the past tries and learn from them
Compensations

From database theory and business processes
– Piece of code to recover from an error
– Moving from the error state to a safe state

For us, piece of code allowing to move
–
–
–
–
From the past consistent state produced by the rollback
To a slightly different state
Keeping into account the past try
Trying to avoid to repeat the same error
Actions with compensations

Instead of actions A we use actions with compensations
– A%0 : try A then stop trying
– A%B%0 : try A then B then stop trying


If the action with compensation is the target of the
rollback, it is replaced by its compensation
Using compensations the programmer may now avoid looping
The croll-π calculus [ESOP 2013]



A causal consistent reversible higher-order π
With a rollback operator
And with compensations attached to messages
– Only messages allowed as compensations

No other reversible calculi with compensations in the
literature
And now?




We have to test the expressive power of messages with
compensations
Can we programme interesting applications exploiting
rollback and compensations?
Can we recover/improve recoverability patterns from
the literature?
And invent new ones?
Messages with compensations are robust

We can encode different idioms:
–
–
–
–
General compensations: not only messages
Finite retry: try n times
Endless retry: try forever (same as roll-π)
Triggers with compensations: we attach compensations to
triggers instead of to messages
What can we model?

Interesting problems, programmed on top of a Maude
interpreter
– State space exploration with backtracking: 8 queens problem
– Error handling scenario: Automotive case study from Sensoria
project

Can we recover/improve existing techniques?
– Software transactional memory model from Acciai et al.
[ESOP’07]
– Interacting transactions from Hennessy et al. [CONCUR
2010]
Interacting transactions

A transaction is a computation that may
– Succeed, making the results permanent
– Abort, undoing all its effects
– May have a compensation to be executed upon abort

Interacting transactions are allowed to interact with the
environment during their execution
Hennessy interacting transactions
Our approach






A transaction is started by an action with compensation
Undo is modelled by rollback
Effects of the transaction are automatically undone
A compensation can be specified
Our causality tracking is more precise than Hennessy
embedding mechanism
We avoid some spurious rollbacks they have
Summary


Causal consistent reversible calculi
Mechanisms for controlling reversibility
– Roll operator


Compensations for programming what to do after
rollback
Some interesting applications
Future work





A long road in front of us
Which other mechanisms for controlling reversibility
can one define?
Can we recover/improve/combine other techniques for
dependable systems from the literature?
Studying the behavioral theory of reversible calculi
Going towards more complex languages
– Klaim, Concurrent ML, Erlang

What about a reversible debugger?
Finally
Descargar

Synchronization strategies for global computing