基于分離邏輯的云存儲系統并發正確性驗證

王子豪, 王捍貧

(廣州大學 計算機科學與網絡工程學院, 廣東 廣州 510006)

隨著數據的快速增長，高性價比的海量存儲系統已成為剛需，基于塊的云存儲系統又因其低成本、易擴展的特點而成為最經濟可靠的選擇[1]。市場研究報告表明，2020年我國云存儲市場規模已達400億元[2]。隨著公共云平臺的推廣，依賴于云存儲服務的應用日益增加，云存儲故障可能會造成意想不到的負面影響。例如，2016年微軟的云存儲平臺宕機以致部分用戶在長達8天的時間內無法獲得郵件服務[3]；2018年騰訊云存儲發生故障，多重冗余失效，導致部分客戶的數據滅失[4]。云存儲系統的可靠性成為了研究熱點。

驗證云存儲系統的正確性是提高系統可靠性的有效方法。形式化驗證方法可以分析、證明程序的正確性，盡管代價略高，卻能從邏輯角度保證程序中不存在特定的錯誤[5]。Reynolds[6]提出的分離邏輯是霍爾邏輯[7]的一種擴展，是描述和驗證含地址操作和復雜數據結構的程序的有效工具[8]。文獻[9]基于分離邏輯提出了塊分離邏輯，用于描述云存儲系統特有的存儲結構和驗證云存儲管理程序的正確性，但需進一步考慮對系統并發正確性的驗證方法。

并發程序的執行過程復雜,執行結果易受外界影響，其正確性驗證一直是學界關注的熱點。早在1976年Owicki等[10-11]便基于霍爾邏輯提出了“依賴-保障”方法，刻畫共享內存沖突，驗證并發程序的正確性。2007年，在分離邏輯出現后，O′Hearn[12]進一步提出并發分離邏輯(Concurrent Separation Logic, CSL)，認為并發正確性驗證的難點在于不同線程共享存儲區域所引起的沖突，同時給出了針對互不干擾的并發線程的正確性驗證規則。在此基礎上，CSL進一步提出了資源所有權假設和分離性假設，規定一般的存儲單元不可共享、可共享的存儲單元需滿足特定性質。上述規定避免了并發沖突的產生，使得CSL成為基于分離邏輯的并發程序正確性驗證的基礎方法。

為提升并發程序正確性驗證方法的可用性，研究人員在CSL的基礎上引入了不同的輔助機制。例如：

(1)資源權限。在CSL中，所有權假設已經為資源引入了權限機制。Dinsdale-Young等[13]在此基礎上提出了并發抽象謂詞(Concurrent Abstract Predicate, CAP)，用于描述指定共享空間的性質及其所允許執行的動作，并預先完成小模塊的驗證。CAP細化了并發驗證的粒度[14]。后續的改進包括TaDA[15]、HOCAP[16]等驗證方案，為線程訪問共享資源和線程間通信提供了更靈活的描述方式。另有針對存儲單元本身的計數式權限模型，能更直觀地反映存儲資源的使用狀態。如Bizjak等[17]提出的Iron驗證方案,為存儲資源賦予分數量化每個進程所使用的存儲資源，通過分數變化的追蹤實現對失控存儲單元的識別，幫助驗證者發現內存泄漏錯誤。

(2)協議機制。協議機制即消息傳遞機制，主要用于描述線程間的交互行為。在CSL中，線程間的交互動作通過資源完成，交互的具體動作受限于對應的資源不變式。協議機制傾向于詳細追蹤線程間的交互過程，為驗證者提供了更為靈活的描述方法。例如，Lei等[18]提出了一種基于事件和通信代理的并發通信正確性驗證模型，針對異步非阻塞通信程序給出了2組驗證實例，證明了并發程序局部化、模塊化驗證的可行性。Hinrichsen等[19]提出的Actris驗證方案更可描述消息所附帶的存儲關系、數量關系等性質，同時支持互斥體等并發規范，并提出了MapReduce框架下并發程序正確性驗證的初步思路。上述方案在不同程度上支持對歷史狀態的描述和推理[20]。

(3)幽靈狀態。幽靈狀態是描述系統性質時有助于確定真實執行進度但不影響程序實際執行的輔助部分，一種典型的實現方法是在程序或斷言中引入不參與運算的變量并在驗證過程中持續跟進。在幽靈狀態機制下，驗證者可以直接描述一些存儲單元難以直觀反映的系統性質而不必關心是否有相應的命令執行過程，基于此提出的方法有Turon等[21]提出的GPS驗證方案和Jung等[22]提出的高階幽靈狀態等。Clochard等[23]提出的幽靈狀態監視機制則將程序正確性轉化為執行程序過程中幽靈狀態的正確性，驗證者可以在不了解程序具體執行過程的情況下完成驗證工作。幽靈狀態機制能很好地與其他工具相結合，如前文提及的Iron驗證方案中的權限分數便是幽靈狀態的一種，Iris驗證方案[24]也為包括幽靈狀態在內的系統狀態描述方式提供了數學基礎。

