片上多核处理器存储一致性验证

存储一致性验证是片上多核处理器功能验证的重要部分.由于验证并行程序的执行结果是否符合存储一致性模型理论上是np难问题,现有的验证方法中只能采用一些时间复杂度大于o(n3)的不完全方法.发现在支持写原子性的多处理器系统中,两条执行时间不重叠的操作之间存在确定的时间序.通过引入时间序的概念,设计并实现了一种线性时间复杂度的存储一致性验证工具lcheck.lcheck利用时间序将验证局部化,使得在表示程序执行结果的有向图中,序关系边的推导和正确性检测都被限定在有限范围内.与现有其他方法相比,lcheck时间复杂度低,对程序长度和访存地址数没有限制,因此验证效率更高.作为国产片上多核处理器龙芯3号的重要验证工具,lcheck发现了一些存储系统的设计错误.