-
题名并发对象强可线性化性质的检测和验证
- 1
-
-
作者
王超
贾巧雯
吕毅
吴鹏
-
机构
西南大学计算机与信息科学学院软件研究与创新中心
计算机科学国家重点实验室(中国科学院软件研究所)
中国科学院大学
-
出处
《软件学报》
EI
CSCD
北大核心
2024年第9期4141-4159,共19页
-
基金
国家自然科学基金(62002298,62072443,62372386)
国家重点研发计划(2022YFA1005100,2022YFA1005101,2022YFA1005104)
重庆市自然科学基金面上项目(CSTB2022NSCQ-MSX0437)。
-
文摘
可线性化被公认为并发对象正确性标准,但其已被证明不能作为含有随机语句的并发对象的正确性标准.为此,Golab等人提出了强可线性化概念,它在可线性化的定义上增加了前缀保持性质,对并发对象具有更强的约束性.关于强可线性化的研究集中在使用特定的基本对象构造满足强可线性化性质的并发对象的可行性.对常见的并发对象的强可线性化性质的检测和验证方面的研究较为少见.从并发对象的验证算法和证否方法两个方面研究了强可线性化性质.首先,细化强可线性化性质,将它细分为固定生效点和单纯帮助两类,并证明固定生效点是已有的固定可线性化点概念的扩展.其次,提出两种强可线性化的验证算法,其中一种基于固定可线性化点,另一种基于固定生效点.最后,给出一个构造性的证明并发对象违背强可线性化的证明方法,依据该方法证明了Herlihy&Wing队列、一种单读单写寄存器实现和一种并发快照实现违反强可线性化性质.
-
关键词
并发对象
正确性标准
可线性化
强可线性化
-
Keywords
concurrent object
correctness criterion
linearizability
strong linearizability
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-