1 引论

高效实现的并发数据结构能够充分利用多核系统的潜力, 提升并发程序的性能. 并发数据结构的抽象行为往往以顺序规约的形式给出, 正确性条件定义了并发数据结构是否符合顺序规约. 并发数据结构领域实际的正确性条件是可线性化(linearizability)^[1]. 如果一个并发数据结构中的每个函数的执行都等效于在其调用和返回期间的某个时间点的瞬时执行, 那么该并发数据结构满足可线性化.

已有的可线性化验证的研究大部分假定使用顺序一致性(sequential consistency, SC)内存模型^[2]. 在SC内存模型下, 并发程序的执行效果等同于所有进程对内存的访问以某种串行序交织进行, 这个串行序保留了每个进程访问内存动作的序关系, 并且所有对内存的写动作会立即被全局所见. 然而, 当代的多核处理器(如x86/TSO^[3], POWER^[4]和ARM^[5])和编程语言(如C/C++^[6]和Java^[7])并不遵循SC内存模型, 而是遵循松弛内存模型(relaxed memory model). 为了提升性能, 松弛内存模型相比SC内存模型允许更多的行为. 以TSO(total store order)内存模型^[3]为例, 它为每个处理器关联了一个先入先出的存储缓冲区(store buffer), 使得进程对内存的写动作不再立即被全局所见. 尽管在每个实现TSO内存模型的多处理器系统中存储缓冲区的大小是固定的, 为了描述TSO内存模型下任意并发数据结构的实现, 文献中提出的TSO内存模型^[8−11]往往为每个处理器关联一个大小不限界的先入先出存储缓冲区; 否则, 使用固定大小存储缓冲区的TSO内存模型总是无法建模需要更大存储缓冲区的TSO内存模型实现. 在TSO内存模型中, 在执行写动作时, 处理器将待更改的内存单元及其新值先放入对应的存储缓冲区中, 然后在将来某个不确定时刻将缓存的写动作从存储缓冲区中刷出(flush), 并修改对应的内存单元.

之前的文献已经提出了若干可线性化在松弛内存模型下的变种, 例如TSO内存模型下的TSO-to-TSO可线性化^[11]、TSO-to-SC可线性化^[12]和TSO可线性化^[13]、C++11内存模型下的两个可线性化变种^[14]以及C11内存模型下的一个可线性化变种^[15]. TSO-to-TSO可线性化要求当函数调用或函数返回发生时, 进程额外向存储缓冲区放入一个标记; 当标记离开存储缓冲区时, 会引发调用刷出(flushCall)或返回刷出(flushReturn)动作. TSO-to-TSO可线性化使用扩展历史, 即函数调用、函数返回、调用刷出和返回刷出动作的序列, 来表示并发数据结构的行为. 扩展历史记录了并发数据结构和客户程序以及存储缓冲区的交互. TSO-to-SC可线性化只使用函数调用和函数返回动作的序列来表示并发数据结构的行为; TSO可线性化本质上只使用函数调用和返回刷出动作的序列来表示并发数据结构的行为. TSO内存模型下可线性化的这3个变种都可理解为: 在保留特定动作之间的序的前提下, 一个并发数据结构的行为是否可以变换到另一个并发数据结构或者顺序规约的行为. 这3个变种存在一定的内在联系, TSO-to-SC可线性化和TSO可线性化关注的动作种类是TSO-to-TSO可线性化关注的动作种类的子集, TSO-to-SC可线性化和TSO可线性化定义中需要保持的序也是TSO-to-TSO可线性化定义中需要保持的序的子集. 换句话说, TSO-to-TSO可线性化在这3个变种中是最“难”的. TSO可线性化和TSO-to-TSO可线性化也有着显著的区别: 前者定义在并发数据结构和顺序规约之间, 而后者定义在并发数据结构之间.

可线性化的验证问题有着固有的困难性. SC内存模型下的可线性化问题一般是不可判定^[10], 而在进程数目固定时是可判定的^[16]. 迄今为止, 松弛内存模型下可线性化的可判定性结果还很少. 我们已经证明了进程数目固定时, TSO-to-TSO可线性化仍是不可判定的^[17], 而k-限界TSO-to-SC可线性化是可判定的^[18]. 然而进程数目固定时, 限界的TSO-to-TSO可线性化和限界的TSO可线性化的可判定性仍是未知的.

本文提出了k-限界TSO-to-TSO可线性化和k-限界TSO可线性化, 它们是TSO-to-TSO可线性化和TSO可线性化的限界版本, 只考虑限界数目的函数调用、函数返回、调用刷出和返回刷出动作序列. 需要注意的是, TSO内存模型下对可线性化的这3个限界版本的验证问题仍然是非平凡的. 因为读、写、刷出和cas(compare-and-swap)动作的数目是不限的, 因此使用的存储缓冲区大小是无界的, 这导致对应的操作语义是无穷状态迁移系统.

基于TSO内存模型下可线性化的3个变种间的联系, 为了以统一的方式验证TSO内存模型下可线性化的3个限界版本, 我们将TSO内存模型下两个并发数据结构是否符合k-限界TSO-to-TSO可线性化和k-限界TSO-to-SC可线性化以及并发数据结构和顺序规约之间是否符合k-限界TSO可线性化的问题归约为验证两个限界长度扩展历史集合是否满足TSO-to-TSO可线性化的问题, 从而以一种统一的方式对TSO内存模型下可线性化的这3个限界版本进行验证, 并最终证明了可线性化的3个限界版本是可判定的.

具体来说, 我们将验证两个并发数据结构的k-限界TSO-to-TSO可线性化问题归约为验证两个并发数据结构的k-扩展历史集合的TSO-to-TSO可线性化问题. 我们称长度不超过k的扩展历史为k-扩展历史. 一个并发数据结构的k-扩展历史集合, 是指这个并发数据结构的执行对应的长度不超过k的扩展历史的集合. 我们需要计算TSO内存模型下一个并发数据结构的k-扩展历史集合, 计算方法如下: 假定已经有了一种方法来判定TSO内存模型下一个并发数据结构是否有一条给定的k-扩展历史, 然后, 由于可能的k-扩展历史的数目是有限的, 枚举列出所有可能的k-扩展历史, 并使用这个方法来判定每一条可能的k-扩展历史是否属于这个并发数据结构. 我们将验证两个并发数据结构的k-限界TSO-to-SC可线性化问题归约为两个只包含函数调用和函数返回动作的限界扩展历史集合的TSO-to-TSO可线性化问题. 我们将验证并发数据结构k-限界TSO可线性化到正则顺序规约这个问题归约为若干个限界长扩展历史集合间的TSO-to-TSO可线性化问题.

两条k-扩展历史是否符合TSO-to-TSO可线性化是可判定的, 判定方法是: 根据TSO-to-TSO可线性化的定义, 枚举它们之间的一一映射函数并判断是否保留了特定动作之间的序. 两个k-扩展历史集合是否符合TSO-to-TSO可线性化也是可判定的, 判定方法为: 对第1个集合中的每个扩展历史, 寻找第2个集合中是否有与其满足TSO-to-TSO可线性化关系的扩展历史. 因此, 我们给出了判定TSO内存模型下可线性化的3个限界版本的方法.

在上述验证过程中, 只剩下判定TSO内存模型下一个并发数据结构是否有一条给定的k-扩展历史的方法未叙述, 现在给出判定方法. 受到文献[8]的启发, 我们希望将并发数据结构是否有一个特定的k-扩展历史这个问题归约到易失通道机器(lossy channel machine)的控制状态可达问题, 而后者是可判定的^[8]. 然而, 文献[8]中的归约方法在这里并不适用, 因为它对应的并发系统中只包含内部、读、写和cas动作, 而不包含函数调用和函数返回动作. TSO-to-TSO可线性化中的一个函数调用或函数返回动作需要同时完成两个任务: 第1个任务是将一个函数调用或函数返回标记插入对应进程的存储缓冲区, 而第2个任务是修改对应进程的控制状态. 证明中的关键步骤是修改内存模型和并发系统的操作语义, 将原本的一个函数调用或函数返回动作转化为一对写动作和cas动作. 修改后的并发系统与原来的并发系统有着相同的扩展历史集合, 而且更易于使用归约的思想判定其是否有一条给定的k-扩展历史.

对一个函数调用或函数返回动作的转化过程如下: 首先引入一个新的内存单元z_f, 并将一个函数调用或函数返回动作分解为一个“纯粹”的函数调用或函数返回动作和一个对z_f的写动作. 前者只会修改进程的控制状态, 而后者写入一个函数调用标记或函数返回标记. 我们修改了并发系统的操作语义, 使得当z_f的写被刷出到内存时, 依据这个写的值是函数调用标记还是函数返回标记, 发出一个调用刷出或返回刷出动作. 因此, 在原TSO-to-TSO可线性化定义中的函数调用和函数返回动作的第1个任务被对z_f的写动作和对应的调用刷出和返回刷出动作所模拟.

可以使用文献[18]工作中的思想来处理这些“纯粹”的函数调用和函数返回动作. 我们需要每个“纯粹”的函数调用或函数返回动作都能够立刻被其他进程所见, 为此, 修改操作语义, 为每个函数调用和函数返回动作“绑定”一个特定的cas动作. 具体来说, 引入了一个新的内存单元z_w和一个额外的“观察者”进程, 后者以非确定猜测的方式持续地使用cas语句更新z_w. 我们修改了内存模型, 使得观察者进程的每一个cas动作之后都立刻伴随一个函数调用或函数返回动作. 通过这些方法, 扩展历史中的函数调用和函数返回动作与z_w的cas动作相对应, 调用刷出和返回刷出动作与z_f的“刷出”动作相对应.

对并发数据结构的每一条扩展历史, 在修改后的操作语义中存在着一条有着相同扩展历史的执行, 且后者最终清空了每个进程的存储缓冲区, 我们称这样的执行为对应扩展历史的标记见证. TSO内存模型下并发数据结构有一条特定的扩展历史, 当且仅当在修改后的操作语义上存在这个扩展历史的标记见证. 给定一条扩展历史eh, 我们构造一个易失通道机器$M_i^{eh}$来模拟并发系统对应eh的执行中进程i的行为. $M_i^{eh}$只有一个通道, 它既执行进程i的程序, 也非确定地猜测其他进程的动作, 并且在执行每个猜测的其他进程的写动作时也会向通道放入一个数据项. 检测在特定的状态之间是否存在扩展历史eh的标记见证问题, 就被归约为易失通道机器$M_1^{eh - w}, ..., M_{n + 1}^{eh - w}$的乘积上的控制状态可达问题. 易失通道机器$M_i^{eh - w}$是通过将易失通道机器$M_i^{eh}$中的cas迁移转化为写迁移, 再将所有非写迁移转化为内部迁移得到的. 由于$M_i^{eh - w}$保证了通道中不会丢失的数据数目有穷, 并且每个写迁移放入通道的数据项包含了整个内存的快照, 所以丢失一些通道内容不会影响可达, 这使得归约成立. 由于这样的特定状态对数目是有穷的, 能够把检测扩展历史的标记见证问题, 即TSO内存模型下特定扩展历史的存在问题, 归约到易失通道机器上的控制状态可达问题. 即判定了TSO内存模型下一个并发数据结构是否有一条给定的k-扩展历史. 根据之前的讨论, 我们因此证明了TSO内存模型下可线性化的3个限界版本都是可判定的.

最后证明在TSO内存模型下判定可线性化的这3个限界版本的复杂度都在递归函数的Fast-Growing层级^[19]${\mathfrak{F}_{{\omega ^\omega }}}$中. 证明方法是: 证明单通道简单通道机器的可达性这一已知复杂度的问题^[20]和TSO内存模型下可线性化的这3个限界版本可以互相归约.

● 相关工作

SC内存模型上的可线性化验证问题得到了学术界的广泛关注^{[10, 16, 21−25]}. 在可判定性方面, Alur等人^[16]证明了进程数目固定时可线性化问题是可判定的, 而Bouajjani等人^[10]证明了在一般情况下可线性化问题不可判定. 在验证方面, 研究者们提出了多种验证可线性化的方法: Liang等人^{[21, 22]}使用定理证明方法手工证明了一些典型的并发数据结构满足可线性化; Bouajjani等人^{[23, 24]}将可线性化的验证归约到自动机的可达问题; Liu等人^[25]通过模型检测的方式验证并发数据结构是否满足可线性化.

