An Automatic Parameterized Verification of FLASH Cache Coherence Protocol

被引：0
|
作者：
Li, Yongjian [1 ]
Cao, Jialun [1 ,2 ]
Duan, Kaiqiang [1 ,2 ]
机构：
[1] Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing, Peoples R China
[2] Univ Chinese Acad Sci, Beijing, Peoples R China
来源：
2018 IEEE INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY (QRS 2018) | 2018年
关键词：
parameterized verification; verification; formal method; FALSH;
D O I：
10.1109/QRS.2018.00018
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
FLASH protocol is an industrial-scale cache coherence protocol, which is a challenging benchmark in the formal verification area. Verifying such protocol yields both scientific and commercial values. However, the complicated mechanism of protocols and the explosive searching states make it extremely hard to solve. An alternative solution is to carry out proof scripts combining manual work with a computer, which is adopted by most works in this area. However, this alternation makes the verification process neither effective nor rigorous. Therefore, in this paper, we elaborate the detailed process of how paraVerifier generates formal proofs automatically. It can generate a formal proof without manual works, and guarantee the rigorous correctness at the same time. Furthermore, we also illustrate the flow chart of READ and WRITE transactions in FLASH protocol, and analyze the semantics hiding behind the auto-searched invariants. We show that paraVerifier can not only automatically generate formal proofs, but offer comprehensive analyzing reports for better understanding.
引用
收藏
页码：47 / 58
页数：12
相关论文
共 50 条
  • [1] Efficient Verification of Parameterized Cache Coherence Protocols
    Qu, WanXia
    Guo, Yang
    Pang, ZhengBin
    Yang, XiaoDong
    [J]. PROCEEDINGS OF THE 9TH INTERNATIONAL CONFERENCE FOR YOUNG COMPUTER SCIENTISTS, VOLS 1-5, 2008, : 154 - 159
  • [2] A simple method for parameterized verification of cache coherence Protocols
    Chou, CT
    Mannava, PK
    Park, S
    [J]. FORMAL METHODS IN COMPUTER-AIDED DESIGN, 2004, 3312 : 382 - 398
  • [3] Exact and efficient verification of parameterized cache coherence protocols
    Emerson, EA
    Kahlon, V
    [J]. CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2003, 2860 : 247 - 262
  • [4] A simple method for parameterized verification of cache coherence protocols
    Chou, CT
    Mannava, PK
    Park, S
    [J]. FORMAL METHODS IN COMPUTER-AIDED DESIGN, PROCEEDINGS, 2004, 3312 : 382 - 398
  • [5] A Novel Approach to Parameterized Verification of Cache Coherence Protocols
    Li, Yongjian
    Duan, Kaiqiang
    Lv, Yi
    Pang, Jun
    Cai, Shaowei
    [J]. PROCEEDINGS OF THE 34TH IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN (ICCD), 2016, : 560 - 567
  • [6] Counterexample guided invariant discovery for parameterized cache coherence verification
    Pandav, S
    Slind, K
    Gopalakrishnan, G
    [J]. CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2005, 3725 : 317 - 331
  • [7] Constraint-Based Verification of Parameterized Cache Coherence Protocols
    Giorgio Delzanno
    [J]. Formal Methods in System Design, 2003, 23 : 257 - 301
  • [8] Constraint-based verification of parameterized cache coherence Protocols
    Delzanno, G
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2003, 23 (03) : 257 - 301
  • [9] VERIFICATION OF THE FUTUREBUS+ CACHE COHERENCE PROTOCOL
    CLARKE, EM
    GRUMBERG, O
    HIRAISHI, H
    JHA, S
    LONG, DE
    MCMILLAN, KL
    NESS, LA
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 1995, 6 (02) : 217 - 232
  • [10] VERIFICATION OF THE FUTUREBUS+ CACHE COHERENCE PROTOCOL
    CLARKE, EM
    GRUMBERG, O
    HIRAISHI, H
    JHA, S
    LONG, DE
    MCMILLAN, KL
    NESS, LA
    [J]. COMPUTER HARDWARE DESCRIPTION LANGUAGES AND THEIR APPLICATIONS, 1993, 32 : 15 - 30
12345