随着单核处理器越来越不能满足人们的需要，多核
与众核处理器逐渐成为了 目前的主流 ． 如今， 无 论是个
一
对于一个一致性协议 的建模 和验证有很多种方式 ．
般 来说 ， 缓存 一致性 协议都 是强一致 性 的，因此都 是先 将缓存 一致性 协议从存储 系统 中剥离 出来， 用 形 式化语言进 行描述 和建模，通常模 型检测 的方 法是用 状态迁移 系统表示模型，用 时序 逻辑公 式表 示待验证
（ Ｕｎ ｉ ｖ ｅ ｒ ｓ ｉ ｔ ｙ ｏ ｆ Ｃ ｈ ｉ ｎ ｅ ｓ ｅ Ａ ｃ ａ ｄ ｅ ｍｙ ｏ ｆ Ｓ ｃ ｉ ｅ ｎ ｃ ｅ ｓ ， Ｂ ｅ ｉ ｊ ｉ ｎ ｇ １ ０ ０ １ ９ ０ ， Ｃ ｈ ｉ ｎ ａ ）
Ａｂｓ ｔ ｒ ａ ｃ ｔ ：Ｇｏ ｄｓ ｏ ｎ — Ｔ ｃ ａ ｃ ｈ ｅ ｃ ｏ ｈ ｅ ｒ ｅ ｎ ｃ ｅ ｐ ｒ ｏ ｔ ｏ ｃ ｏ ｌ ｉ ｓ ｕ ｓ ｅ ｄ ｉ ｎ Ｇｏ ｄ ｓ ｏ ｎ ． Ｔ ｍａ ｎ ｙ ． ｃ ｏ ｒ ｅ ａ ｒ ｃ ｈ ｉ ｔ ｅ ｃ ｔ ｕ ｒ ｅ ．Ｉ ｎ Ｇｏ ｄ ｓ ｏ ｎ ． Ｔ．ｔ ｈ ｅ ｒ ｅ ｉ Ｓ ａ ｃ ｌ ｏ ｓ ｅ ｔ ｉ ｇ ｈ ｔ ｃ ｏ ｕ ｐ ｌ ｉ ｎ ｇ ｒ ｅ ｌ ａ ｔ ｉ ｏ ｎ ｓ ｈ ｉ ｐ ｂ ｅ ｔ ｗｅ ｅ ｎ ｃ ａ ｃ ｈ ｅ ｃ ｏ ｈｅ ｒ ｅ ｎ ｃ ｅ ｐ ｒ ｏ ｔ ｏ ｃ ｏ ｌ ａ ｎ ｄ ｍｅ ｍｏ ｒ ｙ ｃ ｏ ｎ ｓ ｉ ｓ ｔ ｅ ｎ ｃ ｙ ｍｏ ｄ ｅ １ ． Ｉ ｎ ｏ ｕ ｒ ｒ ｅ ｓ ｅ ａ ｒ ｃ ｈ ｏ ｆ
计 算 机 系 统 应 用
ｈ ｔ ｔ ｐ ： ／ ／ ｗ ｗｗ ． Ｃ — Ｓ － ａ ． ｏ ｒ ｇ ． ｃ ｎ
２ ０ １ ３年 第 ２ ２卷 第 １ ０期
Ｇ ｏ ｄ ｓ ｏ ｎ － Ｔ缓存一致性协议的 Ｍｕ ｒ ｐ ｈ ｉ 建模和验
周 琰
（ 中国科学 院软件研究所，北京 １ ０ ０ １ ９ ０ ） （ 中国科学 院大学，北京 １ ０ ０ １ ９ ０ ）
ｍｏ ｄ ｅ ｌ ｉ ｎ ｇ ｌ ａ ｎ ｇ ｕ ａ ｇ ｅ ａ ｎ ｄ ｖ ｅ ｒ ｉ ｉ ｆ ｃ ａ ｔ ｉ ｏ ｎ ｔ ｏ ｏ １ ． Ｔ ｈ ｕ ｓ ， ｗｈ ｅ ｎ ｗｅ ｍｏ ｄ ｅ ｌ ｉ ｎ ｇ Ｇｏ ｄ ｓ ｏ ｎ — Ｔ ， ｃ ｏ ｒ ｅ ， ｃ ａ ｃ ｈ ｅ ａ ｎ ｄ ｍｅ ｍｏ ｙ ｒ ｍｕ ｓ ｔ ｂ ｅ ｔ ａ ｋ ｅ ｉ ｎ ｔ ｏ
Ｇｏ ｄ ｓ ｏ ｎ － Ｔ ＇ ｗｅ ｆ ｏ ｕ ｎ ｄ ｔ ｈ ａ ｔ ｉ ｔ ｓ ｃ ａ ｃ ｈ ｅ ｃ ｏ ｈ ｅ ｒ ｅ ｎ ｃ ｅ ｉ Ｓ ｒ ｅ ｌHale Waihona Puke Baiduａ ｘ ｅ ｄ ｕ ｎ ｌ ｉ ｋ ｅ ｏ ｔ ｈ ｅ ｒ ｃ ａ ｃ ｈ ｅ ｃ ｏ ｈ ｅ ｒ ｅ ｎ ｃ ｅ ｐ ｒ ｏ ｔ ｏ ｃ ｏ ｌ ｓ ． Ｗｅ ｃ ｈ ｏ ｏ ｓ ｅ Ｍｕ ｒ ｐ ｈ ｉ ａ ｓ
： （ Ｉ ｎ ｓ ｔ ｉ ｔ ｕ ｔ ｅ ｏ ｆ Ｓ ｏ ｆ ｔ ｗ ａ ｒ ｅ ， Ｃ ｈ ｉ ｎ ｅ ｓ ｅ Ａ ｃ ａ ｄ ｅ ｍ ｙ ｏ ｆ Ｓ ｃ ｉ ｅ ｎ ｃ ｅ ｓ ， Ｂ ｅ ｉ ｊ ｉ ｎ ｇ １ ０ ０ １ ９ ０ ， Ｃ ｈ ｉ ｎ ａ ）
Ｍｏ ｄｅ ｌ ｉ ｎ ｇ ａ ｎｄ Ｖｅ ｒ ｉ ｉｃ ｆ ａ ｔ ｉ ｏ ｎ ｏ ｆ Ｇｏ ｄｓ ｏ ｎ － Ｔ Ｃａ ｃ ｈｅ Ｃｏ ｈｅ ｒ ｅ ｎｃ ｅ Ｐｒ ｏ ｔ ｏ ｃ ｏ ｌ ｗｉ ｔ ｈ Ｍ ｕｒ ｐｈｉ Ｔｏ ｏ ｌ
ＺＨ０Ｕ Ｙａ ｎ
性质 ， 然 后使用模 型检测 工具进行 全 自动验证 ．目前
人 电脑还 是大型服务器， 甚至是智能手机，都在使用 多 核或众核处理器． 多核和众核处理器 的发展中存在着一
系列重大的挑战． 其中一个重要的挑 战就是如何验证多
核处理器及其高速缓存之间的一致性问题． Ｇ ｏ ｄ ｓ ｏ ｎ － Ｔ是
致性协议和存储 一致性模 型存在紧密 的紧耦合关系，分析协 议的一致性 时发现 该协议满足 的缓存一致性不 是强
一
证工具． 在对 Ｇ ｏ ｄ ｓ ｏ ｎ — Ｔ缓存一 致性协议 建模 的时候，由于协议 的上述特点， 我们需要对处理器核结 点，高速缓 存 和 内存作为一个整体建模，并成功地验证 了协议的相关性质． 关键 词： 众核处理器；内存一致性模 型；缓存一致性协议；模型检测
摘
要： Ｇ ｏ ｄ ｓ ｏ ｎ － Ｔ 缓存一致 性协议 是用于 Ｇ ｏ ｄ ｓ ｏ ｎ ． Ｔ众核处理器 的缓存一致性协议． 在Ｇ ｏ ｄ ｓ ｏ ｎ ． Ｔ协议 中， 缓存 一
致性，不满足传统意 义上缓存透明的一致 性要求 ． 我们选取 了 Ｍｕ ｒ ｐ ｈ ｉ模型检测 工具作 为我们 建模的语 言和 验
ａ ｃ ｃ ｏ ｕ ｎ ｔ ａ ｓ ａ ｗｈ ｏ ｌ ｅ ． Ｓ ｏ ｍｅ ｉ ｎ ｖ ｒｉ ａ ｎｔ ａ ｓ ａ ｎ ｄ ｐ ｒ ｏ ｐ ｅ ｒ ｔ ｉ ｅ ｓ ｈ ａ ｓ ｂ ｅ ｅ ｎ ｖ ｅ ｒ ｉ ｆ ｉ ｅ ｄ ｗｉ ｔ ｈ Ｍｕ ｒ ｐｈ ｉ ． Ｋｅ ｙ ｗｏ ｒ ｄｓ ： ｍａ ｎ ｙ － ｃ ｏ ｒ ｅ ｐｒ ｏ ｃ ｅ ｓ ｓ ｅ ｒ ； ｍｅ ｍｏ ｙ ｒ ｃ ｏ ｎ ｓ ｉ ｓ ｔ ｅ ｎｃ ｙ ｍｏ ｄｅ ｌ ； ｃ ａ ｃ ｈｅ ｃ ｏ ｈ ｅ ｒ ｅ ｎ ｃ ｅ ｐ ｒ ｏ ｔ ｏ ｃ ｏ ｌ ； ｍｏ ｄ ｅ ｌ ｃ ｈ ｅ ｃ ｋｉ ｎ ｇ