張 瑜,孫文輝

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

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

張 瑜,孫文輝

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

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

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

1 引言

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

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

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

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

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

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

2 German 協(xié)議描述

2.1 協(xié)議內容描述

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

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

圖1 Home 和 Client節(jié)點傳遞的消息

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

① Client向Home節(jié)點發(fā)送的請求共享或者獨占內存的請求消息;

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

③ 共享或獨占內存的Client節(jié)點發(fā)送的無效響應消息;

④ Home向有請求的Client節(jié)點發(fā)送的請求響應消息.

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

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

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

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

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

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

2.2 協(xié)議流圖描述

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

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

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

① 一個Client節(jié)點請求需要共享數(shù)據(jù)緩存副本,執(zhí)行規(guī)則SendReqS,向Home發(fā)送ReqS請求;

② Home節(jié)點接收到ReqS請求后查詢目錄directory的狀態(tài)信息,執(zhí)行規(guī)則RecvReqS;

③ 當沒有其他Client節(jié)點處于獨占狀態(tài)時,則直接從 memory中讀取數(shù)據(jù),執(zhí)行規(guī)則 SendGntS,Home節(jié)點向有請求的Client節(jié)點發(fā)送GntS消息;

④ 當有其他Client節(jié)點處于獨占狀態(tài)時,執(zhí)行規(guī)則SendInv,Home節(jié)點先對這些獨占狀態(tài)的Client節(jié)點發(fā)送Invalidate消息,使獨占緩存無效; 獨占狀態(tài)的Client節(jié)點發(fā)送無效響應消息,執(zhí)行規(guī)則SendInvAck,向Home節(jié)點發(fā)送InvAck消息,Home節(jié)點收到InvAck消息,執(zhí)行規(guī)則RecvInvAck,從InvAck消息中讀取數(shù)據(jù),執(zhí)行規(guī)則SendGntS,Home節(jié)點向有請求的Client節(jié)點發(fā)送GntS消息;

⑤ 有請求的這個Client節(jié)點收到GntS消息,執(zhí)行規(guī)則RecvGntS,將緩存副本的狀態(tài)為共享.

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

① 一個Client節(jié)點請求需要獨占數(shù)據(jù)緩存副本,執(zhí)行規(guī)則SendReqE,向Home發(fā)送ReqE請求;

② Home節(jié)點接收到ReqE請求后查詢目錄directory的狀態(tài)信息,執(zhí)行規(guī)則RecvReqE;

③ 當沒有其他Client節(jié)點處于獨占狀態(tài)時,則直接從 memory中讀取數(shù)據(jù),執(zhí)行規(guī)則 SendGntE,Home節(jié)點向有請求的Client節(jié)點發(fā)送GntE消息;

④ 當有其他Client節(jié)點處于獨占狀態(tài)時,執(zhí)行規(guī)則SendInv,Home節(jié)點先對這些獨占狀態(tài)的Client節(jié)點發(fā)送Invalidate消息,使獨占緩存無效; 獨占狀態(tài)的Client節(jié)點發(fā)送無效響應消息,執(zhí)行規(guī)則SendInvAck,向Home節(jié)點發(fā)送InvAck消息,Home節(jié)點收到InvAck消息,執(zhí)行規(guī)則RecvInvAck,從InvAck消息中讀取數(shù)據(jù),執(zhí)行規(guī)則SendGntE,Home節(jié)點向有請求的Client節(jié)點發(fā)送GntE消息;

⑤ 有請求的這個Client節(jié)點收到GntE消息,執(zhí)行規(guī)則RecvGntE,將緩存副本的狀態(tài)為獨占,并執(zhí)行規(guī)則Store,將數(shù)據(jù)寫入緩存副本中.

圖3 German 協(xié)議 ReqS 請求

圖4 German 協(xié)議 ReqE 請求

3 German 協(xié)議的歸納不變式

3.1 輔助不變式

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

表1 German 協(xié)議的實驗結果

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

圖5 部分不變式

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

inv_27:節(jié)點1的緩存狀態(tài)是獨占狀態(tài),則該節(jié)點的獨占狀態(tài)標識為TRUE.

inv_28:節(jié)點1發(fā)送無效應答給Home節(jié)點,而節(jié)點的獨占狀態(tài)標識為TRUE,則節(jié)點1發(fā)送的數(shù)據(jù)是正確的數(shù)據(jù).

inv_36:Home節(jié)點向節(jié)點1發(fā)送同意獨占消息,則該節(jié)點的獨占狀態(tài)標識為TRUE.

inv_37:節(jié)點的獨占狀態(tài)標識為TRUE,并且節(jié)點1的cache狀態(tài)不是獨占狀態(tài),則Home節(jié)點不會向節(jié)點1發(fā)送無效消息.

inv_45:節(jié)點1的緩存狀態(tài)不是獨占狀態(tài),Home發(fā)送空消息給節(jié)點1,節(jié)點1對應的InvSet為TRUE,則獨占狀態(tài)標識為FALSE.

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

inv_53:Home節(jié)點向節(jié)點1發(fā)送同意共享消息,則該節(jié)點的獨占狀態(tài)標識為FALSE.

inv_55:節(jié)點 1發(fā)送無效應答給 Home節(jié)點,而節(jié)點的獨占狀態(tài)標識為FALSE,則Home當前命令是請求共享.

inv_61:Home 向節(jié)點 1 發(fā)送無效消息,而節(jié)點的獨占狀態(tài)標識為FALSE,則Home當前命令是請求共享.

inv_68:節(jié)點 1 對應的 InvSet為 TRUE,且獨占狀態(tài)標識為TRUE,則節(jié)點2對應的InvSet為FALSE.

inv_69:節(jié)點 2 對應的 ShrSet為 TRUE,且獨占狀態(tài)標識為TRUE,則節(jié)點1對應的ShrSet為FALSE.

3.2 轉移規(guī)則與輔助不變式

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

圖6 規(guī)則與不變式

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

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

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

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

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

圖7 部分不變式

當節(jié)點1請求共享,沒有其他節(jié)點處于獨占狀態(tài)時,執(zhí)行規(guī)則SendGntS時,Home節(jié)點發(fā)送同意共享的消息到節(jié)點1,那么Home發(fā)送的數(shù)據(jù)一定是正確的數(shù)據(jù),節(jié)點1和節(jié)點2的緩存狀態(tài)肯定不是獨占狀態(tài),節(jié)點 1 對應的 ShrSet為 TRUE,對應不變式 inv_22,25,32,39 所示.

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

5 結論

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

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 協(xié)議驗證.計算機系統(tǒng)應用,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緩存一致性協(xié)議的Murphi建模和驗證.計算機系統(tǒng)應用,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協(xié)議驗證.計算機系統(tǒng)應用,2017,26(10):156–160.http://www.c-s-a.org.cn/1003-3254/6020.html

國家自然科學基金(61672503)

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