Flat Committed Join in Join
Roberto L. Bruni, Hernán Melgratti, Ugo Montanari · Electronic Notes in Theoretical Computer Science · 2004
Committed Join (cJoin) is an extension of Join with high-level primitives for programming dynamic nested negotiations with compensations. In this paper we show that flat cJoin processes (i.e. processes without sub-negotiations) can be encoded in ordinary Join calculus by exploiting a distributed two-phase commit protocol (D2PC). In particular, we first define a type system that singles out flat processes and prove subject reduction for it. Then, we show that all flat cJoin processes can be written in an equivalent canonical form, where a few elementary definition patterns are used. Finally, we show that canonical flat processes can be implemented in Join. It is worth noting that negotiation primitives are encoded as fully distributed agreements between all participants, thus avoiding a centralized coordinator. 1