关于TSO内存模型下可线性化的研究工作目前较少. 在可判定性方面, 文献[17]中证明了TSO-to-TSO可线性化问题在进程数目固定时已经不可判定, 文献[18]证明了k-限界TSO-to-SC可线性化问题在进程数目固定时是可判定的. 在验证方面, Derrick等人^[26]和Travkin等人^[27]使用定理证明器KIV验证了一些并发数据结构满足TSO内存模型下的可线性化.

Atig对TSO内存模型下有穷状态并发程序的安全性和活性的已知可判定性问题进行了综述^[28]. 一般而言, 并发数据结构的正确性和活性是在函数粒度, 基于函数调用和函数返回动作定义的, 而文献[28]中的安全性和活性关注的是并发程序的特定状态, 这两者的粒度不同. 文献[17, 18]受到了Atig等人^[8]工作的启发, 他们揭示了TSO内存模型下并发系统和易失通道机器的联系, 将并发系统的状态可达问题归约到易失通道机器的控制状态可达问题.

文献[18]考虑对k-限界TSO-to-SC可线性化的验证, 每个函数调用或函数返回动作只修改进程的控制状态. 在本文中, 我们考虑的情况更加复杂, 每个函数调用或函数返回动作同时完成两个任务. 文献[18]中对k-限界TSO-to-SC可线性化的结论是本文的一个推论.

2 并发系统

本节引入了并发数据结构、客户程序、最一般客户(most general client)和并发系统的概念, 并引入了并发系统的两个操作语义, 即文献[11]中定义的TSO-to-TSO可线性化时使用的操作语义以及在SC内存模型下的操作语义.

2.1 基本概念

我们用l=α₁·α₂·…·α_k表示字母表Σ上的一个有穷序列l, 这里, ·是连接符号, 且每个元素α_i(1≤i≤k)都属于字母表Σ. 令|l|和l(i)分别表示有穷序列l的长度和第i个元素, 即|l|=k且l(i)=α_i. 令l↑Σ′为有穷序列l在字母表Σ′上的投影. 给定函数f, 令f[x: y]为这样的一个函数: 除了将x映射为y之外, 对其他元素的映射都和f一样.令ε为空序列, _表示某个数据项而不关注其值.

一个标号迁移系统(labelled transition system, LTS)是一个四元组A=(Q, Σ, →, q₀). 这里, Q是状态(也称为格局)的集合, Σ是迁移标号的字母表, →⊆Q×Σ×Q是迁移关系, 而q₀是初始状态. A的一条路径是一个有穷迁移序列${q_0}\xrightarrow{{{\beta _1}}}{q_1}\xrightarrow{{{\beta _2}}}...\xrightarrow{{{\beta _k}}}{q_k}$. 如果存在A的路径${q_0}\xrightarrow{{{\beta _1}}}{q_1}\xrightarrow{{{\beta _2}}}...\xrightarrow{{{\beta _k}}}{q_k}$, 则称有穷序列t=β₁·β₂·…·β_k是A的一条迹.

2.2 并发数据结构和客户程序

一个并发系统包含着并发运行的客户程序, 这些客户程序之间的交互是通过调用并发数据结构的函数来完成的. 一个并发数据结构提供若干函数以访问该数据结构. 为了简化符号, 假定每个函数有着一个参数并返回一个值. 并发数据结构和客户程序都可以有私有的内存.

令X, M和D是有穷的内存单元集合、有穷的函数名集合和有穷的数据域. 一个原语命令有着如下形式:

$ \tau \mid { read }(x, a) \mid { write }(x, a) \mid { cas\_suc }(x, a, b) \mid { cas\_fail }(x, a, b)|{call}(m, a)| {return}(m, a) . $

这里, a, b∈D, x∈X且m∈M. 为了以标号迁移系统的方式定义并发数据结构和客户程序的语义, 我们在原语命令中包含了命令涉及的值. 例如, 读命令read(x, a)中包含了读到的值a. τ是对应内部动作的原语命令. 一个cas(compare-and-swap)命令原子地执行一个读和(可能的)一个写动作. 一个成功执行的cas命令被写为cas_suc(x, a, b), 它仅在x的值为a时执行, 并将x的值修改为b. 一个失败的cas命令被写为cas_fail(x, a, b), 它仅在x的值不为a时执行, 它的执行不会修改任何内存单元的值.

一个并发数据结构L被定义为一个五元组L=(X_L, M_L, D_L, Q_L, →_L). 这里, X_L, M_L和D_L分别是有穷的内存单元集合、有穷的函数名集合和有穷数据域. ${Q_L} = \bigcup\nolimits_{m \in {M_L}} {{Q_m}} $是各个函数m∈M_L的程序位置集合的并集. 这里的一个程序位置存储了当前程序计数器以及当前进程的寄存器的值, 被视为一个状态. ${ \to _L} = \bigcup\nolimits_{m \in {M_L}} {{ \to _m}} $是各个函数m∈M_L的迁移关系的并集. 令PCom_L是使用内存单元集合X_L、函数名集合M_L和数据域D_L的(不包含函数调用和函数返回命令)原语命令的集合, 则→_m定义为Q_m×PCom_L×Q_m的一个子集. 任取m∈M_L和a∈D_L, 在Q_m中都存在一个特殊的“初始状态”is_{(m, a)}和“终止状态”fs_{(m, a)}: is_{(m, a)}表示函数m被调用且参数值为a时, 开始执行的第1个状态; fs_{(m, a)}表示函数m在执行返回且返回值为a之前执行的最后一个状态.

一个客户程序C被定义为一个五元组C=(X_C, M_C, D_C, Q_C, →_C). 这里, X_C, M_C, D_C和Q_C分别是有穷的内存单元集合、有穷的函数名集合、有穷的数据域和有穷的程序位置集合. 令PCom_C是使用内存单元集合X_C、函数名集合M_C和数据域D_C的原语命令集合, 则→_C定义为Q_C×PCom_C×Q_C的一个子集.

一个最一般客户是一个特殊的客户程序, 它不断以非确定的方式调用任意的函数并使用任意的参数. 最一般客户用来展示并发数据结构的所有可能行为. 一个最一般客户MGC被定义为一个五元组(∅, M_c, D_c, {in_clt, in_lib}, →_mgc). 这里, →_mgc={(in_clt, call(m, a), in_lib), (in_lib, return(m, a), in_clt)|m∈M_c, a∈D_c}是迁移关系. in_clt代表当前没有库函数正在执行, 而in_lib代表当前有库函数正在执行.

2.3 操作语义

让我们使用文献[11]中的思想来给出定义TSO-to-TSO可线性化时使用的操作语义. 假定并发系统C(L)包含n个进程, 每个进程P_i(1≤i≤n)运行一个客户程序C_i=(X_C, M_C, D_C, Q_C, →_C), 而且所有的客户程序使用同一个并发数据结构L=(X_L, M_L, D_L, Q_L, →_L). 这里的C是一个函数, 将每一个进程P_i映射到客户程序C_i. 文献[11]中将C(L)的操作语义定义为一个标号迁移系统$ [[ $C(L), n$ ]] $_tt=(Conf_tt, Σ_tt, →_tt, InitConf_tt). 这里的下标tt表示TSO-to-TSO可线性化, 且Conf_tt, Σ_tt, →_tt和InitConf_tt分别定义如下.

● 每个Conf_tt中的格局是一个三元组(p, d, u), 其中, p存储了每个进程的当前控制状态, d存储了每个内存单元的取值, 而u存储了每个进程的存储缓冲区的内容;

● Σ_tt是动作的集合, 包含如下元素:

τ(i)|read(i, x, a)|write(i, x, a)|cas(i, x, a, b)|flush(i, x, b)|call(i, m, a)|return(i, m, a)|flushCall(i)|flushReturn(i).

其中, 1≤i≤n, m∈M, x∈X_L∪X_C且a, b∈D;

● 对每个进程P_i(1≤i≤n), 迁移关系→_tt包含如下迁移: 读动作read(i, x, a)需要确保或者当前进程存储缓冲区u(i)中对应x的最新项是(x, a), 或者这样的项不存在且内存中x的值是a(d(x)=a); 写动作write(i, x, a)并不直接修改内存, 而是将一个数据对(x, a)放入当前进程存储缓冲区u(i)的尾部; 刷出动作flush(i, x, a)从当前进程的存储缓冲区u(i)的头部取出数据对(x, a), 并将内存中x的取值修改为a; cas动作cas(i, x, a, b)会清空当前进程存储缓冲区u(i), 之后, 或者原子地确认内存中x的值a并将其修改为b, 或者原子地确认内存中x的值不为a之后不修改任何内存; 函数调用动作call(i, m, a)将一个标记call放入当前进程存储缓冲区u(i)的尾部, 并开始执行函数m在参数为a时的代码; 函数返回动作retun(i, m, a)将一个标记ret放入当前进程存储缓冲区u(i)的尾部并从函数m中返回, 返回值a并回到客户程序; 当标记call或ret从进程的存储缓冲区u(i)的头部刷出时, 会触发一个调用刷出动作flushCall(i)或返回刷出动作flushReturn(i);

● 初始格局InitConf_tt是一个三元组(p_init, d_init, u_init), 其中, p_init将每个进程ID映射到一个初始状态, d_init规定了X_L∪X_C中的内存单元的初始值, 而u_init将每个进程ID映射到一个空的存储缓冲区. 当每个进程都使用最一般客户时, 我们将此时的标号迁移系统$ [[ $C(L), n$ ]] $_tt简写为$ [[ $L, n$ ]] $_tt.

根据文献[12], 并发系统在SC内存模型上的操作语义定义为一个标号迁移系统$ [[ $C(L), n$ ]] $_sc=(Conf_sc, Σ_sc, →_sc, InitConf_sc). $ [[ $C(L), n$ ]] $_sc与$ [[ $C(L), n$ ]] $_tt相似, 不同点是: 在Conf_sc的每个格局中, 每个进程的存储缓冲区都固定为空; 每个写动作不再修改存储缓冲区而是直接修改内存; 函数调用和函数返回动作不再向存储缓冲区中放入标记, 因此也不再有调用刷出和返回刷出动作. 当每个进程都使用最一般客户时, 我们将此时的标号迁移系统$ [[ $C(L), n$ ]] $_sc简写为$ [[ $L, n$ ]] $_sc. 在本文的技术报告版本^[29]中, 可以找到$ [[ $C(L), n$ ]] $_tt和$ [[ $C(L), n$ ]] $_sc的详细定义.

3 正确性条件

在本节中, 我们引入TSO-to-TSO可线性化、(k-限界)TSO-to-SC可线性化和TSO可线性化的定义, 并提出k-限界TSO-to-TSO可线性化和k-限界TSO可线性化的定义.

3.1 (限界)TSO-to-TSO可线性化

TSO-to-TSO可线性化^[11]是可线性化^[1]在TSO内存模型下的一个变种. TSO-to-TSO可线性化满足抽象定理^{[11, 12, 14]}, 后者是正确性条件的一个重要属性. 一个正确性条件满足抽象定理, 如果使用并发数据结构时的每个客户程序行为, 在将并发数据结构替换为抽象实现时仍会发生.

在TSO内存模型中, 数据结构和客户程序都可能通过存储缓冲区展示出副作用. 为了确保抽象定理成立, 除了函数调用和函数返回, 并发数据结构还需要记录如下两种时刻: 一个函数写进存储缓冲区的第1个数据项(如果存在), 从存储缓冲区中刷出到内存的时间点; 以及一个函数写进存储缓冲区的最后一个数据项(如果存在), 从存储缓冲区中刷出到内存的时间点. 这两种时间点分别对应了调用刷出和返回刷出动作. 令Σ_cal, Σ_ret, Σ_fcal和Σ_fret分别为函数调用动作、函数返回动作、调用刷出动作和返回刷出动作的集合. 一个扩展历史是一个字母表(Σ_cal∪Σ_ret∪Σ_fcal∪Σ_fret)^*上的有穷序列, 它用来表示并发数据结构的行为, 记录了数据结构和客户程序之间的交互以及数据结构和存储缓冲区之间的交互. 我们称eh为标号迁移系统A的一条扩展历史, 如果存在A的一条迹, 且其上的扩展历史为eh. 令ehistory(A)表示标号迁移系统A的扩展历史的集合, 令eh|_i为扩展历史eh在进程P_i的动作集合上的投影.

给定两个扩展历史eh₁和eh₂, 如果对每个进程P_i(1≤i≤n), eh₁|_i=eh₂|_i都成立, 那么称这两个扩展历史是等价的. 给定两个扩展历史eh₁和eh₂, 如果:

