On asynchronous eventful session semantics
File(s)on-asynchronous-eventful-session-semantics.pdf (410.11 KB)
Accepted version
Author(s)
Kouzapas, D
Yoshida, N
Hu, R
Honda, K
Type
Journal Article
Abstract
© Cambridge University Press 2014. 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 or asynchronous bisimulation, capturing the semantic nature of eventful session-based processes. The bisimilarity coincides with reduction-closed barbed congruence. We demonstrate the features and benefits of ESP and the behavioural theory through two key use cases. 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.
Date Issued
2014-11-10
Date Acceptance
2014-01-23
Citation
Mathematical Structures in Computer Science, 2014, 29 (5)
ISSN
0960-1295
Publisher
Cambridge University Press
Journal / Book Title
Mathematical Structures in Computer Science
Volume
29
Issue
5
Copyright Statement
© Cambridge University Press 2014. The final publication is available via Cambridge Journals Online at http://dx.doi.org/10.1017/S096012951400019X
Description
AAM can be deposited in Spiral as 6 month embargo has already expired