TSO内存模型下限界可线性化的可判定性研究
CSTR:
作者:
作者单位:

作者简介:

王超(1985-),男,博士,副教授,CCF专业会员,主要研究领域为形式化方法,并发数据结构,分布式数据类型;
吴鹏(1977-),男,博士,副研究员,CCF高级会员,主要研究领域为形式化方法,并发测试,机器学习;
吕毅(1972-),男,博士,副研究员,CCF专业会员,主要研究领域为并发理论,形式化方法;
贾巧雯(1992-),女,博士生,主要研究领域为并发系统,可线性化验证.

通讯作者:

王超,E-mail:wangch1@swu.edu.cn;吕毅,E-mail:lvyi@ios.ac.cn

中图分类号:

TP311

基金项目:

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


Decidability of Bounded Linearizability on TSO Memory Model
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    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内存模型下可线性化的这3个限界版本都是可判定的,进而证明了在TSO内存模型下判定可线性化的这3个限界版本的复杂度都在递归函数的Fast-Growing层级Fωω中.通过证明已知对应复杂度的单通道简单通道机器的可达问题和TSO内存模型下可线性化的3个限界版本可以互相归约得到这个结论.

    Abstract:

    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 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, an observer process and bind specific cas actions of the observer process are introduced to each call or return actions. In this way, three bounded versions of linearizability are decidable on the TSO memory model are proved. Three bounded versions of linearizability on the TSO memory model are at level Fωω are further proved 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.

    参考文献
    相似文献
    引证文献
引用本文

王超,吕毅,吴鹏,贾巧雯. TSO内存模型下限界可线性化的可判定性研究.软件学报,2022,33(8):2896-2917

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-09-05
  • 最后修改日期:2021-10-14
  • 录用日期:
  • 在线发布日期: 2022-01-28
  • 出版日期: 2022-08-06
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号