● eh₁和eh₂是等价的;

● 存在{1, …, |eh₁|}和{1, …, |eh₂|}之间的一一映射π, 使得对任意的1≤i≤|eh₁|, eh₁(i)=eh₂(π(i))都成立;

● 任取1≤i < j≤|eh₁|, 如果eh₁(i)∈Σ_ret∪Σ_fret且eh₁(j)∈Σ_cal∪Σ_fcal, 则π(i) < π(j)成立.

我们称eh₁是TSO-to-TSO可线性化到扩展历史eh₂的.

给定扩展历史的集合S₁和S₂, 如果对每条扩展历史eh₁∈S₁, 都存在着扩展历史eh₂∈S₂, 使得eh₁是TSO-to-TSO可线性化到eh₂的, 则称S₂是TSO-to-TSO线性化了S₁的. 给定并发数据结构L₁和L₂, 如果ehistory($ [[ $L₂, n$ ]] $_tt)是TSO-to-TSO线性化了ehistory($ [[ $L₁, n$ ]] $_tt)的, 称L₂在n进程下TSO-to-TSO线性化了L₁.

一条k-扩展历史是一条包含不超过k个动作的扩展历史. 给定数字k和标号迁移系统A, 令k-ehistory(A)表示标号迁移系统A上的k-扩展历史集合. 我们提出了k-限界TSO-to-TSO可线性化这个概念, 它只考虑k-扩展历史, 是TSO-to-TSO可线性化的一个限界且可判定(在后面章节证明)的子类. 它的定义如下:

定义1(k-限界TSO-to-TSO可线性化). 给定并发数据结构L和L′, 如果对每条k-扩展历史eh∈k-ehistory($ [[ $L, n$ ]] $_tt), 都存在k-扩展历史eh′∈k-ehistory($ [[ $L′, n$ ]] $_tt), 使得eh是TSO-to-TSO可线性化到eh′的, 那么我们称L′在n进程下k-限界TSO-to-TSO线性化了L.

3.2 (限界)TSO-to-SC可线性化

TSO-to-SC可线性化^[12]是可线性化在TSO内存模型下的另一个变种, 它也满足抽象定理. 它关联了一个运行在TSO内存模型下的并发数据结构以及一个运行在SC内存模型上的数据结构的抽象实现. 一条历史是一个函数调用动作和函数返回动作的序列. TSO-to-SC可线性化使用历史来表示并发数据结构的行为. 我们称h为标号迁移系统A的一条历史, 如果存在A的一条迹, 且其上的历史为h. 令history(A)为标号迁移系统A的历史的集合.

给定历史h₁和h₂, 如果:

● h₁和h₂是等价的;

● 存在{1, …, |h₁|}和{1, …, |h₂|}之间的一一映射π, 使得对任意的1≤i≤|h₁|, h₁(i)=h₂(π(i))都成立;

● 取1≤i < j≤|eh₁|, 如果eh₁(i)∈Σ_ret且eh₁(j)∈Σ_cal, 则π(i) < π(j)成立.

那么称h₁是TSO-to-SC可线性化到h₂的.

给定并发数据结构L₁和L₂, 如果对每一条历史h₁∈history($ [[ $L₁, n$ ]] $_tt), 存在历史h₂∈history($ [[ $L₂, n$ ]] $_sc), 使得h₁是TSO-to-SC可线性化到h₂的, 那么称L₂在n进程下TSO-to-SC线性化了L₁.

一条k-历史是一条包含不超过k个动作的历史. 给定数字k和标号迁移系统A, 令k-history(A)表示标号迁移系统A上的k-历史集合. 文献[18]提出了k-限界TSO-to-SC可线性化, 它只考虑k-历史, 是TSO-to-SC的一个限界且可判定^[18]的子类. 它的定义如下:

定义2(k-限界TSO-to-SC可线性化)^[18]. 给定并发数据结构L和L′, 如果对每条k-历史h∈k-ehistory($ [[ $L, n$ ]] $_tt), 都存在k-历史h′∈k-ehistory($ [[ $L′, n$ ]] $_sc), 使得h是TSO-to-SC可线性化到h′的, 那么我们称L′在n进程下k-限界TSO-to-SC线性化了L.

3.3 (限界)TSO可线性化

TSO可线性化^[13]是可线性化在TSO内存模型下的另一个变种. 和TSO-to-TSO可线性化以及TSO-to-SC可线性化不同的是, TSO可线性化并不满足抽象定理. 给定函数返回动作return(i₁, m₁, a₁)和函数调用动作call(i₂, m₂, a₂), 如果i₁=i₂且m₁=m₂, 则称这两个动作配对. 一条顺序历史是一条以函数调用开始, 并且除了最后一个动作之外, 每个函数调用之后紧接着配对的函数返回动作, 而每个函数返回动作之后紧接着函数调用动作的历史. TSO可线性化将一个运行在TSO内存模型下的并发数据结构和其顺序规约关联起来, 后者是顺序历史的集合.

本质上, TSO可线性化使用函数调用动作和调用刷出动作来表示并发数据结构的行为. 给定一个扩展历史eh及函数返回动作eh(j₁)=return(i, m, a)和返回刷出动作eh(j₂)=flushReturn(i), 如果存在自然数g, 使得在eh|_i上, eh(j₁)是第g个函数返回动作, 而eh(j₂)是第g个返回刷出动作, 则称这两个动作配对. 给定扩展历史eh, 令Trans(eh)是通过先删除函数返回和调用刷出动作, 再将返回刷出动作转化为配对的函数返回动作所得到的历史. Trans(eh)将一条扩展历史转化为一条“对应的历史”. TSO可线性化使用通过Trans转化扩展历史所得到的历史集合来表示并发数据结构的行为.

给定历史h, 令complete(h)为h的包含配对的函数调用动作和函数返回动作的最大子序列. 一条历史中的一个操作e包含一对函数调用动作inv(e)以及之后配对的函数返回动作res(e). 一个顺序规约是一个对前缀封闭的顺序历史的集合. 给定扩展历史eh和顺序规约Spec, 如果存在一条顺序历史s∈Spec, 并且Trans(eh)可以通过添加零个或若干个函数返回操作被扩展为一条历史h′, 使得:

● complete(h′)和s是等价的;

● 对Trans(eh)上的每一对操作e₁和e₂, 如果在Trans(eh)中, res(e₁)先于inv(e₂)发生, 则在s中, res(e₁)也先于inv(e₂)发生.

称eh是TSO可线性化到Spec的.

给定并发数据结构L和顺序规约Spec, 如果对任意扩展历史eh∈ehistory($ [[ $L, n$ ]] $_tt), eh都是TSO可线性化到顺序规约Spec的, 则称L在n进程下TSO可线性化到顺序规约Spec.

我们提出了k-限界TSO可线性化这个概念, 它只考察限界的扩展历史, 是TSO可线性化的一个限界且可判定(在后面章节证明)的子类. 它的定义如下:

定义3(k-限界TSO可线性化). 给定并发数据结构L和顺序规约Spec, 如果对每条满足Trans(eh)≤k的扩展历史eh∈ehistory($ [[ $L, n$ ]] $_tt), eh都是TSO可线性化到Spec的, 那么称L在n进程下k-限界TSO可线性化到Spec.

需要注意的是, 尽管k-限界TSO-to-TSO可线性化、k-限界TSO-to-SC可线性化和k-限界TSO可线性化只考虑限界数目的函数调用、函数返回、调用刷出和返回刷出动作, 但在每一对函数调用和函数返回之间可能发生的动作数目是不限的, 进而使用的存储缓冲区大小是不限的. 因此, 对这3个TSO内存模型下可线性化的限界版本的验证需要对无穷状态标号迁移系统(操作语义)进行验证, 是非平凡的.

4 TSO内存模型下可线性化的3个限界版本的验证思路

本节给出验证TSO内存模型下可线性化的3个限界版本(k-限界TSO-to-TSO可线性化、k-限界TSO-to-SC可线性化和k-限界TSO可线性化)的验证思路. 我们将验证两个并发数据结构符合k-限界TSO-to- TSO可线性化和k-限界TSO-to-SC可线性化问题, 以及验证并发数据结构k-限界TSO可线性化到正则的顺序规约这3个问题归约到验证两个k-扩展历史集合符合TSO-to-TSO可线性化问题, 从而以一种统一的方法来完成对TSO内存模型下可线性化的3个限界版本的验证. 注意: 在考虑k-限界TSO可线性化的可判定性问题时, 假定顺序规约是正则的.

● 统一的验证方法

我们通过如下两个步骤完成针对并发数据结构以及正则顺序规约之间的k-限界TSO-to-TSO可线性化、k-限界TSO-to-SC可线性化和k-限界TSO可线性化的验证.

(1) 在第1步, 构造出两个限界长度(限界的长度为k或k+n)扩展历史集合S₁和S₂. 由于函数名集合有穷、进程数目有穷且数据域有穷, 所有可能的k-扩展历史集合和k+n-扩展历史集合(不管是否属于S₁和S₂)都是有穷集合, 因此S₁和S₂也是有穷集合;

(2) 在第2步, 依据定义1以如下方式检测S₂是否TSO-to-TSO线性化了S₁: 对每一对扩展历史eh∈S₁和eh′∈S₂, 显然它们之间的一一映射的数目是有穷的, 通过枚举这些映射并检测是否保留了特定动作之间的序, 我们可以判定eh是否TSO-to-TSO可线性化到eh′. 通过对S₁中的每条扩展历史, 寻找S₂中是否有与其满足TSO-to-TSO可线性化关系的扩展历史, 我们可以判定S₂是否k-限界TSO-to-TSO线性化了S₁. 由于S₁和S₂都是有穷集合, 因此第2步的计算一定终止.

当分别验证并发数据结构以及正则顺序规约之间的k-限界TSO-to-TSO可线性化、k-限界TSO-to-SC可线性化和k-限界TSO可线性化时, 需要叙述此时集合S₁和S₂的定义, 以及如何构造这两个集合. 我们还需要确保对这两个集合的构造过程一定终止.

● 验证k-限界TSO-to-TSO可线性化

在验证两个并发数据结构是否符合k-限界TSO-to-TSO可线性化时, 集合S₁和S₂分别是k-ehistory($ [[ $L, n$ ]] $_tt)和k-ehistory($ [[ $L′, n$ ]] $_tt). 集合S₁可以通过如下方法构造.

(1) 首先, 枚举出所有可能的k-扩展历史的集合(不管是否对应并发数据结构的执行). 由于进程数目、函数名集合和数据域都是有穷的, 所以所有可能的k-扩展历史集合是有穷的, 并且可以通过枚举来构造;

(2) 然后, 对每一条k-扩展历史, 使用某种方法检测其是否属于$ [[ $L, n$ ]] $_tt的某条实际执行. 通过反复使用这种方法判定每一条可能的k-扩展历史, 我们得到了$ [[ $L, n$ ]] $_tt的实际的k-扩展历史集合.

集合S₂可以通过类似的方法处理并发数据结构L′来构造.

判定一条特定的扩展历史是否属于并发数据结构的实际执行是较为复杂的, 我们将在第5节−第7节详细叙述判定方法.

● 判定k-限界TSO-to-SC可线性化

由定义2可以推导出, n进程下并发数据结构L′是k-限界TSO-to-SC线性化了并发数据结构L的, 当且仅当k-history($ [[ $L′, n$ ]] $_sc)是TSO-to-TSO线性化了k-history($ [[ $L, n$ ]] $_tt)的. 这里需要注意的是, 一条历史同时也是一条扩展历史, 因此在两条历史之间也有着TSO-to-TSO可线性化关系. 因此, 验证两个并发数据结构是否符合k-限界TSO-to-SC可线性化时, 集合S₁和S₂分别是k-history($ [[ $L, n$ ]] $_tt)和k-history($ [[ $L′, n$ ]] $_sc).

由于每个调用刷出或返回刷出动作都来自于一个之前发生的函数调用或函数返回动作, 如果扩展历史eh在函数调用动作和函数返回动作上的投影的长度为k, 则原扩展历史最长有2k. 因此, 可以通过如下方法计算出S₁: 先依照之前的方法计算出$ [[ $L, n$ ]] $_tt的长度不超过2k的扩展历史的集合, 再将这些扩展历史投影到函数调用动作和函数返回动作上, 筛选出长度不超过k的历史的集合.

