Structured, safe and high-level communications programming with session types.
File(s)
Author(s)
Hu, Raymond
Type
Thesis or dissertation
Abstract
Communication is a fundamental element in computing systems. Unfortunately, language design and typing support for communications programming are considerably underdeveloped in contrast to that for sequential programming. Session types, a typing discipline for structured interaction between concurrent processes, offers a promising approach. To date, however, there has been no implementation of session types for general-purpose, distributed communications programming. This thesis investigates the design and implementation of a practical communications- oriented language with session types. SJ is an extension of Java that supports a wide range of features studied in session type theory as well as new features developed to meet the demands of real-world application implementation. First, we discuss the core design of SJ and the integration of session types into Java. The central idea is the notion of communication endpoints as session-typed objects. SJ follows Java through explicit declaration of session types as protocol specifications; implementations are statically type-checked against their specifications by the SJ compiler to ensure the key property of communication safety. SJ supports asynchronous, distributed message passing, session delegation, and session subtyping with type-safe failure handling. Second, we evaluate SJ programming through several applications from different communications-based domains, including Web services, parallel algorithms and an SMTP server. These applications motivate and demonstrate novel SJ features, such as event-driven session programming and multisession operations. Our experiences of SJ programming highlight the benefits of session types for structured, safe and high-level communications programming. Third, we discuss the SJ Runtime implementation, which provides a comprehensive, transport-independent platform for executing session programs. Key components include safe, distributed session delegation, and type-directed zero-copy messaging in shared memory sessions. Benchmark performance evaluation shows that session-typed communication can be realised with minimal overhead. Finally, we formalise the SJ features for event-driven session programming and prove communication safety.
Date Awarded
2011
Copyright Statement
Creative Commons Attribution NonCommercial NoDerivatives Licence
Description
Open access
Publisher Department
Computing
Publisher Institution
University of London - Imperial College London
Qualification Level
Doctoral
Qualification Name
Doctor of Philosophy (PhD)