云存儲系統不僅是一個單純的并發程序，它與本地機器一同構成了獨特的并發執行環境。在邏輯上，以固定大小的數據塊為基本存儲單元所構成的“文件-塊-數據”3層結構與分離邏輯所描述的“變量-可尋址內存”2層結構有顯著差異；在執行上，3層存儲架構的實現有賴于本地機器的2層存儲架構。上述并發方案并未給出存儲結構改變后的處理方式。為此，本文基于塊分離邏輯提出一種云存儲系統并發正確性驗證方法，并給出相應的驗證實例證明本文所提方法的有效性。

在存儲資源控制上，本文通過擴展斷言語言在塊結構上實現了計數式權限機制，輔助驗證者推理線程間競爭行為的性質。計數機制屬于幽靈狀態，能夠直觀反映可用存儲空間的大小，可以更方便地描述云存儲中“大小固定的數據塊”以及本地機器上“不便擴展的內存資源”，實現2層結構與3層結構的統一。對塊本身的計數限制并不影響塊數量的擴增，云存儲系統易擴展的特性和CSL原有的靈活程度不受減損。驗證者也可以通過全局和局部資源計數的變化識別內存溢出和泄漏風險。

針對線程間交互，本文考慮異步通信環境和云存儲系統對存儲資源的管理需求，選擇以信道作為描述進程間交互的工具，并相應地更新了建模語言、斷言語言和狀態更新規則。信道作為全局共享資源，同時支持數值信息的非阻塞傳遞以及存儲資源使用權的顯式轉移。本文將使用權轉移視為輔助驗證的標記之一，允許驗證者以更直觀的方式追蹤交互細節。

本文第1節介紹預備知識和相關工作；第2節提出云存儲管理系統的并發建模語言，當中新增了與信道相關的命令并完善了對系統狀態的描述；第3節提出基于塊分離邏輯的斷言語言，在塊斷言中引入了計數機制，新增信道斷言分量以描述線程間通信的性質；第4節提出一組驗證規則，給出了與新命令相關的公理以及與信道相關的狀態更新規則；第5節給出一組驗證實例；第6節總結全文。

1 預備知識

霍爾邏輯和分離邏輯的特征都是形如

{P}C{Q}

的霍爾三元組。在部分正確性假設下，三元組成立意指在滿足前置斷言P的情況下執行程序C，若能終止則得到的新狀態必能滿足后置斷言Q。分離邏輯在邏輯上將存儲器劃分為2層：被稱為堆(Heap)的可變存儲區和被稱為棧(Store)的不可變存儲區。其中堆以地址為索引，用于實現尋址操作；棧以變量名為唯一訪問依據，功能與霍爾邏輯一致。這種結構可以很直觀地描述指針等與地址相關的操作。

分離邏輯中的“分離”指一個堆可以被劃分為多個互不相交的部分，多個互不相交的小堆也可以合取為一個堆。分離合取以符號“*”表示。在此定義下，形如

p*p

的式子將因*號兩側的子堆擁有相同地址的單元恒為假，即在一個有效的斷言中相同地址的存儲單元只能出現一次。這個要求解決了可變存儲區潛在的別名問題。

分離邏輯同時提出局部推理規則(Frame Rule)

局部推理規則使得驗證者只需關注與命令直接相關的存儲單元的局部狀態，降低了驗證復雜度。局部推理規則支持組合驗證，為對局部狀態的推理擴展至對全局狀態的推理提供了路徑。

1.1 基于分離邏輯的并發程序驗證技術

并發分離邏輯(CSL)是基于分離邏輯的并發程序驗證技術的重要基礎，已衍生出大量并發程序驗證工具[20,25]。

CSL首先就完全不共享存儲單元的并發程序給出了推理規則，即互不干涉的并發推理規則，定義如下：

其中，線程1對線程2不構成干擾是指線程1的執行不影響線程2中任一命令的前置條件,不改變其自由變量。

互補干擾條件不足以描述并發程序的行為。CSL進一步提出資源所有權假設和分離性假設：一般存儲單元只可被一個線程使用，可被復用的存儲單元應歸屬于某一資源組；在任意時刻，一個資源組最多被一個線程使用，且系統的所有存儲單元可被線程和資源組完整劃分；資源組被使用前后均需使對應的資源不變式成立。在此限制下，線程間的交互由資源組實現，交互的結果及其影響范圍由資源不變式提前給定。使用資源時的驗證規則定義如下：

上述規則限制了進程間的交互，規避了并發執行可能帶來的沖突。

鎖式權限機制能夠幫助控制并發沖突，分數式權限機制可以幫助驗證者識別并發執行過程中資源分配不當的問題。例如，在Iorn方案[17]中存儲資源獲得的權限分數與線程無關,與資源大小無關，分數值僅取決于驗證時執行分離和分離合取的次數。Iorn為系統初始堆的分數賦值為1，其后每次分離動作會將原堆的分數均分至劃分所得的子堆上，而每次執行分離合取的所得的堆的分數為原子堆的分數和，即