$ [[ $L′, n$ ]] $_sc使用有穷的内存单元集合、有穷的函数名集合、有穷的控制状态集合、限界的进程数目以及有穷的数据域, 并且没有实际使用存储缓冲区. 因此, $ [[ $L′, n$ ]] $_sc是一个有穷状态的标号迁移系统. 通过将$ [[ $L′, n$ ]] $_sc中的非函数调用和非函数返回动作都转化为空迁移, 我们可以证明, history($ [[ $L′, n$ ]] $_sc)是一个正则语言. 由于使用同一个函数名集合、进程集合和数据域的可能的k-历史集合是有穷的, 进而是正则的, 所以可以通过枚举计算出来. 通过计算这两个正则语言的交, 可以得到S₂=k-history($ [[ $L′, n$ ]] $_sc), 它是一个有穷且正则的集合.

● 判定k-限界TSO可线性化

给定标号迁移系统A, 令k-transHistory(A)为这样的历史h的集合: 存在扩展历史eh∈ehistory(A), 使得|Trans(eh)|≤k, 且h=Trans(eh). 由定义3可知: n进程下并发数据结构L是k-限界TSO可线性化到正则的顺序规约Spec的, 当且仅当对k-transHistory($ [[ $L, n$ ]] $_tt)中的每条历史h, 都存在一条顺序历史s∈Spec, h可以通过先添加零个或若干个函数返回动作, 再去掉不配对的函数调用动作得到历史h′, 使得h′是TSO-to-TSO可线性化到s的.

给定历史集合S, 令k-history(S)表示S中k-历史的集合. 不难证明: n进程下并发数据结构L是k-限界TSO可线性化到顺序规约Spec的, 当且仅当posSet(k-transHistory($ [[ $L, n$ ]] $_tt))(一个集合的集合)中至少一个元素是TSO-to-TSO可线性化到(k+n)-history(Spec)的. 这里的k+n来自于一个长度为k的历史, 最多被添加n个函数返回动作. posSet(k-transHistory($ [[ $L, n$ ]] $_tt))集合的每个元素S是一个历史集合, 且S包含了和k-transHistory($ [[ $L, n$ ]] $_tt)相同数目的历史. S中的每个历史, 是k-transHistory($ [[ $L, n$ ]] $_tt)中的某个历史通过添加零个或若干个函数返回动作, 再去掉不配对的函数调用动作得到的. 而且, k-transHistory($ [[ $L, n$ ]] $_tt)中的每个历史也能通过添加若干调用, 再去掉若干返回的方式对应到S中的某条历史. 因此, 验证并发数据结构L是否k-限界TSO可线性化到正则顺序规约Spec时, 我们进行多次TSO-to-TSO可线性化验证, 每次验证使用的集合S₁和S₂分别是posSet(k-transHistory($ [[ $L, n$ ]] $_tt))的一个元素和(k+n)-history(Spec).

每个返回刷出动作来自于之前的一个函数返回动作, 进而关联到之前的一个函数调用动作; 每个返回刷出动作发生前, 对应的调用刷出动作一定已经发生; 一个调用刷出动作来自于之前的一个函数调用动作. 因此, 如果扩展历史eh在函数调用动作和返回刷出动作上的投影的长度为k, 则原扩展历史最长有3k. 可以通过如下方法计算出k-transHistory($ [[ $L, n$ ]] $_tt): 先计算出$ [[ $L, n$ ]] $_tt的长度不超过3k的扩展历史的集合, 然后依次进行Tran处理, 保留Trans处理后长度不超过k的结果. 之后, 通过枚举k-transHistory($ [[ $L, n$ ]] $_tt)中每个历史可能的添加函数返回和删除无配对的函数调用的方式, 我们就得到了S₁=posSet(k-transHistory($ [[ $L, n$ ]] $_tt)).

因为k-transHistory($ [[ $L, n$ ]] $_tt)中只有有穷数目的历史, 且添加的函数返回动作的函数名集合、进程集合和数据域都是有穷的, 所以这个计算过程是终止的. 由于函数名集合、进程集合和数据域都有穷, 可能的(k+n)-历史的集合是有穷的, 进而是正则的, 可以通过枚举计算出来. 因此, 通过计算这个集合和Spec的交, 可以构造S₂=k-history(Spec), 这个集合是有穷的, 也是正则的.

5 修改后的操作语义

根据第4节中的思路, 我们需要解决判定TSO内存模型下并发数据结构是否有着一条特定的扩展历史的问题. 为此, 在后面章节中参考了文献[8]的思路, 将操作语义和易失通道机器关联起来. 文献[8]中的方法未涉及函数调用、函数返回、调用刷出和返回刷出动作. 处理函数调用和函数返回动作的难点在于, $ [[ $L, n$ ]] $_tt中的一个函数调用或函数返回动作会同时完成两个任务: 一个任务是将一个函数调用或函数返回标记放入对应进程的存储缓冲区, 一个任务是修改对应进程的控制状态.

本节提出了如何修改原有的客户程序和并发数据结构, 提出了新的内存模型及其操作语义, 它使用“刷出”动作和cas动作来对应扩展历史中的函数调用、函数返回、调用刷出和返回刷出动作. 我们修改后的内存模型和操作语义与$ [[ $L, n$ ]] $_tt有着相同的扩展历史集合, 因此, 判断操作语义是否存在一条特定的扩展历史这个问题, 在修改后的操作语义和$ [[ $L, n$ ]] $_tt上是等价的问题. 而且由于函数调用、函数返回、调用刷出和返回刷出动作都被转化为刷出和cas动作, 使得我们更易于使用文献[8]的思路, 将这样的操作语义和易失通道机器关联起来.

5.1 针对调用刷出和返回刷出修改操作语义

令z_f是一个新的内存单元. 我们希望将$ [[ $L, n$ ]] $_tt中的一个同时完成两个任务的函数调用动作变成紧邻的两个动作, 其中, 前者是一个只影响对应进程控制状态的“纯粹”的函数调用动作, 后者是一个对z_f的写动作.$ [[ $L, n$ ]] $_tt中, 函数调用动作的向存储缓冲区中放入函数调用标号的任务, 在新的操作语义中, 实际上由对z_f的写动作完成. 当z_f的写从存储缓冲区中刷出到内存中时, 新的操作语义不是发出刷出动作, 而是发出调用刷出动作. 通过这样的方式, 在新的操作语义中, 我们用对z_f的写和刷出来对应了$ [[ $L, n$ ]] $_tt中的函数调用动作对存储缓冲区的影响.

在新的操作语义中, 我们修改了客户程序和并发数据结构, 添加了对z_f的写动作. 确切地说, 给定一个并发数据结构L=(X_L, M_L, D_L, Q_L, →_L), 新的操作语义是一个标号迁移系统$ [[ $C_f(Mod(L)), n$ ]] $_f. 这里的C_f是一个映射函数, 它将每个进程P_i映射到一个修改后的最一般客户Mod(MGC). $ [[ $C_f(Mod(L)), n$ ]] $_f中改进的最一般客户使用修改后的并发数据结构Mod(L), 其中,

● 修改后的最一般客户Mode(MGC)是一个五元组({z_f}, M, D_L∪{call, ret}, {in_clt, inl_ib1, in_lib2}, →).

我们扩展了原有的最一般客户, 在函数返回动作发生后加入了一个对z_f的写动作, 写入一个函数返回标记. 迁移关系→被定义为→={(in_clt, call(m, a), in_lib1), (in_lib1, return(m, a), in_lib2), (in_lib2, write(z_f, ret), in_clt)|m∈M, a∈D_L};

