A Process Calculus of Atomic Commit

详细信息    查看全文

• 作者：Laura Bocchi ; Lucian Wischik
• 关键词：synchronous rendezvous ; pi calculus bisimulation ; atomic commit protocol ; 2PCP
• 刊名：Electronic Notes in Theoretical Computer Science
• 出版年：2004
• 出版时间：10 December 2004
• 年：2004
• 卷：105
• 期：Complete
• 页码：119-132
• 全文大小：297 K

文摘

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].