RCC高速缓存一致性协议的带参验证
DOI:
CSTR:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:


Parameterized Verifation of RCC Cache Coherence Protocol
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    Godson-T众核处理器的RCC高速缓存一致性协议是一种非常有特色的带参并发系统, 对此协议的带参验证是一个很大的挑战. Cubicle是最近出现的基于SMT求解器的带参模型检测工具. 我们使用了Cubicle带参模型检测工具, 成功对RCC协议进行了建模和验证. 实验结果表明, RCC协议在结点个数为任意规模时均满足协议的各种安全性质.

    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.

    参考文献
    相似文献
    引证文献
引用本文

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

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2014-03-11
  • 最后修改日期:2014-04-14
  • 录用日期:
  • 在线发布日期: 2014-11-20
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京海淀区中关村南四街4号 中科院软件园区 7号楼305房间,邮政编码:100190
电话:010-62661041 传真: Email:csa (a) iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号