cJoin: Join with communicating transactions

ROBERTO BRUNI; HERNÁN MELGRATTI; UGO MONTANARI

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE

CAMBRIDGE UNIV PRESS

Año: 2011

0960-1295

This paper proposes a formal approach to the design and programming of Long RunningTransactions (lrt). We exploit techniques from process calculi to de ne cJoin, which isan extension of the Join calculus with few well-disciplined primitives for lrt.Transactions in cJoin are intended to describe the transactional interaction of severalpartners, under the assumption that any partner executing a transaction maycommunicate only with other transactional partners. In such case, the transactions runby any party are bound to achieve the same outcome (i.e., all succeed or all fail). Hence,a distinguishing feature of cJoin, called dynamic joinability, is that ongoing transactionscan be merged to complete their tasks and when this happens either all succeed or allabort. Additionally, cJoin is based on compensations, i.e., partial executions oftransactions are recovered by executing user-de ned programs instead of providingautomatic roll-back. The expressiveness and generality of cJoin is demonstrated by manyexamples addressing common programming patterns. The mathematical foundation isaccompanied by a prototype language implementation, which is an extension of theJoCaml compiler.