Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Fri 22 Jan 2021 16:05 - 16:15 at POPL-B - Concurrency (Message Passing)

Session subtyping is a cornerstone of refinement of communicating processes: a process implementing a session type (i.e., a communication protocol) T can be safely used whenever a process implementing one of its supertypes T′ is expected, in any context, without introducing deadlocks nor other communication errors. As a consequence, whenever T ≤ T′ holds, it is safe to replace an implementation of T′ with an implementation of the subtype T, which may allow for more optimised communication patterns.

This paper presents the first formalisation of the precise subtyping relation for asynchronous multiparty sessions. We show that our subtyping relation is sound (i.e., guarantees safe process replacement, as outlined above) and also complete: any extension of the relation is unsound. To achieve our results, we develop a novel session decomposition technique, from full session types (including internal/external choices) into single input/output session trees (without choices.)

Previous work studies precise subtyping for binary sessions (with just two participants), or multiparty sessions (with any number of participants) and synchronous interaction. Here, we cover multiparty sessions with asynchronous interaction, where messages are transmitted via FIFO queues (as in the TCP/IP protocol), and prove that our subtyping is both operationally and denotationally precise. In the asynchronous multiparty setting, finding the precise subtyping relation is a highly complex task: this is because, under some conditions, participants can permute the order of their inputs and outputs, by sending some messages earlier or receiving some later, without causing errors; the precise subtyping relation must capture all such valid permutations — and consequently, its formalisation, reasoning and proofs become challenging. Our session decomposition technique overcomes this complexity, expressing the subtyping relation as a composition of refinement relations between single input/output trees, and providing a simple reasoning principle for asynchronous message optimisations.

Fri 22 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:45 - 16:45
Concurrency (Message Passing)POPL at POPL-B
15:45
10m
Talk
On Algebraic Abstractions for Concurrent Separation Logics
POPL
František FarkaIMDEA Software Institute, Spain, Aleksandar NanevskiIMDEA Software Institute, Anindya BanerjeeIMDEA Software Institute, Germán Andrés DelbiancoNomadic Labs, Ignacio FábregasUniversidad Complutense de Madrid
Link to publication DOI
15:55
10m
Talk
Transfinite Step-Indexing for Termination
POPL
Simon SpiesMPI-SWS and University of Cambridge, Neel KrishnaswamiComputer Laboratory, University of Cambridge, Derek DreyerMPI-SWS
Link to publication DOI
16:05
10m
Talk
Precise Subtyping for Asynchronous Multiparty Sessions
POPL
Silvia GhilezanUniversity of Novi Sad, Mathematical Institute SASA, Jovanka PantovićUniversity of Novi Sad, Ivan ProkićUniversity of Novi Sad, Alceste ScalasTechnical University of Denmark, Nobuko YoshidaImperial College London
Link to publication DOI Media Attached
16:15
10m
Talk
A Separation Logic for Effect Handlers
POPL
Link to publication DOI
16:25
10m
Talk
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
POPL
Léon GondelmanAarhus University, Simon Oddershede GregersenAarhus University, Abel NietoAarhus University, Amin TimanyAarhus University, Lars BirkedalAarhus University
Link to publication DOI
16:35
10m
Talk
PerSeVerE: Persistency Semantics for Verification under Ext4
POPL
Michalis KokologiannakisMPI-SWS, Germany, Ilya KaysinNational Research University Higher School of Economics, JetBrains Research, Azalea RaadImperial College London, Viktor VafeiadisMPI-SWS
Link to publication DOI