Transactors: A Programming Model for Maintaining Globally Consistent Distributed State in Unreliable Environments John Field Carlos A. Varela Distributed state Transactor Tau-calculus 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 tau-calculus, an extended lambdacalculus based on the actor model, and illustrate its usage through a number of examples. The tau-calculus incorporates constructs which distributed processes can use to create globally-consistent checkpoints. We provide an operational semantics for the tau-calculus, and formalize the following safety and liveness properties: first, we show that globally-consistent checkpoints have equivalent execution traces without any node failures or application-level failures, and second, we show that it is possible to reach globally-consistent checkpoints provided that there is some bounded failure-free interval during which checkpointing can occur. Department of Computer Science, Rensselaer Polytechnic Institute, Troy, NY cs-04-15
Transactors: A Programming Model for Maintaining Globally Consistent Distributed State in Unreliable Environments
John Field
Carlos A. Varela
Distributed state
Transactor
Tau-calculus
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 tau-calculus, an extended lambdacalculus based on the actor model, and illustrate its usage through a number of examples. The tau-calculus incorporates constructs which distributed processes can use to create globally-consistent checkpoints. We provide an operational semantics for the tau-calculus, and formalize the following safety and liveness properties: first, we show that globally-consistent checkpoints have equivalent execution traces without any node failures or application-level failures, and second, we show that it is possible to reach globally-consistent checkpoints provided that there is some bounded failure-free interval during which checkpointing can occur.
Department of Computer Science, Rensselaer Polytechnic Institute, Troy, NY
cs-04-15