empπempπ/2*empπ/2
empπ1*empπ2empπ1+π2

。

權限分數不影響程序分配、釋放、讀寫等命令的執行，僅反映驗證過程。若權限分數出現損失、全局分數和不等于1，則證明驗證過程遺漏了對部分可變存儲區的控制,可能存在內存泄漏風險。驗證者可以追溯局部分數的變化定位出錯的代碼段。

1.2 基于分離邏輯的云存儲系統驗證技術

云平臺為并發程序提供了特殊的運行環境，其本身也是一個計算機程序。保障平臺本身的正確性是驗證平臺上各類并發程序正確性的基礎之一。

云存儲系統中的塊結構有以下功能和特點：塊內存儲具體數據、分散存放，塊與塊結合組成文件；用戶對數據的讀寫和系統對結構的維護以塊為最小單元；系統通過塊定位存儲數據的具體機器乃至具體位置。塊本身具備了可尋址、可擴展的特性，且塊與數據之間也存在“地址-數據”的映射。王捍貧等[9,26-28]就塊結構的描述、推理和驗證做了一系列的研究工作。這些工作將分離邏輯原有的2層存儲架構擴展為Store、HeapB和HeapV3層結構，分別代表不可變存儲區、可變的塊存儲區和可變的本地存儲區。HeapB和HeapV各自擁有堆所具備的分離屬性，Store、HeapB和HeapV3者之間可構成“文件-數據塊-數值”的3層體系，Store和HeapV兩者之間可以構成“變量-數值”的傳統2層體系。

文獻[9]提出的驗證方法由建模語言、斷言語言和規范語言共同構成。在建模語言中，該方法引入了與文件和塊結構相關的變量和命令，改善了存儲架構并相應地擴展了論域。有關表達式的語法詳列如下：

經擴增后的命令語法詳列如下：

|ifbethenCelseC′|whilebedoC。

在斷言語言部分，該方法沿用分離邏輯的斷言語言描述與塊無關的系統性質，引入塊斷言描述與塊相關的系統性質，2個分量共同構成全局斷言以完整描述系統狀態。其中，塊斷言具體語法如下：

|β1→β2|bk==bk1…bkn|?x.β

|?x.β|?b.β|?b.β|?f.β|?f.β|empB

|bk

|b1b2|bk1==bk2。

在云存儲環境下，并發程序之間不僅需要競爭云存儲資源，還需要與本地機器上的其他線程競爭本地存儲資源。即使將云存儲資源視為可擴展資源，對于特定的數據或數據塊的使用權卻不可隨意擴張，資源的競爭和調度受云存儲管理系統控制。同時，本地內存資源有限、擴展不易，資源競爭帶來的內存復用難以避免?，F有工具對上述擴張限制的描述較為復雜，容易遺漏。

2 并發云存儲管理系統建模語言

并發云存儲管理系統的建模語言是MLBCSS[9]的擴展，新增的元素主要用于描述和支持信道等并發機制。

2.1 信道機制設計

信道機制用于滿足線程間的交互需求，主要是平臺管理程序與其他任務線程的通信需求，包括傳輸數值和存儲資源使用權的上收下發。本文以信道模擬和描述兩者的通信過程：每個信道都是緩存隊列，信道內分別對數值信息和塊權限采用先進先出的交互方式；為確保寫入成功，信道容量不設限制；以非阻塞方式讀取，目標信道無消息可讀是不改變系統狀態、執行下一命令。

對于線程的執行而言，在讀取動作完成前不可得知信道的具體狀態、不可利用信道內的數值信息或存儲資源權限；在讀取動作完成后，被讀取的信息出隊、被讀取的塊權限歸線程所有。線程向信道輸出數值時，需要額外在存儲器中作寫入，直至該數值被讀取后對應的存儲單元方可被釋放，輸出數值是一個明顯改變內存狀態的操作。在轉移數據塊使用權時，涉及的是數據塊的使用權而并未改變數據塊的內容或者數據塊與分布式文件之間的關系，即未對系統狀態作實質性的改變。綜上，本文新增一函數StoreC，用于描述信道內的數值信息，定義如下：

StoresCCHVar→Values*Values*=

{(n1,…,nk)|ni∈Valurs,k∈}。

經信道轉移的存儲權限可用下式表示：

b.n.(l1,…,li)，

式中包含3個分量，分別是塊表達式b，指代部分使用權被轉移的塊；一個不大于塊b容量的整數n，指代被轉移的存儲單元數量；一個長度不大于n的地址序列(l1,…,li)、且序列中的本地地址應屬于b，列明被轉移權限的非空閑單元所存儲的具體數據。

2.2 建模語言語法

在表達式部分，本文沿用MLBCSS所有的數值表達式、文件表達式、塊表達式和布爾表達式，另新增一類信道表達式che。在命令部分，新增與信道相關的命令、修改與數據塊容量相關的語句。其中信道相關命令根據2.1小節的說明給定，塊命令則配合計數式權限機制作相應修改。增改后的語法詳列如下：

