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

Strong Linearizability Checking and Determination for Concurrent Objects

作　　者：王超 贾巧雯 吕毅[2,3] 吴鹏 WANG Chao;JIA Qiao-Wen;LU Yi;WU Peng(Centre for Research and Innovation in Software Engineering,College of Computer and Information Science,Southwest University,Chongqing 400715,China;State Key Laboratory of Computer Science(Institute of Software,Chinese Academy of Sciences),Beijing 100190,China;University of Chinese Academy of Sciences,Beijing 100049,China)

机构地区：[1]西南大学计算机与信息科学学院软件研究与创新中心,重庆400715 [2]计算机科学国家重点实验室(中国科学院软件研究所),北京100190 [3]中国科学院大学,北京100049

出　　处：《软件学报》2024年第9期4141-4159,共19页Journal of Software

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

摘　　要：可线性化被公认为并发对象正确性标准,但其已被证明不能作为含有随机语句的并发对象的正确性标准.为此,Golab等人提出了强可线性化概念,它在可线性化的定义上增加了前缀保持性质,对并发对象具有更强的约束性.关于强可线性化的研究集中在使用特定的基本对象构造满足强可线性化性质的并发对象的可行性.对常见的并发对象的强可线性化性质的检测和验证方面的研究较为少见.从并发对象的验证算法和证否方法两个方面研究了强可线性化性质.首先,细化强可线性化性质,将它细分为固定生效点和单纯帮助两类,并证明固定生效点是已有的固定可线性化点概念的扩展.其次,提出两种强可线性化的验证算法,其中一种基于固定可线性化点,另一种基于固定生效点.最后,给出一个构造性的证明并发对象违背强可线性化的证明方法,依据该方法证明了Herlihy&Wing队列、一种单读单写寄存器实现和一种并发快照实现违反强可线性化性质.Linearizability is universally accepted as a correctness criterion for concurrent objects.However,it has been shown that linearizability cannot be adopted as a correctness criterion for concurrent objects with random sentences.Thus,Golab et al.proposed the concept of strong linearizability,which adds prefix preservation properties based on the linearizability definition and has more constraints for concurrent objects.The research on strong linearizability focuses on the feasibility of generating strongly linearizable objects with certain basic objects,while only a few studies are about checking and verification of strong linearizability.This study investigates strong linearizability from two aspects including the verification algorithm and approach for proving non-strong linearizability of concurrent objects.First,it divides strong linearizability into fixed effective points and pure help and proves that the notion of fixed effective points is an extension of that of fixed linearizability points.Then,two verification algorithms for strong linearizability are put forward.One algorithm is based on checking the fixed linearizability points,and the other is based on the fixed effective points.Finally,an approach is provided for proving that the concurrent objects violate strong linearizability,and it helps verify that the Herlihy&Wing queue,a singlereader single-write register,and a snapshot object violate strong linearizability.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]