Research Results
The researchers František Farka, Aleksandar Nanevski, Anindya Banerjee (from the IMDEA Software Institute), Germán Andrés Delbianco (Nomadic Labs), and Ignacio Fábregas (Universidad Complutense de Madrid) have recently published “On Algebraic Abstractions for Concurrent Separation Logics”, that has been accepted at POPL 2021.
Concurrent separation logic is a logic for verification of stateful programs. This logic is distinguished by transfer of state ownership upon parallel composition of threads. The semantics ownership transfer is given by the algebraic structure of partial commutative monoids(PCMs). Extant research considers ownership transfer primarily from the logical perspective while comparatively less attention is drawn to the symbolic manipulation on the level of specifications expressed in the assertion language.
This paper provides an algebraic formalization of assertion language for 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.That is, when verifying software, they can assert specifications in symbolic languages of standard mathematics; the only concession they are forced to is relaxation from total domains to partial ones.
Morphisms, that is structures preserving maps, are a standard concept in algebra and category theory. However, morphisms 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.
The presented work constitutes a novel approach to assertion language of separation logics as the algebra of PCMs, their morphisms and constructions has not been considered before in this context.
