Logical Concurrency Control from Sequential Proofs
Logical Concurrency Control from Sequential Proofs
复制标题
顺序证明的逻辑并发控制
DOI：
10.2168/lmcs-7(3:10)2011
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
K. Vaswani
中科院分区：
文献类型：
--
作者：
Jyotirmoy V. Deshmukh;G. Ramalingam;Venkatesh Prasad Ranganath;K. Vaswani
我们感兴趣的是识别和执行并发程序的隔离需求，即确保程序满足其规范的并发控制。本文的论点是，这可以从一个顺序证明开始系统地完成，即在没有并发交织的情况下证明程序的正确性。我们通过提出一个为并发客户机提供线程安全的顺序库的解决方案来说明我们的论点。我们考虑一个带有断言注释的顺序库，以及这些断言在顺序执行中保持不变的证明。我们将展示如何使用证明来派生并发控制，以确保库方法的任何执行在被并发客户机调用时都满足相同的断言。我们还提供了一个扩展，以保证库相对于其顺序规范是线性化的。
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 is linearizable with respect to its sequential specification.