使用前向模拟证明线性化
Proving linearizability using forward simulations
摘要：
可线性化性是并发数据结构（如堆栈和队列）的标准正确性标准。它允许在并发实现和原子参考实现之间建立观测精化。证明线性化需要沿着所有可能的计算为每个方法调用确定线性化点，从而导致有效的顺序执行，或者建立向前和向后模拟。在这两种情况下，进行证明是困难和复杂的。特别地，在具有数据结构的程序的上下文中，向后推理是困难的，并且不能为所有现有实现定义用于识别静态线性化点的策略。在本文中，我们表明，与普遍的看法相反，许多这样的复杂实现，包括，例如，Herlihy&Wing队列和时间戳堆栈，可以证明是正确的，只使用前向模拟参数。这就为这些易于自动化的实现提供了概念上简单而自然的正确性证明。
英文摘要：
Linearizability is the standard correctness criterion concurrent data structures such as stacks and queues. It allows to establish observational refinement between a concurrent implementation and an atomic reference implementation.Proving linearizability requires identifying linearization points for each method invocation along all possible computations, leading to valid sequential executions, or alternatively, establishing forward and backward simulations. In both cases, carrying out proofs is hard and complex in general. In particular, backward reasoning is difficult in the context of programs with data structures, and strategies for identifying statically linearization points cannot be defined for all existing implementations. In this paper, we show that, contrary to common belief, many such complex implementations, including, e.g., the Herlihy&Wing Queue and the Time-Stamped Stack, can be proved correct using only forward simulation arguments. This leads to conceptually simple and natural correctness proofs for these implementations that are amenable to automation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
