基于學(xué)習(xí)的緩存一致性協(xié)議帶參驗證

作者 李勇堅 中國科學(xué)院軟件研究所(北京100190)

李勇堅，博士，研究生導(dǎo)師，人工智能開放創(chuàng)新平臺*聯(lián)合學(xué)者，主要研究方向：計算機(jī)科學(xué)理論和軟件理論。

*注：人工智能開放創(chuàng)新平臺：是由貴陽市政府與中國人工智能產(chǎn)業(yè)創(chuàng)新聯(lián)盟、英特爾三方共同打造的開放平臺。平臺結(jié)合端到端的全面技術(shù)，打造軟硬件開放創(chuàng)新平臺，加速產(chǎn)業(yè)應(yīng)用創(chuàng)新，通過打造人工智能開放平臺、創(chuàng)立人工智能創(chuàng)新加速器等，建立完善的技術(shù)生態(tài)、在人工智能垂直領(lǐng)域應(yīng)用、產(chǎn)業(yè)對接和市場推廣等發(fā)揮各方優(yōu)勢和資源特色，加速中國人工智能的發(fā)展和應(yīng)用創(chuàng)新。

　　0引言

　　帶參系統(tǒng)存在于許多應(yīng)用領(lǐng)域中，比如緩存一致協(xié)議等。因為它的研究價值，驗證這樣的系統(tǒng)也就吸引來了形式化驗證、模型檢測和定理證明等社區(qū)的關(guān)注。要想驗證帶參系統(tǒng)的正確性，就必須驗證任意實例大小的系統(tǒng)中的正確性，而這被證明是一個無法判定的問題。

　　盡管這樣的難度，但是很多方法仍然被提出來試圖解決這個問題。CMP方法是其中最成功的方法之一。它用模型檢測的方法來驗證Intel、flash等大型的協(xié)議。通過保留m個節(jié)點(diǎn)，并用一個抽象的節(jié)點(diǎn)NOther來替代其他所有剩余節(jié)點(diǎn)的行為。通過這樣的抽象，一個原始的協(xié)議就被抽象成了一個由m+1個節(jié)點(diǎn)組成的抽象寫意。然后通過分析模型檢測器提供的反例，循環(huán)構(gòu)造一系列引理來限制抽象節(jié)點(diǎn)NOther的行為，使得協(xié)議可以收斂，且不會違反原有性質(zhì)。如果最終原始性質(zhì)和引理都能在抽象協(xié)議中被檢驗通過，那么就能推導(dǎo)出原始協(xié)議在任意大小的實例下也都能成立。但是，CMP方法是在模型檢測機(jī)給出反例之后，采取的是被動補(bǔ)救措施。這樣的被動方法由于依賴于人工理解和指導(dǎo)，而無法自動化。而且“尋找反例-衛(wèi)式加強(qiáng)”這樣的循環(huán)，所需要的次數(shù)未知，這也就使得可達(dá)集是否能收斂、抽象協(xié)議能否滿足安全性質(zhì)成為未知。

　　CMP存在的缺點(diǎn)啟發(fā)我們?nèi)ジ钊氲厮伎迹菏欠衲軌蛲ㄟ^主動地探索滿足上述條件的可達(dá)集邊緣，以使可達(dá)集收斂，并滿足安全性質(zhì)?如果能夠主動的限定可達(dá)集能到達(dá)的范圍，則可以更主動地搜索輔助不變式，從而更精確地加強(qiáng)抽象系統(tǒng)。

　　因此，在這篇論文中，我們提出了L-CMP，一種自動的學(xué)習(xí)框架，通過較小實例可達(dá)集學(xué)習(xí)/挖掘輔助不變式，并且自動的用這些輔助不變式對抽象協(xié)議進(jìn)行限制，最終，抽象協(xié)議的可達(dá)集可以被收斂在合理范圍，安全性質(zhì)也就能夠保證。

