软件学报

作者：王超，贾巧雯，吕毅，吴鹏

单位：王超，西南大学 计算机与信息科学学院 软件研究与创新中心, 重庆 40071511,贾巧雯，计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004902,吕毅，计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004903,吴鹏，计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004904

关键词：并发对象;正确性标准;可线性化;强可线性化

基金：国家自然科学基金(62002298, 62072443, 62372386); 国家重点研发计划(2022YFA1005100, 2022YFA1005101, 2022YFA1005104); 重庆市自然科学基金面上项目(CSTB2022NSCQ-MSX0437)

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

来源：2024年第9期

《软件学报》期刊编辑部

查看软件学报杂志2024年第9期