Semantics, Verification, and Compilation of Reo

Reo offers a fully-compositional model of concurrency that allows arbitrary user-defined primitives, arbitrary mix of synchrony and asynchrony, and relational constraints among inputs and outputs. These features make Reo highly adaptable and very expressive. They also make defining its formal semantics challenging, in spite of the relative simplicity and elegance of the resulting formal models. In this talk we present an overview of some of the major classes of formal models that capture the semantics of Reo, and their utility in verification, model checking, analysis, and executable code generation. Interestingly, interaction abstractions in Reo also leave more room for compilers to perform novel optimizations in mapping high-level protocol specifications into lower-level instructions that implement them. In on-going work we currently develop code generators that produce executable code whose performance and scalability on multi-core platforms compare favorably with those of hand-crafted, hand-optimized programs written in, e.g., Java or C.