We introduce transactors, a fault-tolerant programming model for composing loosely-coupled distributed components running in an unreliable environment such as the internet into systems that reliably maintain globally consistent distributed state. The transactor model incorporates certain elements of traditional transaction processing, but allows these elements to be composed in different ways without the need for central coordination, thus facilitating the study of distributed fault-tolerance from a semantic point of view. We formalize our approach via the -calculus, an extended lambdacalculus based on the actor model, and illustrate its usage through a number of examples. The -calculus incorporates constructs which distributed processes can use to create globally-consistent checkpoints. We provide an operational semantics for the -calculus, and formalize the following safety and liveness properties: first, we show that globally-consistent checkpoints have equivalent execution traces ...
John Field, Carlos A. Varela