みなさま， 京都大学の五十嵐です．
以下の通り，来週水曜日に京都大学にて吉田展子さん(Oxford)によるご講演を 予定しております．是非ご参加ください． -- 五十嵐 淳 (IGARASHI Atsushi) E-mail: [email protected] url: http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/
========================= Time: 11:00-12:00, July 19th, Wednesday, 2023 Place: Seminar Room #2 (Room 131), Research Building #7, Main Campus, Kyoto University 京都大学 総合研究７号館 1階セミナー室２(131号室)
Title: Deadlock-free asynchronous message reordering in Rust with multiparty session types Speaker: Nobuko Yoshida (Joint work with Zack Cutner and Martin Vassor), University of Oxford
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.