　　1關(guān)聯(lián)規(guī)則學(xué)習(xí)

　　在本文中，我們巧妙地將關(guān)聯(lián)規(guī)則學(xué)習(xí)(Association rule learning)與衛(wèi)式加強(qiáng)做結(jié)合，成功達(dá)到了尋找輔助不變式及自動衛(wèi)式加強(qiáng)的目的。

　　關(guān)聯(lián)規(guī)則學(xué)習(xí)是Agrawal等人提出的基于規(guī)則的機(jī)器學(xué)習(xí)方法。它的目的是利用一些有趣性的量度來識別數(shù)據(jù)庫中發(fā)現(xiàn)的強(qiáng)規(guī)則?；趶?qiáng)規(guī)則的概念，Rakesh Agrawal等人引入了關(guān)聯(lián)規(guī)則以發(fā)現(xiàn)由超市的POS系統(tǒng)記錄的大批交易數(shù)據(jù)中產(chǎn)品之間的規(guī)律性。許多有效的關(guān)聯(lián)規(guī)則算法，如Apriori, Eclat和FP-growth。在本文中，我們使用Apriori作為關(guān)聯(lián)規(guī)則的學(xué)習(xí)算法進(jìn)行學(xué)習(xí)。

　　給定由一組事務(wù)組成的數(shù)據(jù)集D，記為D={t1，t2，…，tm}。設(shè)I={i1，i2，…，in}是一組包含許多項目的項集。每個交易t包含一個項目子集。一個關(guān)聯(lián)規(guī)則的形式是X→Y，其中X，Y∈I.X被稱為前件，Y是規(guī)則的后件。此外，還有一些約束條件來衡量規(guī)則的重要性。在本文中，我們重點(diǎn)關(guān)注兩個標(biāo)準(zhǔn)：支持度和置信度。

　　支持度：它測量在同一事務(wù)中發(fā)生的項目集的頻率。K頻繁項目集是頻繁集合中包含K個項目的項目集?？梢詫⒅С钟嬎銥樵谕皇聞?wù)中出現(xiàn)多個項目的概率。支持價值的最低閾值被稱為最小支持度。

　　2框架

　　L-CMP可以分為以下兩個階段，如圖1。

　　2.1學(xué)習(xí)不變式

　　這個階段旨在通過學(xué)習(xí)算法尋找出輔助不變量。在這個階段，我們首先收集協(xié)議的一個小實例m(通常是m=2)的可達(dá)狀態(tài)集合(步驟1)。然后，我們直接從協(xié)議描述中提取原子謂詞，并將它們看作項目集以指導(dǎo)數(shù)據(jù)集的轉(zhuǎn)換(步驟2)。這一步對于第二階段是必要的，第四節(jié)解釋了背后的原因。接下來，通過關(guān)聯(lián)規(guī)則學(xué)習(xí)，可以學(xué)習(xí)一組關(guān)聯(lián)規(guī)則(步驟3)。值得注意的是，我們使用的數(shù)據(jù)集由一個小型的協(xié)議實例進(jìn)行轉(zhuǎn)換，因此由于實例的大小有限，無法表示整個參數(shù)化協(xié)議的行為。此外，我們已經(jīng)應(yīng)用了對稱減少技術(shù)來使一些大協(xié)議中的可達(dá)狀態(tài)最小化，導(dǎo)致數(shù)據(jù)集的不完整性。因此，需要額外的步驟(步驟4)。我們將這些關(guān)聯(lián)規(guī)則視為候選不變量并將它們輸入模型檢查器Murphi。如果他們持有協(xié)議的一些小實例(大于m)，則它們被視為輔助不變量。如果某些失敗，失敗的將從候選不變集中消除。最后，左邊的候選不變量作為輔助不變量。

　　2.2參數(shù)抽象和衛(wèi)式加強(qiáng)

