Computer Science – Programming Languages
Scientific paper
2011-07-22
LMCS 7 (3:10) 2011
Computer Science
Programming Languages
Scientific paper
10.2168/LMCS-7(3:10)2011
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.
Deshmukh Jyotirmoy
Ramalingam Gopalakrishnan
Ranganath Venkatesh-Prasad
Vaswani Kapil
No associations
LandOfFree
Logical Concurrency Control from Sequential Proofs does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Logical Concurrency Control from Sequential Proofs, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Logical Concurrency Control from Sequential Proofs will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-676033