|C:C′|ifbethenCelseC′|whilebedoC

|C1‖C2。

新增的信道變量包括空信道、數值信息、存儲資源使用權3種元素以及他們的自由組合，用于描述信道的狀態。存儲資源使用權一式的涵義與2.1小節所述一致。

新增語句主要涉及信道操作，可滿足管理線程與任務線程間的通信需求。另外，新增的塊容量限制將影響原有的塊命令。增改后的命令釋義詳列如下：

·allocated，分配新的數據塊并給定容量上限；

·append，數據塊追加寫，受塊容量限制；

·delete，刪除數據塊并釋放對應的存儲單元；

·remove，釋放數據塊內指定的存儲單元；

·newch，開設新的信道；

·close，停用沒有待收取消息的信道；

·send，向信道傳出數值消息；

·tryre，嘗試從信道內取出數值消息；

·pass，向信道內傳出數據塊使用權；

·get，嘗試接收數據塊使用權。

2.3 機器狀態描述

系統的狀態由7個函數組成，其中包括LRBCSS中使用的5個函數：由本地變量到本地存儲地址的映射StoresV、由數據塊變量到數據塊地址的映射StoresB、由文件變量到一組數據塊變量的映射StoresF、由已使用的本地存儲地址最終指向數值的映射HeapsV、由已使用的數據塊地址最終指向一組本地存儲地址的映射HeapsB。新增的2個函數StoresC和Size分別表示信道的狀態和數據塊的容量上限。各個函數的具體定義如下：

Var?{x,y,…} BKVar?{b1,b2,…}

FVar?{f1,f2,…} CHVar?(ch1,ch2,…)

StoresV?Var→Values

StoresB?BKVar→BLoc

StoresF?FVar→BLoc*

HeapsB?BLoc→Loc*

HeapsV?Loc→Values

StoresC?CHVar→Values*

Size?BLoc→。

為方便起見，各類數值都限于整數范圍內，各類地址限于非負整數范圍內，則表示不包含任何地址的nil可以被定義為-1。

根據2.1小節給出的信道機制，數值信息的讀寫操作將改變存儲器的狀態；塊權限的轉移在執行時不改變存儲器內的映射關系，在驗證時影響各線程可用的存儲區。因此，StoresC是一個由信道變量指向數值隊列的映射，而通過信道轉移的數據塊使用權僅用于輔助推理。

塊的容量限制主要用于對云存儲系統中塊結構以及機器中有限內存資源的建模。在各類分布式存儲系統中，數據塊可以視為存儲的基本單位，容量大多是固定的。如HDFS通常會將一個大文件劃分為多個64 MB的數據塊，TFS則會將多個小文件整合成為64 MB的數據塊。在機器中，擴展內存資源通常需要停機后更新硬件才得以實現。模型中的數據塊容量上限在數據塊建立之初被指定，但在此后不可擴增，以表征云存儲中固定大小的塊結構和機器中內存不可增長的特性。在程序運行時，允許進程將自己所擁有的數據塊作劃分而不改變數據塊的總容量，以支持對本地內存調度的建模。因此，Size是一個由已使用的數據塊地址指向自然數的映射。

2.4 建模語言的指稱語義

指稱語義為語句和表達式在特定狀態下的具體意義給出說明。機器的狀態由一個七元組給定，但并非所有表達式或所有命令的釋義都同時依賴于所有的狀態函數。簡便起見下文只列出釋義所依賴的必不可缺的部分，給出本文新引入的表達式和語句的語義。

新增的信道表達式的語義給定如下：

ifche1(sC)=(loc1,…,loci)and

其中，n為數值信息，ch為信道變量。

新增的數值表達式$bk表征地址為bk的數據塊的容量。原有的表達式#bk可以代表該數據塊內已使用的空間，應不大于$bk。其語義分別如下：

wherehB(bkσ)=(loc1,…,locn)

andk<=$bk(sF)(sB)(sV)(hB)(Size)。

與數據塊有關的命令中，追加寫操作需受數據塊容量的限制、刪除塊時需一并釋放存儲內容實際占用的內存空間，以確保驗證過程的內存資源限制與執行狀態一致；新增的remove操作是用于模擬內存和分布式文件的擦寫過程。有關命令的語義給定如下：

hB[(loc1,…,loci)/bloc],[hV|loc1:e1σ,…,

loci:eiσ],Size[n/b])wherebloc?dom(hB)

and(loc1,…,locn)?dom(hV);

Size[0/bkσ]);

wherehB(bkσ)=(loc1,…,locm),thetermofsequence(loc1,…,locm)belongtodom(hV),theblockhadnotbeenfullm

andhB(bkσ)=(loc1,…,locm)(1≤i≤m),

otherwiseremove(bk,e)σ=(sF,sB,sV,sC,hB,hV,Size)wherethestatecannotbechangedlegally。

