We present in this paper a fine-grained rollback primitive for the higher-order pi-calculus (HOpi), that builds on the reversibility apparatus of reversible HOpi. 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 in this paper a high-level operational semantics which we prove sound and complete with respect to reversible HOpi backward reduction. We also define a lower-level distributed semantics, which is closer to an actual implementation of the rollback primitive, and we prove it to be fully abstract with respect to the high-level semantics.
Controlling Reversibility in Higher-Order Pi / I. Lanese; C. A. Mezzina; A. Schmitt; J. Stefani. - STAMPA. - 6901:(2011), pp. 297-311. (Intervento presentato al convegno CONCUR 2011, 22nd International Conference on Concurrency Theory tenutosi a Aachen, Germany nel 5-10/9/2011) [10.1007/978-3-642-23217-6_20].
Controlling Reversibility in Higher-Order Pi
LANESE, IVAN;
2011
Abstract
We present in this paper a fine-grained rollback primitive for the higher-order pi-calculus (HOpi), that builds on the reversibility apparatus of reversible HOpi. 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 in this paper a high-level operational semantics which we prove sound and complete with respect to reversible HOpi backward reduction. We also define a lower-level distributed semantics, which is closer to an actual implementation of the rollback primitive, and we prove it to be fully abstract with respect to the high-level semantics.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
