Global consensus through local synchronization: A formal basis for partially-distributed coordination

Sung-Shik Jongmans*, Farhad Arbab

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

4 Citations (Web of Science)


A promising new application domain for coordination languages is expressing interaction protocols among threads/processes in multicore programs: coordination languages typically provide high-level constructs and abstractions that more easily compose into correct (with respect to a programmer's intentions) protocol specifications than do low-level synchronization constructs (e.g., locks, semaphores, etc.) provided by conventional languages. However, a crucial step toward adoption of coordination languages for multicore programming is the development of compiler technology: programmers must have tools to automatically generate efficient code for high-level protocol specifications.

In ongoing work, we are developing compilers for a coordination language, Reo, based on that language's automata semantics. As part of the compilation process, our tool computes the product of a number of automata, each of which models a constituent of the protocol to generate code for. This approach ensures that implementations of those automata at run-time reach a consensus about their global behavior in every step. However, this approach has two problems: state space explosion at compile-time and oversequentialization at run-time. In this paper, we provide a solution by defining a new, local product operator on those automata that avoids these problems. We then identify a sufficiently large class of automata for which using our new product instead of the existing one is semantics-preserving.
Original languageEnglish
Pages (from-to)199-224
Number of pages26
JournalScience of computer programming
Publication statusPublished - Jan 2016
Externally publishedYes


Dive into the research topics of 'Global consensus through local synchronization: A formal basis for partially-distributed coordination'. Together they form a unique fingerprint.

Cite this