π-calculus, Session Types research at Imperial College
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.
@inproceedings{CY2021, author = {Zak Cutner and Nobuko Yoshida}, title = {{Safe Session-Based Asynchronous Coordination in Rust}}, booktitle = {23rd International Conference on Coordination Models and Languages}, series = {LNCS}, volume = {12717}, pages = {89--80}, publisher = {Springer}, year = 2021 }
@inproceedings{CY2021, author = {Zak Cutner and Nobuko Yoshida}, title = {{Safe Session-Based Asynchronous Coordination in Rust}}, booktitle = {23rd International Conference on Coordination Models and Languages}, series = {LNCS}, volume = {12717}, pages = {89--80}, publisher = {Springer}, doi = "10.1007/978-3-030-78142-2 5", year = 2021 }