arXiv subjects

Matthew Parkinson

Publications and source records attributed to Matthew Parkinson.

3 recordsLinked to original sources

arXiv2017

Proving Linearizability Using Partial Orders (Extended Version)

Linearizability is the commonly accepted notion of correctness for concurrent data structures. It requires that any execution of the data structure is justified by a linearization --- a linear order on operations satisfying the data structure's sequential specification. Proving linearizability is often challenging because an operation's position in the linearization order may depend on future operations. This makes it very difficult to incrementally construct the linearization in a proof. We propose a new proof method that can handle data structures with such future-dependent linearizations. Our key idea is to incrementally construct not a single linear order of operations, but a partial order that describes multiple linearizations satisfying the sequential specification. This allows decisions about the ordering of operations to be delayed, mirroring the behaviour of data structure implementations. We formalise our method as a program logic based on rely-guarantee reasoning, and demonstrate its effectiveness by verifying several challenging data structures: the Herlihy-Wing queue, the TS queue and the Optimistic set.

cs.PL↗

arXiv2016

New Lace and Arsenic: adventures in weak memory with a program logic

We describe a program logic for weak memory (also known as relaxed memory). The logic is based on Hoare logic within a thread, and rely/guarantee between threads. It is presented via examples, giving proofs of many weak-memory litmus tests. It extends to coherence but not yet to synchronised assignment (compare-and-swap, load-logical/store-conditional). It deals with conditionals and loops but not yet arrays or heap. The logic uses a version of Hoare logic within threads, and a version of rely/guarantee between threads, with five stability rules to handle various kinds of parallelism (external, internal, propagation-free and two kinds of in-flight parallelism). There are $\mathbb{B}$ and $\mathbb{U}$ modalities to regulate propagation, and temporal modalities $\mathsf{since}$, $\mathbb{S}\mathsf{ofar}$ and $\mathbb{O}\mathsf{uat}$ to deal with global coherence (SC per location). The logic is presented by example. Proofs and unproofs of about thirty weak-memory examples, including many litmus tests in various guises, are dealt with in detail. There is a proof of a version of the token ring. In version 2: The correspondence with Herding Cats has been clarified. The stability rules have been simplified: in particular the sat and x= x tests have been eliminated from external stability checks. The embedding is simplified and has a more transparent relation to the mechanisms of the logic. Definitions of U, Sofar and Ouat have been considerably altered. The description of modalities and the treatment of termination has been reworked. Many proofs are reconstructed. A comprehensive summary of the logic is an appendix.

cs.LO↗

arXiv2016

A Generic Logic for Proving Linearizability (Extended Version)

Linearizability is a commonly accepted notion of correctness for libraries of concurrent algorithms, and recent years have seen a number of proposals of program logics for proving it. Although these logics differ in technical details, they embody similar reasoning principles. To explicate these principles, we propose a logic for proving linearizability that is generic: it can be instantiated with different means of compositional reasoning about concurrency, such as separation logic or rely-guarantee. To this end, we generalise the Views framework for reasoning about concurrency to handle relations between programs, required for proving linearizability. We present sample instantiations of our generic logic and show that it is powerful enough to handle concurrent algorithms with challenging features, such as helping.

cs.PL↗