Formal Foundations for Reowolf Multi-party Sessions via Synchronous Protocol Programming

The Reowolf project developed connectors as a replacement of two-party network sockets for multi-party communication in next-generation internet applications. Users control connectors via protocols in the bespoke protocol description language (PDL), which is based on synchronous languages such as Reo and Esterel. The novelty lies in the emphasis on dynamism: users refine protocols throughout their execution.
We formalise the semantics of PDL, distinguishing dual notions of protocol behaviour: accepted behaviour is highly (de)compositional and specifies what communication is allowed, while constructed behaviour arises from protocol execution and accounts for how execution steps interdepend and interleave via messages sent and received. Toward machine-checking the correctness of the connector runtime reference implementation, we specify the API and correctness criteria of PDL runtime systems.