信道機制中，塊權限的轉移用于輔助驗證，對內存狀態不作實質性的修改，有關命令對系統的影響由3.2小節說明。信道命令的語義給定如下：

forpassingtherightwillnotchangethestate。

hB,Size)wherech?dom(sC);

locm+1)/ch],[hV|locm+1:eσ],hB);

wheresV(chσ)=(loc1,…,locm)and

locm+1∈Loc-dom(hV);

sC[(n2,…,nm/ch)],hV,hB,Size)wheresC(ch)=(n1,…,nm)andm∈+,otherwise

wheresC(ch)=?。

3 斷言語言

斷言語言可以用于描述某特定狀態下系統所具備的性質。文獻[9]提出的斷言語言LRBCSS分別使用地址斷言和塊斷言2個分離描述與塊無關的系統特征以及愉快相關的系統特征。本文進一步描述存儲資源所面臨的限制，新增信道斷言以描述線程間交互的性質，相應修改了全局斷言。

3.1 塊斷言

與LRBCSS相比，塊斷言在語法上主要是為數據塊引入下標以表示當前可用的空閑空間。新增的remove指令將塊由只寫不擦變為可擦寫，塊有可能完全空閑，需新增相應的語句描述。塊斷言的語法詳列如下：

|β1→β2|bk1==bk2|?x.β|?x.β|?b.β

|?b.β|?f.β|?f.β|bk==bk1…bkn

|β1-*β2|fe=fe′|b1b2。

塊斷言在語義上增加了關于塊容量的說明。增改的后語義給定如下：

-$σbk==bk1…bkniffbkσ=

andbkiσ⊥bkjσforallthei,j∈,

1≤i

-$σ{bkσ},

hB(bkσ)=(e1σ,…,ekσ),bkσ=

k+nandforall1≤i≤k,ekσ∈dom(hV);

-$σbkn(emp)iffdom(hB)={bkσ},

hB(bkσ)=?,andbkσ=n。

上式未列出的bk1==bk2和fe=fe′語句在成立時可說明不同的塊表達式指向同一塊地址，不必強調兩者容量相同；b1b2一式表示2塊內容一致，其關注重點在于內容而非空間，語義不變。

通過顯式的容量說明，驗證者可以直觀得知數據塊或對應的內存區的容量能否滿足程序運行所需、是否有溢出的可能。通過對各線程持有的存儲單元數量求和，可以直觀得知在驗證過程當中是否有被遺漏的存儲單元，避免內存泄露的風險。

帶計數機制的塊結構也可以描述本地機器上有限的內存資源。為滿足其調度所需，塊斷言支持塊的切分使用，即

bkn(emp)?n1,n2,n1+n2=n∧

bkn1(emp)*bkn2(emp)。

通過上式，本地機器不必拘束于傳統的2層結構，同時驗證者可以使用信道機制描述本地機器的內存調度行為。

3.2 信道斷言

信道斷言主要包括表征信道內容的語句和基本的邏輯結構。對其他存儲結構而言，由于同一時刻只能在一個線程中出現，期間不應出現2個相沖突的狀態描述，在應用分離合取和分離析取時必然滿足“互不相交”的要求。但對信道而言，通信內容至少有發送方和接收方2者可見，即同一時刻至少有2個不同線程的狀態斷言會包含同一信道的內容，應用分離合取和分離析取時可能會有沖突，需另外給出說明。由于涉及存儲單元所有權的轉移，這一部分斷言同時依賴于不可變存儲器Store以及可變存儲器HeapV和HeapB的狀態。信道斷言的語法詳列如下：

|γ1→γ2|cheche′|?x.γ|?x.γ|?b.γ

|?b.γ|?f.γ|?f.γ|empC|γ1*γ2|γ1-*γ2。

相應的語義給定如下：

-σtrueC;

-σ?x.γiffsF,sB,sV(n/x),sC,hB,hV,Size

-σ?b.γiffsF,sB(n/b),sV,sC,hB,hV,Size

-σ

-σγ1→γ2iffifσγ1thenσγ2;

-σcheche′iffcheσ=che′σand

theyarepassingrightofBlocksinthesameway;

-σempCiffdom(sC)=?;

-σγ1*γ2iffthereexistwithsC=

需要注意的是，盡管信道中的內容可能因為不同線程執行進度的差異而無法保證在每次執行中都能保持一致，但對某一特定信道而言，在同一時刻向不同線程所展示的數據流應當是一致的。因此，在對信道斷言執行分離合取操作時，相同的信道應當包含內容完全相同的信息流。

3.3 全局斷言

全局斷言的形式是地址斷言、塊斷言和信道斷言組成的三元組

α,β,γ。

其中，塊斷言、信道斷言分別由3.1小節和3.2小節給出。地址斷言沿用自LRBCSS，具體定義如下：

|α1→α2|e1=e2|e1≤e2|?x.α|?x.α

|?b.α|?b.α|?f.α|?f.α|empV

