Jyotirmoy Deshmukh, G. Ramalingam, Venkatesh-Prasad Ranganath, and Kapil Vaswani
July 2009
In this paper, 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 consdier 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.
![]() PDF file |
| Type: | TechReport |
| Number: | MSR-TR-2009-81 |
| Pages: | 31 |