A Formal Model for Compensable Transactions

Different from traditional transactions, a compensable transaction relies on compensations to amend partial execution whenever an error occurs. The compensation is preserved on successful completion of its forward transaction for possibly later use. In this paper, we pay attention to the compositional structure of compensable transactions. Except for sequential and parallel compositions, other useful compositional constructs, such as speculative choice, exception handling, alternative forwarding and programmable compensation, are also investigated. All these constructs are not only devised to describe distinct business flow but also used to enhance the capability for dealing with errors, t-calculus is such a transactional language that involves a variety of primitives for composing compensable transactions in a wise way. We present a clear operational semantics for this language and the corresponding concept of bisimulation is defined, which is used to derive equational laws for compensable transactions.