来自顺序证明的逻辑并发控制
Logical Concurrency Control from Sequential Proofs
摘要：
我们感兴趣的是识别和执行并发程序的隔离要求，即，确保程序满足其规范的并发控制。本文的论点是，这可以从顺序证明开始系统地进行，即，在没有并发交织的情况下证明程序的正确性。我们说明我们的论文提出了一个解决方案的问题，使一个顺序库线程安全的并发客户端。我们考虑一个顺序库注释断言以及证明这些断言在顺序执行。我们展示了如何使用证明来导出并发控制，以确保库方法的任何执行在由并发客户端调用时满足相同的断言。我们还提出了一个扩展，以保证库方法是线性化或原子。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
