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 the ordinary Join calculus by exploiting a distributed two-phase commit protocol. 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.
Flat Committed Join in Join
BRUNI, ROBERTO;MONTANARI, UGO GIOVANNI ERASMO
2004-01-01
Abstract
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 the ordinary Join calculus by exploiting a distributed two-phase commit protocol. 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
