中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 软件所图书馆  > 期刊论文
Title:
Godson-T缓存一致性协议的Murphi建模和验证
Alternative Title: Modeling and Verification of Godson-T Cache Coherence Protocol with Murphi Tool
Author: 周琰
Keyword: 众核处理器 ; 内存一致性模型 ; 缓存一致性协议 ; 模型检测 ; many-core processer ; memory consistency model ; cache coherence protocol ; model checking
Source: 计算机系统应用
Issued Date: 2013
Issue: 10, Pages:124-128
Department: 中国科学院软件研究所,北京 100190; 中国科学院大学,北京 100190
Abstract: Godson-T 缓存一致性协议是用于Godson-T众核处理器的缓存一致性协议。在Godson-T协议中,缓存一致性协议和存储一致性模型存在紧密的紧耦合关系,分析协议的一致性时发现该协议满足的缓存一致性不是强一致性,不满足传统意义上缓存透明的一致性要求。我们选取了 Murphi 模型检测工具作为我们建模的语言和验证工具。在对Godson-T缓存一致性协议建模的时候,由于协议的上述特点,我们需要对处理器核结点,高速缓存和内存作为一个整体建模,并成功地验证了协议的相关性质。 Godson-T cache coherence protocol is used in Godson-T many-core architecture. In Godson-T, there is a close tight coupling relationship between cache coherence protocol and memory consistency model. In our research of Godson-T, we found that its cache coherence is relaxed unlike other cache coherence protocols. We choose Murphi as modeling language and verification tool. Thus, when we modeling Godson-T, core, cache and memory must be take into account as a whole. Some invariants and properties has been verified with Murphi.
Language: 中文
Content Type: 期刊论文
URI: http://ir.iscas.ac.cn/handle/311060/17004
Appears in Collections:软件所图书馆_期刊论文

Files in This Item:

There are no files associated with this item.


Recommended Citation:
周琰. Godson-T缓存一致性协议的Murphi建模和验证[J]. 计算机系统应用,2013-01-01(10):124-128.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[周琰]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[周琰]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2020  中国科学院软件研究所 - Feedback
Powered by CSpace