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.