Logical Concurrency Control From Sequential Proofs
The authors 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. This can be done systematically starting from a sequential proof, i.e., a proof of correctness of the program in the absence of concurrent inter-leavings. They illustrate their paper by presenting a solution to the problem of making a sequential library thread-safe for concurrent clients. They consider a sequential library annotated with assertions along with a proof that these assertions hold in a sequential execution.