● 修改后的并发数据结构Mod(L)是一个五元组(X_L∪{z_f}, M, D_L∪{call, ret}, Q_L∪Q′, $ { \to '_L} $).

修改后的并发数据结构在每个函数调用动作之后, 先执行一个对z_f的写动作, 写入函数调用标记. 确切地说, 迁移关系$ { \to '_L} $是通过对迁移关系→_L进行如下修改而得到的: 任取a∈D_L, m∈M且q∈Q_L, 如果有着$i{s_{(m, a)}}{\xrightarrow{{act}}_L}{q_1}$迁移关系, 则将其修改为$i{s_{(m, a)}}{\xrightarrow{{write({z_f}, call)}}^\prime }_L{q_{(m, a, {q_1})}}$和${q_{(m, a, {q_1})}}{\xrightarrow{{act}}^\prime }_L{q_1}$. 状态集合Q′就是这些新加入的中间状态${q_{(m, a, {q_1})}}$的集合. 给定并发数据结构L的原操作语义$ [[ $C(L), n$ ]] $_tt=(Conf_tt, Σ_tt, →_tt, InitConf_tt), 修改后的操作语义$ [[ $C_f(Mod(L)), n$ ]] $_f仍是一个标号迁移系统(Conf_f, Σ_f, →_f, InitConf_f). 这里的下标f表明, 这个操作语义是为了解决调用刷出和返回刷出动作而提出的. 状态集合Conf_f是通过向状态集合Conf_tt中加入内存单元z_f并修改最一般客户和并发数据结构的控制状态(如上面所述)得到的, 迁移标号集合Σ_f是通过向迁移标号集合Σ_tt中加入内存单元z_f的写得到的, 格局InitConf_f是通过向格局InitConf_tt中加入内存单元z_f的求值得到的.

迁移关系→_f是通过对迁移关系→_tt进行如下修改得到的.

● 在进行函数调用和函数返回迁移时, 只修改当前进程的控制状态, 而不将函数调用标记或函数返回标记放入进程的存储缓冲区. 以函数调用迁移为例, $ [[ $C_f(Mod(L)), n$ ]] $_f中, 对函数调用和函数返回的迁移规则如下, 我们可以看到, 只修改了进程的控制状态:

$ \frac{{p(i) = i{n_{clt}}}}{{(p, d, u){{\xrightarrow{{call(i, m, a)}}}_t}(p[i:(i{s_{(m, a)}}, i{n_{lib1}})], d, u)}}, {\text{ }}\frac{{p(i) = (f{s_{(m, a)}}, i{n_{lib1}})}}{{(p, d, u){{\xrightarrow{{return(i, m, a)}}}_t}(p[i:i{n_{lib2}}], d, u)}}; $

● 修改$ [[ $L, n$ ]] $_tt中调用刷出、返回刷出和刷出迁移的迁移规则. 当存储缓冲区中z_f的写刷出时, 如果对应的数据是call, 则发动调用刷出迁移; 如果对应的数据是ret, 则发动返回刷出迁移. 具体的迁移规则如下:

$ \frac{{u(i) = l \cdot ({z_f}, call)}}{{(p, d, u){{\xrightarrow{{flushCall(i)}}}_f}(p, d[{z_f}:call], u[i:l])}}, {\text{ }}\frac{{u(i) = l \cdot ({z_f}, ret)}}{{(p, d, u){{\xrightarrow{{flush{Re} turn(i)}}}_f}(p, d[{z_f}:ret], u[i:l])}}; $

● 当存储缓冲区中其他内存单元的写刷出时, 发动刷出迁移:

$ \frac{{u(i) = l \cdot (x, a), x \ne {z_f}}}{{(p, d, u){{\xrightarrow{{flush(i, x, a)}}}_f}(p, d[x:a], u[i:l])}}. $

下面的引理说明了操作语义$ [[ $C_f(Mod(L)), n$ ]] $_f和操作语义$ [[ $L, n$ ]] $_tt有着相同的扩展历史集合. 这个引理的证明可以在本文的技术报告版本^[29]中找到.

引理1. ehistory($ [[ $C_f(Mod(L)), n$ ]] $_f)=ehistory($ [[ $L, n$ ]] $_tt).

5.2 针对函数调用和函数返回修改内存模型和操作语义

在原本的TSO内存模型下, 使用读、写或cas动作对应函数调用和函数返回动作有着固有的困难, 这个困难来自于一个进程无法“及时观察”到其他进程做了函数调用或函数返回动作. 对此的解释如下: 由于一个进程P的函数调用和函数返回动作不影响存储缓冲区和内存, 因此其他进程是观测不到进程P的函数调用或函数返回动作的. 如果通过在进程P的函数调用和函数返回动作之后加入对某个内存单元x的写动作来产生其他进程可见的动作来完成这个目标, 则这个写动作需要在进程P的存储缓冲区中的其他数据项都被刷出后才能被刷出. 假定我们希望复现这样的执行, 某个进程P在执行函数调用之前, 其存储缓冲区已经有一个某内存单元y的写, 这个进程在之后的执行中从来没有刷出这个对y的写, 而且正因为这些y的写一直没刷出, 另一个进程P′的函数才能两次返回特定值(假定这两次函数返回之间执行了cas指令). 当我们尝试复现历史时, 会发现复现的历史“不真实”, 因为在复现的历史中进程P对x的写一定在进程P′的第1个函数返回之后才可能刷出到内存, 这导致在复现的历史中进程P的这个函数调用的位置在进程P′的第1个函数返回之后.如果通过在进程P的函数调用和函数返回动作之后加入cas动作来完成这个目标, 由于cas动作会清空存储缓冲区, 所以同样无法复现上面提到的执行. 为了解决这个问题, 文献[18]修改了内存模型本身. 在修改后的内存模型中, 我们将函数调用和函数返回动作与特定的cas动作“绑定”在一起. 确切地说, 引入了一个“观察者”进程和一个新的内存单元z_w, 观察者进程不断地用cas动作修改z_w, 修改的值是非确定猜测的; 内存模型要求在观察者进程每次对z_w的cas动作后, 下一个动作必须是对应的函数调用或函数返回动作.只有观察者进程修改z_w的cas动作必须被对应的进程的函数调用或函数返回动作响应, 而其他内存单元的刷出和cas动作不会让其他进程进行响应. 本节叙述如何通过这个思想来修改第5.1节构造的操作语义.

令markedVal(M, D_L, n)={call(i, m, a}, return(i, m, a)|1≤i≤n, a∈D_L, m∈M}为z_w做cas动作使用的值, 为了对应函数调用和函数返回动作, 这些值本身就记录了函数调用或函数返回. 给定并发数据结构L=(X_L, M_L, D_L, Q_L, →_L), 我们修改并发系统如下.

● 进程P₁到P_n仍然运行修改后的最一般客户;

● 观察者进程P_n+1运行如下客户程序: Cmarked=({z_w}, M, markedVal(M, D_L, n), {q_wit}, →_wit), 这里, 迁移关系→_wit定义为{q_wit, cas_suc(z_w, _, a), q_wit|a∈markedVal(M, D_L, n)}. 在观察者进程中, 我们只考虑成功的cas动作, 可以认为另有一个陷阱状态, 当cas动作失败时, 观察者进程进入陷阱状态并终止执行.

令$ [[ $C_f(Mod(L)), n$ ]] $_f=(Conf_f, Σ_f, →_f, InitConf_f)为第5.1节修改后的操作语义. 本节提出的修改后的操作语义$ [[ $Clt_f(Mod(L)), n+1$ ]] $_b是一个标号迁移系统(Conf_b, Σ_b, →_b, InitConf_b). 这里的Clt_f是一个映射函数, 它将进程P₁到P_n映射到修改后的最一般客户, 将进程P_n+1映射到C_marked. Conf_b中的一个格局是一个四元组(p, d, u, mak), 其中, 三元组(p, d, u)是通过向Conf_f中的某个格局添加内存单元z_w和观察者进程的控制状态得到的, 而mak是一个取自{⊥}∪markedVal(M, D_L, n)集合中的元素, 它用来确保观察者进程的每个cas动作都被绑定到对应的函数调用或函数返回动作. ⊥是一个特定的值. 字母表Σ_b是通过向字母表Σ_f中加入z_w的动作而得到的. 初始格局InitConf_b是通过向格局InitConf_f中加入z_w的求值和观察者进程的控制状态而得到的. 迁移关系→_b是通过以如下方式改动迁移关系→_f而得到的.

● 进程P_n+1, 即观察者进程, 对应的迁移规则如下:

$ \frac{{p(n + 1) = {q_{wit}}, {q_{wit}}{{\xrightarrow{{cas\_suc({z_w}, a, b)}}}_{wit}}{q_{wit}}, a, b \in markedVal(\mathcal{M}, {\mathcal{D}_\mathcal{L}}, n), d({z_w}) = a, u(n + 1) = \varepsilon }}{{(p, d, u, \bot ){{\xrightarrow{{cas(n + 1, {z_w}, a, b)}}}_b}(p, d[{z_w}:b], u, b)}}. $

这里, →_wit是观察者进程的客户程序C_marked的迁移关系.

注意, 只有这种迁移会将当前格局的第4个元组从⊥修改为markedVal(M, D_L, n)中的值;

● 除函数调用、函数返回动作之外, 进程P₁到P_n其他的迁移规则不变, 且这些迁移只能在当前格局的第4个元组为⊥时发生;

● 一个函数调用迁移call(i, m, a)只有当格局的第4个元组的值为call(i, m, a)时才能发生, 并且这个函数调用迁移将会把这个元组的值置为⊥. 函数调用动作的迁移规则如下:

$ \frac{{p(i) = i{n_{clt}}}}{{(p, d, u, call(i, m, a)){{\xrightarrow{{call(i, m, a)}}}_b}(p[i:(i{s_{(m, a)}}, i{n_{lib1}})], d, u, \bot )}}. $

函数返回动作的迁移规则类似.

通过对当前格局的第4个元组的要求, 我们将观察者进程的对z_w的cas动作和进程P₁到P_n的函数调用和函数返回动作绑定在了一起. 下面引理说明$ [[ $Clt_f(Mod(L)), n+1$ ]] $_b和$ [[ $C_f(Mod(L)), n$ ]] $_f有着相同的扩展历史集合.这个引理的证明可以在本文的技术报告版本^[29]中找到.

引理2. ehistory($ [[ $Clt_f(Mod(L)), n+1$ ]] $_b)=ehistory($ [[ $C_f(Mod(L)), n$ ]] $_f).

6 构造对应特定扩展历史的通道机器

本节引入(易失)通道机器的定义. 之后, 我们先用一个例子直观说明如何使用通道机器模拟$ [[ $Clt_f(Mod(L)), n+1$ ]] $_b中对应特定扩展历史的执行中特定进程的行为, 然后给出这样的通道机器的构造.

6.1 (易失)通道机器的定义

一个经典的通道机器包含了有穷的控制状态和一个容量无界的通道, 通道机器的一步迁移在修改控制状态的同时, 也可以向通道中放入数据或者从通道中取出数据. 一个易失通道是一个在任意时刻都可能有任意数量的数据从通道中丢失的通道, 且这个数据丢失过程不会对通道机器有任何通知. 一个易失通道机器是一个使用易失通道的通道机器. 文献[8]在如下几个方面扩展了(易失)通道机器的定义.

● 每一个迁移中加入了正则卫士表达式, 判断某个通道的内容是否属于一个正则语言;

● 在每一个迁移发生之前, 允许将某个通道的元素进行替换;

● 引入了强符号的概念. 强符号是通道内容的一部分, 它们在迁移过程中是不会丢失的, 并且一个通道内的强符号数目有着上界.

在文献[18]中, 我们稍微扩展了文献[8]中(易失)通道机器的定义, 允许使用多种强符号, 并对每个通道里的每种强符号的数目分别限界. 本文使用文献[18]中的(易失)通道机器定义.

一个正则卫士表达式形如c∈L, 这里, c是一个通道名, L是一个正则集合. 给定一个序列l, 如果u∈L, 则称u‘c∈L成立. 为了表示的简便, 我们把正则卫士表达式c∈Σ^*aΣ^*简写为a∈c, 把正则卫士表达式c∈ε简写为c=ε, 把正则卫士表达式c∈Σ^*简写为c: Σ. 一个通道集合C上的正则卫士表达式为每个通道c∈C关联一个正则卫士表达式. 我们使用Guard(C)表示通道集合C上的正则卫士表达式的集合. 关系‘也被扩展到Guard(C)上.给定函数u为每个通道分配内容以及g∈Guard(C), 如果对每个通道c∈C, u(c)‘g(c)都成立, 则称u‘g成立.

通道c上有3种操作: nop操作不修改通道, c[σ]!a操作先依据替换σ进行元素替换再向通道中插入数据a, c?a操作从通道中取出数据a. 这里, σ是一个元素替换, 当σ把每个元素替换为自己时, 将此时的c[σ]!a操作简写为c!a. 我们为每一种通道操作定义一个序列之间的关系如下: 任取有穷序列u和u′, 如果u=u′, 则$ [[ $nop$ ]] $(u, u′)成立; 如果u′=a·u[σ], 则$ [[ $c[σ]!a$ ]] $(u, u′)成立; 如果u=u′·a, 则$ [[ $c?a$ ]] $(u, u′)成立. 一个通道集合C上的通道操作为每个通道c∈C关联一个通道操作. 我们使用Op(C)表示通道集合C上的通道操作的集合. 关系$ [[ $·$ ]] $也被扩展到Op(C)上. 给定为每个通道分配内容的函数u和u′以及通道集合C上的通道操作op∈Op(C), 如果对每个通道, $ [[ $op(c)$ ]] $(u(c), u′(c))都成立, 则$ [[ $op$ ]] $(u, u′)成立.

一个通道机器M被定义为一个五元组M=(Q, CH, Σ_CH, Λ, Δ), 其中, Q是一个有穷的状态集合, CH是一个有穷的通道名集合, Σ_CH是通道内容的有穷字母表, Λ是有穷的迁移标号集合, Δ⊆Q×(Λ∪{ε})×Guard(CH)×Op(CH)×Q是有穷的迁移关系集合. 为了阅读的方便, 我们把(q, l, g, op, q′)∈Δ写为$q\xrightarrow{{l, g, op}}q'$. 通道机器M的操作语义是一个标号迁移系统(Conf, Λ∪{ε}, →_M, initConf). 每个格局是一个二元组(q, u), 其中, q∈Q且u: CH→$\varSigma _{CH}^*$. 如果存在通道集合CH上的通道操作op, 使得$q\xrightarrow{{l, g, op}}q'$, u‘g且$ [[ $op$ ]] $(u, u′)都成立, 则迁移((q, u), l, (q′, u′)))属于迁移关系→_M.

给定有穷序列l和l′, 如果可以通过删除l′的零个或若干个元素得到l, 则称l是l′的子串. 令S=〈SET₁, …, SET_m〉为一个向量, 其中每个SET_i都是一个有穷集合, 代表一种强符号, 且m是一个正整数. 令K=〈k₁, …, k_m〉为一个向量, 其中每个元素都是一个自然数, 代表对应种类的强符号在一个通道中的数目限制. 下面定义带有强符号约束(S, K)的易失通道机器, 称为(S, K)-易失通道机器. 给定u, u′: CH→$\varSigma _{CH}^*$, 如果对任意通道c∈CH和1≤i≤m, u(c)是u′(c)的子串, u(c)↑_S(i)=u′(c)↑_S(i), 且u(c)在S(i)上的投影的长度小于等于K(i), 则称u和u′满足关系$u \preccurlyeq _S^Ku'$. (S, K)-易失通道机器是使用易失通道并遵守强符号约束(S, K)的通道机器, 它的操作语义是一个标号迁移系统(Conf, Λ∪{ε}, $ { \to '_M} $, initConf). 给定q, q′∈Q, u, u′: CH→$\varSigma _{CH}^*$和l∈Λ∪{ε}, 如果存在v, v′: CH→$\varSigma _{CH}^*$, 使得$v \preccurlyeq _S^Ku$, ((q, v), l, (q′, v′))∈$ { \to '_M} $和$u' \preccurlyeq _S^Kv'$都成立, 则迁移((q, u), l, (q′, u′))属于迁移关系$ { \to '_M} $.

