多核处理器存储系统的验证方法研究

发布时间：2018-06-28 10:03

本文选题：多核处理器 + 存储一致性模型　；参考：《西北大学》2013年博士论文

【摘要】：片上多核处理器和片上众核处理器已成为目前处理器结构的主流方向。在处理器从单核向多核(众核)演进过程中,多核处理器中的存储系统的变化最为显著,并对多核处理器存储系统的验证工作形成了新的挑战。本文在多核处理器存储系统的验证方面进行了研究,论文研究的主要内容是Cache一致性协议的验证和存储一致性模型的正确性确认,并在Intel MESIF协议的形式建模和模型检测,存储一致性模型的快速验证方法和工具实现方面取得了一定的进展。本文创造性的工作主要有三个方面： (1)分析了用于Intel Nehalem微结构的MESIF Cache一致性协议,使用SMV形式语言对其建模。通过分析NuSMV工具在协议的模型检测过程中的反例,对协议进行了精化,首次建立了MESIF协议在微结构级的SMV形式模型。Cache一致性协议验证的难点在于带参协议的验证,我们使用PaTLV工具对带参MESIF协议并进行了验证,这是带参模型检测方法在工业级Cache一致性协议验证方面的有益尝试。 (2)提出了一种快速动态验证存储一致性模型的方法。利用多核处理器系统中通用的性能计数器,通过定期扫描性能计数器以获得关键的活动访存指令集合的信息。在此基础上,可以获得访存指令集合之间一种自然存在的时间序关系。在时间序约束下,对存储一致性模型的验证可以局部化,因此存储一致性验证的时间复杂度被大大降低,是目前能用于流片后阶段验证的时间复杂度最低的方法。 (3)实现了一个通用的存储一致性模型验证工具MOTEC+。MOTEC+能够验证多种存储一致性模型,包括：顺序一致性模型,处理器一致性模型,释放一致性模型等。实验结果表明MOTEC+工具能够快速地验证多种存储一致性模型。
[Abstract]:Multi-core processors and multi-core processors on-chip have become the mainstream of the current processor architecture. In the process of processor evolution from single core to multi-core (multi-core), the storage system in multi-core processor has the most significant changes, and has posed a new challenge to the verification of multi-core processor storage system. In this paper, the verification of multi-core processor storage system is studied. The main content of this paper is the verification of cache conformance protocol and the correctness confirmation of storage consistency model, and the formal modeling and model checking of Intel MESIF protocol. Some progress has been made in the fast verification method and tool implementation of the storage consistency model. The creative work of this paper mainly includes three aspects: (1) the MESIF Cache conformance protocol for Intel Nehalem microstructure is analyzed, and the SMV formal language is used to model it. By analyzing the counterexample of NuSMV tool in the process of protocol model checking, the protocol is refined, and the difficulty of verifying the SMV formal model. Cache consistency protocol of MESIF protocol at the microstructure-level for the first time is the verification of reference protocol. We use the PaTLV tool to verify the parameterized MESIF protocol, which is a useful attempt of the parameterized model checking method in the industrial Cache conformance protocol verification. (2) A fast and dynamic method to verify the storage conformance model is proposed. Using the common performance counter in the multi-core processor system, the information of the key active memory access instruction set is obtained by scanning the performance counter periodically. On this basis, a kind of natural time order relation between memory access instruction set can be obtained. Under the time order constraint, the verification of the storage consistency model can be localized, so the time complexity of the storage consistency verification is greatly reduced. It is the method with the lowest time complexity that can be used in the post-stream phase verification. (3) A general storage consistency model verification tool MOTEC. MOTEC can verify a variety of storage consistency models, including: sequential consistency model. Processor consistency model, release consistency model, etc. Experimental results show that MOTEC tools can quickly verify multiple storage consistency models.
【学位授予单位】：西北大学
【学位级别】：博士
【学位授予年份】：2013
【分类号】：TP333

【参考文献】