Abstract | ||
---|---|---|
We present in this paper a fine-grained rollback primitive for the higher-order π-calculus (HOπ), that builds on the reversibility apparatus of reversible HOπ [9]. 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 HOπ backward reduction. We also define a lowerlevel 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. |
Year | Venue | Keywords |
---|---|---|
2011 | CONCUR | delicate matter,high-level operational semantics,reversible ho,potential interference,high-level semantics,controlling reversibility,concurrent rollback,fine-grained rollback,proper semantics,higher-order pi,actual implementation,reversibility apparatus |
Field | DocType | Volume |
Operational semantics,Computer science,Theoretical computer science,Transitive closure,Rollback,Semantics | Conference | 6901 |
ISSN | Citations | PageRank |
0302-9743 | 30 | 1.29 |
References | Authors | |
9 | 4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Ivan Lanese | 1 | 733 | 53.86 |
Claudio Antares Mezzina | 2 | 145 | 16.93 |
Alan Schmitt | 3 | 96 | 7.30 |
Jean-Bernard Stefani | 4 | 1201 | 77.02 |