Hostname: page-component-586b7cd67f-t7czq Total loading time: 0 Render date: 2024-11-29T08:16:59.376Z Has data issue: false hasContentIssue false
  • English
  • Français

On asynchronous eventful session semantics

Published online by Cambridge University Press:  10 November 2014

DIMITRIOS KOUZAPAS ,
NOBUKO YOSHIDA ,
RAYMOND HU  and
KOHEI HONDA
DIMITRIOS KOUZAPAS
Affiliation:
Department of Computing, Imperial College London, South Kensington Campus, London SW7 2AZ, United Kingdom School of Computing Science, University of Glasgow, Sir Alwyn Williams Building, Lilybank Gardens, Glasgow G12 8QQ, Scotland Emails: [email protected], [email protected], [email protected]
NOBUKO YOSHIDA
Affiliation:
Department of Computing, Imperial College London, South Kensington Campus, London SW7 2AZ, United Kingdom
RAYMOND HU
Affiliation:
Department of Computing, Imperial College London, South Kensington Campus, London SW7 2AZ, United Kingdom
KOHEI HONDA
Affiliation:
School of Electronic Engineering and Computer Science, Queen Mary University of London, Mile End Road, London E1 4NS, United Kingdom
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 26 , Special Issue 2: Special Issue: Behavioural Types Part 1 , February 2016 , pp. 303 - 364
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abadi, M., Cardelli, L., Pierce, B. C. and Plotkin, G. D. (1991) Dynamic typing in a statically typed language. Transactions on Programming Languages and Systems 13 (2) 237–268.Google Scholar
Abadi, M., Cardelli, L., Pierce, B. C. and Rémy, D. (1995) Dynamic typing in polymorphic languages. Journal of Functional Programming 5 (1) 111–130.Google Scholar
Adya, A., Howell, J., Theimer, M., Bolosky, W. J. and Douceur, J. R. (2002) Cooperative task management without manual stack management or, event-driven programming is not the opposite of threaded programming. In: Proceedings of the 2002 Usenix ATC 289–302.Google Scholar
Banga, G., Druschel, P. and Mogul, J. C. (1998) Better operating system features for faster network servers. SIGMETRICS Performance Evaluation Review 26 (3) 23–30.Google Scholar
Beauxis, R., Palamidessi, C. and Valencia, F. D. (2008) On the asynchronous nature of the asynchronous pi-calculus. In: Concurrency, Graphs and Models. Springer Lecture Notes in Computer Science 5065 473–492.Google Scholar
Bettini, L. et al. (2008) Global progress in dynamically interleaved multiparty sessions. In: CONCUR. Springer Lecture Notes in Computer Science 5201 418–433.Google Scholar
Busi, N., Gorrieri, R. and Zavattaro, G. (2000) Comparing three semantics for linda-like languages. Theoretical Computer Science 240 (1) 49–90.CrossRefGoogle Scholar
Caires, L. and Pfenning, F. (2010) Session types as intuitionistic linear propositions. In: CONCUR. Springer Lecture Notes in Computer Science 6269 222–236.Google Scholar
Caires, L. and Vieira, H. T. (2010) Conversation types. Theoretical Computer Science 411 (51–52) 4399–4440.Google Scholar
Castagna, G. and Padovani, L. (2009) Contracts for mobile processes. In: CONCUR 2009. Lecture Notes in Computer Science 5710 211–228.Google Scholar
Castagna, G. et al. (2009) Foundations of session types. In: Principles and Practice of Declarative Programming'09, ACM 219–230.Google Scholar
Coppo, M., Dezani-Ciancaglini, M. and Yoshida, N. (2007) Asynchronous session types and progress for object-oriented languages. In: FMOODS'07. Lecture Notes in Computer Science 4468 1–31.Google Scholar
Gay, S. and Vasconcelos, V. T. (2010) Linear type theory for asynchronous session types. Journal of Functional Programming 20 (1) 19–50.Google Scholar
Hennessy, M. (2007) A Distributed Pi-Calculus, Cambridge University Press.Google Scholar
Honda, K. and Tokoro, M. (1991) An object calculus for asynchronous communication. In: ECOOP'91. Lecture Notes in Computer Science 512 133–147.Google Scholar
Honda, K., Vasconcelos, V. T. and Kubo, M. (1998) Language primitives and type disciplines for structured communication-based programming. In: ESOP'98. Springer Lecture Notes in Computer Science 1381 22–138.Google Scholar
Honda, K. and Yoshida, N. (1995) On reduction-based process semantics. Theoretical Computer Science 151 (2) 437–486.Google Scholar
Honda, K. and Yoshida, N. (2007) A uniform type structure for secure information flow. Transactions on Programming Languages and Systems 29 (6) 81–92.Google Scholar
Honda, K., Yoshida, N. and Carbone, M. (2008) Multiparty synchronous session types. In: Principles of programming languages'08, ACM 273–284.Google Scholar
Hu, R. (2011) SJ homepage. Available at http://www.doc.ic.ac.uk/~rhu/sessionj.html.Google Scholar
Hu, R., Kouzapas, D., Pernet, O., Yoshida, N. and Honda, K. (2010) Type-safe eventful sessions in Java. In: ECOOP. Springer-Verlag Lecture Notes in Computer Science 6183 329–353.Google Scholar
Hu, R., Yoshida, N. and Honda, K. (2008) Session-based distributed programming in Java. In: ECOOP'08. Springer Lecture Notes in Computer Science 5142 516–541.Google Scholar
Kouzapas, D. (2009) A Session Type Discipline for Event Driven Programming Models, Master's thesis, Imperial College London. Available at http://www.doc.ic.ac.uk/teaching/distinguished-projects/2010/d.kouzapas.pdf.Google Scholar
Kouzapas, D., Yoshida, N. and Honda, K. (2011) On asynchronous session semantics. In: FMOODS/FORTE. Lecture Notes in Computer Science 6722 228–243.Google Scholar
Krohn, M. (2004) Building secure high-performance web services with OKWS. In: ATEC'04, USENIX Association 15–15.Google Scholar
Krohn, M., Kohler, E. and Kaashoek, M. F. (2007) Events can make sense. In: Annual Technical Conference'07, USENIX Association 1–14.Google Scholar
Lauer, H. C. and Needham, R. M. (1979) On the duality of operating system structures. SIGOPS Operating Systems Review 13 (2) 3–19.Google Scholar
Lea, D. (2003) Scalable IO in Java. Available at http://gee.cs.oswego.edu/dl/cpjslides/nio.pdf.Google Scholar
Li, P. and Zdancewic, S. (2007) Combining events and threads for scalable network services implementation and evaluation of monadic, application-level concurrency primitives. SIGPLAN Not. 42 (6) 189–199.Google Scholar
Lowe, G. (2009) Extending CSP with tests for availability. In: Proceedings of Communicating Process Architectures (CPA 2009) 325–347.Google Scholar
Lowe, G. (2010) Models for CSP with availability information. In: Fröschle, S. B. and Valencia, F. D. (eds.) EXPRESS'10. Electronic Proceedings in Theoretical Computer Science 41 91–105.Google Scholar
Milner, R. (1980) A Calculus of Communicating Systems, Lecture Notes in Computer Science volume 92, Springer, Berlin.Google Scholar
Milner, R., Parrow, J. and Walker, D. (1992) A alculus of mobile processes, parts I and II. Information and Computer 100 (1) 1–40.Google Scholar
Mostrous, D. and Yoshida, N. (2009) Session-based communication optimisation for higher-order mobile processes. In: TLCA'09. Springer Lecture Notes in Computer Science 5608 203–218.Google Scholar
Pérez, J. A., Caires, L., Pfenning, F. and Toninho, B. (2012) Linear logical relations for session-based concurrency. In: ESOP. Springer Lecture Notes in Computer Science 7211 539–558.Google Scholar
Philippou, A. and Walker, D. (1997) On confluence in the pi-calculus. In: ICALP'97. Springer Lecture Notes in Computer Science 1256 314–324.Google Scholar
Pierce, B. and Sangiorgi, D. (1996) Typing and subtyping for mobile processes. Mathematical Structures in Computer Science 6 (5) 409–454.Google Scholar
Pierce, B. C. (2002) Types and Programming Languages, MIT Press.Google Scholar
SJ (2010) SJ homepage. Available at http://www.doc.ic.ac.uk/~rhu/sessionj.html.Google Scholar
Sun Microsystems Inc. (2011) New IO APIs. Available at http://java.sun.com/j2se/1.4.2/docs/guide/nio/index.html.Google Scholar
Takeuchi, K., Honda, K. and Kubo, M. (1994) An interaction-based language and its typing system. In: PARLE'94. Lecture Notes in Computer Science 817 398–413.Google Scholar
von Behren, R., Condit, J. and Brewer, E. (2003a) Why events are a bad idea (for high-concurrency servers) In: Proceedings of HOTOS'03, USENIX Association 4–4.Google Scholar
von Behren, R. et al. (2003b) Capriccio: Scalable threads for internet services. In: Proceedings of SOSP '03, ACM 268–281.Google Scholar
Welsh, M., Culler, D. E. and Brewer, E. A. (2001) SEDA: An architecture for well-conditioned, scalable internet services. In: Proceedings of SOSP'01, ACM Press 230–243.Google Scholar