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.