利用前向模拟证明线性izability
编程语言
2017-02-10 v1
摘要
线性izability（linearizability）是诸如栈和队列等并发数据结构的标准正确性准则。它允许在并发实现与原子参考实现之间建立观测精化。证明线性izability需要沿所有可能计算为每次方法调用识别线性化点，从而得到有效的顺序执行，或者 alternatively，建立前向与后向模拟。在这两种情况下，一般地执行证明都是困难且复杂的。特别是，后向推理在带有数据结构的程序上下文中是困难的，并且针对所有现有实现静态识别线性化点的策略无法定义。在本文中，我们表明，与普遍看法相反，许多此类复杂实现，包括例如 Herlihy&Wing 队列和 Time-Stamped 栈，可以仅使用前向模拟论证来证明正确。这导致了这些实现的概念上简单且自然的正确性证明，易于自动化。
引用
@article{arxiv.1702.02705,
title = {Proving linearizability using forward simulations},
author = {Ahmed Bouajjani and Michael Emmi and Constantin Enea and Suha Orhun Mutluergil},
journal= {arXiv preprint arXiv:1702.02705},
year = {2017}
}