Linearizability is a commonly accepted correctness criterion for concurrent data structures. However, verifying linearizability of highly concurrent data structures is still a challenging task. In this paper, we present a simple and complete proof technique for verifying linearizability of concurrent stacks. Our proof technique reduces linearizability of concurrent stacks to establishing a set of conditions. These conditions are based on the happened-before order of operations, intuitively express the LIFO semantics and can be proved by simple arguments. Designers of concurrent data structures can easily and quickly learn to use the proof technique. We have successfully applied the method to several challenging concurrent stacks: the TS stack, the HSY stack, and the FA stack, etc.

翻译：线性化性是并发数据结构普遍接受的正确性标准。然而，验证高并发数据结构的线性化性仍然是一项具有挑战性的任务。本文提出一种用于验证并发栈线性化性的简单且完备的证明技术。该证明技术将并发栈的线性化性验证归结为一组条件的建立。这些条件基于操作的发生前序关系，直观地表达了后进先出语义，且可通过简单论证进行证明。并发数据结构的设计者能够轻松快速地掌握该证明技术的使用方法。我们已成功将该方法应用于多个具有挑战性的并发栈：TS栈、HSY栈与FA栈等。