Concurrent data structures or CDS such as concurrent stacks, queues, sets etc. have become very popular in the past few years partly due to the rise of multi-core systems. But one of the greatest challenges with CDSs has been developing correct structures and then proving the correctness of these structures. We believe that techniques that help prove the correctness of these CDSs can also guide in developing new CDSs. An intuitive technique to prove the correctness of CDSs is using Linearization Points or LPs. An LP is an atomic event in the execution interval of each method such that the execution of the entire method seems to have taken place in the instant of that event. One of the main challenges with the LP based approach is to identify the correct LPs of a CDS. Identifying the correct LPs can be deceptively wrong in many cases. In fact, in many cases, the LP identified or even worse the CDS itself could be wrong. To address these issues, several automatic tools for verifying linearizability have been developed. But we believe that these tools don't provide insight to a programmer to develop the correct concurrent programs or identify the LPs. Considering the complexity of developing a CDS and verifying its correctness, we address the most basic problem of this domain in this paper: given the set of LPs of a CDS, how to show its correctness? We assume that we are given a CDS and its LPs. We have developed a hand-crafted technique of proving the correctness of the CDS by validating its LPs. As observed earlier, identifying the correct LPs is very tricky and erroneous. But since our technique is hand-crafted, we believe that the process of proving correctness might provide insight to identify the correct LPs, if the currently chosen LP is incorrect. We also believe that this technique might also offer the programmer some insight to develop more efficient variants of the CDS.
翻译:在过去几年中,平行数据结构或CDS(如同时的堆叠、队列、集集等)已经变得非常流行,部分原因是多核心系统的崛起。但CDS的最大挑战之一是建立正确的结构,然后证明这些结构的正确性。我们认为,有助于证明这些CDS正确性的技术也可以指导开发新的CDS。一种证明CDS正确性的直观技术正在使用线性点或LPs。在每种方法的执行间隔中,LP是一个原子事件,因此,整个方法的实施似乎在事件发生之时就已经发生。但基于 CDS 的最大挑战之一是建立正确的结构,然后证明这些结构的正确性。在很多情况下,确定这些CDS正确性的方法也可能被误解。事实上,在许多情况下,所查明的CDS本身的LP(LP)本身可能存在错误。为了解决这些问题,我们已经开发了数个自动工具来核查直线性。但是我们认为,这些工具能为一个程序提供洞察到整个方法的直截面性,而LS的精度是用来早期校正的CDS(L)的精度,这是我们用来校正的R(L)进程的精度。