并发对象强可线性化性质的检测和验证

可线性化被公认为并发对象正确性标准,但其已被证明不能作为含有随机语句的并发对象的正确性标准.为此,Golab等人提出了强可线性化概念,它在可线性化的定义上增加了前缀保持性质,对并发对象具有更强的约束性.关于强可线性化的研究集中在使用特定的基本对象构造满足强可线性化性质的并发对象的可行性.对常见的并发对象的强可线性化性质的检测和验证方面的研究较为少见.从并发对象的验证算法和证否方法两个方面研究了强可线性化性质.首先,细化强可线性化性质,将它细分为固定生效点和单纯帮助两类,并证明固定生效点是已有的固定可线性化点概念的扩展.其次,提出两种强可线性化的验证算法,其中一种基于固定可线性化点,另一种基于固定生效点.最后,给出一个构造性的证明并发对象违背强可线性化的证明方法,依据该方法证明了Herlihy&Wing队列、一种单读单写寄存器实现和一种并发快照实现违反强可线性化性质.