国防科技大学学报
國防科技大學學報
국방과기대학학보
JOURNAL OF NATIONAL UNIVERSITY OF DEFENSE TECHNOLOGY
2008年
6期
47-52
,共6页
屈婉霞%郭阳%庞征斌%杨晓东
屈婉霞%郭暘%龐徵斌%楊曉東
굴완하%곽양%방정빈%양효동
形式化验证%模型检验%多处理机系统%Cache一致性协议
形式化驗證%模型檢驗%多處理機繫統%Cache一緻性協議
형식화험증%모형검험%다처리궤계통%Cache일치성협의
针对Cache一致性协议状态空间爆炸问题,提出共享集合伪临界值(Pseudo-cutoff)的概念,并以采用释放一致性模型的CC-NUMA系统为例,分析了共享数据的分布情况,推导出在一定条件下共享集合伪临界值为4的结论,有效优化了目录Cache协议状态空间,并提出了解决小概率的宽共享事件的方法.实验数据表明,基于伪临界值的协议模型优化,能够有效缩小Cache协议状态空间,加快验证速度,扩大验证规模.
針對Cache一緻性協議狀態空間爆炸問題,提齣共享集閤偽臨界值(Pseudo-cutoff)的概唸,併以採用釋放一緻性模型的CC-NUMA繫統為例,分析瞭共享數據的分佈情況,推導齣在一定條件下共享集閤偽臨界值為4的結論,有效優化瞭目錄Cache協議狀態空間,併提齣瞭解決小概率的寬共享事件的方法.實驗數據錶明,基于偽臨界值的協議模型優化,能夠有效縮小Cache協議狀態空間,加快驗證速度,擴大驗證規模.
침대Cache일치성협의상태공간폭작문제,제출공향집합위림계치(Pseudo-cutoff)적개념,병이채용석방일치성모형적CC-NUMA계통위례,분석료공향수거적분포정황,추도출재일정조건하공향집합위림계치위4적결론,유효우화료목록Cache협의상태공간,병제출료해결소개솔적관공향사건적방법.실험수거표명,기우위림계치적협의모형우화,능구유효축소Cache협의상태공간,가쾌험증속도,확대험증규모.
