Practical Session Types in Rust - Developing safe communication protocols for real-world applications
MSc Thesis Defence by Philip Munksgaard and Thomas Bracht Laumann Jespersen
We provide an implementation of session types in Rust and demonstrate how to incorporate session-typed channels in the Servo browser engine to guarantee protocol safety among concurrent, communicating threads.
Session types provide a protocol abstraction, expanding on traditional typed communication channels, to ensure communication takes place according to a specified protocol.
Existing browser engines are over a decade old and unfit for modern computer architectures, where parallelism and energy efficiency are prioritized over raw power. To take advantage of modern computing platforms Mozilla Research is developing Servo, a next-generation rendering engine. Servo is implemented in Rust, a new systems programming language that provides memory-safety and simple concurrency mechanisms, while retaining the speed of C or C++, all of which is essential to Servo.
We present and discuss the overall design of Servo and its internal communication patterns and demonstrate how the design can lead to discrepancies in communication expectations and potentially result in errors. The communication patterns employed in Servo are defined in an ad-hoc manner without any imposed overall structure. The ad-hoc communication patterns make it difficult to reason about communication flow and it is therefore hard to make assertions concerning safety and deadlock-freedom.
To address these issues, we design and implement a session type library in Rust called session-types, and discuss practical use cases through examples and demonstrate how they may be used in a large-scale application. Specifically, we replace parts of Servo's internal communication infrastructure with session-typed channels, and demonstrate that the use of session types allows us to provide compile-time guarantees, without incurring any significant run-time penalties. We also discuss challenges and drawbacks we discovered when using session-typed communication in a large real-world application. Our work is publicly available as a fork of the Servo project and we are currently seeking to land these changes in Servo.
While developing session-types, we have also developed several examples and examined different use cases for session-types. Among these are a solution to the Santa Claus problem first described in Trono94, an implementation of the recursive arithmetic server described in Gay99, as well as many others. Along with our continual examination of the communication patterns in Servo, these examples and case studies have guided us towards a practical and usable library design that enforces a strict communication discipline, while still allowing many useful communication patterns.
We draw inspiration from implementations of session types in other languages, while taking advantage of some of the unique features of Rust, to provide a practical, usable library that provides static guarantees about communication correctness. Our results show how session-typed communication, while requiring more careful implementation by the user, helps to enforce sound communication patterns that are less error-prone, a property of particular importance to large-scale, massively concurrent applications. The implementation also serves to demonstrate how a library for session-typed channels can be directly implemented in a polymorphic language that supports affine types, without having to worry about aliasing.
Finally, we consider the limitations of our session type design, which relies on the affine types of Rust. In an attempt to address the biggest limitation - channel end-points may be voluntarily or involuntarily dropped at any time - we implement a compiler plugin for Rust called humpty_dumpty, which attempts to enable the user to track linearity of specially annotated types.
Our contributions are: a library implementation of session types that relies on affine types, the humpty_dumpty plugin for the Rust compiler, which enables the user to track linear types, a fork of the Servo browser engine which incorporates session-typed channels as part of the internal communication schemes, contributions to both the Rust and Servo projects, and a paper submission currently in review about our work to the 11th ACM SIGPLAN Workshop on Generic Programming (WGP 2015).
External Examiner: Peter Sestoft, ITU
Supervisor: Ken Friis Larsen, DIKU
External Mentor: Lars Bergstrom, Mozilla Research