A Process Calculus of Atomic Commit

This article points out a strong connection between process calculi and atomic commit. Process calculus rendezvous is an abstract semantics for atomic commitment. An implementation of process-calculus rendezvous is an atomic commit protocol. Thus, the traditional correctness properties for atomic commit are entailed by a bisimulation proof of a calculus implementation. Actually, traditional rendezvous as found in the pi calculus corresponds to just a special case of atomic commit called a binary cohesion. If we take the general case of atomic commit, this induces a richer form of calculus rendezvous similar to the join calculus [Fournet, C. and G. Gonthier, The reflexive chemical abstract machine and the join-calculus, in: Proceedings of POPL '96, ACM (1996), pp. 372–385. URL http://research.microsoft.com/~fournet/papers/reflexive-cham-join-calculus.ps]. As an extended example of the analogy between calculus and atomic commit, we use the induced calculus to reformulate an earlier 2PCP correctness result by Berger and Honda [Berger, M. and K. Honda, The two-phase commitment protocol in an extended pi-calculus, in: EXPRESS '00, Electronic Notes in Theoretical Computer Science 39 (2000). URL ftp://ftp.dcs.qmw.ac.uk/lfp/martinb/express00.ps.gz].