AIPUB归智期刊联盟

WeChat

Mobile website

2025-4-3- 19
Home > Archive>Volume 23, Issue 11, 2014 >10-15
PDF HTML XML Export Cite reminder
Parameterized Verifation of RCC Cache Coherence Protocol
CSTR:
[cstr]
Author:
  • Article
    • | |
  • Metrics
    • |
  • Reference [15]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    RCC cache coherence protocol in Godson-T many-core processor is a characteristic parameterized concurrent system. It is a challenge to verify this protocol. Cubicle is a recently built parameterized model checking tool based on SMT solver. We used Cubicle to model and verify RCC protocol successfully. The experimental results show that RCC protocol satisfies all kinds of safety properties regardless of how many nodes it has.

    Reference
    1 周琰.Godson-T缓存一致性协议的murphi建模和验证.计算机系统应用,2013,22(10):124-128.
    2 Abdulla PA, Delzanno G, Rezine A. Parameterized verification of infinite-state processes with global conditions. Computer Aided Verification. Springer Berlin Heidelberg, 2007: 145-157.
    3 Abdulla PA, Delzanno G, Henda NB, et al. Regular model checking without transducers (on efficient verification of parameterized systems). Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, 2007: 721-736.
    4 Chou CT, Mannava PK, Park S. A simple method for parameterized verification of cache coherence protocols. Formal Methods in Computer-Aided Design. Springer Berlin Heidelberg, 2004: 382-398.
    5 Cimatti A, Clarke E, Giunchiglia F, et al. NuSMV: A new symbolic model verifier. Computer Aided Verification. Springer Berlin Heidelberg, 1999: 495-499.
    6 Conchon S, Goel A, Krstić S, et al. Cubicle: A parallel SMT-based model checker for parameterized systems. Computer Aided Verification. Springer Berlin Heidelberg, 2012: 718-24.
    7 Das S, Dill D L, Park S. Experience with predicate abstraction. Computer Aided Verification. Springer Berlin Heidelberg, 1999: 160-171.
    8 Dill DL. The Murφ verification system. Computer Aided Verification. Springer Berlin Heidelberg, 1996: 390-393.
    9 Emerson EA, Kahlon V. Reducing model checking of the many to the few. Automated Deduction-CADE-17. Springer Berlin Heidelberg, 2000: 236-254.
    10 Fan D, Zhang H, Wang D, et al. Godson-T: An efficient many-core processor exploring thread-level parallelism. Micro, IEEE, 2012, 32(2): 38-47.
    11 Graf S, Saïdi H. Construction of abstract state graphs with PVS. Computer aided verification. Springer Berlin Heidelberg, 1997: 72-83.
    12 Holzmann GJ. The model checker SPIN. IEEE Trans. on Software Engineering, 1997, 23(5): 279-295.
    13 Cadence Berkeley Labs. Cadence smv, http://www.kenmcmil. com/smv.html, 1998.
    14 O'Leary J, Talupur M, Tuttle MR. Protocol verification using flows: An industrial experience. Formal Methods in Computer-Aided Design, 2009. FMCAD 2009. IEEE, 2009: 172-179.
    15 Pnueli A, Ruah S, Zuck L. Automatic deductive verification with invisible invariants. Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, 2001: 82-97.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

孙鲁明,周琰. RCC高速缓存一致性协议的带参验证.计算机系统应用,2014,23(11):10-15

Copy
Share
Article Metrics
  • Abstract:2171
  • PDF: 3691
  • HTML: 0
  • Cited by: 0
History
  • Received:March 11,2014
  • Revised:April 14,2014
  • Online: November 20,2014
Article QR Code
Links:Journal of Software中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会
You are the first990457Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-3
Address：4# South Fourth Street, Zhongguancun,Haidian, Beijing,Postal Code：100190
Phone：010-62661041 Fax： Email：csa (a) iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063