Logical Concurrency Control from Sequential Proofs

TL;DR

This paper proposes a systematic method to derive concurrency control mechanisms from sequential proofs, ensuring thread safety and linearizability of libraries in concurrent environments.

Contribution

It introduces a novel approach to automatically generate concurrency control from sequential correctness proofs, bridging sequential verification and concurrent safety.

Findings

Method successfully enforces isolation requirements

Ensures correctness and linearizability in concurrent executions

Applies to annotated sequential libraries

Abstract

We are interested in identifying and enforcing the isolation requirements of a concurrent program, i.e., concurrency control that ensures that the program meets its specification. The thesis of this paper is that this can be done systematically starting from a sequential proof, i.e., a proof of correctness of the program in the absence of concurrent interleavings. We illustrate our thesis by presenting a solution to the problem of making a sequential library thread-safe for concurrent clients. We consider a sequential library annotated with assertions along with a proof that these assertions hold in a sequential execution. We show how we can use the proof to derive concurrency control that ensures that any execution of the library methods, when invoked by concurrent clients, satisfies the same assertions. We also present an extension to guarantee that the library methods are linearizable or atomic.