隨著高性能計算機(jī)性能的不斷提升、規(guī)模不斷增大,Cache一致性協(xié)議變得異常復(fù)雜,協(xié)議的狀態(tài)數(shù)隨系統(tǒng)規(guī)模成指數(shù)級增長,導(dǎo)致狀態(tài)空間爆炸。為了緩解狀態(tài)空間爆炸問題對Cache一致性協(xié)議模型檢驗的影響,迫切需要研究模型檢驗優(yōu)化技術(shù)。本文深入剖析了模型檢驗工具M(jìn)urphi,介紹了Murphi的語法、模型檢驗的流程、執(zhí)行模式和采用的優(yōu)化技術(shù)。通過對簡單協(xié)議進(jìn)行驗證,分析并總結(jié)出模型檢驗中狀態(tài)數(shù)目與狀態(tài)分量的值域之間的關(guān)系,并歸納出Murphi中狀態(tài)空間分配規(guī)律,找出狀態(tài)空間爆炸現(xiàn)象出現(xiàn)的原因。抽象是緩解狀態(tài)空間爆炸問題的重要技術(shù)之一,它借助等價關(guān)系將原始模型映射到一個簡化的抽象模型。抽象模型相對于原始模型大大化簡,從而減少了模型檢驗時需要遍歷的狀態(tài)數(shù)目。本文提出了一種基于SMT求解器的謂詞抽象技術(shù)。首先對高級描述語言Murphi進(jìn)行BDD建模,將Murphi描述轉(zhuǎn)換成相應(yīng)的BDD公式；然后結(jié)合給定的謂詞,將抽象問題轉(zhuǎn)換成可滿足性模型理論問題,并利用最新的SMT求解器進(jìn)行求解；最后利用模型檢驗工具對抽象模型進(jìn)行驗證。實驗表明,基于SMT求解器的謂詞抽象能夠在保證驗證結(jié)果正確的同時顯著減少對狀態(tài)空間... 

【文章頁數(shù)】：65 頁

【學(xué)位級別】：碩士

【文章目錄】：
摘要
ABSTRACT
第一章 緒論
    1.1 研究背景
        1.1.1 Cache一致性協(xié)議是實現(xiàn)多處理機(jī)系統(tǒng)的關(guān)鍵
        1.1.2 Cache一致性協(xié)議驗證
    1.2 模型檢驗
        1.2.1 模型檢驗的發(fā)展歷程
        1.2.2 模型檢驗的過程
        1.2.3 模型檢驗的優(yōu)化技術(shù)
    1.3 Cache一致性協(xié)議模型檢驗研究現(xiàn)狀及存在的問題
    1.4 本文主要工作
    1.5 論文組織結(jié)構(gòu)
第二章 顯式模型檢驗中的狀態(tài)空間分析
    2.1 顯式模型檢驗工具M(jìn)urphi
        2.1.1 Murphi語法組成
        2.1.2 Murphi模型檢驗過程
        2.1.3 Murphi執(zhí)行模式
        2.1.4 Murphi壓縮技術(shù)
    2.2 Murphi狀態(tài)空間分析
        2.2.1 狀態(tài)空間爆炸分析
        2.2.2 Murphi的狀態(tài)空間分配規(guī)律
        2.2.3 各種壓縮方法的比較
    2.3 本章小結(jié)
第三章 基于SMT求解器的謂詞抽象技術(shù)
    3.1 謂詞抽象
        3.1.1 抽象算子和精化算子
        3.1.2 謂詞抽象算法
        3.1.3 謂詞抽象舉例
    3.2 基于SMT求解器的謂詞抽象
        3.2.1 SMT求解器
        3.2.2 BDD建模
        3.2.3 基于cvc3的謂詞抽象算法
    3.3 實驗結(jié)果
        3.3.1 經(jīng)典互斥協(xié)議簡介
        3.3.2 實驗結(jié)果
    3.4 本章小結(jié)
第四章 抽象算法改進(jìn)與Cache一致性協(xié)議模型檢驗
    4.1 關(guān)鍵算法及算法分析
        4.1.1 計算下一抽象狀態(tài)的公式與算法
        4.1.2 基于遞歸的一種改進(jìn)實現(xiàn)
        4.1.3 H函數(shù)遞歸實現(xiàn)算法分析
    4.2 關(guān)鍵算法的改進(jìn)
        4.2.1 遞歸與非遞歸的比較
        4.2.2 H函數(shù)的非遞歸實現(xiàn)
    4.3 Cache一致性協(xié)議建模
        4.3.1 Cache一致性協(xié)議模型
        4.3.2 Cache一致性協(xié)議流程
    4.4 Cache一致性協(xié)議的模型檢驗分析
        4.4.1 Cache一致性協(xié)議的模型檢驗測試
        4.4.2 Cache一致性協(xié)議的基于謂詞抽象的模型檢驗測試
        4.4.3 對比分析
    4.5 本章小結(jié)
第五章 結(jié)束語
    5.1 主要工作和創(chuàng)新點
    5.2 下一步研究展望
致謝
參考文獻(xiàn)
作者在學(xué)期間取得的學(xué)術(shù)成果


【參考文獻(xiàn)】：
期刊論文
[1]一種基于廣播的cache一致性協(xié)議的設(shè)計和驗證[J]. 李俊,袁愛東,高劍剛.  計算機(jī)科學(xué)與探索. 2008(05)
[2]謂詞抽象技術(shù)研究?[J]. 屈婉霞,李暾,郭陽,楊曉東.  軟件學(xué)報. 2008(01)
[3]模型檢驗中抽象技術(shù)研究綜述[J]. 屈婉霞,李暾,郭陽,楊曉東.  計算機(jī)工程與應(yīng)用. 2006(33)
[4]CMP中Cache一致性協(xié)議的驗證[J]. 李崇民,王海,李兆麟.  電子技術(shù)應(yīng)用. 2005(12)
[5]并發(fā)和實時系統(tǒng)的模型檢驗技術(shù)[J]. 董威,王戟,齊治昌.  計算機(jī)研究與發(fā)展. 2001(06)

碩士論文
[1]形式驗證技術(shù)的應(yīng)用研究[D]. 朱學(xué)仕.哈爾濱工程大學(xué) 2004



本文編號：3654392