Global Consensus through Local Synchronization (Technical Report)
Sung-Shik Jongmans, Farhad Arbab · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 2013
Coordination languages have emerged for the specification and implementation of interaction protocols among concurrent entities. Currently, we are developing a code generator for one such a language, based on the formalism of constraint automata (CA). As part of the compilation process, our tool computes the CA-specific synchronous product of a number of CA, each of which models a constituent of the protocol to generate code for. This ensures that implementations of those CA at run-time reach a consensus about their global behavior in every step. However, using the existing product operator on CA can be practically problematic. In this paper, we provide a solution by defining a new, local product operator on CA that avoids those problems. We then identify a sufficiently large class of CA for which using our new product instead of the existing one is semantics-preserving. Finally, we describe how to apply this result to code generation and also sketch how to use the same theory for projecting choreographies.