###

DOI:

计算机系统应用英文版:2014,23(11):10-15

View/Add Comment 过刊浏览高级检索 HTML

←前一篇 | 后一篇→

码上扫一扫！

下载全文

RCC高速缓存一致性协议的带参验证

孙鲁明^1,2, 周琰³

(1.中国科学院软件研究所, 北京 100190;2.中国科学院大学, 北京 100490;3.微软中国有限公司, 苏州 215000)

Parameterized Verifation of RCC Cache Coherence Protocol

SUN Lu-Ming^1,2, ZHOU Yan³

(1.Institute of Software, Chinese Academy of Sciences, Beijing 100190, China;2.University of Chinese Academy of Sciences, Beijing 100190, China;3.MicrosoftChina Corporation, Ltd., Suzhou 215000, China)

摘要

图/表

参考文献

相似文献

本文已被：浏览 2037次下载 3446次
Received:March 11, 2014 Revised:April 14, 2014

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

中文关键词: 众核处理器缓存一致性协议带参模型检测 RCC Godson-T

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.

keywords: many-core processor cache coherence protocol parameterized model checking RCC Godson-T

文章编号： 中图分类号： 文献标志码：

基金项目:

Author Name	Affiliation
SUN Lu-Ming	Institute of Software, Chinese Academy of Sciences, Beijing 100190, China University of Chinese Academy of Sciences, Beijing 100190, China
ZHOU Yan	MicrosoftChina Corporation, Ltd., Suzhou 215000, China

Author Name	Affiliation
SUN Lu-Ming	Institute of Software, Chinese Academy of Sciences, Beijing 100190, China University of Chinese Academy of Sciences, Beijing 100190, China
ZHOU Yan	MicrosoftChina Corporation, Ltd., Suzhou 215000, China

引用文本：
孙鲁明,周琰.RCC高速缓存一致性协议的带参验证.计算机系统应用,2014,23(11):10-15
SUN Lu-Ming,ZHOU Yan.Parameterized Verifation of RCC Cache Coherence Protocol.COMPUTER SYSTEMS APPLICATIONS,2014,23(11):10-15