[logic-ml] Talk by Nobuko Yoshida (July 19th, Wednesday, 11:00-)

[Atsushi Igarashi]

みなさま，    京都大学の五十嵐です．

以下の通り，来週水曜日に京都大学にて吉田展子さん(Oxford)によるご講演を
予定しております．是非ご参加ください．
--
五十嵐 淳 (IGARASHI Atsushi)
E-mail: igarashi at kuis.kyoto-u.ac.jp
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.