MobilityReadingGroup

Rust is a modern systems language focussed on performance and reliability. Complementing Rust’s promise to provide ‘fearless concurrency,’ developers frequently exploit asynchronous message passing. Unfortunately, sending and receiving messages in an arbitrary order to maximise computation-communication overlap (a popular optimisation in message-passing applications) opens up a Pandora’s box of subtle concurrency bugs. To guarantee deadlock-freedom by construction, we present Rumpsteak: a new Rust framework based on multiparty session types. Previous session type implementations in Rust are either built upon synchronous and blocking communication and/or are limited to two-party interactions. Crucially, none support the arbitrary ordering of messages for efficiency. Rumpsteak instead targets asynchronous async/await code. Its unique ability is allowing developers to arbitrarily order send/receive messages whilst preserving deadlock-freedom. For this, Rumpsteak incorporates two recent advanced session type theories: (1) k-multiparty compatibility, which globally verifies the safety of a set of participants, and (2) asynchronous multiparty session subtyping, which locally verifies optimisations in the context of a single participant. Specifically, we propose a novel algorithm for asynchronous subtyping that is both sound and decidable. We first talk about Rumpsteak and show the new algorithm. We then talk about our evaluation against other Rust implementations and asynchronous verification tools. We conclude the talk with a demonstration of Rumpsteak. This work has been published in PPoPP ‘22: Proceedings of the 17th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2022.

Rust is a popular systems language focused on performance and reliability, with an emphasis on providing “fearless concurrency”. Message passing has become a widely-used pattern by Rust developers although the potential for communication errors leaves developing safe and concurrent applications an unsolved challenge. In this ongoing work, we use multiparty session types to provide safety guarantees such as deadlock-freedom by coordinating message-passing processes. In contrast to previous contributions, our implementation targets asynchronous applications using async/await code in Rust. Specifically, we incorporate asynchronous subtyping theory, which allows program optimisation through reordering input and output actions. We evaluate our ideas by developing several representative use cases from the literature and by taking microbenchmarks. We discuss our plans to support full API generation integrating asynchronous optimisations.

A decentralized application is constituted from independently-constructed software agents that represent autonomous principals. An outstanding challenge in distributed systems is how to coordinate the agents so that they can realize application meaning (the computations envisaged by the users of the application) but without relying on ordering mechanisms fixed in the application’s infrastructure. Forget causal delivery, even TCP is out! He will introduce Mandrake, a programming model for decentralized applications that tackles this challenge. Specifically, He will introduce the idea of specifying an application as an information protocol and then show how to construct protocol-compliant agents that communicate via UDP and can deal with transient failures that manifest as message loss. He will discuss Mandrake in the context of important systems ideas such as the end-to-end argument and why it achieves some of the goals of the founders of networked computing.

Multiparty sessions with asynchronous communications and global types play an important role for the modelling of interaction protocols in distributed systems. In designing such calculi the aim is to enforce, by typing, good properties for all participants, maximising, at the same time, the behaviours accepted. The global types presented in this paper improve the state-of-the-art by extending the set of typeable asynchronous sessions and preserving decidability of type checking together with the key properties of Subject Reduction, Session Fidelity and Progress

Modern web programming involves coordinating interactions between browser clients and a server. Typically, the interactions in web-based distributed systems are informally described, making it hard to ensure correctness, especially communication safety, i.e. all endpoints progress without type errors or deadlocks, conforming to a specified protocol.

We present STScript, a toolchain that generates TypeScript APIs for communication-safe web development over WebSockets, and RouST, a new session type theory that supports multiparty communications with routing mechanisms. STScript provides developers with TypeScript APIs generated from a communication protocol specification based on RouST. The generated APIs build upon TypeScript concurrency practices, complement the event-driven style of programming in full-stack web development, and are compatible with the Node.js runtime for server-side endpoints and the React.js framework for browser-side endpoints.

RouST can express multiparty interactions routed via an intermediate participant. It supports peer-to-peer communication between browser-side endpoints by routing communication via the server in a way that avoids excessive serialisation. RouST guarantees communication safety for endpoint web applications written using STScript APIs.

We evaluate the expressiveness of STScript for modern web programming using several production-ready case studies deployed as web applications.

