皆様、
明日の講演のリマインダーをお送りいたします。
なお、明日は早稲田キャンパス<->西早稲田キャンパス間のシャトルバスは運休ですので、ご注意下さい。
どうぞよろしくお願いいたします。
寺内
2023年7月11日(火) 15:12 Tachio Terauchi terauchi@waseda.jp:
皆様、
先ほどお送りした講演のご案内ですが、曜日が間違っておりました。正しくは、
日時： 8月1日(火) 14:00 ～
となります。(上田先生ご指摘ありがとうございます。)
どうぞよろしくお願いいたします。
寺内
On Tue, Jul 11, 2023 at 1:12 PM Tachio Terauchi terauchi@waseda.jp wrote:
皆さま、
8月1日に早稲田大学にて吉田展子先生によるご講演があります。 詳細は下記の通りです。 よろしければぜひご参加ください。
日時： 8月1日(水) 14:00 ～
場所： 早稲田大学 西早稲田キャンパス 63号館 5階506室
題目： Multiparty Session Types: Specification-Guided Parallel and Distributed Programming
講演者: Nobuko Yoshida (University of Oxford)
概要： I first give a gentle introduction of multiparty session types. Then I will talk about a joint work with Zak Cutner and Martin Vassor.
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.
寺内