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

作者简介:

通讯作者:

中图分类号:

基金项目:

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


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

Fund Project:

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

    可线性化被公认为并发对象正确性标准,但其已被证明不能作为含有随机语句的并发对象的正确性标准。为此,Golab等人提出了强可线性化概念,它在可线性化的定义上增加了前缀保持性质,对并发对象具有更强的约束性。关于强可线性化的研究集中在使用特定的基本对象构造满足强可线性化性质的并发对象的可行性。对常见的并发对象的强可线性化性质的检测和验证方面的研究较为少见。

    Abstract:

    Linearizability is accepted as a de facto correctness condition for concurrent objects. However, it has been shown that linearizability is not suffice as correctness conditions for concurrent objects when processes can exploit randomization. Thus, Golab proposed strong linearizability, which is a variant of linearizability and has more restriction. Most research about strong linearizability focus on possibility of generating strongly linearizable objects with certain basic objects, while only a few research is about checking and verification of strongly linearizability. In this paper we investigate strong linearizability from two aspects, one is algorithm of verification, and the other is approach for proving non-strong linearizability. First, we divide strong linearizability into fixed-effective-points and pure-help, and prove that the notion of fixed-effective-points is an extension of the notion of fixed-linearizability-point. Then, we propose two verification algorithms for strong linearizabilty. One algorithm is based on checking the existence of fixed-linearizability-points, and the other algorithm is based on checking the existence of fixed-effective-points. At last, we propose an approach for proving objects violate strong linearizability, and we prove that Herlihy&Wing queue, a single-reader single-write register and a snapshot object violate strong linearizability with this approach.

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

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

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

京公网安备 11040202500063号