| Model Checking Data Consistency for Cache Coherence Protocols |
| |
| 引用本文： | Hong Pan,Hui-Min Lin,and Yi Lv. Model Checking Data Consistency for Cache Coherence Protocols[J]. 计算机科学技术学报, 2006, 21(5): 765-775. DOI: 10.1007/s11390-006-0765-6 |
| |
| 作者姓名： | Hong Pan Hui-Min Lin and Yi Lv |
| |
| 作者单位： | Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences, Bei＇jing 100080, P.R. China |
| |
| 基金项目： | Supported by the Intel Strategic CAD Labs, the National Natural Science Foundation of China （Grant No. 60421001）, and the Chinese Academy of Sciences. |
| |
| 摘 要： | A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are described as formulas in first-orderμ-calculus. A model checker is employed to check if the protocol under investigation satisfies the required properties. Using this method a data consistency error has been revealed in a well-known cache coherence protocol. The error has been corrected, and the revised protocol has been shown free from data consistency error for any data domain size, by appealing to data independence technique.
|
| 关 键 词： | 共点系统 高速缓存协议 自动校验 误差修正 |
| 收稿时间： | 2006-06-05 |
| 修稿时间： | 2006-06-052006-08-15 |
Model Checking Data Consistency for Cache Coherence Protocols |
| |
| Hong Pan,Hui-Min Lin,Yi Lv. Model Checking Data Consistency for Cache Coherence Protocols[J]. Journal of Computer Science and Technology, 2006, 21(5): 765-775. DOI: 10.1007/s11390-006-0765-6 |
| |
| Authors: | Hong Pan Hui-Min Lin Yi Lv |
| |
| Affiliation: | (1) Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, 100080, P.R. China |
| |
| Abstract: | A method for automatic verification of cache coherence protocols is presented, in which cache coherence protocols are modeled as concurrent value-passing processes, and control and data consistency requirement are described as formulas in first-order p-calculus. A model checker is employed to check if the protocol under investigation satisfies the required properties. Using this method a data consistency error has been revealed in a well-known cache coherence protocol. The error has been corrected, and the revised protocol has been shown free from data consistency error for any data domain size, by appealing to data independence technique. |
| |
| Keywords: | concurrent systems cache coherence protocols value-passing symbolic transition graphs model checking |
| 本文献已被 CNKI 维普 万方数据 SpringerLink 等数据库收录！ |
| 点击此处可从《计算机科学技术学报》浏览原始摘要信息 |
|
点击此处可从《计算机科学技术学报》下载免费的PDF全文 |
