本文選題：多核處理器 + 存儲(chǔ)一致性模型　； 參考：《西北大學(xué)》2013年博士論文

【摘要】：片上多核處理器和片上眾核處理器已成為目前處理器結(jié)構(gòu)的主流方向。在處理器從單核向多核(眾核)演進(jìn)過程中,多核處理器中的存儲(chǔ)系統(tǒng)的變化最為顯著,并對(duì)多核處理器存儲(chǔ)系統(tǒng)的驗(yàn)證工作形成了新的挑戰(zhàn)。本文在多核處理器存儲(chǔ)系統(tǒng)的驗(yàn)證方面進(jìn)行了研究,論文研究的主要內(nèi)容是Cache一致性協(xié)議的驗(yàn)證和存儲(chǔ)一致性模型的正確性確認(rèn),并在Intel MESIF協(xié)議的形式建模和模型檢測(cè),存儲(chǔ)一致性模型的快速驗(yàn)證方法和工具實(shí)現(xiàn)方面取得了一定的進(jìn)展。 本文創(chuàng)造性的工作主要有三個(gè)方面： (1)分析了用于Intel Nehalem微結(jié)構(gòu)的MESIF Cache一致性協(xié)議,使用SMV形式語言對(duì)其建模。通過分析NuSMV工具在協(xié)議的模型檢測(cè)過程中的反例,對(duì)協(xié)議進(jìn)行了精化,首次建立了MESIF協(xié)議在微結(jié)構(gòu)級(jí)的SMV形式模型。Cache一致性協(xié)議驗(yàn)證的難點(diǎn)在于帶參協(xié)議的驗(yàn)證,我們使用PaTLV工具對(duì)帶參MESIF協(xié)議并進(jìn)行了驗(yàn)證,這是帶參模型檢測(cè)方法在工業(yè)級(jí)Cache一致性協(xié)議驗(yàn)證方面的有益嘗試。 (2)提出了一種快速動(dòng)態(tài)驗(yàn)證存儲(chǔ)一致性模型的方法。利用多核處理器系統(tǒng)中通用的性能計(jì)數(shù)器,通過定期掃描性能計(jì)數(shù)器以獲得關(guān)鍵的活動(dòng)訪存指令集合的信息。在此基礎(chǔ)上,可以獲得訪存指令集合之間一種自然存在的時(shí)間序關(guān)系。在時(shí)間序約束下,對(duì)存儲(chǔ)一致性模型的驗(yàn)證可以局部化,因此存儲(chǔ)一致性驗(yàn)證的時(shí)間復(fù)雜度被大大降低,是目前能用于流片后階段驗(yàn)證的時(shí)間復(fù)雜度最低的方法。 (3)實(shí)現(xiàn)了一個(gè)通用的存儲(chǔ)一致性模型驗(yàn)證工具M(jìn)OTEC+。MOTEC+能夠驗(yàn)證多種存儲(chǔ)一致性模型,包括：順序一致性模型,處理器一致性模型,釋放一致性模型等。實(shí)驗(yàn)結(jié)果表明MOTEC+工具能夠快速地驗(yàn)證多種存儲(chǔ)一致性模型。
[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.
【學(xué)位授予單位】：西北大學(xué)
【學(xué)位級(jí)別】：博士
【學(xué)位授予年份】：2013
【分類號(hào)】：TP333

【參考文獻(xiàn)】

相關(guān)期刊論文 前2條

1 林惠民,張文輝;模型檢測(cè):理論、方法與應(yīng)用[J];電子學(xué)報(bào);2002年S1期

2 王朋宇;陳云霽;沈海華;陳天石;張珩;;片上多核處理器存儲(chǔ)一致性驗(yàn)證[J];軟件學(xué)報(bào);2010年04期

相關(guān)博士學(xué)位論文 前1條

1 王耀彬;多核平臺(tái)上支持推測(cè)并行化的事務(wù)存儲(chǔ)體系結(jié)構(gòu)性能優(yōu)化[D];中國科學(xué)技術(shù)大學(xué);2010年

相關(guān)碩士學(xué)位論文 前1條

1 陳石坤;多核處理器中CACHE一致性協(xié)議研究和實(shí)現(xiàn)[D];國防科學(xué)技術(shù)大學(xué);2005年

，

本文編號(hào)：2077617