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

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

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

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

　　0引言

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

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

　　CMP存在的缺點啟發(fā)我們去更深入地思考：是否能夠通過主動地探索滿足上述條件的可達集邊緣，以使可達集收斂，并滿足安全性質?如果能夠主動的限定可達集能到達的范圍，則可以更主動地搜索輔助不變式，從而更精確地加強抽象系統(tǒng)。

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

　　1關聯(lián)規(guī)則學習

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

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

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

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

　　2框架

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

　　2.1學習不變式

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

　　2.2參數抽象和衛(wèi)式加強

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

　　3實驗結果

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

　　4結論

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

　　參考文獻：

　　[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

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