Automata models are well-established in many areas of com-puter science and are supported by a wealth of theoretical results including a wide range of algorithms and techniques to specify and analyse systems. We introduce choreography automatafor the choreographic modelling of communicating systems. The projection of a choreography automaton yields a system of communicating finite-state machines. We consider both the standard asynchronous semantics of communicating systems and a synchronous variant of it. For both, the projections of well-formed automata are proved to be live as well as lock- and deadlock-free.

Go is a statically-typed language for building software in production environments. Its main goal is to provide a reliable and efficient way for developers to write communicating programs. Unfortunately recent work reveals that there are (surprisingly) many concurrent bugs in Go programs, more than half of which are caused by message-passing. A promising approach is the use of session types, a typing discipline that guarantees the absence of deadlocks and communication errors. Yet previous session type-based frameworks do not support dynamic unbounded participants, and cannot express many common Go programming patterns.

In this talk, I present GoScr (Go-Scribble), a toolchain for generating callback-style Go implementations from protocol specifications with unbounded, dynamic participants. GoScr guarantees, by construction, that the different participants will only perform I/O actions that comply with a given protocol specification, and that protocols are deadlock-free and live. We evaluate our toolchain by (1) implementing representative parallel and concurrent algorithms from existing benchmarks, textbooks and literature; (2) showing that GoScr does not introduce significant overheads compared to a naive implementation, for computationally expensive benchmarks; and (3) building three realistic protocols (dynamic task delegation, recursive Domain Name System, and a noughts and crosses game with Min-Max strategy) in GoScr that could not be represented with previous theories of session types.

In this talk, I will survey our POPL 2019 paper introducing a type system for the π-calculus which guarantees that typable processes are well-behaved, in the sense that they never produce a run-time error and, even if they may diverge, there is always achance for them to “finish their work”, i.e., to reduce to an idle process. The type system is based on non-idempotent intersections, and is thus very powerful as for the class of processes it can capture. Indeed, despite the fact that the underlying property is Pi^0_2-complete, there is a way of showing that the system is complete, i.e., that any well-behaved process is typable, although for obvious reasons infinitely many derivations need to be considered.

Real world effects are pervasive, e.g.: concurrency, distribution, exceptions, I/O, and nondeterminism. Effect handlers are a general programming feature that can be used for modularly implementing all of these effects and more. They were introduced by theoretical computer scientists studying the theory of algebraic effects, but now show promise as a practical programming tool. Interest in effect handlers in industry is growing. For instance, Facebook’s React Fiber, the core of the popular React UI library is directly inspired by effect handlers, and Uber’s Pyro tool for probabilistic programming and GitHub’s Semantic library for parsing, analysing, and comparing source code (currently used for code navigation on over 4.5 million public Python repositories) both make essential use of effect handlers.

I will give an overview of effect handler oriented programming by way of a collection of examples and an operational semantics. In particular I will focus on concurrency examples. I will also briefly outline some of my contributions to the theory and practice of effect handler oriented programming as well as discussing challenges and future opportunities.

I first give an overview of recent researches of my group.

Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks.

In this work we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioural types, where the types are model checked for liveness and safety.

We present an end-to-end solution for verified distributed programming. Building upon the foundation of Multiparty Session Types with refinements, we propose a programming language with refinement types and discuss an API generation strategy to allow type checking to statically validate the refinements from the specification of the protocol to the implementation of each of its clients.

According to the folklore, Bitcoin would resist attacks unless the adversaries control the majority of the total computing power of the Bitcoin network. Unfortunately, many scientific works showed that reality is different. This presentation will address Bitcoin security from a theoretical and practical perspective. Firstly, by diving into the details of the protocol, we will prove some fundamental proprieties and the adversarial bound required for its security. Next, we will see some attacks that can exploit Bitcoin weaknesses.

Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks.

In this work, we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioral types, where the types are model checked for liveness and safety.

In this talk I will present a programming framework for static specification and safe programming of message passing protocols where the number and kinds of participants are dynamically instantiated. Our framework is based on Multiparty Session Types (MPST), extended to support parameterised protocols with indexed roles - where the number of roles is known only at run time.

Our framework statically infers the different kinds of participants induced by a protocol definition as role variants, and produces decoupled endpoint projections of the protocol onto each participant. This enables communication-safe, deadlock-free programming of the parameterised endpoint in distributed settings: each endpoint can be implemented (and verified) separately by different programmers/technique/languages.

