MobilityReadingGroup

On Asynchronous Eventful Session Semantics

Dimitrios KOUZAPAS, Nobuko YOSHIDA, Raymond HU, Kohei HONDA

Event-driven programming is one of the major paradigms in concurrent and communication-based programming, where events are typically detected as the arrival of messages on asynchronous channels. Unfortunately, the flexibility and performance of traditional event-driven programming come at the cost of more complex programs: low-level APIs and the obfuscation of event-driven control flow make programs difficult to read, write and verify.

This paper introduces a π-calculus with session types that models event-driven session programming (called ESP) and studies its behavioural theory. The main characteristics of the ESP model are asynchronous, order-preserving message passing, non-blocking detection of event/message arrivals, and dynamic inspection of session types. Session types offer formal safety guarantees, such as communication and event-handling safety, and programmatic benefits that overcome problems with existing event-driven programming languages and techniques. The new typed bisimulation theory developed for the ESP model is distinct from standard synchronous asynchronous bisimulation, capturing the semantic nature of eventful session-based processes.bisimilarity coincides with reduction-closed barbed congruence.

We demonstrate the features and benefits of event-driven session programming and the behavioural theory through two key usecases. First, we examine an encoding and the semantic behaviour of the event selector, a central component of general event-driven systems, providing core results for verifying type-safe event-driven applications. Second, we examine the Lauer-Needham duality, building on the selector encoding and bisimulation theory to prove that a systematic transformation from multithreaded to event-driven session processes is type- and semantics-preserving.

@article{KYHH2015,
  author = {Dimitrios Kouzapas and Nobuko Yoshida and Raymond Hu and Kohei Honda},
  title = {{On Asynchronous Eventful Session Semantics}},
  journal = {MSCS},
  volume = {29},
  issue = {5},
  pages = {1--62},
  publisher = {Cambridge University Press},
  year = 2015
}

@article{KYHH2015,
  author = {Dimitrios Kouzapas and Nobuko Yoshida and Raymond Hu and Kohei Honda},
  title = {{On Asynchronous Eventful Session Semantics}},
  journal = {Mathematical Structures in Computer Science},
  volume = {29},
  issue = {5},
  pages = {1--62},
  publisher = {Cambridge University Press},
  doi = "10.1017/S096012951400019X",
  year = 2015
}