基于流分析與歸納不變式結合的German協議驗證①

張 瑜,孫文輝

(北京交通大學 計算機與信息技術學院,北京 100044)

基于流分析與歸納不變式結合的German協議驗證①

張 瑜,孫文輝

(北京交通大學 計算機與信息技術學院,北京 100044)

German緩存一致性協議是用于共享內存的并發多處理器系統中的緩存一致性協議,對German協議進行形式化驗證一直是學術界和工業界的熱點.我們生成German協議的流圖,對流程圖的各個步驟進行詳細的描述,并提出了流分析與歸納不變式結合對協議驗證的方法,通過輔助不變式與協議流圖的對應關系,從而進一步分析和驗證German協議的正確性.

緩存一致性協議; 流分析; 歸納不變式; 形式化驗證

1 引言

帶參系統廣泛存在于計算機體系的核心模塊中,通常由參數個具有相同結構的并發執行的主體和有限個結構不同的主體組成.帶參系統在很多領域都有實際的應用,如緩存一致性協議,安全協議,網絡通信協議等,都可以用帶參系統描述.

German緩存一致性協議是作為形式化驗證領域的一個挑戰性問題于2000年由Steven German提出的一個基于地址目錄的緩存一致性協議,是帶參驗證中廣泛使用的例子.常用的驗證策略有兩種,即基于模型檢測的技術[1]和基于定理證明的技術[2].目前,有很多人采用不同的方法對German協議進行了形式化驗證,如:呂毅等采用了參數抽象與衛士加強[3]的方法;Baukus等采用謂詞抽象[4]的方法; Alan hu 采用截止的方法[5]; 曹燊等用了不變式查找[6]的方式,等等.但是這些方法中對German協議內容的描述都是不完整的,只有部分文字性的說明,這對于工程師而言不夠直觀和明確,也不易于準確理解協議的設計.針對這一問題,我們在German協議的驗證中引入了流圖的概念,協議流圖是對協議內容的一個圖形描述,在邏輯上精確地描述了協議的功能,以圖形的方式描述消息在協議流程中流動和處理的遷移過程,可以有效地幫助用戶理解、分析協議的設計.

本文通過生成German協議的流圖,并將流圖分析與歸納不變式結合起來對German協議進行驗證.本文的工作主要體現在以下方面:

① 生成German協議規則的完整的流圖,幫助人們準確理解German協議的設計;

② 將生成的輔助不變式與German協議的規則結合起來對不變式的含義進行說明;

③ 通過將輔助不變式與German協議的流圖對應結合,根據German協議的流圖解釋這些輔助不變式的含義,進一步對協議的設計進行說明.

2 German 協議描述

2.1 協議內容描述

German 協議是 Steven german 2000 年提出的基于地址目錄的緩存一致性協議[7],German協議主要適用共享存儲的并發多處理器系統,用來維護每個節點緩存的一致性.在這個協議中,有一個維護目錄的主節點Home和N個同構的用戶節點Client,Home節點作為地址目錄的一個中心控制部分,并擁有memory,地址目錄的功能是記錄各個Client中的Cache狀態(無效I、共享S、獨占E),多個Client節點(從控制中心申請共享或獨占一個內存地址).cache通過請求共享或者獨占memory,將memory中的數據讀入cache.

Home和Clients節點之間的消息分為4種,如圖1所示.

圖1 Home 和 Client節點傳遞的消息

從圖1可以看出這四種消息分別為:

① Client向Home節點發送的請求共享或者獨占內存的請求消息;

② Home向一個共享或獨占內存的Client節點發送的無效請求消息;

③ 共享或獨占內存的Client節點發送的無效響應消息;

④ Home向有請求的Client節點發送的請求響應消息.

Home和Clients節點之間的消息是通過三個單向的消息通道傳遞的,如圖2所示.

從圖2可以看出這三個單向的消息通道分別是:

① chan1處理Client向Home發送的請求消息(ReqS、ReqE);

② chan2處理Home向Client發送的無效消息(Inv)和請求響應的消息(GntS、GntE);

③ chan3處理Client向Home發送的無效響應消息(InvAck).

圖2 Home 和 Client之間的消息通道

2.2 協議流圖描述

協議流圖對協議的形式化驗證是有促進作用的.首先,流圖描述使協議中各個節點之間執行規則的因果關系變得非常清晰,也對各個節點之間的通信過程進行了說明,易于協議設計的理解; 其次,流圖分析直觀的表示了協議中消息的遷移過程,有助于對協議進行研究與驗證.

我們詳細分析了German協議的內容,并生成了German協議的規則流程圖,對流程圖中的步驟做了具體的說明,如圖3、4所示.

圖3是Client節點向Home節點發送的請求共享的消息,具體步驟如下.

① 一個Client節點請求需要共享數據緩存副本,執行規則SendReqS,向Home發送ReqS請求;

