Transactions in RCCS

We propose a formalisation of the notion of transaction, using a variant of CCS, RCCS, that distinguishes reversible and irreversible actions, and incorporates a distributed backtrack mechanism. Any weakly correct implementation of a given transaction in CCS, once embedded in RCCS, automatically obtains a correct one. We show examples where this method allows for a more concise implementation and a simpler proof of correctness.

• Type: Conference
• Year: 2005
• Where: CONCUR
• Authors: Vincent Danos, Jean Krivine
• Keywords: CONCUR 2005, Distributed Backtrack Mechanism, Irreversible Actions, Weakly Correct Implementation