Communicating Transactions

Abstract

We propose a novel language construct called communicating transactions, obtained by dropping the isolation requirement from classical transactions, which can be used to model automatic error re- covery in distributed systems. We extend CCS with this construct and give a simple semantics for the extended calculus, called TransCCS. We develop a behavioural theory which is sound and complete with respect to the may-testing preorder, and use it to prove interesting laws and reason compositionally about example systems. Finally, we prove that communicating transactions do not increase the observational power of processes; thus CCS equivalences are preserved in the extended language.