-
On Algebraic Abstractions for Concurrent Separation Logics
Authors:
František Farka,
Aleksandar Nanevski,
Anindya Banerjee,
Germán Andrés Delbianco,
Ignacio Fábregas
Abstract:
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…
▽ More
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.
△ Less
Submitted 4 March, 2021; v1 submitted 23 October, 2020;
originally announced October 2020.
-
Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations
Authors:
Aleksandar Nanevski,
Anindya Banerjee,
Germán Andrés Delbianco,
Ignacio Fábregas
Abstract:
In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of resources---a form of state transition system---to describe the state-based program invariants that must be preserved, and to record the permissible atomic changes to program state. In this paper we introduce a novel notion of resource morphism, i.e. st…
▽ More
In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of resources---a form of state transition system---to describe the state-based program invariants that must be preserved, and to record the permissible atomic changes to program state. In this paper we introduce a novel notion of resource morphism, i.e. structure-preserving function on resources, and show how to effectively integrate it into separation logic, using an associated notion of morphism-specific simulation. We apply morphisms and simulations to programs verified under one resource, to compositionally adapt them to operate under another resource, thus facilitating proof reuse.
△ Less
Submitted 15 October, 2019; v1 submitted 15 April, 2019;
originally announced April 2019.
-
Subjective Simulation as a Notion of Morphism for Composing Concurrent Resources
Authors:
Aleksandar Nanevski,
Anindya Banerjee,
Germán Andrés Delbianco
Abstract:
Recent approaches to verifying programs in separation logics for concurrency have used state transition systems (STSs) to specify the atomic operations of programs. A key challenge in the setting has been to compose such STSs into larger ones, while enabling programs specified under one STS to be linked to a larger one, without reverification. This paper develops a notion of morphism between two S…
▽ More
Recent approaches to verifying programs in separation logics for concurrency have used state transition systems (STSs) to specify the atomic operations of programs. A key challenge in the setting has been to compose such STSs into larger ones, while enabling programs specified under one STS to be linked to a larger one, without reverification. This paper develops a notion of morphism between two STSs which permits such lifting. The morphisms are a constructive form of simulation between the STSs, and lead to a general and concise proof system. We illustrate the concept and its generality on several disparate examples, including staged construction of a readers/writers lock and its proof, and of proofs about quiescence when concurrent programs are executed without external interference.
△ Less
Submitted 22 September, 2017;
originally announced September 2017.
-
Concurrent Data Structures Linked in Time
Authors:
Germán Andrés Delbianco,
Ilya Sergey,
Aleksandar Nanevski,
Anindya Banerjee
Abstract:
Arguments about correctness of a concurrent data structure are typically carried out by using the notion of linearizability and specifying the linearization points of the data structure's procedures. Such arguments are often cumbersome as the linearization points' position in time can be dynamic (depend on the interference, run-time values and events from the past, or even future), non-local (appe…
▽ More
Arguments about correctness of a concurrent data structure are typically carried out by using the notion of linearizability and specifying the linearization points of the data structure's procedures. Such arguments are often cumbersome as the linearization points' position in time can be dynamic (depend on the interference, run-time values and events from the past, or even future), non-local (appear in procedures other than the one considered), and whose position in the execution trace may only be determined after the considered procedure has already terminated.
In this paper we propose a new method, based on a separation-style logic, for reasoning about concurrent objects with such linearization points. We embrace the dynamic nature of linearization points, and encode it as part of the data structure's auxiliary state, so that it can be dynamically modified in place by auxiliary code, as needed when some appropriate run-time event occurs. We name the idea linking-in-time, because it reduces temporal reasoning to spatial reasoning. For example, modifying a temporal position of a linearization point can be modeled similarly to a pointer update in separation logic. Furthermore, the auxiliary state provides a convenient way to concisely express the properties essential for reasoning about clients of such concurrent objects. We illustrate the method by verifying (mechanically in Coq) an intricate optimal snapshot algorithm due to Jayanti, as well as some clients.
△ Less
Submitted 18 January, 2017; v1 submitted 27 April, 2016;
originally announced April 2016.
-
Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects
Authors:
Ilya Sergey,
Aleksandar Nanevski,
Anindya Banerjee,
German Andres Delbianco
Abstract:
Designing scalable concurrent objects, which can be efficiently used on multicore processors, often requires one to abandon standard specification techniques, such as linearizability, in favor of more relaxed consistency requirements. However, the variety of alternative correctness conditions makes it difficult to choose which one to employ in a particular case, and to compose them when using obje…
▽ More
Designing scalable concurrent objects, which can be efficiently used on multicore processors, often requires one to abandon standard specification techniques, such as linearizability, in favor of more relaxed consistency requirements. However, the variety of alternative correctness conditions makes it difficult to choose which one to employ in a particular case, and to compose them when using objects whose behaviors are specified via different criteria. The lack of syntactic verification methods for most of these criteria poses challenges in their systematic adoption and application.
In this paper, we argue for using Hoare-style program logics as an alternative and uniform approach for specification and compositional formal verification of safety properties for concurrent objects and their client programs. Through a series of case studies, we demonstrate how an existing program logic for concurrency can be employed off-the-shelf to capture important state and history invariants, allowing one to explicitly quantify over interference of environment threads and provide intuitive and expressive Hoare-style specifications for several non-linearizable concurrent objects that were previously specified only via dedicated correctness criteria. We illustrate the adequacy of our specifications by verifying a number of concurrent client scenarios, that make use of the previously specified concurrent objects, capturing the essence of such correctness conditions as concurrency-aware linearizability, quiescent, and quantitative quiescent consistency. All examples described in this paper are verified mechanically in Coq.
△ Less
Submitted 21 July, 2016; v1 submitted 21 September, 2015;
originally announced September 2015.
