Bisimulations for Communicating Transactions (Extended Abstract)
File Type:
PDFItem Type:
Conference PaperDate:
2014Access:
openAccessCitation:
MATTHEW HENNESSY, VASILEIOS KOUTAVAS, Carlo Spaccasassi, 'Bisimulations for Communicating Transactions (Extended Abstract)', Springer Berlin Heidelberg, Lecture Notes in Computer Science;8412, 2014Download Item:
Abstract:
We develop a theory of bisimulations for a simple language containing communicating transactions, obtained by dropping the isolation requirement of standard transactions. Such constructs have emerged as a useful programming abstraction for distributed systems.
In systems with communicating transactions actions are tentative, waiting for certain transactions to commit before they become permanent. Our theory captures this by making bisimulations history-dependent, in that actions performed by transactions need to be recorded. The main requirement on bisimulations is the systems being compared need to match up exactly in the permanent actions but only those.
The resulting theory is fully abstract with respect to a natural contextual equivalence and, as we show in examples, provides an effective verification technique for comparing systems with communicating transactions.
Sponsor
Grant Number
Science Foundation Ireland (SFI)
SFI 06 IN.1 1898
Other
Microsoft Research (MRL 2011-039)
Author's Homepage:
http://people.tcd.ie/vkoutavhttp://people.tcd.ie/mcbhenne
Sponsor:
Science Foundation Ireland (SFI)Other
Other Titles:
Lecture Notes in Computer ScienceFoundations of Software Science and Computation Structures
Publisher:
Springer Berlin HeidelbergType of material:
Conference PaperCollections
Series/Report no:
Lecture Notes in Computer Science;8412Availability:
Full text availableMetadata
Show full item recordLicences: