论文部分内容阅读
多核时代已经到来了。在多核体系下，能够更好的利用多核处理能力的并发数据结构算法得到了广泛应用。并发数据结构往往采用细粒度锁或者是免锁的机制进行同步，而不是使用更传统的锁机制来进行同步。这带来了更高的并发度和更好的性能，但是也导致了对并发数据结构算法的设计和验证变得更加困难。 本文致力于研究并发数据结构的规约和验证。可线性化是并发数据结构领域一个被广泛接受的正确性条件，也是本领域事实上的标准正确性条件。本文从两个方面研究了可线性化及其变种的验证。一是弱内存模型下可线性化的验证，二是松散可线性化的验证。 论文的第一部分研究了TSO-to-TSO可线性化的判定性问题。TSO-to-TSO可线性化是可线性化在TSO内存模型下的一个变种。我们证明了它是不可判定的。证明的思路是把一个已知的不可判定问题，易失通道系统上节点间的迹包含问题，归约到TSO-to-TSO可线性化问题。 论文的第二部分研究了TSO-to-SC可线性化的判定性问题。TSO-to-SC可线性化是可线性化在TSO内存模型下的又一个变种。我们证明了TSO-to-SC可线性化的一个限界版本，尼限界的TSO-to-SC可线性化，是可判定的。证明的思路是将它归约到一个已知的可判定问题:易失通道系统上的可达性问题。 论文的第三部分研究了拟线性化的判定性问题。拟线性化是一个量化松散可线性化的框架。我们证明了它是不可判定的。证明的思路是把一个已知的不可判定问题，计数机器的k-Z问题，归约到拟线性化问题。 论文的第四部分我们提出了一个定义松散可线性化的框架，称作正则可线性化。这个框架使用有穷状态自动机来表示对顺序规约的松散策略，涵盖了常见可扩展队列、栈和先级队列的松散规约。进一步，我们证明了正则可线性化的队列、栈和优先级队列可以用有穷状态自动机来等价刻画。已有的用自动机等价刻画数据结构的工作只关注了标准的队列、栈，并且不能处理优先级队列。我们把已有研究扩展到了松散队列、栈和优先级队列。为了能处理已有研究无法处理的优先级队列，我们扩展了数据独立的定义，提出了部分数据独立。