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

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:September 11,2023
  • Revised:October 30,2023
  • Adopted:
  • Online: January 05,2024
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063