The Anchor Verifier for Blocking and Non-blocking Concurrent Software

被引：3
|
作者：
Flanagan, Cormac [1 ]
Freund, Stephen N. [2 ]
机构：
[1] Univ Calif Santa Cruz, Santa Cruz, CA 95064 USA
[2] Williams Coll, Williamstown, MA 01267 USA
来源：
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL | 2020年 / 4卷 / 04期
基金：
美国国家科学基金会;
关键词：
concurrent program verification; reduction; synchronization; MODULAR VERIFICATION; REDUCTION; PROGRAMS;
D O I：
10.1145/3428224
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Verifying the correctness of concurrent software with subtle synchronization is notoriously challenging. We present the ANCHOR verifier, which is based on a new formalism for specifying synchronization disciplines that describes both (1) what memory accesses are permitted, and (2) how each permitted access commutes with concurrent operations of other threads (to facilitate reduction proofs). ANCHOR supports the verification of both lock-based blocking and cas-based non-blocking algorithms. Experiments on a variety concurrent data structures and algorithms show that ANCHOR significantly reduces the burden of concurrent verification.
引用
收藏
页数：29
相关论文
共 50 条
  • [41] Experimental research of nine parallel plane jets in non-blocking and blocking conditions
    Wang, Peng
    Qi, Peiyao
    Yuan, Dongdong
    Zhang, Xiaoxuan
    Tan, Sichao
    Li, Dongyang
    ANNALS OF NUCLEAR ENERGY, 2022, 166
  • [42] Non-blocking Patricia Tries with Replace Operations
    Shafiei, Niloufar
    2013 IEEE 33RD INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING SYSTEMS (ICDCS), 2013, : 216 - 225
  • [43] A non-blocking Checkpointing algorithm for distributed systems
    Guoliang L.
    Shuyu C.
    Xiaoqin Z.
    International Journal of Digital Content Technology and its Applications, 2011, 5 (07) : 230 - 238
  • [44] Optimizing non-blocking collective operations for InfiniBand
    Hoefler, Torsten
    Lumsdaine, Andrew
    2008 IEEE INTERNATIONAL SYMPOSIUM ON PARALLEL & DISTRIBUTED PROCESSING, VOLS 1-8, 2008, : 182 - +
  • [45] Modular Termination Verification for Non-blocking Concurrency
    Pinto, Pedro da Rocha
    Dinsdale-Young, Thomas
    Gardner, Philippa
    Sutherland, Julian
    PROGRAMMING LANGUAGES AND SYSTEMS (ESOP 2016), 2016, 9632 : 176 - 201
  • [46] Formalising progress properties of non-blocking programs
    Dongol, Brijesh
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2006, 4260 : 284 - 303
  • [47] Non-blocking transactional mobile agent execution
    Pleisch, S
    Schiper, A
    22ND INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING SYSTEMS, PROCEEDINGS, 2002, : 443 - 444
  • [48] Non-Blocking Testing for Network-on-Chip
    Huang, Letian
    Wang, Junshi
    Ebrahimi, Masoumeh
    Daneshtalab, Masoud
    Zhang, Xiaofan
    Li, Guangjun
    Jantsch, Axel
    IEEE TRANSACTIONS ON COMPUTERS, 2016, 65 (03) : 679 - 692
  • [49] Design and Modeling of a Non-blocking Checkpointing System
    Sato, Kento
    Mohror, Kathryn
    Moody, Adam
    Gamblin, Todd
    de Supinski, Bronis R.
    Maruyama, Naoya
    Matsuoka, Satoshi
    2012 INTERNATIONAL CONFERENCE FOR HIGH PERFORMANCE COMPUTING, NETWORKING, STORAGE AND ANALYSIS (SC), 2012,
  • [50] A LOWER BOUND ON STRICTLY NON-BLOCKING NETWORKS
    FRIEDMAN, J
    COMBINATORICA, 1988, 8 (02) : 185 - 188
12345