并发对象强可线性化性质的检测和验证
CSTR:
作者:
作者单位:

作者简介:

王超(1985-), 男, 博士, 副教授, CCF专业会员, 主要研究领域为形式化方法, 并发数据结构, 分布式数据类型;贾巧雯(1992-), 女, 博士, 主要研究领域为并发系统, 可线性化验证. ;吕毅(1972-), 男, 博士, 副研究员, CCF专业会员, 主要研究领域为并发理论, 形式化方法. ;吴鹏(1977-), 男, 博士, 副研究员, CCF高级会员, 主要研究领域为形式化方法, 并发测试, 机器学习.

通讯作者:

吕毅, E-mail: lvyi@ios.ac.cn

中图分类号:

基金项目:

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


Strong Linearizability Checking and Determination for Concurrent Objects
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    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 single-reader single-write register, and a snapshot object violate strong linearizability.

    参考文献
    相似文献
    引证文献
引用本文

王超,贾巧雯,吕毅,吴鹏.并发对象强可线性化性质的检测和验证.软件学报,2024,35(9):4141-4159

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2023-09-11
  • 最后修改日期:2023-10-30
  • 录用日期:
  • 在线发布日期: 2024-01-05
  • 出版日期: 2024-09-06
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号