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

Decidability of Bounded Linearizability on TSO Memory Model

作　　者：王超 吕毅[2,3] 吴鹏 贾巧雯[2,3] WANG Chao;LÜYi;WU Peng;JIA Qiao-Wen(Centre for Research and Innovation in Software Engineering,College of Computer and Information Science,Southwest University,Chongqing 400715,China;State Key Laboratory of Computer Science(Institute of Software,Chinese Academy of Sciences),Beijing 100190,China;University of Chinese Academy of Sciences,Beijing 100049,China)

机构地区：[1]西南大学计算机与信息科学学院软件研究与创新中心,重庆400715 [2]计算机科学国家重点实验室(中国科学院软件研究所),北京100190 [3]中国科学院大学,北京100049

出　　处：《软件学报》2022年第8期2896-2917,共22页Journal of Software

基　　金：国家自然科学基金(62002298,62072443);中央高校基本科研业务费专项资金(SWU019036);中国科学院对外合作重点项目(GJHZ1844)。

摘　　要：TSO-to-TSO可线性化、TSO-to-SC可线性化和TSO可线性化是Total Store Order(TSO)内存模型下可线性化的3个变种.提出了k-限界TSO-to-TSO可线性化和k-限界TSO可线性化,考察了k-限界TSO-to-TSO可线性化、k-限界TSO-to-SC可线性化和k-限界TSO可线性化的验证问题.它们分别是这3种可线性化的限界版本,都使用k-扩展历史,这样的扩展历史对应的执行有着限界数目(不超过k个)的函数调用、函数返回、调用刷出和返回刷出动作.k-扩展历史对应执行中的写动作数目是不限界的,进而执行中使用的存储缓冲区的大小也是不限界的,对应的操作语义是无穷状态迁移系统,所以3个限界版本可线性化的验证问题是不平凡的.将定义在并发数据结构与顺序规约之间的k-限界TSO-to-TSO可线性化、k-限界TSO-to-SC可线性化和k-限界TSO可线性化的验证问题归约到k-扩展历史集合之间的TSO-to-TSO可线性化问题,从而以统一的方式验证了TSO内存模型下可线性化的3个限界版本.验证方法的关键步骤是判定一个并发数据结构是否有一个特定的k-扩展历史.证明了这个问题是可判定的,证明方法是将这一问题归约为已知可判定的易失通道机器的控制状态可达问题.本质上,这一归约将每一个函数调用或函数返回动作转化为写、刷出或cas(compare-and-swap)动作.在TSO-to-TSO可线性化的定义中,一个函数调用或函数返回动作会同时影响存储缓冲区和控制状态.为了模拟函数调用或函数返回动作对存储缓冲区的影响,在每个函数调用或函数返回动作之后立刻执行一个特定的写动作.这个写动作及其对应的刷出动作模拟了函数调用或函数返回动作对存储缓冲区的影响.引入观察者进程,为每个函数调用或函数返回动作“绑定”一个观察者进程的cas动作,以这种方式模拟了函数调用或函数返回动作对控制状态的影响.因此证明了TSO内存模型下�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.This study proposes k-bounded TSO-to-TSO linearizability and k-bounded TSO linearizability,and investigates 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 a uniform framework for verifying the three bounded versions of linearizability on the TSO memory model.The key point of the proposed approach is to check if a concurrent data structure contains a specific k-extended history.It is proved 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.A specific write action is added immediately after each

关 键 词：并发数据结构 可线性化 TSO内存模型 可判定性 易失通道机器 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]