The Two-Phase Commit Protocol in an Extended Pi-Calculus

We examine extensions to the pi-calculus
for representing basic elements of distributed systems. In spite of
its expressiveness for encoding various programming constructs, some
of the phenomena inherent in distributed systems are hard to model in
the pi-calculus. We consider message loss, sites, timers, site
failure and persistence as extensions to the calculus and examine
their descriptive power, taking the *Two Phase Commit Protocol*
(2PCP), a basic instance of an atomic commitment protocol, as a
testbed. Our extensions enable us to represent the 2PCP under various
failure assumptions, as well as to reason about the essential
properties of the protocol.

Extended abstract: ps.gz, pdf. Bibtex.

$Id: index.html,v 1.4 2006/02/09 19:15:17 martinb Exp $