崩溃停止与崩溃恢复共享内存模型的分离与等价性结果

线性izability 作为并发数据结构的传统正确性条件，被认为对于进程在崩溃后恢复的非易失性共享内存模型是不充分的。对于该崩溃恢复共享内存模型，严格线性izability 被认为是合适的，因为与线性izability 不同，它确保崩溃的操作在崩溃前生效或根本不生效。本工作形式化并回答了以下问题：为崩溃停止共享内存模型导出的数据类型实现在崩溃恢复模型中是否也是严格线性izable 的。本工作提出了一项严谨研究，以证明通常由非阻塞实现采用的帮助机制是区分线性izability 与严格线性izability 的算法抽象。我们的首要贡献形式化了崩溃恢复模型，以及显式进程崩溃与恢复如何在标准崩溃停止共享内存模型之上引入进一步的维度。我们做出如下技术贡献：(i) 我们证明严格线性izability 独立于任何已知的帮助定义；(ii) 我们随后给出帮助自由的自然定义，以证明全对象类型的任何无 obstruction-free、线性izable 且无帮助的实現也是严格线性izable 的；(iii) 最后，我们证明对于一大类对象类型，非阻塞严格线性izable 实现不可能具有帮助。整体来看，本工作首次精确刻画了将针对崩溃停止模型设计的并发实现应用于崩溃恢复模型（以及反之）时的复杂性。