Structured, safe and high-level communications programming with session types.
File(s)
Author(s)
Hu, Raymond
Type
Thesis
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 Issued
2011
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)