论文标题
碰撞停靠站和崩溃 - 恢复共享内存模型的分离和等效结果
Separation and Equivalence results for the Crash-stop and Crash-recovery Shared Memory Models
论文作者
论文摘要
线性化性，并发数据结构的传统正确性条件被认为不足对于非挥发性共享内存模型，在崩溃后过程恢复。对于此崩溃回收共享存储器模型，严格的线条可行性被认为是合适的，因为与线性化性不同，它可以确保在崩溃之前或根本没有生效的操作。 这项工作正式化并回答了一个问题，即在崩溃重新发现模型中，为崩溃 - 停留的共享内存模型得出的数据类型的实现也是严格的。这项工作提出了一项严格的研究，以证明通常如何通过非阻滞实施来实施的帮助机制是如何从严格的线条上描述线性可可线度的算法抽象。我们的第一个贡献正式化了崩溃恢复模型，以及显式过程崩溃和恢复如何在标准崩溃停靠站共享内存模型上引入进一步的维度。我们做出以下技术贡献：（i）我们证明严格的可连接性与任何已知的帮助定义无关； （ii）然后，我们提出了帮助自由的自然定义，以证明任何无障碍，可线化和无帮助的对象类型的实施也是严格可线化的； （iii）最后，我们证明，对于大量的对象类型，非阻止严格可线化的实现无法有所帮助。从整体上看，这项工作提供了对应用于碰撞恢复模型的同时实现的同时实现时的第一个精确表征，而反之亦然。
Linearizability, the traditional correctness condition for concurrent data structures is considered insufficient for the non-volatile shared memory model where processes recover following a crash. For this crash-recovery shared memory model, strict-linearizability is considered appropriate since, unlike linearizability, it ensures operations that crash take effect prior to the crash or not at all. This work formalizes and answers the question of whether an implementation of a data type derived for the crash-stop shared memory model is also strict-linearizable in the crash-recovery model. This work presents a rigorous study to prove how helping mechanisms, typically employed by non-blocking implementations, is the algorithmic abstraction that delineates linearizability from strict-linearizability. Our first contribution formalizes the crash-recovery model and how explicit process crashes and recovery introduces further dimensionalities over the standard crash-stop shared memory model. We make the following technical contributions: (i) we prove that strict-linearizability is independent of any known help definition; (ii) we then present a natural definition of help-freedom to prove that any obstruction-free, linearizable and help-free implementation of a total object type is also strict-linearizable; (iii) finally, we prove that for a large class of object types, a non-blocking strict-linearizable implementation cannot have helping. Viewed holistically, this work provides the first precise characterization of the intricacies in applying a concurrent implementation designed for the crash-stop model to the crash-recovery model, and vice-versa.
