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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

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

  • Christopher A. Esterhuyse,
  • Benjamin Lion,
  • Hans-Dieter A. Hiep,
  • Farhad Arbab

摘要

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.