论文部分内容阅读
片上多核处理器和片上众核处理器已成为目前处理器结构的主流方向。在处理器从单核向多核(众核)演进过程中,多核处理器中的存储系统的变化最为显著,并对多核处理器存储系统的验证工作形成了新的挑战。本文在多核处理器存储系统的验证方面进行了研究,论文研究的主要内容是Cache一致性协议的验证和存储一致性模型的正确性确认,并在Intel MESIF协议的形式建模和模型检测,存储一致性模型的快速验证方法和工具实现方面取得了一定的进展。本文创造性的工作主要有三个方面：(1)分析了用于Intel Nehalem微结构的MESIF Cache一致性协议,使用SMV形式语言对其建模。通过分析NuSMV工具在协议的模型检测过程中的反例,对协议进行了精化,首次建立了MESIF协议在微结构级的SMV形式模型。Cache一致性协议验证的难点在于带参协议的验证,我们使用PaTLV工具对带参MESIF协议并进行了验证,这是带参模型检测方法在工业级Cache一致性协议验证方面的有益尝试。(2)提出了一种快速动态验证存储一致性模型的方法。利用多核处理器系统中通用的性能计数器,通过定期扫描性能计数器以获得关键的活动访存指令集合的信息。在此基础上,可以获得访存指令集合之间一种自然存在的时间序关系。在时间序约束下,对存储一致性模型的验证可以局部化,因此存储一致性验证的时间复杂度被大大降低,是目前能用于流片后阶段验证的时间复杂度最低的方法。(3)实现了一个通用的存储一致性模型验证工具MOTEC+。MOTEC+能够验证多种存储一致性模型,包括：顺序一致性模型,处理器一致性模型,释放一致性模型等。实验结果表明MOTEC+工具能够快速地验证多种存储一致性模型。