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. 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.
@InProceedings{bocwis04_acommit_rendezvous,
author = "Laura Bocchi and Lucian Wischik",
title = "A Process Calculus of Atomic Commit",
booktitle = "WS-FM 2004",
year = 2004,
series = "Electronic Notes in Theoretical Computer Science",
publisher = "Elsevier Science Publishers",
volume = ???,
url = "http:// www.wischik.com/ lu/ research/ analogy.html",
}