|ee′|α1*α2|α1-*α2。

全局斷言并非3個分量的邏輯求和。例如，若某個塊出現在信道斷言中，可變數據塊存儲器HeapB的狀態將由塊斷言和信道斷言2者共同確定，簡單地使用邏輯和聯結2者并不能準確表示當中的劃分關系，使用分離合取“*”聯結也不能準確地描述當前數據塊權限的歸屬。對機器狀態而言，這個三元組是一個不可簡單分割的整體。全局斷言的語法詳列如下：

|?b.|?f.|?f.|?ch.|?ch.

|emp|1*2|1-*2。

相應的語義給定如下：

-σα,β,γiffσα,σβ,andσγ;

-σ

theypasstheonwershipofBlocks;

-$σ

topasstheonwershipofBlocks;

-σempiffdom(hV)=?,dom(hB)=?,and

dom(sC)=?;

-$sF,sB,sV,sC,hB,hV,Size1*2iffthere

-$sF,sB,sV,sC,hB,hV,Size1-*2ifffor

anyheaph′Handcommunicationsstatus

s′C,ifhH#h′H,sC*s′Cexistsand

sF,sB,sV,s′C,h′B,h′V,Size1then

sF,sB,sV,sC*s′C,hB*h′B,hV*h′V,Size2。

4 證明系統

有效的霍爾三元組

{P}C{Q}

由前置條件P、程序指令序列C以及后置條件Q組成。其中，前置條件和后置條件均為全局斷言，程序指令序列遵循2.2小節給出的語法。本文考慮部分正確性斷言，即對一個成立的霍爾三元組，要求：

(1)程序指令序列中所讀寫的變量或存儲單元，必須被包含在前置條件P中或是在程序C中以allocated等語句合法分配所得。即程序對出現在其前置條件內的存儲單元擁有完整的權限、對新存儲單元自分配成功時起擁有完整權限，直至有關存儲單元被剔出成立的全局斷言后權限滅失；

(2)對于任何能令前置條件P成立的狀態σ，C,σ是安全的，即在狀態σ下運行程序C不會出現導致程序意外退出的故障；

(3)在任何能令前置條件P成立的狀態σ下運行程序C，若程序終止于一個新的狀態σ‘，則狀態σ’必須能令后置條件Q成立。

4.1 證明規則

本節主要為每一個語句給出一個基本的證明公理。這些公理僅依賴于語句本身，而與程序結構無關。不論涉及何種存儲結構，公理都采用全局命題。第一部分是適用于原有命令的公理：

{p}skip{p}

(A1)

(A2)

(A3)

(A4)

(A5)

dispose(e){emp}

(A6)

(A7)

attach(f,bk1,…,bkn)

bkn[f′/f])/f],empC}

(A8)

delete(f)

(A9)

(A10)

(A11)

第二部分是與塊命令相關的公理。由于本文引入了計數式機制，相關公理被改寫如下：

(A12)

(A13)

(A14)

(A15)

信道相關操作主要依據先進先出的原則給出相應的公理，同時考慮消息讀取失敗時的情形。有關基本公理詳列如下：

(A16)

{?ch′.e=i,empB,chch′}send(ch,e)

{?ch′.e=i,empB,chch′·i}

(A17)

(A18)

(A18a)

(A19)

(A20)

{?ch′.empV,empB,ch?}

get(ch)

{?ch′.empV,empB,ch?}

(A20a)

(A21)

4.2 基本推理規則

推理規則依賴于特定的程序結構而成立。下列基本推理規則沿用自霍爾邏輯[7]、分離邏輯[6]、并發分離邏輯[12]以及LRBCSS[9]。

(R1)

(R2)

(R3)

(R4)

(R5)

(R6)

上式中FV (p)為命題p中的自由變量集，ModifyS(C)涵蓋被程序C修改過的除信道變量以外的存儲單元集合。T (be)是將布爾表達式轉換為全局斷言的函數,定義如下：

T(e1=e2)=e1=e2,trueβ,trueγ;

T(e1≤e2)=e1≤e2,trueβ,trueγ;

T(bk1==bk2)=trueα,bk1==bk2,trueγ;

T(true)=true;T(false)=false;

T(be1∧be2)=T(be1)∧T(be2);

T(be1∨be2)=T(be1)∨T(be2)。

在并發規則中要求的“互不干涉”原本指可能被任一程序修改的存儲空間不得被另一程序讀寫。本文允許以下例外：

(1)與信道相關的消息和權限傳遞。信道機制是在全局層面服務于線程間通信，如若受限則線程間再無交互的渠道；

(2)通過信道傳遞數據塊使用權實現的復用。這部分復用對程序運行的影響可以通過對信道操作進行驗證得以釋明。

4.3 涉及信道的狀態更新規則

在4.2節中，考慮到信道的內容可能會被多個線程知悉，且不要求線程關注所有信道的變化，本文對分離合取給出了新的限制。同理，在推理時驗證者可以按需引入或剔除可能可用的信道。下述的推理規則給出了一些可以向語句的前后置條件引入新的信道狀態的情景。

