TSO-to-TSO Linearizability Is Undecidable

被引：4
|
作者：
Wang, Chao [1 ,2 ]
Lv, Yi [1 ]
Wu, Peng [1 ]
机构：
[1] Chinese Acad Sci, State Key Lab Comp Sci, Inst Software, Beijing, Peoples R China
[2] Univ Chinese Acad Sci, Beijing, Peoples R China
来源：
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015 | 2015年 / 9364卷
关键词：
D O I：
10.1007/978-3-319-24953-7_24
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
TSO-to-TSO linearizability is a variant of linearizability for concurrent libraries on the Total Store Order (TSO) memory model. It is proved in this paper that TSO-to-TSO linearizability for a bounded number of processes is undecidable. We first show that the trace inclusion problem of a classic-lossy single-channel system, which is known undecidable, can be reduced to the history inclusion problem of specific libraries on the TSO memory model. Based on the equivalence between history inclusion and extended history inclusion for these libraries, we then prove that the extended history inclusion problem of libraries is undecidable on the TSO memory model. By means of extended history inclusion as an equivalent characterization of TSO-to-TSO linearizability, we finally prove that TSO-to-TSO linearizability is undecidable for a bounded number of processes.
引用
收藏
页码：309 / 325
页数：17
相关论文
共 50 条
  • [1] TSO-to-TSO linearizability is undecidable
    Wang, Chao
    Lv, Yi
    Wu, Peng
    [J]. ACTA INFORMATICA, 2018, 55 (08) : 649 - 668
  • [2] TSO-to-TSO linearizability is undecidable
    Chao Wang
    Yi Lv
    Peng Wu
    [J]. Acta Informatica, 2018, 55 : 649 - 668
  • [3] Verifying Linearizability on TSO Architectures
    Derrick, John
    Smith, Graeme
    Dongol, Brijesh
    [J]. INTEGRATED FORMAL METHODS, IFM 2014, 2014, 8739 : 341 - 356
  • [4] TSO THERE
    GOETZ, MA
    [J]. DATAMATION, 1971, 17 (13): : 13 - &
  • [5] TSO-CC: Consistency directed cache coherence for TSO
    Elver, Marco
    Nagarajan, Vijay
    [J]. 2014 20TH IEEE INTERNATIONAL SYMPOSIUM ON HIGH PERFORMANCE COMPUTER ARCHITECTURE (HPCA-20), 2014, : 165 - 176
  • [6] REXX ON TSO/E
    HOERNES, GE
    [J]. IBM SYSTEMS JOURNAL, 1989, 28 (02) : 274 - 293
  • [7] NARRATIVES IN 'TSO CHUAN'
    EGAN, RC
    [J]. HARVARD JOURNAL OF ASIATIC STUDIES, 1977, 37 (02) : 323 - 352
  • [8] DISCUSSION OF TSO,WK
    POPELAR, CH
    [J]. JOURNAL OF APPLIED MECHANICS, 1968, 35 (04): : 841 - &
  • [9] 'ROSE ANN TSO'
    TAPAHONSO, L
    [J]. BELOIT POETRY JOURNAL, 1980, 30 (02): : 30 - 30
  • [10] Quasi-Linearizability is Undecidable
    Wang, Chao
    Lv, Yi
    Liu, Gaoang
    Wu, Peng
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2015, 2015, 9458 : 369 - 386
12345