IPSJ-PRO関係各位:
名古屋大学の結縁です.
下記,吉田展子さん(オックスフォード)の講演会を実施します.
よろしければご参加くだされば幸いです.
============================================================
タイトル:Deadlock-free asynchronous message reordering in Rust with
multiparty session types
講演者:Nobuko Yoshida (Joint work with Zack Cutner and Martin Vassor)
University of Oxford
場所:名古屋大学IB電子情報館中棟IB011 (名古屋地下鉄名城線名古屋大学駅出口3すぐ)
日時:2023年7月27日(木)13:30-14:30
概要:
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.
--
Shoji Yuen
Graduate School of Informatics,
Nagoya University, Japan
+81-52-789-3649