　　這個階段是抽象協(xié)議，并使用輔助不變量加強(qiáng)抽象規(guī)則的衛(wèi)式部分。首先，輔助不變量以及協(xié)議中的轉(zhuǎn)換規(guī)則將通過分配具體索引來實例化(步驟5)。這一步為加強(qiáng)步驟提供了便利。接下來，通過以關(guān)聯(lián)規(guī)則的形式添加輔助不變量的結(jié)果，遞歸地加強(qiáng)規(guī)則守護(hù)(步驟6)。然后，通過刪除關(guān)于不可觀察節(jié)點(diǎn)的局部變量來抽象加強(qiáng)的規(guī)則(步驟7)。值得注意的是，我們提出了一個映射操作，它建立了守衛(wèi)與行動之間的關(guān)系，以便最大限度地加強(qiáng)規(guī)則。之后，加強(qiáng)和抽象的規(guī)則將附加到原始協(xié)議并送入模型檢查器(步驟8)。請注意，用于加強(qiáng)守則規(guī)則的輔助不變量也需要驗證將它們翻譯成Murphi代碼后。自動翻譯的過程較為簡單，所以我們在本文中就不贅述。如果抽象協(xié)議實例通過大小為$m+1$的模型檢測器，則結(jié)束框架(步驟10)，否則就需要調(diào)整學(xué)習(xí)算法中的參數(shù)，并且框架開始下一輪學(xué)習(xí)(步驟9)。

　　3實驗結(jié)果

　　我們將L-CMP應(yīng)用于5個經(jīng)典的帶參協(xié)議上進(jìn)行實驗，實驗結(jié)果如表1。其中，列名分別為協(xié)議名稱、頻繁集個數(shù)、最小支持度、關(guān)聯(lián)規(guī)則個數(shù)、輔助不變式個數(shù)、所用不變式個數(shù)、總運(yùn)行時長、所耗內(nèi)存峰值、抽象協(xié)議能否通過驗證?？梢钥吹剑覀兊腖-CMP能夠很好地對包括Flash協(xié)議在內(nèi)的各個協(xié)議進(jìn)行很好的驗證。

　　4結(jié)論

　　在本文中，我們提出了一個自動框架L-CMP，它可以在一個統(tǒng)一的框架中自動學(xué)習(xí)輔助不變量，并進(jìn)行抽象參數(shù)和衛(wèi)式加強(qiáng)。我們工作的創(chuàng)新性集中體現(xiàn)在于以下兩個方面：1.我們不是通過分析計數(shù)器例子來手動制定不同的變體，而是通過關(guān)聯(lián)規(guī)則學(xué)習(xí)從協(xié)議的可達(dá)狀態(tài)集合中導(dǎo)出不變量;2.在反例生成之后，我們不再強(qiáng)化協(xié)議，而是根據(jù)自動學(xué)習(xí)的不變量直接進(jìn)行衛(wèi)式加強(qiáng)。在未來的工作中，我們希望擴(kuò)展L-CMP的驗證能力，使其能證明一般的安全性質(zhì)和活性性質(zhì)，而不僅局限于不變式。

　　參考文獻(xiàn)：

　　[1]Lv Y,Lin H,Pan H.Computing invariants for parameter abstraction.In: Proceedings of the 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign, IEEE Computer Society (2007):29–38

　　[2]Apt K R, Kozen D C.Limits for automatic verification of finite-stateconcurrent systems. Information Processing Letters 22(6) (1986) :307–309

　　[3]Chou C T,Mannava P K,Park S.A simple method for parameterized verification of cache coherence protocols. In: FMCAD. Volume 4., Springer (2004):382–398

　　[4]Agrawal R,Imielin ?ski,T.,Swami A.Mining association rules between sets of items in large databases. In: Acm sigmod record. Volume 22.,ACM (1993):207–216

本文來源于中國科技期刊《電子產(chǎn)品世界》2019年第1期第82頁，歡迎您寫論文時引用，并注明出處