Concurrent objects form the foundation of many applications that exploit multicore architectures. Reasoning about the fine-grained complexities (interleavings, invariants, etc.) of those data structures, however, is notoriously difficult. Formal proof methodologies for arguing about the correctness -- i.e.,~linearizability -- of these data structures are still somewhat disconnected from the intuitive correctness arguments. Intuitions are often about a few canonical executions, possibly with few threads, whereas formal proofs would often use generic but complex arguments about arbitrary interleavings over unboundedly many threads. As a way to bring formal proofs closer to intuitive arguments, we introduce a new methodology for characterizing the interleavings of concurrent objects, based on their \emph{commutativity quotient}. This quotient represents every interleaving up to reordering of commutative steps and, when chosen carefully, admits simple abstractions in the form of regular or context-free languages that enable simple proofs of linearizability. We demonstrate these facts on a large class of lock-free data structures and the infamously difficult Herlihy-Wing Queue. We automate the discovery of these execution quotients and show it can be automatically done for challenging data-structures such as Treiber's stack, Michael/Scott Queue, and a concurrent Set implemented as a linked list.
翻译:同步对象构成许多应用的基础, 利用多核心结构。 但是, 以这些数据结构的细微复杂( 互换、 变异等) 为由来解释这些复杂( 互换、 变异等), 却非常困难。 正式证明这些数据结构的正确性( 即 ~ 线性) 的争论方法仍然多少与直观正确性论点脱节 。 这种理论往往代表着一些反复的处决, 可能只有很少的线条, 而正式证明往往使用关于任意互换的简单而复杂的论据, 而不是许多直观的线索。 为了让正式证据更接近直观的论据, 我们引入了一种新的方法, 来说明并行物体的互换性( 即 线性) 。 这个理论代表着每一个互相调整顿的转变, 并且当仔细选择时, 接受简单但复杂的抽象的抽象语言形式, 使得直线性证据能够被接受。 我们用这些不直截面的列表的形式, 在一个不直线性的数据结构中, 自动地展示这些直线性数据结构的 。