Partner event: Huawei Coffee House Tech Talk Series - May About this event: When: Tuesday 24 May 2022 at 11am (UK time). Where (in person): Room G.03, Bayes Centre (47 Potterrow, Edinburgh EH8 9BT). Where (virtually): Zhumu link (https://meeting.zhumu.me/wc/0148144957/join?track_id=&jmf_code=&meeting_result=&tk=&cap=d7cec&prefer=0), everybody is welcome! You can access it from your own browser or Zoom app, without installing anything. Speakers: Nobuko Yoshida and Martin Vassor (Imperial College London) Title: Deadlock-free asynchronous message reordering in Rust with multiparty session types Abstract: Rust is a modern systems language focused 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 while preserving deadlock-freedom. For this, Rumpsteak incorporates two recent advanced session type theories: (1) k-multiparty compatibility (k-MC), 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 Rumsteak and show the new algorithm. We then talk about evaluations against other Rust implementations and asynchronous verification tools. We conclude the talk with a demo of Rumsteak.This work have been published in PPoPP '22: Proceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2022. Brief speakers bio: Nobuko Yoshida is Professor of Computing at Imperial College London. Last 10 years, her main research interests are theories and applications of protocols specifications and verifications. She introduced multiparty session types [ POPL’08, JACM ] which received Most Influential POPL Paper Award in 2018 (judged by its influence over the last decade). This work enlarged the community and widened the scope of applications of session types, e.g. runtime monitoring based on Scribble (co-developed with Red Hat) has been deployed to other projects such as cyberinfrastructure in the US Ocean Observatories Initiative (OOI); and widened the scope of her research areas. She was awarded CNRS and JSSP visiting fellowships and visiting professorships at Paris VI and Paris VII. She is an editor of ACM Transactions on Programming Languages and Systems, Mathematical Structures in Computer Science, Journal of Logical Algebraic Methods in Programming, and the chief editor of The Computer-aided Verification and Concurrency Column for EATCS Bulletin. Her current industry partners include: Cognizant, Estafet, J.P. Morgan, Red Hat, Weaveworks, November Group, ABB, EDF Energy, Xilinx, EPCC Ltd, Codeplay Software Ltd and Mexeler. Martin Vassor is a Research Associate in the Department of Computing at Imperial College London. Before coming to Imperial, he did his PhD in the SPADES team at Inria Grenoble, France. His research interests include: component based systems, concurrency theory, type systems and reversibility of concurrent systems. The Tech Talk lecture series is a part of the Huawei Coffee House offering. May 24 2022 00.00 - 23.59 Partner event: Huawei Coffee House Tech Talk Series - May Nobuko Yoshida and Martin Vassor (Imperial College London) will give a talk, in person and online, for the Coffee House Tech Talk Series. The Tech Talk lecture series is a part of the Huawei Coffee House offering
Partner event: Huawei Coffee House Tech Talk Series - May About this event: When: Tuesday 24 May 2022 at 11am (UK time). Where (in person): Room G.03, Bayes Centre (47 Potterrow, Edinburgh EH8 9BT). Where (virtually): Zhumu link (https://meeting.zhumu.me/wc/0148144957/join?track_id=&jmf_code=&meeting_result=&tk=&cap=d7cec&prefer=0), everybody is welcome! You can access it from your own browser or Zoom app, without installing anything. Speakers: Nobuko Yoshida and Martin Vassor (Imperial College London) Title: Deadlock-free asynchronous message reordering in Rust with multiparty session types Abstract: Rust is a modern systems language focused 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 while preserving deadlock-freedom. For this, Rumpsteak incorporates two recent advanced session type theories: (1) k-multiparty compatibility (k-MC), 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 Rumsteak and show the new algorithm. We then talk about evaluations against other Rust implementations and asynchronous verification tools. We conclude the talk with a demo of Rumsteak.This work have been published in PPoPP '22: Proceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2022. Brief speakers bio: Nobuko Yoshida is Professor of Computing at Imperial College London. Last 10 years, her main research interests are theories and applications of protocols specifications and verifications. She introduced multiparty session types [ POPL’08, JACM ] which received Most Influential POPL Paper Award in 2018 (judged by its influence over the last decade). This work enlarged the community and widened the scope of applications of session types, e.g. runtime monitoring based on Scribble (co-developed with Red Hat) has been deployed to other projects such as cyberinfrastructure in the US Ocean Observatories Initiative (OOI); and widened the scope of her research areas. She was awarded CNRS and JSSP visiting fellowships and visiting professorships at Paris VI and Paris VII. She is an editor of ACM Transactions on Programming Languages and Systems, Mathematical Structures in Computer Science, Journal of Logical Algebraic Methods in Programming, and the chief editor of The Computer-aided Verification and Concurrency Column for EATCS Bulletin. Her current industry partners include: Cognizant, Estafet, J.P. Morgan, Red Hat, Weaveworks, November Group, ABB, EDF Energy, Xilinx, EPCC Ltd, Codeplay Software Ltd and Mexeler. Martin Vassor is a Research Associate in the Department of Computing at Imperial College London. Before coming to Imperial, he did his PhD in the SPADES team at Inria Grenoble, France. His research interests include: component based systems, concurrency theory, type systems and reversibility of concurrent systems. The Tech Talk lecture series is a part of the Huawei Coffee House offering. May 24 2022 00.00 - 23.59 Partner event: Huawei Coffee House Tech Talk Series - May Nobuko Yoshida and Martin Vassor (Imperial College London) will give a talk, in person and online, for the Coffee House Tech Talk Series. The Tech Talk lecture series is a part of the Huawei Coffee House offering
May 24 2022 00.00 - 23.59 Partner event: Huawei Coffee House Tech Talk Series - May Nobuko Yoshida and Martin Vassor (Imperial College London) will give a talk, in person and online, for the Coffee House Tech Talk Series. The Tech Talk lecture series is a part of the Huawei Coffee House offering