每個信道都可以傳輸數值和數據塊使用權2種消息，2種消息均采用先進先出的隊列模式，且2種消息是分別使用不同的命令完成出隊入隊操作。因此，在驗證時只需保證同一種消息的時序能維持一致，而不必在所有消息隊列上保證時序關系不變，即

(RC1)

循此操作多次變換，則對任意信道都可以表示為

ch

。

在線程間通信中，以接收信息后程序所執行的動作為標準，信道可作如下劃分：

(1)單向傳輸消息，線程接收信息后不必根據該消息對外作出特定反應；

(2)雙向響應消息，線程依據接收到的信息對外作出特定反應。

對于第一類行為，線程對外傳出消息可能影響任何訪問該信道的線程。盡管在讀取消息前受信一方不知曉信道的具體狀態，但對驗證者而言，任一線程都有權獲取該新消息。綜上，對某一涉及信道操作語句的前置條件有：

(RC2)

對于第二類行為，若某一線程在接收一個特定信息a后，能在不訪問其他信道的前提下傳出另一組特定信息b，則可認為傳出信息a的進程期望獲取信息b。即對某一涉及發信操作語句的后置條件為

(RC3)

上式中的“?”可用于信道操作的限制條件，表明在執行操作之前信道可能出現的狀態，在有多個可能性時前后置條件可用下標區別各自的配對。出于限制信道混用帶來的沖突考慮，在建模和驗證期間可以限制線程對信道的讀寫權限，以維持“互不干涉”的狀態。

在實際驗證過程中，驗證者可以主動區分不同信道的用途和使用者，以便追蹤線程間通信行為對全局狀態的影響。

5 程序驗證實例

本節給出的實例由3個線程組成，分別為用戶發出寫請求、主節點分配任務和數據節點執行存儲，為一個完整的寫數據過程。本節首先給出實例及其說明：

(1)線程 1. 用戶端

CHVar:appW,upD;

LocalVarList

BKVar:Btemp;

send(appW, 4);

whileBtemp==0do

endwhile;

send(upD,Btemp, 4, 3, 2, 1);

線程1有2次發信行為，分別為向主節點發送寫請求和向數據節點提供具體數據，均為數值信息傳遞。另有一次等待主節點響應的收信過程，由于非阻塞條件下tryre命令不具備等待功能，需用循環語句輔助。

(2)線程 2. 主節點

CHVar:disW,disD;

LocalVarList

Var：i;

BKVar:Bpool;

whiletruedo

ifi>0then

send(disW,Bpool);

pass(disD,Bpool,i);

endif;

endwhile;

線程2有2次發信行為，向用戶端反饋可用數據塊地址時是傳遞“地址”這一數值信息，令數據節點開辟塊空間則是存儲資源使用權的轉移。

(3)線程 3. 數據節點

LocalVarList

Var：len,j;

BKVar:Bdisk;

while#Bdisk=0do

endwhile;

whilej=0do

endwhile;

ifBdisk==jthen

whilelen<$Bdiskthen

endwhile;

endif;

線程3有2組信息接收行為：首先從主節點獲得數據塊權限；其后從用戶端獲得需寫入的數據、核對寫入地址后完成操作。

后續分3部分給出各自線程的驗證過程。系統的初始狀態與emp等價。

1)用戶端線程驗證過程

appW?}(A16)

appW?,upD?}(A16)

appW?,upD?}(A11)

send(appW, 4);

appW4,upD?}(A17)

appW0,disW?,upD?}1(,RC2)

⑧ {?bd≠0.empV,Btemp0(emp)∧Btemp=0,appW0,disWbd,upD?}2(-,RC3)

此處對信道狀態的更新依賴于主節點的驗證過程。驗證式⑦由RC2推出，是其他線程對信道操作的影響在全局的體現。驗證式⑧依賴于主節點的響應行為，在后續部分會詳細列出對應的條件。由主節點的驗證過程可知，驗證式⑧的首次成立不會早于驗證式⑦的首次成立。

此后為一循環，驗證式⑦及⑧均可以成為循環體執行前成立的狀態。現以驗證式⑦為基礎考慮第一次循環體執行，有：

appW0,disW?,upD?}1(⑦)

appW0,disW?,upD?}1(A18a)

由于信道內無消息可讀，在非阻塞通信的要求下，讀操作不改變任何系統狀態。同時由于驗證式⑨與驗證式⑩等價，可以構成循環不變式。

再考慮以驗證式⑧為前置條件的執行過程：

Btemp=0,appW0,disWbd,upD?}2(⑧)

Btemp=bd,appW0,disW?,upD?}2(A18)

后續可有如下驗證：

send(upD,Btemp, 4, 3, 2, 1);

2)主節點程驗證過程

disW?,disD?}(A16)

Bpool=0,disW?,disD?}(A11)

Bpool=0,disW?,disD?}(A15)

Bpool=0,disW?,disD?,

