Controlling reversibility in rhopi

In rhopi every step can always be undone, and each process freely moves back and forward. To make rhopi usable to program recoverable systems, the ability to go back has to be controlled. Many possibilities in this direction exist. We analyze one such possibility, namely the introduction in rhopi of an explicit rollback primitive. The definition of a proper semantics for such a primitive is a surprisingly delicate matter because of the potential interferences between concurrent rollbacks. We define a high-level operational semantics allowing to capture concurrent rollbacks. We also define a lower-level distributed semantics, which is closer to an actual implementation of the rollback primitive. The two semantics are equivalent with respect to weak barbed congruence.