some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

   Volume 1 (2005)

   Volume 2 (2006)

   Volume 3 (2007)

   Volume 4 (2008)

   Volume 5 (2009)

   Volume 6 (2010)

   Volume 7 (2011)

      Issue 1

      Issue 2

      Issue 3

      Issue 4

   Volume 8 (2012)

   Volume 9 (2013)

   Volume 10 (2014)

   Volume 11 (2015)

   Volume 12 (2016)

   Volume 13 (2017)

SPECIAL ISSUES

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

VOLUME 7, ISSUE 3, PAPER 10


Logical Concurrency Control from Sequential Proofs

©Jyotirmoy Deshmukh, University of Texas at Austin
©G. Ramalingam, Microsoft Research India
©Venkatesh-Prasad Ranganath, Microsoft Research India
©Kapil Vaswani, Microsoft Research India

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.

Publication date: September 2, 2011

Full Text: PDF | PostScript
DOI: 10.2168/LMCS-7(3:10)2011

Hit Counts: 5771

Creative Commons