TSO内存模型下限界可线性化的可判定性研究

TSO-to-TSO可线性化、TSO-to-SC可线性化和TSO可线性化是Total Store Order（简称TSO）内存模型下可线性化的三个变种。在本文中我们提出了?-限界TSO-to-TSO可线性化和?-限界TSO可线性化，考察了?-限界TSO-to-TSO可线性化、?-限界TSO-to-SC可线性化和?-限界TSO可线性化的验证问题。它们分别是这三种可线性化的限界版本，都使用?-扩展历史，这样的扩展历史对应的执行有着限界数目（不超过?个）的函数调用、函数返回、调用刷出和返回刷出动作。?-扩展历史对应执行中的写动作数目是不限界的，进而执行中使用的存储缓冲区的大小也是不限界的，对应的操作语义是无穷状态迁移系统，所以三个限界版本可线性化的验证问题是不平凡的。 我们将定义在并发数据结构与顺序规约之间的?-限界TSO-to-TSO可线性化、?-限界TSO-to-SC可线性化和?-限界TSO可线性化的验证问题归约到?-扩展历史集合之间的TSO-to-TSO可线性化问题，从而以统一的方式验证了TSO内存模型下可线性化的三个限界版本。验证方法的关键步骤是判定一个并发数据结构是否有一个特定的?-扩展历史。我们证明了这个问题是可判定的，证明方法是将这一问题归约为已知可判定的易失通道机器的控制状态可达问题。本质上，这一归约将每一个函数调用或函数返回动作转化为写、刷出或cas（compare-and-swap）动作。在TSO-to-TSO可线性化的定义中，一个函数调用或函数返回动作会同时影响存储缓冲区和控制状态。为了模拟函数调用或函数返回动作对存储缓冲区的影响，我们在每个函数调用或函数返回动作之后立刻执行一个特定的写动作。这个写动作及其对应的刷出动作模拟了函数调用或函数返回动作对存储缓冲区的影响。我们引入观察者进程，为每个函数调用或函数返回动作“绑定”一个观察者进程的cas动作，以这种方式模拟了函数调用或函数返回动作对控制状态的影响。因此，我们证明了TSO内存模型下可线性化的这三个限界版本都是可判定的。我们进而证明了在TSO内存模型下判定可线性化的这三个限界版本的复杂度都在递归函数的Fast-Growing层级中。我们通过证明已知对应复杂度的单通道简单通道机器的可达问题和TSO内存模型下可线性化的三个限界版本可以互相归约得到这个结论。

Decidability of Bounded Linearizability on TSO Memory Model

TSO-to-TSO linearizability, TSO-to-SC linearizability and TSO linearizability are three typical variants of linearizability on the Total Store Order (TSO) memory model. In this paper we propose k-bounded TSO-to-TSO linearizability and k-bounded TSO linearizability, and investigate the verification problems of k-bounded TSO-to-TSO linearizability, k-bounded TSO-to-SC linearizability and k-bounded TSO linearizability that are bounded versions of the above variants of linearizability, defined on k-extended histories. Although the corresponding executions of k-extended histories contain a bounded number (less or equal than k) of call, return, flushCall and flushReturn actions, the verification problems of these three bounded versions of linearizability are non-trivial since the corresponding executions of k-extended histories may still contain an unbounded number of write actions and use store buffers with an unbounded capacity, which makes their operational semantics built upon infinite state transition systems. The k-bounded TSO-to-TSO linearizability problem, k-bounded TSO-to-SC linearizability problem and k-bounded TSO linearizability problem between concurrent data structures and their sequential specifications are reduced into TSO-to-TSO linearizability problem between sets of k-extended histories, which provides an uniform framework for verifying the three bounded versions of linearizability on the TSO memory model. The key point of our approach is to check if a concurrent data structure contains a specific k-extended history. We prove that this problem is decidable by reducing it into the control state reachability problem of lossy channel machines, which is known decidable. This reduction essentially requires call and return actions to be transformed into write, flush or cas (compare-and-swap) actions. In the definition of TSO-to-TSO linearizability, a call or return action taken by a process changes the store buffer and the control state of the process at the same time. We add a specific write action immediately after each call or return action; thus the influence on store buffers is mimicked by these specific write actions and their corresponding flush actions. To mimic the influence on control states, we introduce an observer process and bind specific cas actions of the observer process to each call or return actions. In this way, we prove that the three bounded versions of linearizability are decidable on the TSO memory model. We further prove that the three bounded versions of linearizability on the TSO memory model are at level F!! in the fast-growing hierarchy of recursive functions. This is proved by stating that the reachability problem of single-channel basic lossy channel machines, which is known in such complexity class, can be reduced into the three bounded versions of linearizability problems on the TSO memory model, while the latter problem can also be reduced into the former problem.