appW?}1(③,RC2)

Bpool=0,disW?,disD?,

appW4}2(⑥,RC2)

初始化各變量后，線程進入循環狀態。參考用戶端線程的驗證過程，循環體內可有驗證過程如下：

Bpool=-,disW?,disD?,

appW?}1()

Bpool=-,disW?,disD?,

appW4}2()

Bpool=-,disW?,disD?,

appW?}1(,A18a)

Bpool=-,disW?,disD?,

appW?}2(,A18)

ifi>0then

Bpool=-,disW?,disD?,

appW?}2(,TRUE)

Bpool=bd,disW?,disD?,

appW?}2(A12)

send(disW,Bpool);

Bpool=bd,disWbd,disD?,

appW?}2(A17)

pass(disD,Bpool,i);

Bpool=bd,disWbd,disDbd.4.(φ),

appW?}2(③,RC2)

Bpool=bd,disW?,disD?,

appW?}2(,,RC2)

else

Bpool=-,disW?,disD?,

appW?}1(,FACSE)

skip;

Bpool=-,disW?,disD?,

appW?}1(A1)

endif;

Bpool=-,disW?,disD?,

appW?}1()

Bpool=bd,disW?,disD?,

appW?}2()

Bpool=-,disW?,disD?,

appW?}1(,A2)

Bpool=bd,disW?,disD?,

appW?}2(,A2)

Bpool=-,disW?,disD?,

appW?}(,)

3)數據點程驗證過程

*empB,empC}(Var)

∧Bdisk=0,empC}(A11)

∧Bdisk=0,empC}(A2)

∧Bdisk=0,empC}(A2)

Bdisk0(emp)

∧Bdisk=0,upDbd·4·3·2·1∧

disDbd.4.(?)}(,,RC2)

初始化各變量后，數據節點進入循環，等待主節點的寫權限分配。與其他線程的循環等待相似，有效的讀信道行為對應下列驗證過程：

(emp)∧Bdisk=0,upDbd·4·3·2·1∧

disDbd.4.(?)}()

(emp)∧Bdisk=bd,upDbd·4·3·2·1∧

disD?}(A20)

(emp)∧Bdisk=bd,upDbd·4·3·2·1∧

disD?}(,R3)

Bdisk4(emp)∧Bdisk=bd,

upD4·3·2·1∧disD?}(A18)

用戶端按時序提交了寫入地址和4個待寫入的數據共5條數值信息。在執行過程中，數據節點無法得知信道內尚未被讀取的信息狀態，但能在讀取地址之后確認循環條件已不再成立。故驗證式為循環執行后的最終結果。

后續的驗證過程有：

Bdisk4(emp)∧Bdisk=bd,

upD4·3·2·1∧disD?}(,R3)

ifBdisk==jthen

Bdisk4(emp)∧Bdisk=bd,

upD4·3·2·1∧disD?}(,TRUE)

其后是一個以len為循環變量的循環體。為方便起見，對循環體驗證前先對驗證式進行等價變換，具體過程如下：

upD(elen+1,…,e4)∧disD?}()

upD(el′+1,…,e4)∧disD?}()

upD(el′+2,…,e4)∧disD?}(A18)

upD(el′+2,…,e4)∧disD?}(A13)

upD(el′+2,…,e4)∧disD?}(A2)

upD(elen+1,…,e4)∧disD?}()

∧Bdisk=bd,upD?∧disD?}(,R3)

endif;

∧Bdisk=bd,upD?∧disD?}(,,TRUE)

至此可知，用戶端發起的寫請求得到了響應，數據節點在主節點賦予的權限范圍內執行寫入，被寫入的塊的地址與主節點向用戶端反饋的塊地址相同，被寫入的數據與用戶端提交的數據一致，寫功能正確。該實例涵蓋了循環、通信的重要的驗證環節，可以說明本文所提方法的有效性。

6 小 結

本文基于分離邏輯提出了一種適用于并發云存儲系統正確性驗證的系統方法，在建模語言中引入新的命令和表達式以描述線程間交互行為、擴展斷言語言，以準確描述資源受限的執行環境，并基于此完善了推理規則。驗證實例說明本文提出方法的可行性。

本文所提邏輯能直觀描述存儲容量的限制、信道機制能描述權限的轉移過程，幫助驗證者驗證存儲管理行為的正確性，識別潛在的溢出和泄漏風險，滿足云存儲系統的驗證所需。本文擴展了塊分離邏輯的驗證范圍，所提方法也可推廣到云存儲環境下的普通并發程序的正確性驗證上，為實現MapReduce、Spark等并發框架下的程序驗證提供了理論上的可能性。

未來的工作包括：①降低信道機制的復雜度，改變現有通過驗證者主動規避沖突的狀態，提升其對時序關系的描述精度；②完善所用幽靈狀態的數理基礎；③探究驗證規則的可表達性、相對完備性；④擴展并發正確性驗證的適用范圍；⑤設計輔助驗證工具和算法。