Deshmukh, Jyotirmoy and Ramalingam, G. and Ranganath, Venkatesh-Prasad and Vaswani, Kapil - Logical Concurrency Control from Sequential Proofs

lmcs:986 - Logical Methods in Computer Science, September 2, 2011, Volume 7, Issue 3
Logical Concurrency Control from Sequential Proofs

Authors: Deshmukh, Jyotirmoy and Ramalingam, G. and Ranganath, Venkatesh-Prasad and Vaswani, Kapil

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.


Source : oai:arXiv.org:1107.4422
DOI : 10.2168/LMCS-7(3:10)2011
Volume: Volume 7, Issue 3
Published on: September 2, 2011
Submitted on: June 25, 2015
Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,Computer Science - Software Engineering,D.1.3, D.2.4, F.3.1


Share

Browsing statistics

This page has been seen 29 times.
This article's PDF has been downloaded 4 times.