RT Conference Proceedings
T1 On algebraic abstractions for concurrent separation logics
A1 Farka, Frantisek
A1 Nanevski, Aleksandar
A1 Banerjee, Anindya
A1 Delbianco, Germán Andrés
A1 Fábregas Alfaro, Ignacio
AB Concurrent separation logic is distinguished by transfer of state ownership upon parallel composition and framing. The algebraic structure that underpins 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.
YR 2021
FD 2021-01-01
LK https://hdl.handle.net/20.500.14352/98240
UL https://hdl.handle.net/20.500.14352/98240
LA eng
NO Farka, F.; Nanevski, A.; Banerjee, A.; Delbianco, G. A.; Fábregas, I. On algebraic abstractions for concurrent separation logics. Proceedings of the ACM on Programming Languages 2021, 5(POPL), 1–32. doi:10.1145/3434286.
DS Docta Complutense
RD 25 abr 2025