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

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.

• View at Publisher

Full Text ( Final Version , 817kb )