SHF:Small: Enriching Session Types for Practical Concurrent Programming

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

Concurrent programming is becoming increasingly prevalent because of the distributed nature of many applications and the prospect of performance gains. However, concurrent programming is also notoriously error-prone because of the presence of data races and deadlocks. A promising approach to concurrent programing is message-passing concurrency, due to its higher-level of abstraction. Message-passing concurrency has been adopted by various practical programming languages, such as Erlang, Go, and Rust. Servo, for example, is an experimental browser engine developed in Rust that exploits message-passing concurrency for tasks, such as DOM traversal, layout painting, and JavaScript execution. This research project studies the application of session types to practical message-passing concurrency, while addressing the pitfalls of data races and deadlocks. Session types allow the expression and compile-time checking of the protocols of message exchange. The project's intellectual merits are to lift the expressiveness of session types to accommodate today's concurrent communication patterns, while remaining truthful to their logical foundation. The project's broader significance and importance are its provision of both a foundational and practical view on concurrent programming, the development of curricular material at the sophomore-level, and a session type extension for Rust. The logical foundation of this research project is the recently discovered Curry-Howard isomorphism between intuitionistic linear logic and session types, which relates linear propositions to session types, sequent calculus proofs to concurrent processes, and cut reduction to message-passing communication. Existing work building on this foundation provides strong guarantees, but also narrows the applicability of session types. The aim of this research is two-fold: (i) to increase the applicability of session types, while keeping their logical foundation intact, and (ii) to demonstrate practicality of the resulting techniques to real-world software development. For (ii), the project explores the application of the techniques resulting from (i) to the Servo code base. For (i), the project first explores the introduction of shared channels to support programs that demand sharing by the nature of circumstances or for performance considerations. Key concerns in this exploration are the prevention of data races along shared channels to guarantee session fidelity and the assurance of a form of global progress. In its simplest form, global progress will lack deadlock freedom, a property holding in the purely linear setting. In a second phase, a logical interpretation of deadlock prevention is derived. In a third phase, the project explores the enrichment of session types with dependent typing for the expression and verification of properties that are not primarily protocol-related. In all cases, proofs of soundness as well as a prototype of a session-typed concurrent programming language accommodating the developed techniques are given.