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

Concurrent separation logic is distinguished by transfer of state ownership upon parallel composition and framing. The algebraic structure that underpins the ownership transfer is that of partial commutative monoids (PCMs). Extant research considers ownership transfer primarily from the logical perspective while comparatively less attention is drawn to the algebraic considerations.

This paper provides an algebraic formalization of ownership transfer in concurrent separation logic by means of structure-preserving partial functions (i.e., morphisms) between PCMs, and an associated notion of separating relations. Morphisms of structures are a standard concept in algebra and category theory, but haven’t seen ubiquitous use in separation logic before. Separating relations are binary relations that generalize disjointness and characterize the inputs on which morphisms preserve structure. The two abstractions facilitate verification by enabling concise ways of writing specs, by providing abstract views of threads’ states that are preserved under ownership transfer, and by enabling user-level construction of new PCMs out of existing ones.

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