We implemented our framework with Scribble-Go, a tool chain for programming such role-parametric protocols in the mainstream programming language of Go. We generate API families of lightweight, protocol- and variant-specific type wrappers for I/O. The API ensures a well-typed Go endpoint program (by native Go type checking) will perform only the compliant I/O actions wrt to the source protocol. We leverage the abstractions of MPST to support the specification of Go applications involving multiple channels, possibly over mixed transport, and channel passing via a unified programming interface. We evaluate the applicability and runt-time performance of our generated API using microbenchmarks and real-world applications.

Concurrent and distributed programming is notoriously hard. Many languages and software toolkits address the challenge by offering high-level abstractions, such as message-passing processes and actors; they allow for intuitive reasoning, but do not formally ensure that a program implements a given specification.

I will talk about Effpi, a toolkit for strongly-typed concurrent programming in Dotty (a.k.a. Scala 3). Effpi allows to specify the intended behaviour of a message-passing application using types: i.e., if a program type-checks and compiles, then it will run and communicate as prescribed by its types.

The foundation of Effpi is a concurrent functional language with a novel blend of behavioural types (from the π-calculus theory), and a form of dependent types, extending to higher-order interaction (i.e., sending/receiving program thunks). This design has three main advantages. First, it allows to verify programs through a combination of type checking and model checking techniques. Second, it is directly implemented (via deep embedding) in Dotty, including a simplified API for strongly-typed actor-based programming. And third, its functional nature allows for an efficient runtime system, supporting highly concurrent programs with millions of interacting processes/actors.

Concurrent and distributed programming is notoriously hard. Many languages and software toolkits address the challenge by offering high-level abstractions, such as message-passing processes and actors; they allow for intuitive reasoning, but do not formally ensure that a program implements a given specification.

I will talk about Effpi, a toolkit for strongly-typed concurrent programming in Dotty (a.k.a. Scala 3). Effpi allows to specify the intended behaviour of a message-passing application using types: i.e., if a program type-checks and compiles, then it will run and communicate as prescribed by its types.

The foundation of Effpi is a concurrent functional language with a novel blend of behavioural types (from the π-calculus theory), and a form of dependent types, extending to higher-order interaction (i.e., sending/receiving program thunks). This design has three main advantages. First, it allows to verify programs through a combination of type checking and model checking techniques. Second, it is directly implemented (via deep embedding) in Dotty, including a simplified API for strongly-typed actor-based programming. And third, its functional nature allows for an efficient runtime system, supporting highly concurrent programs with millions of interacting processes/actors.

Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks. In this work we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioural types, where the types are model checked for liveness and safety.

This work exploits the logical foundation of session types to determine what kind of type discipline for the π-calculus can exactly capture, and is captured by, λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

This work exploits the logical foundation of session types to determine what kind of type discipline for the π-calculus can exactly capture, and is captured by, λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

We first give an overview of recent research developments of our mobility group at Imperial College London.

Session types is a typing discipline for concurrent and distributed processes that allows errors such as communication mismatches and deadlocks to be detected statically. Refinement types are types elaborated by logical constraints that allow richer and finer-grained specification of application properties, combining types with logical formulae that may refer to program values and can constrain types using arbitrary predicates. Type providers, developed in F#, are compile-time components for on-demand code generation. Their architecture relies on an open-compiler, where provider-authors implement a small interface that allows them to inject new names/types into the programming context as the program is written.

In this talk, we will present a library that integrates aspects from the above fields to realise practical applications of multiparty refinement session types (MPST) for any .Net language. Our library supports the specification and validation of distributed message passing protocols based on a formulation of asynchronous MPST enriched with interaction refinements: a collection of features related to the refinement of protocols, such as message-type refinements (value constraints) and value dependent control flow. The combination of these aspects—session types for structured interactions, constraint solving from refinement types, and protocol-specific code generation—enables the specification and implementation of enriched protocols in native F# (and any .Net-compiled language) without requiring language extensions or external pre-processing of user programs. A well-typed endpoint program using our library is guaranteed to perform only compliant session I/O actions w.r.t. to the refined protocol, up to premature termination. The safety guarantees are achieved by a combination of static type checking of the generated types for messages and I/O operations, correctness by construction from code generation, and automated inlining of assertions.

Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks.

In this work we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioural types, where the types are model checked for liveness and safety.

(joint work with Julien Lange, Bernardo Toninho and Nobuko Yoshida)

Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks.

In this work we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioural types, where the types are model checked for liveness and safety.

This is joint work with Julien Lange (Kent), Bernardo Toninho (Imperial) and Nicholas Ng (Imperial).