We present a general methodology for establishing the impossibility of implementing certain concurrent objects on different (weak) memory models. The key idea behind our approach lies in characterizing memory models by their mergeability properties, identifying restrictions under which independent memory traces can be merged into a single valid memory trace. In turn, we show that the mergeability properties of the underlying memory model entail similar mergeability requirements on the specifications of objects that can be implemented on that memory model. We demonstrate the applicability of our approach to establish the impossibility of implementing standard distributed objects with different restrictions on memory traces on three memory models: strictly consistent memory, total store order, and release-acquire. These impossibility results allow us to identify tight and almost tight bounds for some objects, as well as new separation results between weak memory models, and between well-studied objects based on their implementability on weak memory models.
翻译:我们提出了一种通用方法论,用于证明在特定(弱)内存模型上无法实现某些并发对象。该方法的核心思想在于通过内存模型的合并特性来刻画其本质,即识别在何种限制条件下,独立的内存轨迹能够合并为单个有效内存轨迹。相应地,我们证明了底层内存模型的合并特性会对其可实现的并发对象规范施加类似的合并性要求。我们通过三个内存模型案例展示了该方法的应用:严格一致性内存、全序存储模型以及释放-获取模型,证明了在具有不同内存轨迹限制的标准分布式对象上均存在实现不可能性。这些不可能性结果使我们能够为某些对象确定严格或近似严格的可实现性边界,同时揭示了弱内存模型之间以及基于弱内存模型可实现性的经典研究对象之间的新分离关系。