② Home節點接收到ReqS請求后查詢目錄directory的狀態信息,執行規則RecvReqS;

③ 當沒有其他Client節點處于獨占狀態時,則直接從 memory中讀取數據,執行規則 SendGntS,Home節點向有請求的Client節點發送GntS消息;

④ 當有其他Client節點處于獨占狀態時,執行規則SendInv,Home節點先對這些獨占狀態的Client節點發送Invalidate消息,使獨占緩存無效; 獨占狀態的Client節點發送無效響應消息,執行規則SendInvAck,向Home節點發送InvAck消息,Home節點收到InvAck消息,執行規則RecvInvAck,從InvAck消息中讀取數據,執行規則SendGntS,Home節點向有請求的Client節點發送GntS消息;

⑤ 有請求的這個Client節點收到GntS消息,執行規則RecvGntS,將緩存副本的狀態為共享.

圖4是Client節點向Home節點發送的請求獨占內存的消息,具體步驟如下.

① 一個Client節點請求需要獨占數據緩存副本,執行規則SendReqE,向Home發送ReqE請求;

② Home節點接收到ReqE請求后查詢目錄directory的狀態信息,執行規則RecvReqE;

③ 當沒有其他Client節點處于獨占狀態時,則直接從 memory中讀取數據,執行規則 SendGntE,Home節點向有請求的Client節點發送GntE消息;

④ 當有其他Client節點處于獨占狀態時,執行規則SendInv,Home節點先對這些獨占狀態的Client節點發送Invalidate消息,使獨占緩存無效; 獨占狀態的Client節點發送無效響應消息,執行規則SendInvAck,向Home節點發送InvAck消息,Home節點收到InvAck消息,執行規則RecvInvAck,從InvAck消息中讀取數據,執行規則SendGntE,Home節點向有請求的Client節點發送GntE消息;

⑤ 有請求的這個Client節點收到GntE消息,執行規則RecvGntE,將緩存副本的狀態為獨占,并執行規則Store,將數據寫入緩存副本中.

圖3 German 協議 ReqS 請求

圖4 German 協議 ReqE 請求

3 German 協議的歸納不變式

3.1 輔助不變式

我們在四核 Intel Xeon 2.4 GHz 處理器,8 GB 內存,64 位 Linux 3.15.10,Murphi版本為 cmurphi5.4.9 的環境下對German協議的Murphi[8,9]模型進行了實驗,實驗結果如表1所示.

表1 German 協議的實驗結果

從實驗結果可以看出,German協議共有69個輔助不變式,我們已經把查找到的所有輔助不變式放到了網上[10].我們選擇了有關ExGntd的所有不變式進行具體的描述分析,這些不變式也是協議性質的直觀描述,幫助我們理解協議變量的功能.

圖5 部分不變式

inv_21:(ExGntd=FALSE)Client節點的獨占狀態標識為FALSE,那么內存中的數據就一定是正確的數據.

inv_27:節點1的緩存狀態是獨占狀態,則該節點的獨占狀態標識為TRUE.

inv_28:節點1發送無效應答給Home節點,而節點的獨占狀態標識為TRUE,則節點1發送的數據是正確的數據.

inv_36:Home節點向節點1發送同意獨占消息,則該節點的獨占狀態標識為TRUE.

inv_37:節點的獨占狀態標識為TRUE,并且節點1的cache狀態不是獨占狀態,則Home節點不會向節點1發送無效消息.

inv_45:節點1的緩存狀態不是獨占狀態,Home發送空消息給節點1,節點1對應的InvSet為TRUE,則獨占狀態標識為FALSE.

inv_50:節點1的緩存狀態不是獨占狀態,Home發送空消息給節點1,節點1對應的ShrSet為TRUE,Home當前命令為空,則獨占狀態標識為FALSE.

inv_53:Home節點向節點1發送同意共享消息,則該節點的獨占狀態標識為FALSE.

inv_55:節點 1發送無效應答給 Home節點,而節點的獨占狀態標識為FALSE,則Home當前命令是請求共享.

inv_61:Home 向節點 1 發送無效消息,而節點的獨占狀態標識為FALSE,則Home當前命令是請求共享.

inv_68:節點 1 對應的 InvSet為 TRUE,且獨占狀態標識為TRUE,則節點2對應的InvSet為FALSE.

inv_69:節點 2 對應的 ShrSet為 TRUE,且獨占狀態標識為TRUE,則節點1對應的ShrSet為FALSE.

3.2 轉移規則與輔助不變式

我們選取規則RecvGntS和不變式((Cache[1].State= e)& (!(Cache[2].State = i)))進行具體的說明.

圖6 規則與不變式

轉移規則RecvGntS的賦值部分不改變不變式((Cache[1].State = e)& (!(Cache[2].State = i)))中的變量,那么不變式((Cache[1].State = e)& (!(Cache[2].State =i)))在規則RecvGntS執行后的狀態s1下成立.

