%0 Journal Article
%T 片上多核处理器存储一致性验证
%A 王朋宇？
%A 陈云霁？
%A 沈海华？
%A 陈天石？
%A 张珩？
%J 软件学报
%P 863-874
%D 2010
%X 存储一致性验证是片上多核处理器功能验证的重要部分.由于验证并行程序的执行结果是否符合存储一致性模型理论上是np难问题,现有的验证方法中只能采用一些时间复杂度大于o(n3)的不完全方法.发现在支持写原子性的多处理器系统中,两条执行时间不重叠的操作之间存在确定的时间序.通过引入时间序的概念,设计并实现了一种线性时间复杂度的存储一致性验证工具lcheck.lcheck利用时间序将验证局部化,使得在表示程序执行结果的有向图中,序关系边的推导和正确性检测都被限定在有限范围内.与现有其他方法相比,lcheck时间复杂度低,对程序长度和访存地址数没有限制,因此验证效率更高.作为国产片上多核处理器龙芯3号的重要验证工具,lcheck发现了一些存储系统的设计错误.
%K 存储一致性模型
%K 验证
%K 时间序
%K 片上多核处理器
%K 缓存一致性
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=3705&flag=1