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.

翻译：对并行数据结构而言,线性是普遍接受的正确性标准。然而,核实高度并行数据结构的线性仍然是一项艰巨的任务。在本文件中,我们提出了一个简单而完整的验证技术,用于核查并行堆叠的线性。我们的证据技术减少了同时堆叠线性,以建立一套条件。这些条件以操作前发生的情况为基础,直观地表示LIFO的语义,并且可以用简单的论点来证明。同时数据结构的设计者可以很容易和迅速地学会使用验证技术。我们已经成功地将这种方法应用于几个具有挑战性的同时堆叠:TS堆、HSY堆和FA堆,等等。