给定通道机器M的状态q和q′, 如果将M视为(S, K)-易失通道机器, 我们称其在操作语义上从格局(q, c_init)到格局(q′, c_init)的迹的集合为$LT_{q, q'}^{S, K}(M)$. 这里, c_init的作用是将每个通道名映射到ε. (S, K)-易失通道机器的控制状态可达问题是指: 给定通道机器M、强符号限制(S, K)和状态q和q′, 判定$LT_{q, q'}^{S, K}(M)$是否为空集. 文献[8]说明了控制状态可达问题是可判定的, 其考虑的易失通道机器相当于S只包含一个集合时的情况. 使用类似的思想不难证明, (S, K)-易失通道机器的控制状态可达问题是可判定的. 将M视为(S, K)-易失通道机器时, 我们称其在操作语义上从格局(q, c_init)到格局(q′, c_init), 且通道不丢失任何内容的迹的集合为$T_{q, q'}^{S, K}(M)$. 或者说, $T_{q, q'}^{S, K}(M)$是“非易失通道”版本的$LT_{q, q'}^{S, K}(M)$.

给定两个采用不同通道的通道机器M=(Q, CH, Σ_CH, Λ, Δ)和M′=(Q′, CH′, Σ_CH, Λ, Δ′), 即CH∩CH′=∅, M和M′的乘积被定义为另一个通道机器M⊗M′=(Q×Q′, CH∪CH′, Σ_CH, Λ, Δ″). Δ″中的一步非ε迁移会同时完成M和M′中使用同样标号的两个迁移, 此时, 新的卫士表达式是这两个卫士表达式的交, 新的通道操作正好包含这两个迁移的通道操作; Δ″中的一步ε迁移完成M或M′中的一步ε迁移. 文献[8]中给出了如下引理, 说明了两个易失通道机器乘积的LT集合等于两个易失通道机器各自的LT集合的交:

引理3. 给定$ {q_1}, {q'_1}, {q_2}, {q'_2} $以及S和K, $LT_{q, q'}^{S, K}({M_1} \otimes {M_2}) = LT_{{q_1}, {{q'}_1}}^{S, K}({M_1}) \cap LT_{{q_1}, {{q'}_1}}^{S, K}({M_1}).$

这里, q=(q₁, q₂)且$ q' = ({q'_1}, {q'_2}) $.

6.2 使用通道机器模拟$ [[ $Cltf(Mod(L)), n+1$ ]] $_b执行一条特定的扩展历史

本节通过一个例子说明如何使用通道机器模拟并发系统对应一条特定的扩展历史的执行. 给定并发系统$ [[ $Clt_f(Mod(L)), n+1$ ]] $_b的一条k-扩展历史eh, 我们为每个进程P_i构造一个通道机器$M_i^{eh}$来模拟进程P_i的行为. 下一节将证明易失通道机器$M_1^{eh - w} \otimes ... \otimes M_{n + 1}^{eh - w}$模拟了并发系统对应eh的执行. 这里, $M_i^{eh - w}$是从$M_i^{eh}$构造得到的通道机器. $M_i^{eh}$的定义见第6.3节, $M_i^{eh - w}$的定义见第7节.

通道机器$M_i^{eh}$需要包含进程P_i的状态, 包括客户程序状态和并发数据结构状态, 并依据这些状态进行迁移. 为了进行通道机器的同步, $M_i^{eh}$也需要处理其他进程的动作, 为此, 它不断非确定地猜测其他进程的动作. 其他进程的写动作和cas动作都会被猜测为一个对应的写动作. 为了保证$M_i^{eh}$对应的扩展历史一定是eh (或其前缀), 我们向$M_i^{eh}$的状态加入了一个元组来确保这一点. $M_i^{eh}$只有一个通道, 对应了进程P_i的存储缓冲区. $M_i^{eh}$在猜测其他进程的写动作时, 也会向通道中放入对应的内存单元和值. 为了保证丢失部分通道内容不影响执行, 通道中的每个元素都包含内存的快照.

$M_i^{eh}$会将进程P_n+1对z_w的cas动作猜测为对应的写动作并向通道写入z_w, 这些写入的z_w被设置为强符号.它们离开通道时将触发刷出迁移, 并且$M_i^{eh}$在下一步的迁移一定是对应的函数调用或函数返回动作(不管这些函数调用和函数返回动作是否属于进程P_i). $M_i^{eh}$在函数调用和函数返回动作后会向通道写入z_f, 也会猜测其他进程对z_f的写动作. 这些写入的z_f也被设置为强符号, 它们离开通道将触发调用刷出或返回刷出迁移. 这就是$M_i^{eh}$捕捉扩展历史的机制.

图 1给出了一个$M_i^{eh}$模拟并发系统中进程P_i执行的例子. 这里, eh是一个包含8个动作的扩展历史, 图 1(a)给出了eh对应的并发系统$ [[ $Clt_f(Mod(L)), 3$ ]] $_b的执行, 而图 1(b)~图 1(d)分别给出了$M_1^{eh}, {\text{ }}M_2^{eh}$和$M_3^{eh}$的对应执行, 其中, 进程P₃是观察者进程.

图 1中的每条执行按照时间顺序从左到右画出动作, 依据属于不同的进程从上到下画动作. 为了强调每一对函数调用和函数返回动作, 我们在每个函数调用和函数返回动作下面画一条竖线, 且用横线连接一对函数调用和函数返回动作对应的竖线. 为了强调每一对调用刷出和返回刷出动作, 在每个调用刷出和返回刷出动作下面画一个圆圈, 且用横线连接一对调用刷出和返回刷出对应的圆圈. 当函数调用、函数返回、调用刷出和返回刷出动作是进程P_i的动作时, 对应的横线画为实线; 当函数调用、函数返回、调用刷出和返回刷出动作来自猜测其他进程的动作时, 画为虚线.

图 1中的术语解释如下: 为了节省空间, 我们用w(x)1表示将x的值写为1的动作, 用r(x)1表示从x读到1的动作, 用f(x)1表示从存储缓冲区中刷出一项且其将x写为1的动作, 用cas(y)1表示使用cas成功地将y的值修改为1的动作. 通道机器$M_i^{eh}$用g(z_f)b₂和g(z_w)a₁分别表示两个猜测的写动作: 前者将z_f的值写为b₂, 后者将z_w的值写为a₁. 可以看到: 一些猜测的写(如g(z_f)b₂)在并发系统的执行中对应写动作(如w(z_f)b₂), 另一些猜测的写(如g(z_w)a₁)在并发系统的执行中对应cas动作(如cas(z_w)a₁). 为了节省空间, 图上用a₁~a₄分别代表向z_w写入的4个函数调用或函数返回的值, 用b₁~b₄分别代表向z_f写下的4个标号, 即a₁=call(1, M₁, _), a₂=call(2, M₂, _), a₃=return(1, M₁, _), a₄=return(2, M₂, _), b₁=b₂=call且b₃=b₄=ret. 需要注意的是: 在图 1(b)~图 1(d)中的动作来自$M_i^{eh}$, 因此每个动作还带有内存快照. 为了理解方便, 我们仍沿用图 1(a)的写法.

我们分别称图 1(a)~图 1(d)中的执行为t, t₁~t₃. 可以看到, 各个进程模拟的执行(即t₁~t₃)和原执行t有着相同的对内存单元修改动作的序列. 这里的内存单元修改指刷出和cas动作, 这里不对两者进行区分. 然而, t₁和t有一点很大的不同在于: t中有多个存储缓冲区, 而t₁只有一个通道. 为了保证相同的内存修改动作的序列, t₁中猜测其他进程动作的写时, 可能会让一些写“提前”发生. 例如: 在t中, P₁中的w(x)1先发生但P₂中的cas(y)1先修改内存; 而在t₁中, 只能先让猜测的对y的写先发生, 这样对y的修改才能先发生.

6.3 通道机器$M_i^{eh}$

本节简述通道机器$M_i^{eh}$的构造. 在本文的技术报告版本^[29]中, 可以找到$M_i^{eh}$的详细定义.

给定一条长度为k的扩展历史eh=α₁·…·α_k, 可以构造一个识别eh的确定型有穷自动机A_eh=(Q_s, Σ_s, →_s, F_s, $ {q_{{s_0}}} $). 这里, $ Q = \{ {q_{{s_0}}}, ..., {q_{{s_k}}}\} $是有穷的状态集合, Σ_s={call(i, m, a), return(i, m, a), flushCall(i), flushReturn(i)|1≤i≤n, a∈D, m∈M}是迁移标号的集合且M和D是对应的函数名集合和数据域, $ {q_{{s_0}}} $是初始状态, $ {F_s} = \{ {q_{{s_k}}}\} $是接收状态的集合, 迁移关系→_s包含迁移${q_{{s_0}}}{\xrightarrow{{{\alpha _1}}}_s}{q_{{s_1}}}, ..., {q_{{s_{k - 1}}}}{\xrightarrow{{{\alpha _k}}}_s}{q_{{s_k}}}$.

给定并发数据结构L=(X_L, M_L, D_L, Q_L, →_L), 令修改后的并发数据结构Mod(L)为五元组(X_L∪{z_f}, M, D_L∪{call, ret}, Q_L∪Q′, $ { \to '_M} $). 令Val是一个为内存单元分配值的函数的集合, 且每个属于Val的函数将X_L中的内存单元映射到D_L中元素, 将z_w映射到{⊥}∪markedVal(M, D_L, n)中的元素, 将z_f映射到{⊥, call, ret}中的元素. 对i≠n+1, 通道机器$M_i^{eh}$定义为五元组$ (Q_i^{eh}, \{ {c_i}\} , \varSigma , \varLambda , \varDelta _i^{eh}) $. $M_i^{eh}$只使用一个通道c_i, 而$Q_i^{eh}$, Σ和Λ定义如下.

● $Q_i^{eh}$=({in_clt, in_lib2}∪((Q_L∪Q′)×{in_lib1})×Val×Val×Q_s×{⊥}∪markedVal(M, D_L, n))是状态的集合, 这里, in_clt, in_lib1和in_lib2是修改后的最一般客户的状态. 一个$Q_i^{eh}$中的状态是一个五元组(q, d_c, d_g, q_s, mak), 其中: q是修改后的最一般客户和修改后的并发数据结构的控制状态; d_c存储一个内存单元求值函数, 表示并发系统当前的内存求值; d_g存储另一个内存单元求值函数, 它是通过使用将通道c_i缓存的所有写更新d_c得到的; q_s是有穷自动机A_eh的状态, 用来记录当前执行产生的扩展历史; mak是一个标记, 用来确保$M_i^{eh}$每次从通道中取出一个z_w的写(来自$M_i^{eh}$猜测进程P_n+1对z_w的cas动作)之后都紧跟着一个对应的函数调用或函数返回动作;

● 通道字母表$ \varSigma = {\varSigma _{{s_1}}} \cup {\varSigma _{{s_2}}} \cup {\varSigma _{{s_3}}} $是3个集合的并集.其中$ {\varSigma _{{s_1}}} $={(n+1, z_w, d}|d∈Val){(j, z_f, d)|1≤j≤n, d∈Val}中的一个元素代表一个猜测的对z_w的写(对应进程P_n+1上对z_w的cas操作), 或者是进程P_i对z_f的写(在函数调用和函数返回之后), 或者是猜测的其他进程对z_f的写. $ {\varSigma _{{s_2}}} $={((j, x, d), #)|1≤j≤n, x∈X_L, d∈Val}中的一个元素代表当前缓存的进程P_i对相应内存单元的最新的写. 而$ {\varSigma _{{s_3}}} = \{ a|(a, \# ) \in {\varSigma _{{s_2}}}\} $中的一个元素代表当前缓存的对相应内存的一个写, 且这个写要么是进程P_i猜测的(其他进程的写), 要么这个写是进程P_i执行的写, 但不是进程P_i对这个内存单元的最新写;

● Λ是迁移标号的集合, 包含写、cas、刷出、函数调用、函数返回、调用刷出、返回刷出和ε迁移. τ动作和读动作对应的迁移的标号都是ε.

$\varDelta _i^{eh} \in Q_i^{eh} \times (\varLambda \cup \{ \varepsilon \} \times Guard(\{ {c_i}\} ) \times Op(\{ {c_i}\} )) \times Q_i^{eh}$是迁移关系. 在本文的技术报告版本^[29]中, 可以找到$\varDelta _i^{eh}$的详细定义. 由于空间所限, 本文只展示如下迁移的构造: 并发数据结构和客户程序对z_f的写、猜测其他进程对z_f的写、调用刷出(来自从通道中取出z_f的写)、猜测进程P_n+1对z_w的写、刷出对z_w的写、函数调用以及猜测函数调用. 任取q∈{in_clt, in_lib2}∪((Q_L∪Q′)×{in_lib1}), q_t∈Q′, d_c, d_g∈Val和q_s∈Q_s:

● 并发数据结构对z_f的写: 令$i{s_{(m, a)}}{\xrightarrow{{write({z_f}, call)}}^\prime }_\mathcal{L}{q_t}$为Mod(L)的迁移, 则:

$ ((i{s_{(m, a)}}, i{n_{lib1}}), {d_c}, {d_g}, {q_s}, \bot ){\xrightarrow{{op, {c_i}:\varSigma , {c_i}!\beta }}_{\varDelta _i^{eh}}}(({q_t}, i{n_{lib1}}), {d_c}, {d'_g}, {q_s}, \bot ). $

这里, ${d'_g}$=d_g[z_f: call], β=(i, z_f, ${d'_g}$), 迁移标号op=write(i, z_f, ${d'_g}$). 注意, 放入通道的每个数据项包含写动作发生的进程号、被修改的内存单元以及一个内存快照. 被修改的内存单元的新值可以从内存快照中读取;

● 客户程序对z_f的写:

$ (i{n_{lib2}}, {d_c}, {d_g}, {q_s}, \bot ){\xrightarrow{{op, {c_i}:\varSigma , {c_i}!\beta }}_{\varDelta _i^{eh}}}(i{n_{clt}}, {d_c}, {d'_g}, {q_s}, \bot ). $

这里, ${d'_g}$=d_g[z_f: ret], β=(i, z_f, ${d'_g}$), 迁移标号op=write(i, z_f, ${d'_g}$);

● $M_i^{eh}$猜测其他进程的一个对z_f的写: 令1≤j≤n, j≠i且a∈{call, ret}, 则:

$ (q, {d_c}, {d_g}, {q_s}, \bot ){\xrightarrow{{op, {c_1}:\varSigma , {c_1}!\beta }}_{\varDelta _i^{eh}}}(q, {d_c}, {d'_g}, {q_s}, \bot ). $

这里, ${d'_g}$=d_g[z_f: a], β=(j, z_f, ${d'_g}$), 迁移标号op=write(j, z_f, ${d'_g}$). 这个猜测不影响$M_i^{eh}$中修改后的并发数据结构或客户程序的控制状态;

● 刷出一个对z_f赋值为call的写, 引发一个调用刷出迁移: 令1≤j≤n, 如果${q_s}{\xrightarrow{{flushCall(j)}}_s}{q'_s}$, 则:

$ (q, {d_c}, {d_g}, {q_s}, \bot ){\xrightarrow{{op, {c_i}:\varSigma , {c_i}?(j, {z_f}, d)}}_{\varDelta _i^{eh}}}(q, d, {d_g}, {q'_s}, \bot ). $

这里, d(z_f)=call, 迁移标号op=flushCall(j);

● $M_i^{eh}$猜测进程P_n+1的一个对z_w的写: 令a∈markedVal(M, D_L, n), 则:

$ (q, {d_c}, {d_g}, {q_s}, \bot ){\xrightarrow{{op, {c_i}:\varSigma , {c_i}!\beta }}_{\varDelta _i^{eh}}}(q, {d_c}, {d'_g}, {q_s}, \bot ). $

这里, ${d'_g}$=d_g[z_w: a], β=(n+1, z_w, ${d'_g}$), 且迁移标号op=write(n+1, z_w, ${d'_g}$). 这个猜测不影响$M_i^{eh}$中修改后的并发数据结构或客户程序的控制状态;

● 刷出通道中缓存的对z_w的一个写: 以这个写将z_w赋值为一个函数调用为例:

$ (q, {d_c}, {d_g}, {q_s}, \bot ){\xrightarrow{{op, {c_i}:\varSigma , {c_i}?(n + 1, {z_w}, d)}}_{\varDelta _i^{eh}}}(q, d, {d_g}, {q_s}, call(j, m, c)). $

这里, d(z_w)=call(j, m, c), 且迁移标号op=flush(n+1, z_w, d). 这个迁移修改了$M_i^{eh}$的状态的第5个元组, 将其设置为一个函数调用的信息;

● 进程P_i做函数调用: 令${q_s}{\xrightarrow{{call(i, m, a)}}_s}{q'_s}$, 则:

$ (i{n_{clt}}, {d_c}, {d_g}, {q_s}, call(i, m, a)){\xrightarrow{{call(i, m, a), {c_i}:\varSigma , nop}}_{\varDelta _i^{eh}}}((i{s_{(m, a)}}, i{n_{lib1}}), {d_c}, {d_g}, {q'_s}, \bot ). $

这里, nop不改变通道c_i的内容. 这个迁移将$M_i^{eh}$的状态的第5个元组赋值为⊥;

● 猜测其他进程的函数调用: 令${q_s}{\xrightarrow{{call(j, m, a)}}_s}{q'_s}$, 1≤j≤n且j≠i, 则:

$ (q, {d_c}, {d_g}, {q_s}, call(j, m, a)){\xrightarrow{{call(j, m, a), {c_i}:\varSigma , nop}}_{\varDelta _i^{eh}}}(q, {d_c}, {d_g}, {q'_s}, \bot ). $

这个迁移将$M_i^{eh}$的状态的第5个元组赋值为⊥.

7 TSO内存模型下可线性化的3种限界版本的可判定性和复杂度

如果把$ [[ $Clt_f(Mod(L)), n+1$ ]] $_b的一条有穷执行e投影到函数调用、函数返回、调用刷出和返回刷出动作集合上, 得到的扩展历史为eh, 并且在e的最后一个格局中所有进程的存储缓冲区都被清空, 那么我们称有穷执行e是$ [[ $Clt_f(Mod(L)), n+1$ ]] $_b的扩展历史eh的标记见证. 引入标记见证的原因是: 这样的执行的开始格局和终止格局都无需考察存储缓冲区的内容, 方便完成从TSO内存模型下可线性化的限界版本到易失通道机器的控制状态可达问题的归约. 下面的引理将判定特定扩展历史是否存在这个问题归约到了判定特定的标记见证是否存在这个问题.

引理4. ehistory($ [[ $L, n$ ]] $_tt)上存在扩展历史eh, 当且仅当$ [[ $Clt_f(Mod(L)), n+1$ ]] $_b存在eh的一条标记见证.

引理4的简要证明如下: 引理的“当”方向由引理1和引理2显然可以得到. 对“仅当”方向, 根据引理1和引理2, ehistory($ [[ $L, n$ ]] $_tt)上存在扩展历史eh, 当且仅当$ [[ $Clt_f(Mod(L)), n+1$ ]] $_b上存在执行t, 且t的扩展历史为eh. 在t的最后一个动作之后, 我们令进程P₁到P_n都清空自己的存储缓冲区, 就得到了eh的一条标记见证.

令$M_i^{eh - f}$是通过对$M_i^{eh}$做如下更改得到的通道机器: 首先, 将除了刷出、cas、调用刷出和返回刷出之外的迁移都转化为τ迁移; 然后, 将每个cas(j, x, d₁, d₂)迁移转化为flush(j, x, d₂)迁移; 再将每个调用刷出flushCall(j)迁移转化为flush(j, z_f, d)迁移, 这里的d是$M_i^{eh}$产生flushCall(j)迁移时刷出的对应z_f的项中的内存快照; 最后, 用类似的方法处理返回刷出迁移.

下面的引理说明: 给定k-扩展历史eh和一对格局, 以这对格局为起点和终点的eh对应的标记见证的存在问题(根据引理4, 即eh的存在问题)可以被归约到判断$\bigcap\nolimits_{i = 1}^{n + 1} {T_{({q_i}, {{q'}_i})}^{(S, {K_1})}M_i^{eh - f}} \ne \emptyset $. 注意, 这里的机器并未采用易失通道. 这个引理的成立, 来自我们事实上用z_w的刷出之后紧邻的τ迁移对应了函数调用和函数返回迁移, 用z_f的“刷出”对应了调用刷出和返回刷出迁移. 这个引理的证明可以在本文的技术报告版本^[29]中找到.

引理5. 给定一条k-扩展历史eh. $ [[ $Clt_f(Mod(L)), n+1$ ]] $_b上存在从(p_in, d_init, $ {u'_{init}} $, ⊥)开始、到(p_w, d_w, $ {u'_{init}} $, ⊥)结束的eh的标记见证, 当且仅当$\bigcap\nolimits_{i = 1}^{n + 1} {T_{({q_i}, {{q'}_i})}^{(S, {K_1})}M_i^{eh - f}} \ne \emptyset $. 这里, p_in将进程P₁到P_n映射到in_clt, 且将进程P_n+1映射到q_wit. $ {u'_{init}} $将进程P₁到P_n+1映射到ε. 对1≤i≤n+1, q_i=(p_in(i), d_init, d_init, q_is, ⊥), 且$ {q'_i} $=(p_w(i), d_w, d_w, q_ends, ⊥).

令$M_i^{eh - w}$是通过对$M_i^{eh}$做如下更改得到的通道机器: 首先, 将除了写和cas之外的迁移都转化为τ迁移; 然后, 将每个cas(j, x, d₁, d₂)迁移转化为write(j, x, d₂)迁移. 由于非易失通道不丢失内容, 因此, $M_i^{eh - f}$的刷出动作序列和$M_i^{eh - w}$的写动作序列一致. 进而, 引理5在将$M_i^{eh - f}$替换为$M_i^{eh - w}$时仍成立.

当把$M_i^{eh - w}$视为易失通道机器时, 为了保证不丢失通道内对应扩展历史eh的z_f和z_w, 通道中的字母表$ {\varSigma _{{s_1}}} $中的元素不应丢失. 值得注意的是: 虽然$M_i^{eh - w}$中的函数调用、函数返回、调用刷出和返回刷出迁移被转化为了τ迁移, 但$M_i^{eh}$的状态中的第4个元组, 即自动机A_eh的状态, 仍在记录扩展历史, 记录的扩展历史来自于通道中缓存的z_f和z_w. 为了保证$M_i^{eh - w}$的读动作总能成功读到对相应内存单元的最新的写, 通道中的字母表$ {\varSigma _{{s_2}}} $中的元素不应丢失, 因此, 强符号集合的向量为$ S = ({\varSigma _{{s_1}}}, {\varSigma _{{s_2}}}) $. 由于扩展历史eh的长度为k, 通道里的对应扩展历史的项(z_f和z_w)的数目不超过k. 每个通道里字母表$ {\varSigma _{{s_2}}} $中的元素数目不会超过|X_L|, 因此, 强符号约束为(S, K), 其中, K=〈k, |X_L|〉. 下面的引理说明了引理5在将通道机器$M_i^{eh - f}$替换为(S, K)-易失通道机器$M_i^{eh - w}$时仍成立. 这个引理的证明可以在本文的技术报告版本^[29]中找到.

引理6. 给定一条k-扩展历史eh. $ [[ $Clt_f(Mod(L)), n+1$ ]] $_b上存在从(p_in, d_init, $ {u'_{init}} $, ⊥)开始、到(p_w, d_w, $ {u'_{init}} $, ⊥)结束的eh的标记见证, 当且仅当$\bigcap\nolimits_{i = 1}^{n + 1} {LT_{({q_i}, {{q'}_i})}^{(S, {K_1})}M_i^{eh - f}} \ne \emptyset $. 这里, p_in将进程P₁到P_n映射到in_clt, 且将进程P_n+1映射到q_wit. $ {u'_{init}} $将进程P₁到P_n+1映射到ε. 对1≤i≤n+1, q_i=(p_in(i), d_init, d_init, q_is, ⊥), 且$ {q'_i} $=(p_w(i), d_w, d_w, q_ends, ⊥).

根据引理3, $\bigcap\nolimits_{i = 1}^{n + 1} {LT_{({q_i}, {{q'}_i})}^{(S, {K_1})}M_i^{eh - w}} \ne \emptyset $成立, 当且仅当$LT_{(p, p')}^{(S, {K_1})}M_1^{eh - w} \otimes ... \otimes M_{n + 1}^{eh - w} \ne \emptyset $成立. 后者正是(S, K)-易失通道机器的控制状态可达问题, 是可判定的. 这里, p=(q₁, …, q_n+1), 且$ p' = ({q'_1}, ..., {q'_{n + 1}}) $. 引理6中的p_w和d_w的数目是有穷的. 通过枚举所有的p_w和d_w并多次使用引理6, 可以判定$ [[ $Clt_f(Mod(L)), n+1$ ]] $_b上是否存在eh的标记见证. 根据引理4, 这个方法判定了eh是否是$ [[ $L, n$ ]] $_tt上的k-扩展历史. 根据第4节的讨论, 我们可以得到TSO内存模型下可线性化的3种限界版本是可判定的, 如下面的定理所述.

定理7. 给定并发数据结构L和L′、顺序规约Spec以及正整数n, n进程下L′是否k-限界TSO-to-TSO线性化了L是可判定的, n进程下L′是否k-限界TSO-to-SC线性化了L是可判定的, n进程下L是否k-限界TSO可线性化到Spec是可判定的.

我们使用简单通道机器来称呼只使用迁移标号ε、且迁移规则中不使用正则卫士表达式和替换的通道机器. 简单通道机器的可达问题^[20]是指: 给定简单通道机器M、格局s₁和s₂(一个格局包含控制状态和通道内容), 判断作为易失通道机器的M是否有一条从s₁和s₂的有穷执行. 文献[20]证明了简单通道机器的可达问题的复杂度在递归函数的Fast-Growing层级^[19]${\mathfrak{F}_{{\omega ^\omega }}}$中.

为了证明的方便, 我们使用单通道简单通道机器, 为此需要证明简单通道机器的可达问题与单通道的简单通道机器的可达问题可以相互归约.

● 一方面, 后者是前者的一个子问题;

● 另一方面, 我们通过如下方式将前者归约为后者: 给定简单通道机器M, 可以构造一个单通道简单通道机器M′. M′的通道内容就是使用分隔符分隔开的M的各个通道的内容. M的一步迁移中对通道内容的修改被M′上若干步迁移所模拟, 这些迁移读取整个通道的内容, 并分别修改“M的每个通道”的内容(根据分隔符确定是哪个通道). 因此, 单通道简单通道机器的可达问题与简单通道机器的可达问题有着相同的复杂度. 通过类似的思想, 可以根据易失通道机器M构造单通道简单通道机器M′. 为了M的一步迁移中对通道内容的修改被M′上若干步迁移所模拟, 这些迁移读取整个通道的内容, 使用正则卫士表达式进行判断, 进行可能的元素替换, 并分别修改“M的每个通道”的内容. 因此可以证明, 易失通道机器的控制状态可达问题和单通道的简单通道机器的可达问题可以互相归约.

由于TSO内存模型下可线性化的3种限界版本的验证问题被归约为易失通道机器的控制状态可达问题, 因此可以看到, TSO内存模型下可线性化的3种限界版本的验证问题可以被归约到单通道的简单通道机器的可达问题. 注意: 由于易失通道机器$M_i^{eh}$能较为自然地建模进程i的执行, 因此在可线性化的3种限界版本的可判定性证明中, 我们将其归约到易失通道系统的控制状态可达, 而不是单通道的简单通道机器的可达问题.

采用类似于文献[17]的思想, 我们构造了并发数据结构$L_{({s_1}, {s_2})}^M$, 它使用运行在两个进程上的两个函数M₁和M₂的合作来模拟单通道简单通道机器M使用易失通道时, 从s₁开始的迁移. 两个函数不断地读取来自因对方的存储缓冲区刷出而导致的更新, 并将读到的值写入自己的存储缓冲区(在必要时, 根据M的迁移规则修改读到的值, 并将新的值写入自己的存储缓冲区). 通过这种方法, 模拟了通道及通道机器的迁移. 由于TSO内存模型下, 一个进程的刷出未必会被另一个进程读到, 这导致模拟的通道可能“丢失”一些内容, 即模拟了易失通道. 只有当模拟的通道机器的执行到达s₂之后, $L_{({s_1}, {s_2})}^M$的两个函数才可以返回. 通过这种方法, 我们将单通道简单通道机器M的可达问题, 归约到是否某条${[[L_{({s_1}, {s_2})}^M, 2]]_{tt}}$的扩展历史包含函数返回动作. 并发数据结构$L_{({s_1}, {s_2})}^M$的构造以及这个归约的证明, 可以在本文的技术报告版本^[29]中找到.

下面叙述如何通过将单通道简单通道机器的可达问题, 归约到判定$L_{({s_1}, {s_2})}^M$是否符合TSO内存模型下可线性化的3种限界版本的方法. 具体的证明可以在本文的技术报告版本^[29]中找到.

● k-限界TSO-to-TSO可线性化的复杂度

令并发数据结构L_pend包含M₁和M₂两个函数, 且这两个函数从不返回. 一种实现方法为M₁和M₂内只包含一条while(true); 语句. 当${[[L_{({s_1}, {s_2})}^M, 2]]_{tt}}$中存在一条包含至少一个函数返回动作的执行时, 令t为这样的执行, 且不妨设这个函数返回动作发生在进程P₁. 基于t, 我们构造另一个执行t′如下: 如果进程P₁尚未做调用刷出, 则进程P₁的存储缓冲区内缓存着(z_f, call), 将其刷出并进行一次调用刷出动作; 由于需要M₁和M₂的合作来模拟M的行为, 进程P₂一定有至少一次函数调用; 如果进程P₂尚未做调用刷出, 则进程P₂的存储缓冲区内缓存着(z_f, call), 将其刷出并进行一次调用刷出动作. 执行t′显然属于${[[L_{({s_1}, {s_2})}^M, 2]]_{tt}}$且至少包含5个函数调用、函数返回、调用刷出或返回刷出动作. 显然, 执行t′的扩展历史不属于${[[L_{({s_1}, {s_2})}^M, 2]]_{tt}}$的扩展历史集合.

可以证明: ${[[L_{({s_1}, {s_2})}^M, 2]]_{tt}}$存在一条包含至少一个函数返回动作的执行, 当且仅当${[[L_{({s_1}, {s_2})}^M, 2]]_{tt}}$的扩展历史集合不是$ [[ $L_pend, 2$ ]] $_tt的扩展历史集合的子集, 当且仅当2进程下L_pend并未TSO-to-TSO线性化了$L_{({s_1}, {s_2})}^M$. 由于$ [[ $L_pend, 2$ ]] $_tt的每条扩展历史最多包含4个动作, 且执行t′的扩展历史包含至少5个动作, 因此在考察${[[L_{({s_1}, {s_2})}^M, 2]]_{tt}}$的扩展历史集合时, 只需要考察长度不超过5的扩展历史集合即可. 因此, 我们将易失通道机器M上的可达问题归约到判定2进程下L_pend是5-限界TSO-to-TSO线性化了$L_{({s_1}, {s_2})}^M$.

● k-限界TSO-to-SC可线性化的复杂度

当${[[L_{({s_1}, {s_2})}^M, 2]]_{tt}}$中存在一条包含至少一个函数返回动作的执行时, 令t为这样的执行, 且不妨设这个函数返回动作发生在进程P₁. 由于需要M₁和M₂的合作来模拟M的行为, 进程P₂一定有至少一次函数调用. 执行t至少包含3个函数调用或函数返回动作. 显然, 这样的执行的历史不属于$ [[ $L_pend, 2$ ]] $_tt的历史集合.

可以证明: ${[[L_{({s_1}, {s_2})}^M, 2]]_{tt}}$存在一条包含至少一个函数返回动作的执行, 当且仅当2进程下L_pend并未TSO-to- SC线性化了$L_{({s_1}, {s_2})}^M$. 由于$ [[ $L_pend, 2$ ]] $_tt的每条历史最多包含2个动作, 且执行t的历史包含至少3个元素, 因此在考察${[[L_{({s_1}, {s_2})}^M, 2]]_{tt}}$的历史集合时, 只需要考察长度不超过3的历史集合即可. 因此, 我们将易失通道机器M上的可达问题归约到判定2进程下L_pend是否3-限界TSO-to-SC线性化了$L_{({s_1}, {s_2})}^M$.

● k-限界TSO可线性化的复杂度

在并发数据结构$L_{({s_1}, {s_2})}^M$的构造中, 要求一旦M₁或者M₂可以返回, 则其会修改一个flag, 使得之后不管在哪个进程上的M₁和M₂都直接返回. 令顺序规约Spec为包含不超过两个M₁或M₂操作的顺序历史集合. 显然, S是正则的, 且可以通过枚举构造. 当${[[L_{({s_1}, {s_2})}^M, 2]]_{tt}}$中存在一条包含至少一个函数返回动作的执行时, 令t为这样的执行, 且不妨设这个函数返回动作发生在进程P₁. 基于t, 我们构造另一个执行t′如下: 此时, M₁和M₂都变成了实质上的空函数. 如果进程P₁尚未做调用刷出或返回刷出, 则清空进程P₁的存储缓冲区, 并做调用刷出或返回刷出. 由于需要M₁和M₂的合作来模拟M的行为, 进程P₂一定有至少一次函数调用. 如果进程P₂的函数还未返回, 则在进程P₂执行一次函数返回动作. 之后, 清空进程P₂的存储缓冲区, 并做调用刷出或返回刷出. 最后, 在进程P₁上调用一个函数并返回, 并做调用刷出和返回刷出. 执行t′显然属于${[[L_{({s_1}, {s_2})}^M, 2]]_{tt}}$且至少包含6个函数调用或返回刷出动作, 对应至少3个操作. 显然, Spec中的顺序历史包含的操作少于3个.

可以证明: ${[[L_{({s_1}, {s_2})}^M, 2]]_{tt}}$存在一条包含至少一个函数返回动作的执行, 当且仅当2进程下$L_{({s_1}, {s_2})}^M$并未TSO可线性化到Spec. 由于Spec中的每个历史包含不超过两个操作, 且执行t′对应至少3个操作, 包含至少6个函数调用或返回刷出动作, 因此在考察${[[L_{({s_1}, {s_2})}^M, 2]]_{tt}}$的函数调用和返回刷出动作序列时, 只需要考察长度不超过6的序列集合即可. 因此, 我们将易失通道机器M上的可达问题归约到判定2进程下$L_{({s_1}, {s_2})}^M$是否6-限界TSO可线性化到S.

因此, 我们将TSO内存模型下可线性化的3种限界版本的验证问题归约到单通道的简单通道机器的可达问题, 又将后者归约到了前者. 根据以上讨论, 得到了如下定理, 它说明TSO内存模型下可线性化的3种限界版本的复杂度都在递归函数的Fast-Growing层级${\mathfrak{F}_{{\omega ^\omega }}}$中.

定理8. 在n进程下, 检测k-限界TSO-to-TSO可线性化、k-限界TSO-to-SC可线性化和k-限界TSO可线性化的复杂度都在递归函数的Fast-Growing层级${\mathfrak{F}_{{\omega ^\omega }}}$中.

8 结论和未来工作

据我们所知, TSO-to-TSO可线性化、TSO-to-SC可线性化和TSO可线性化是文献中针对TSO内存模型提出的全部可线性化变种. 本文研究了k-限界TSO-to-TSO可线性化、k-限界TSO-to-SC可线性化和k-限界TSO可线性化的可判定性. TSO内存模型下可线性化的3种限界版本都是非平凡的, 因为写动作的数目不限界, 因此使用的存储缓冲区大小不限界, 进而其操作语义是无穷状态迁移系统. 我们证明了TSO内存模型下可线性化的这3种限界版本都是可判定的. 我们的工作解决了TSO内存模型下限界可线性化的可判定性问题.

本文将并发数据结构以及顺序规约之间的k-限界TSO-to-TSO可线性化、k-限界TSO-to-SC可线性化和k-限界TSO可线性化的验证归约到k-扩展历史集合之间的TSO-to-TSO可线性化的验证, 从而以一种统一的方式验证TSO内存模型下可线性化的3个限界版本. 验证的重点在于判定TSO内存模型下并发数据结构是否有一条特定的扩展历史. 我们证明了这个问题是可判定的, 证明的方法是将其归约到已知可判定的易失通道机器的控制状态可达问题. 归约的难点在于: 已有的关联TSO内存模型下并发系统和易失通道机器的工作关注的问题是基于状态定义的, 而并发数据结构的正确性定义是基于函数调用、函数返回、调用刷出和返回刷出动作的, 这两个问题的粒度不同. 更加复杂的是, 函数调用和函数返回动作以一种复杂的方式同时影响控制状态和存储缓冲区. 我们的工作通过修改内存模型、并发数据结构、客户程序和操作语义, 使得内存单元z_f和z_w的动作序列对应了函数调用、函数返回、调用刷出和返回刷出的序列. 然后, 将修改的操作语义上是否存在特定的扩展历史这个问题归约到了易失通道机器$M_1^{eh - w} \otimes ... \otimes M_{n + 1}^{eh - w}$的控制状态可达问题. 我们提出的这个归约方法将有助于验证松弛内存模型上的其他粗粒度性质.

进而证明了在TSO内存模型下判定可线性化的这3个限界版本的复杂度都在递归函数的Fast-Growing层级${\mathfrak{F}_{{\omega ^\omega }}}$中. 通过证明单通道简单通道机器的可达问题这一已知的有着这样复杂度的问题和TSO内存模型下可线性化的这3个限界版本可以互相归约得到这个结论. 我们的工作展示了在TSO内存模型下对限界可线性化的验证具有理论可行性, 为TSO内存模型一致性验证的进一步研究打下了理论基础. 非限界版本的TSO-to-SC可线性化和TSO可线性化的可判定性问题目前仍是开放的. 作为未来工作, 我们准备研究非限界版本的TSO-to-SC可线性化和TSO可线性化的可判定性问题.