For a transaction to be truly distributed, coordination between the component processes should not require the services of a single coordinating component. Rather, the coordination should be achieved locally by each component. This paper describes a calculus that can be used to ensure a globally consistent distributed state in unreliable environments.

This &tgr;-calculus is an extension of the &lgr;-calculus, and is based on the actor model of a distributed system. A transactor embodies a component’s behavior, specifically, its volatile state, its persistent state (which is the value at its last checkpoint operation), and a dependence set that models the transactors upon which it is dependent. Intuitively, this provides the transactor with the information that it will need to commit its effects. A transactor configuration is a pair, consisting of a multi-set of messages between transactors, and a nameserver map from names to transactors.

The calculus introduced by the authors serves to model the evolution of the configuration, and includes, importantly, consideration of lost messages. The authors demonstrate several significant results. In particular, they show that checkpointing is possible, assuming certain reasonable preconditions that are given in the paper (the reader is referred to another paper for the proof). It is also shown that global reasoning about state consistencies can be reduced to local reasoning about the possibility of message loss.

The paper is heavily weighted with the formal definitions for the &tgr;-calculus. However, the authors do an admirable job of presenting a conceptual view of the formalism. Readers interested in getting a handle on the complexities of consistency in distributed systems will find this a valuable contribution to the field.