如果狀態s滿足規則RecvGntS的衛士條件,并且存在輔助不變式 inv__22:((Cache[1].State = e)&(Chan2[2].Cmd = gnts)),執行規則 RecvGntS 后的狀態是 s1,那么不變式((Cache[1].State = e)& (!(Cache[2].State = i)))在狀態 s1成立.

4 通過不變式描述一個典型流

輔助不變式可以用來分析和驗證German協議的正確性,給出協議性質的完整描述.輔助不變式所反映的協議性質也是對協議運行過程的說明.

我們選取圖7的部分不變式,將這些不變式與German協議的ReqS請求的一個典型流結合,對German協議的內容做更深層的分析,幫助我們進一步理解German協議的設計.

圖7 部分不變式

當節點1請求共享,沒有其他節點處于獨占狀態時,執行規則SendGntS時,Home節點發送同意共享的消息到節點1,那么Home發送的數據一定是正確的數據,節點1和節點2的緩存狀態肯定不是獨占狀態,節點 1 對應的 ShrSet為 TRUE,對應不變式 inv_22,25,32,39 所示.

有其他節點處于獨占狀態,執行規則SendInvAck,節點1發送無效應答消息給Home,Home肯定不會給節點1發送同意共享消息,對應不變式inv_47.然后執行規則SendGntS時,Home節點發送同意共享的消息到節點1,那么ExGntd一定為FALSE.

5 結論

German緩存一致性協議是帶參驗證中經常使用一種帶參協議.我們提出了流分析與歸納不變式結合對協議驗證的方法,這種方法實現了對German協議的流圖分析,查找到German協議的所有輔助不變式,對這些輔助不變式的含義做了具體說明,并將輔助不變式與German協議的流圖對應結合,進一步分析和驗證了German協議設計的正確性.這種方法相對于現有的方法,對協議內容的描述更加直觀和明確,以圖形和文字結合的方式對German協議的內容做了完整的描述,流圖分析在邏輯上精確描述了協議的功能和消息在協議流程中的遷移過程,這對于人們理解和分析協議的內容和設計是非常有效的; 其次,根據已查找到的輔助不變式描述German協議流圖中的典型流,這些輔助不變式是協議性質的直觀描述,將不變式與協議流圖中的典型流結合,是對協議的內容和遷移過程更直觀的分析,從而驗證German協議設計的正確性.

1Clarke EM,Grumberg O,Peled DA.Model Checking.Cambridge:The MIT Press,1999.

2Nipkow T,Paulson LC,Wenzel M.Isabelle/HOL:A proof assistant for higher-order logic.Berlin Heidelberg:Springer,2002.

3Lv Y,Lin HM,Pan H.Computing invariants for parameter abstraction.Proc.of the 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign.Nice,France.2007.29–38.

4Baukus K,Lakhnech Y,Stahl K.Parameterized verification of a cache coherence protocol:Safety and liveness.Proc.of the 3rd International Workshop on Verification,Model Checking,and Abstract Interpretation.Venice,Italy.2002.317–330.

5Bingham J,Hu AJ.Empirically efficient verification for a class of infinite-state systems.Proc.of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Berlin Heidelberg,Germany.2005.77–92.

6曹燊,李勇堅.基于不變量查找的 German 協議驗證.計算機系統應用,2015,24(11):173–178.[doi:10.3969/j.issn.1003-3254.2015.11.028]

7German SM.Tutorial on verification of distributed cache memory protocols.Formal Methods in Computer-Aided Design.2004.1–77.

8Dill DL.The Murphi verification system.Proc.of the 8th International Conference on Computer Aided Verification.Berlin Heidelberg,Germany.1996.390–393.

9周琰.Godson-T緩存一致性協議的Murphi建模和驗證.計算機系統應用,2013,22(10):124–128.[doi:10.3969/j.issn.1003-3254.2013.10.024]

10All auxiliary invariants of German protocol.https://github.com/zy311/German/blob/master/invariants.[2017].

Verification of German Cache Coherence Protocol by Flow Analysis and Inductive Invariants

ZHANG Yu,SUN Wen-Hui
(School of Computer and Information Technology,Beijing Jiaotong University,Beijing 100044,China)

German cache coherence protocol is used in parallel multi-processor systems,and the verification of German protocol has always been a hot spot in international industry and academia.We generate the flow chart of German protocol and describe each step of the flow chart.Besides,we present a method to verify the cache coherence protocol by flow analysis and inductive invariants in this paper.By searching for the relations between the invariants and the flow chart of German protocol,we can further analyze and verify the correctness of German protocol.

cache coherence protocol; flow analysis; inductive invariants; formal verification

張瑜,孫文輝.基于流分析與歸納不變式結合的German協議驗證.計算機系統應用,2017,26(10):156–160.http://www.c-s-a.org.cn/1003-3254/6020.html

國家自然科學基金(61672503)

2017-01-12; 采用時間:2017-02-23