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

lmcs:986 - Logical Methods in Computer Science, September 2, 2011, Volume 7, Issue 3 - https://doi.org/10.2168/LMCS-7(3:10)2011
Logical Concurrency Control from Sequential ProofsArticle

Authors: Jyotirmoy Deshmukh ; G. Ramalingam ; Venkatesh-Prasad Ranganath ORCID; Kapil Vaswani

    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.


    Volume: Volume 7, Issue 3
    Published on: September 2, 2011
    Imported on: June 26, 2010
    Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,Computer Science - Software Engineering,D.1.3, D.2.4, F.3.1

    Consultation statistics

    This page has been seen 1023 times.
    This article's PDF has been downloaded 250 times.