期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

RCC高速缓存一致性协议的带参验证 被引量：1

Parameterized Verifation of RCC Cache Coherence Protocol
下载PDF
导出
摘要 Godson-T众核处理器的RCC高速缓存一致性协议是一种非常有特色的带参并发系统,对此协议的带参验证是一个很大的挑战.Cubicle是最近出现的基于SMT求解器的带参模型检测工具.我们使用了Cubicle带参模型检测工具,成功对RCC协议进行了建模和验证.实验结果表明,RCC协议在结点个数为任意规模时均满足协议的各种安全性质. 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.
作者 孙鲁明 周琰
机构地区 中国科学院软件研究所 中国科学院大学 微软中国有限公司
出处 《计算机系统应用》 2014年第11期10-15,共6页 Computer Systems & Applications
关键词 众核处理器 缓存一致性协议 带参模型检测 RCC Godson-T many-core processor cache coherence protocol parameterized model checking RCC Godson-T
分类号 TP332 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献15

  • 1周琰.Godson-T缓存一致性协议的Murphi建模和验证[J].计算机系统应用,2013,22(10):124-128. 被引量：3
  • 2Abdulla PA, Delzanno Q Rezine A. Parameterized verification ofinfinite-state processes with global conditions. Computer AidedVerification. Springer Berlin Heidelbei^, 2007:145-157.
  • 3Abdulla PA, Delzanno G, Henda NB, et al. Regular modelchecking without transducers (on efficient verification ofparameterized systems). Tools and Algorithms for theConstruction and Analysis of Systems. Springer BerlinHeidelberg, 2007: 721-736.
  • 4Chou CT, Mannava PK, Park S. A simple method forparameterized verification of cache coherence protocols.Formal Methods in Computer-Aided Design. Springer BerlinHeidelberg, 2004: 382-398.
  • 5Cimatti A, Clarke E,Giunchiglia F,et al. NuSMV: A newsymbolic model verifier. Computer Aided Verification.Springer Berlin Heidelberg, 1999: 495-499.
  • 6Conchon S, Goel A, ICrstic S,et al. Cubicle: A parallelSMT-based model checker for parameterized systems.Computer Aided Verification. Springer Berlin Heidelberg,2012:718-24.
  • 7Das S,Dill D L,Park S. Experience with predicate abstraction.Computer Aided Verification. Springer Berlin Heidelberg,1999: 160-171.
  • 8Dill DL. The Mur<p verification system. Computer AidedVerification. Springer Berlin Heidelberg, 1996: 390-393.
  • 9Emerson EA, Kahlon Y. Reducing model checking of themany to the few. Automated Deduction-CADE-17. SpringerBerlin Heidelberg, 2000: 236-254.
  • 10Fan D, Zhang H,Wang D,et al. Godson-T: An efficientmany-core processor exploring thread-level parallelism.Micro, IEEE, 2012,32(2): 38-47.

二级参考文献7

  • 1Cadence Berkeley Lab. Cadence SMV.http://www.kenmcmil.com/smv.html, 1998.
  • 2Shahar E, Pnueli A. The TLV system and its applications[Master Thesis]. Weizmann Institute of Science. Israel, 1996.
  • 3Cimatti A, Clarke E, Giunchiglia F,Roveri M. NuSMV: A newsymbolic model verifier. In: Halbwachs N, Peled D,eds. CAV1999. LNCS, Springer Berlin Heidelberg, 1999,1633:682-682.
  • 4Cimatti A, Clarke E,Giunchiglia E, Giunchiglia F, Pistore M,Roveri M, Sebastiani R,Tacchella A. NuSMV 2: An openso-urce tool for symbolic model checking. In: Brinksma E,Larsen K, eds. CAV 2002,LNCS, Springer Berlin Heidelberg,2002, 2404: 359-364.
  • 5School of Computing. Stanford: Murphi Model Check, http://Avwwxs.titah.edu/formal_verification/Murphi/.
  • 6Sorin DJ, Hill MD, Wood DA. A primer on memoryconsistency and cache coherenc. Synthesis Lectures onComputer Architecture, 2011.
  • 7林伟,叶笑春,宋风龙,张浩.众核处理器中使用写掩码实现混合写回/写穿透策略[J].计算机学报,2008,31(11):1918-1928. 被引量：5

共引文献2

同被引文献15

  • 1Dill DL.The Murphi verification system.Computer Aided Verification.Springer Berlin Heidelberg,1996:390-393.
  • 2Cimatti A.,Clarke E,Giunchiglia R NuSMV:a new symbolic model verifier.Computer Aided Verification,1999:495-499.
  • 3Park S,Dill DL.Protocol verification by aggregation of distributed Trans.ComputerAided Verification,1996:300-310.
  • 4Clarke E,Long D,McMillan K.Compositional model checking.LICS,1989:353-362.
  • 5Cadence Berkeley Labs.Cadence smv,http://www.kemncmil.com/smv.html.1998.
  • 6McMillan KL.Parameterized verification of the FLASH cache coherence protocol by compositional model checking.CHARME,2001:179-195.
  • 7McMillan KL.Verification of infinite state systems by compositional model checking.CHARME,1999:219-237.
  • 8Chou CT,Mannava PK,Park S.A simple method for parameterized verification of cache coherence protocols.Formal Methods in Computer-Aided Design,2004:382-398.
  • 9Conchon S,Goelz A,Krsticz S.Invariants for finite instances and beyond.Formal Methods in Computer-Aided Design,2013:61-68.
  • 10Conchon S,Goel A,Krstic S,Mebsout A,Zaidi F.Cubicle:a parallel SMT-based model checker for parameterized systems.Computer Aided Verification,2012:718-724.

引证文献1

二级引证文献2

计算机系统应用
2014年 第11期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部