Elsevier

Science of Computer Programming

Volumes 115–116, 1 January–1 February 2016, Pages 199-224
Science of Computer Programming

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

https://doi.org/10.1016/j.scico.2015.09.001Get rights and content
Under an Elsevier user license
open archive

Highlights

  • We identify problems with (automaton-based) implementation approaches for connectors.

  • We define a new, relatively cheap product operator on port automata (PA).

  • We study when substituting the existing product with our new product is correct.

  • This yields a new implementation approach that avoids the stated problems.

  • We study the consequences of (non)associativity of PA product operators in practice.

Abstract

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.

Keywords

Reo
Port automata
Nonassociative product
Parallel composition
Connector implementation

Cited by (0)