Talks & Seminars
Title: Logical Concurrency Control from Sequential Proofs
Dr. Ganesh Ramalingam, Microsoft Research India
Date & Time: April 28, 2009 14:30
Venue: Conference Room, 01st floor, ā€˜Cā€™ Block, Kanwal Rekhi Building
In this talk, we consider the problem of making a sequential library safe for concurrent clients. Informally, given a sequential library that works satisfactorily when invoked by a sequential client, we wish to synthesize concurrency control code for the library that ensures that it will work satisfactorily even when invoked by a concurrent client (which may lead to overlapping executions of the library's procedures). Formally, we consider a sequential library annotated with assertions along with a proof that these assertions hold in a sequential execution. We show how such a proof can be used to derive a concurrency control for the library that guarantees that the library's execution will satisfy the same assertions even when invoked by a concurrent client. Secondly, we generalize this result by considering 2-state assertions that correspond to relations over a pair of program states. Such assertions can be used (as postconditions) to specify the desired functionality of procedures. Thus, the synthesized concurrency control ensures that procedures have the desired functionality even in a concurrent setting. Finally, we extend the approach to guarantee linearizability: any concurrent execution of a procedure is not only guaranteed to satisfy its specification, it also appears to take effect instantaneously at some point during its execution. A notable feature of our solution is that it is based on a _logical_notion of interference between threads: the derived concurrency control prevents threads from violating properties (by executing statements) that are to be preserved at a given program point, rather than preventing threads from accessing/modifying specific data. Time permitting, I will also talk about other ongoing work in our lab.
Speaker Profile:
Dr. Ramalingam has done Ph.D. in Computer Science at the University of Wisconsin - Madison in 1993 under the guidance of Prof. Thomas Reps. From 1993 to 2006 July, he was with the IBM T. J. Watson Research Center. He is now a Senior Researcher in the Rigorous Software Engineering Group at Microsoft Research India. He is broadly interested in the areas of Programming Languages and Software Engineering, in making software development easier, more enjoyable, more reliable, and more productive. Some of his more specific interests include static program analysis and programming tools.
List of Talks


Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback