(link to the article.)

This is joint work with Christopher Esterhuyse, Hans-Dieter Hiep, and Farhad Arbab.

Abstract

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.

References

[1]: Christopher A. Esterhuyse, Benjamin Lion, Hans-Dieter A. Hiep, and Farhad Arbab, Formal Foundations for Reowolf: Multi-Party Sessions via Synchronous Protocol Programming https://ir.cwi.nl/pub/35250/35250.pdf.

[2]: Christopher Esterhuyse, Benjamin Lion, Hans-Dieter Hiep, Rocq implementation of the theory presented in the paper. https://zenodo.org/records/15247834.