王子豪, 王捍貧

(廣州大學(xué) 計(jì)算機(jī)科學(xué)與網(wǎng)絡(luò)工程學(xué)院, 廣東 廣州 510006)

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

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

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

為提升并發(fā)程序正確性驗(yàn)證方法的可用性，研究人員在CSL的基礎(chǔ)上引入了不同的輔助機(jī)制。例如：

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

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

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

云存儲(chǔ)系統(tǒng)不僅是一個(gè)單純的并發(fā)程序，它與本地機(jī)器一同構(gòu)成了獨(dú)特的并發(fā)執(zhí)行環(huán)境。在邏輯上，以固定大小的數(shù)據(jù)塊為基本存儲(chǔ)單元所構(gòu)成的“文件-塊-數(shù)據(jù)”3層結(jié)構(gòu)與分離邏輯所描述的“變量-可尋址內(nèi)存”2層結(jié)構(gòu)有顯著差異；在執(zhí)行上，3層存儲(chǔ)架構(gòu)的實(shí)現(xiàn)有賴于本地機(jī)器的2層存儲(chǔ)架構(gòu)。上述并發(fā)方案并未給出存儲(chǔ)結(jié)構(gòu)改變后的處理方式。為此，本文基于塊分離邏輯提出一種云存儲(chǔ)系統(tǒng)并發(fā)正確性驗(yàn)證方法，并給出相應(yīng)的驗(yàn)證實(shí)例證明本文所提方法的有效性。

在存儲(chǔ)資源控制上，本文通過擴(kuò)展斷言語言在塊結(jié)構(gòu)上實(shí)現(xiàn)了計(jì)數(shù)式權(quán)限機(jī)制，輔助驗(yàn)證者推理線程間競(jìng)爭(zhēng)行為的性質(zhì)。計(jì)數(shù)機(jī)制屬于幽靈狀態(tài)，能夠直觀反映可用存儲(chǔ)空間的大小，可以更方便地描述云存儲(chǔ)中“大小固定的數(shù)據(jù)塊”以及本地機(jī)器上“不便擴(kuò)展的內(nèi)存資源”，實(shí)現(xiàn)2層結(jié)構(gòu)與3層結(jié)構(gòu)的統(tǒng)一。對(duì)塊本身的計(jì)數(shù)限制并不影響塊數(shù)量的擴(kuò)增，云存儲(chǔ)系統(tǒng)易擴(kuò)展的特性和CSL原有的靈活程度不受減損。驗(yàn)證者也可以通過全局和局部資源計(jì)數(shù)的變化識(shí)別內(nèi)存溢出和泄漏風(fēng)險(xiǎn)。

針對(duì)線程間交互，本文考慮異步通信環(huán)境和云存儲(chǔ)系統(tǒng)對(duì)存儲(chǔ)資源的管理需求，選擇以信道作為描述進(jìn)程間交互的工具，并相應(yīng)地更新了建模語言、斷言語言和狀態(tài)更新規(guī)則。信道作為全局共享資源，同時(shí)支持?jǐn)?shù)值信息的非阻塞傳遞以及存儲(chǔ)資源使用權(quán)的顯式轉(zhuǎn)移。本文將使用權(quán)轉(zhuǎn)移視為輔助驗(yàn)證的標(biāo)記之一，允許驗(yàn)證者以更直觀的方式追蹤交互細(xì)節(jié)。

本文第1節(jié)介紹預(yù)備知識(shí)和相關(guān)工作；第2節(jié)提出云存儲(chǔ)管理系統(tǒng)的并發(fā)建模語言，當(dāng)中新增了與信道相關(guān)的命令并完善了對(duì)系統(tǒng)狀態(tài)的描述；第3節(jié)提出基于塊分離邏輯的斷言語言，在塊斷言中引入了計(jì)數(shù)機(jī)制，新增信道斷言分量以描述線程間通信的性質(zhì)；第4節(jié)提出一組驗(yàn)證規(guī)則，給出了與新命令相關(guān)的公理以及與信道相關(guān)的狀態(tài)更新規(guī)則；第5節(jié)給出一組驗(yàn)證實(shí)例；第6節(jié)總結(jié)全文。

1 預(yù)備知識(shí)

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

{P}C{Q}

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

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

p*p

的式子將因*號(hào)兩側(cè)的子堆擁有相同地址的單元恒為假，即在一個(gè)有效的斷言中相同地址的存儲(chǔ)單元只能出現(xiàn)一次。這個(gè)要求解決了可變存儲(chǔ)區(qū)潛在的別名問題。

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

局部推理規(guī)則使得驗(yàn)證者只需關(guān)注與命令直接相關(guān)的存儲(chǔ)單元的局部狀態(tài)，降低了驗(yàn)證復(fù)雜度。局部推理規(guī)則支持組合驗(yàn)證，為對(duì)局部狀態(tài)的推理擴(kuò)展至對(duì)全局狀態(tài)的推理提供了路徑。

1.1 基于分離邏輯的并發(fā)程序驗(yàn)證技術(shù)

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

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

其中，線程1對(duì)線程2不構(gòu)成干擾是指線程1的執(zhí)行不影響線程2中任一命令的前置條件,不改變其自由變量。

互補(bǔ)干擾條件不足以描述并發(fā)程序的行為。CSL進(jìn)一步提出資源所有權(quán)假設(shè)和分離性假設(shè)：一般存儲(chǔ)單元只可被一個(gè)線程使用，可被復(fù)用的存儲(chǔ)單元應(yīng)歸屬于某一資源組；在任意時(shí)刻，一個(gè)資源組最多被一個(gè)線程使用，且系統(tǒng)的所有存儲(chǔ)單元可被線程和資源組完整劃分；資源組被使用前后均需使對(duì)應(yīng)的資源不變式成立。在此限制下，線程間的交互由資源組實(shí)現(xiàn)，交互的結(jié)果及其影響范圍由資源不變式提前給定。使用資源時(shí)的驗(yàn)證規(guī)則定義如下：

上述規(guī)則限制了進(jìn)程間的交互，規(guī)避了并發(fā)執(zhí)行可能帶來的沖突。

鎖式權(quán)限機(jī)制能夠幫助控制并發(fā)沖突，分?jǐn)?shù)式權(quán)限機(jī)制可以幫助驗(yàn)證者識(shí)別并發(fā)執(zhí)行過程中資源分配不當(dāng)?shù)膯栴}。例如，在Iorn方案[17]中存儲(chǔ)資源獲得的權(quán)限分?jǐn)?shù)與線程無關(guān),與資源大小無關(guān)，分?jǐn)?shù)值僅取決于驗(yàn)證時(shí)執(zhí)行分離和分離合取的次數(shù)。Iorn為系統(tǒng)初始堆的分?jǐn)?shù)賦值為1，其后每次分離動(dòng)作會(huì)將原堆的分?jǐn)?shù)均分至劃分所得的子堆上，而每次執(zhí)行分離合取的所得的堆的分?jǐn)?shù)為原子堆的分?jǐn)?shù)和，即

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

。

權(quán)限分?jǐn)?shù)不影響程序分配、釋放、讀寫等命令的執(zhí)行，僅反映驗(yàn)證過程。若權(quán)限分?jǐn)?shù)出現(xiàn)損失、全局分?jǐn)?shù)和不等于1，則證明驗(yàn)證過程遺漏了對(duì)部分可變存儲(chǔ)區(qū)的控制,可能存在內(nèi)存泄漏風(fēng)險(xiǎn)。驗(yàn)證者可以追溯局部分?jǐn)?shù)的變化定位出錯(cuò)的代碼段。

1.2 基于分離邏輯的云存儲(chǔ)系統(tǒng)驗(yàn)證技術(shù)

云平臺(tái)為并發(fā)程序提供了特殊的運(yùn)行環(huán)境，其本身也是一個(gè)計(jì)算機(jī)程序。保障平臺(tái)本身的正確性是驗(yàn)證平臺(tái)上各類并發(fā)程序正確性的基礎(chǔ)之一。

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

文獻(xiàn)[9]提出的驗(yàn)證方法由建模語言、斷言語言和規(guī)范語言共同構(gòu)成。在建模語言中，該方法引入了與文件和塊結(jié)構(gòu)相關(guān)的變量和命令，改善了存儲(chǔ)架構(gòu)并相應(yīng)地?cái)U(kuò)展了論域。有關(guān)表達(dá)式的語法詳列如下：

經(jīng)擴(kuò)增后的命令語法詳列如下：

|ifbethenCelseC′|whilebedoC。

在斷言語言部分，該方法沿用分離邏輯的斷言語言描述與塊無關(guān)的系統(tǒng)性質(zhì)，引入塊斷言描述與塊相關(guān)的系統(tǒng)性質(zhì)，2個(gè)分量共同構(gòu)成全局?jǐn)嘌砸酝暾枋鱿到y(tǒng)狀態(tài)。其中，塊斷言具體語法如下：

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

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

|bk

|b1b2|bk1==bk2。

在云存儲(chǔ)環(huán)境下，并發(fā)程序之間不僅需要競(jìng)爭(zhēng)云存儲(chǔ)資源，還需要與本地機(jī)器上的其他線程競(jìng)爭(zhēng)本地存儲(chǔ)資源。即使將云存儲(chǔ)資源視為可擴(kuò)展資源，對(duì)于特定的數(shù)據(jù)或數(shù)據(jù)塊的使用權(quán)卻不可隨意擴(kuò)張，資源的競(jìng)爭(zhēng)和調(diào)度受云存儲(chǔ)管理系統(tǒng)控制。同時(shí)，本地內(nèi)存資源有限、擴(kuò)展不易，資源競(jìng)爭(zhēng)帶來的內(nèi)存復(fù)用難以避免?，F(xiàn)有工具對(duì)上述擴(kuò)張限制的描述較為復(fù)雜，容易遺漏。

2 并發(fā)云存儲(chǔ)管理系統(tǒng)建模語言

并發(fā)云存儲(chǔ)管理系統(tǒng)的建模語言是MLBCSS[9]的擴(kuò)展，新增的元素主要用于描述和支持信道等并發(fā)機(jī)制。

2.1 信道機(jī)制設(shè)計(jì)

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

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

StoresCCHVar→Values*Values*=

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

經(jīng)信道轉(zhuǎn)移的存儲(chǔ)權(quán)限可用下式表示：

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

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

2.2 建模語言語法

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

|C:C′|ifbethenCelseC′|whilebedoC

|C1‖C2。

新增的信道變量包括空信道、數(shù)值信息、存儲(chǔ)資源使用權(quán)3種元素以及他們的自由組合，用于描述信道的狀態(tài)。存儲(chǔ)資源使用權(quán)一式的涵義與2.1小節(jié)所述一致。

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

·allocated，分配新的數(shù)據(jù)塊并給定容量上限；

·append，數(shù)據(jù)塊追加寫，受塊容量限制；

·delete，刪除數(shù)據(jù)塊并釋放對(duì)應(yīng)的存儲(chǔ)單元；

·remove，釋放數(shù)據(jù)塊內(nèi)指定的存儲(chǔ)單元；

·newch，開設(shè)新的信道；

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

·send，向信道傳出數(shù)值消息；

·tryre，嘗試從信道內(nèi)取出數(shù)值消息；

·pass，向信道內(nèi)傳出數(shù)據(jù)塊使用權(quán)；

·get，嘗試接收數(shù)據(jù)塊使用權(quán)。

2.3 機(jī)器狀態(tài)描述

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

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→。

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

根據(jù)2.1小節(jié)給出的信道機(jī)制，數(shù)值信息的讀寫操作將改變存儲(chǔ)器的狀態(tài)；塊權(quán)限的轉(zhuǎn)移在執(zhí)行時(shí)不改變存儲(chǔ)器內(nèi)的映射關(guān)系，在驗(yàn)證時(shí)影響各線程可用的存儲(chǔ)區(qū)。因此，StoresC是一個(gè)由信道變量指向數(shù)值隊(duì)列的映射，而通過信道轉(zhuǎn)移的數(shù)據(jù)塊使用權(quán)僅用于輔助推理。

塊的容量限制主要用于對(duì)云存儲(chǔ)系統(tǒng)中塊結(jié)構(gòu)以及機(jī)器中有限內(nèi)存資源的建模。在各類分布式存儲(chǔ)系統(tǒng)中，數(shù)據(jù)塊可以視為存儲(chǔ)的基本單位，容量大多是固定的。如HDFS通常會(huì)將一個(gè)大文件劃分為多個(gè)64 MB的數(shù)據(jù)塊，TFS則會(huì)將多個(gè)小文件整合成為64 MB的數(shù)據(jù)塊。在機(jī)器中，擴(kuò)展內(nèi)存資源通常需要停機(jī)后更新硬件才得以實(shí)現(xiàn)。模型中的數(shù)據(jù)塊容量上限在數(shù)據(jù)塊建立之初被指定，但在此后不可擴(kuò)增，以表征云存儲(chǔ)中固定大小的塊結(jié)構(gòu)和機(jī)器中內(nèi)存不可增長(zhǎng)的特性。在程序運(yùn)行時(shí)，允許進(jìn)程將自己所擁有的數(shù)據(jù)塊作劃分而不改變數(shù)據(jù)塊的總?cè)萘?，以支持?duì)本地內(nèi)存調(diào)度的建模。因此，Size是一個(gè)由已使用的數(shù)據(jù)塊地址指向自然數(shù)的映射。

2.4 建模語言的指稱語義

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

新增的信道表達(dá)式的語義給定如下：

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

其中，n為數(shù)值信息，ch為信道變量。

新增的數(shù)值表達(dá)式$bk表征地址為bk的數(shù)據(jù)塊的容量。原有的表達(dá)式#bk可以代表該數(shù)據(jù)塊內(nèi)已使用的空間，應(yīng)不大于$bk。其語義分別如下：

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

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

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

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。

信道機(jī)制中，塊權(quán)限的轉(zhuǎn)移用于輔助驗(yàn)證，對(duì)內(nèi)存狀態(tài)不作實(shí)質(zhì)性的修改，有關(guān)命令對(duì)系統(tǒng)的影響由3.2小節(jié)說明。信道命令的語義給定如下：

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 斷言語言

斷言語言可以用于描述某特定狀態(tài)下系統(tǒng)所具備的性質(zhì)。文獻(xiàn)[9]提出的斷言語言LRBCSS分別使用地址斷言和塊斷言2個(gè)分離描述與塊無關(guān)的系統(tǒng)特征以及愉快相關(guān)的系統(tǒng)特征。本文進(jìn)一步描述存儲(chǔ)資源所面臨的限制，新增信道斷言以描述線程間交互的性質(zhì)，相應(yīng)修改了全局?jǐn)嘌浴?/p>

3.1 塊斷言

與LRBCSS相比，塊斷言在語法上主要是為數(shù)據(jù)塊引入下標(biāo)以表示當(dāng)前可用的空閑空間。新增的remove指令將塊由只寫不擦變?yōu)榭刹翆?，塊有可能完全空閑，需新增相應(yīng)的語句描述。塊斷言的語法詳列如下：

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

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

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

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

-$σ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′語句在成立時(shí)可說明不同的塊表達(dá)式指向同一塊地址，不必強(qiáng)調(diào)兩者容量相同；b1b2一式表示2塊內(nèi)容一致，其關(guān)注重點(diǎn)在于內(nèi)容而非空間，語義不變。

通過顯式的容量說明，驗(yàn)證者可以直觀得知數(shù)據(jù)塊或?qū)?yīng)的內(nèi)存區(qū)的容量能否滿足程序運(yùn)行所需、是否有溢出的可能。通過對(duì)各線程持有的存儲(chǔ)單元數(shù)量求和，可以直觀得知在驗(yàn)證過程當(dāng)中是否有被遺漏的存儲(chǔ)單元，避免內(nèi)存泄露的風(fēng)險(xiǎn)。

帶計(jì)數(shù)機(jī)制的塊結(jié)構(gòu)也可以描述本地機(jī)器上有限的內(nèi)存資源。為滿足其調(diào)度所需，塊斷言支持塊的切分使用，即

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

bkn1(emp)*bkn2(emp)。

通過上式，本地機(jī)器不必拘束于傳統(tǒng)的2層結(jié)構(gòu)，同時(shí)驗(yàn)證者可以使用信道機(jī)制描述本地機(jī)器的內(nèi)存調(diào)度行為。

3.2 信道斷言

信道斷言主要包括表征信道內(nèi)容的語句和基本的邏輯結(jié)構(gòu)。對(duì)其他存儲(chǔ)結(jié)構(gòu)而言，由于同一時(shí)刻只能在一個(gè)線程中出現(xiàn)，期間不應(yīng)出現(xiàn)2個(gè)相沖突的狀態(tài)描述，在應(yīng)用分離合取和分離析取時(shí)必然滿足“互不相交”的要求。但對(duì)信道而言，通信內(nèi)容至少有發(fā)送方和接收方2者可見，即同一時(shí)刻至少有2個(gè)不同線程的狀態(tài)斷言會(huì)包含同一信道的內(nèi)容，應(yīng)用分離合取和分離析取時(shí)可能會(huì)有沖突，需另外給出說明。由于涉及存儲(chǔ)單元所有權(quán)的轉(zhuǎn)移，這一部分?jǐn)嘌酝瑫r(shí)依賴于不可變存儲(chǔ)器Store以及可變存儲(chǔ)器HeapV和HeapB的狀態(tài)。信道斷言的語法詳列如下：

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

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

相應(yīng)的語義給定如下：

-σ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=

需要注意的是，盡管信道中的內(nèi)容可能因?yàn)椴煌€程執(zhí)行進(jìn)度的差異而無法保證在每次執(zhí)行中都能保持一致，但對(duì)某一特定信道而言，在同一時(shí)刻向不同線程所展示的數(shù)據(jù)流應(yīng)當(dāng)是一致的。因此，在對(duì)信道斷言執(zhí)行分離合取操作時(shí)，相同的信道應(yīng)當(dāng)包含內(nèi)容完全相同的信息流。

3.3 全局?jǐn)嘌?/h3>

全局?jǐn)嘌缘男问绞堑刂窋嘌浴K斷言和信道斷言組成的三元組

α,β,γ。

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

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

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

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

全局?jǐn)嘌圆⒎?個(gè)分量的邏輯求和。例如，若某個(gè)塊出現(xiàn)在信道斷言中，可變數(shù)據(jù)塊存儲(chǔ)器HeapB的狀態(tài)將由塊斷言和信道斷言2者共同確定，簡(jiǎn)單地使用邏輯和聯(lián)結(jié)2者并不能準(zhǔn)確表示當(dāng)中的劃分關(guān)系，使用分離合取“*”聯(lián)結(jié)也不能準(zhǔn)確地描述當(dāng)前數(shù)據(jù)塊權(quán)限的歸屬。對(duì)機(jī)器狀態(tài)而言，這個(gè)三元組是一個(gè)不可簡(jiǎn)單分割的整體。全局?jǐn)嘌缘恼Z法詳列如下：

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

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

相應(yīng)的語義給定如下：

-σα,β,γ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 證明系統(tǒng)

有效的霍爾三元組

{P}C{Q}

由前置條件P、程序指令序列C以及后置條件Q組成。其中，前置條件和后置條件均為全局?jǐn)嘌?，程序指令序列遵?.2小節(jié)給出的語法。本文考慮部分正確性斷言，即對(duì)一個(gè)成立的霍爾三元組，要求：

(1)程序指令序列中所讀寫的變量或存儲(chǔ)單元，必須被包含在前置條件P中或是在程序C中以allocated等語句合法分配所得。即程序?qū)Τ霈F(xiàn)在其前置條件內(nèi)的存儲(chǔ)單元擁有完整的權(quán)限、對(duì)新存儲(chǔ)單元自分配成功時(shí)起擁有完整權(quán)限，直至有關(guān)存儲(chǔ)單元被剔出成立的全局?jǐn)嘌院髾?quán)限滅失；

(2)對(duì)于任何能令前置條件P成立的狀態(tài)σ，C,σ是安全的，即在狀態(tài)σ下運(yùn)行程序C不會(huì)出現(xiàn)導(dǎo)致程序意外退出的故障；

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

4.1 證明規(guī)則

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

{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)

第二部分是與塊命令相關(guān)的公理。由于本文引入了計(jì)數(shù)式機(jī)制，相關(guān)公理被改寫如下：

(A12)

(A13)

(A14)

(A15)

信道相關(guān)操作主要依據(jù)先進(jìn)先出的原則給出相應(yīng)的公理，同時(shí)考慮消息讀取失敗時(shí)的情形。有關(guān)基本公理詳列如下：

(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 基本推理規(guī)則

推理規(guī)則依賴于特定的程序結(jié)構(gòu)而成立。下列基本推理規(guī)則沿用自霍爾邏輯[7]、分離邏輯[6]、并發(fā)分離邏輯[12]以及LRBCSS[9]。

(R1)

(R2)

(R3)

(R4)

(R5)

(R6)

上式中FV (p)為命題p中的自由變量集，ModifyS(C)涵蓋被程序C修改過的除信道變量以外的存儲(chǔ)單元集合。T (be)是將布爾表達(dá)式轉(zhuǎn)換為全局?jǐn)嘌缘暮瘮?shù),定義如下：

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)。

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

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

(2)通過信道傳遞數(shù)據(jù)塊使用權(quán)實(shí)現(xiàn)的復(fù)用。這部分復(fù)用對(duì)程序運(yùn)行的影響可以通過對(duì)信道操作進(jìn)行驗(yàn)證得以釋明。

4.3 涉及信道的狀態(tài)更新規(guī)則

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

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

(RC1)

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

ch

。

在線程間通信中，以接收信息后程序所執(zhí)行的動(dòng)作為標(biāo)準(zhǔn)，信道可作如下劃分：

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

(2)雙向響應(yīng)消息，線程依據(jù)接收到的信息對(duì)外作出特定反應(yīng)。

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

(RC2)

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

(RC3)

上式中的“?”可用于信道操作的限制條件，表明在執(zhí)行操作之前信道可能出現(xiàn)的狀態(tài)，在有多個(gè)可能性時(shí)前后置條件可用下標(biāo)區(qū)別各自的配對(duì)。出于限制信道混用帶來的沖突考慮，在建模和驗(yàn)證期間可以限制線程對(duì)信道的讀寫權(quán)限，以維持“互不干涉”的狀態(tài)。

在實(shí)際驗(yàn)證過程中，驗(yàn)證者可以主動(dòng)區(qū)分不同信道的用途和使用者，以便追蹤線程間通信行為對(duì)全局狀態(tài)的影響。

5 程序驗(yàn)證實(shí)例

本節(jié)給出的實(shí)例由3個(gè)線程組成，分別為用戶發(fā)出寫請(qǐng)求、主節(jié)點(diǎn)分配任務(wù)和數(shù)據(jù)節(jié)點(diǎn)執(zhí)行存儲(chǔ)，為一個(gè)完整的寫數(shù)據(jù)過程。本節(jié)首先給出實(shí)例及其說明：

(1)線程 1. 用戶端

CHVar:appW,upD;

LocalVarList

BKVar:Btemp;

send(appW, 4);

whileBtemp==0do

endwhile;

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

線程1有2次發(fā)信行為，分別為向主節(jié)點(diǎn)發(fā)送寫請(qǐng)求和向數(shù)據(jù)節(jié)點(diǎn)提供具體數(shù)據(jù)，均為數(shù)值信息傳遞。另有一次等待主節(jié)點(diǎn)響應(yīng)的收信過程，由于非阻塞條件下tryre命令不具備等待功能，需用循環(huán)語句輔助。

(2)線程 2. 主節(jié)點(diǎn)

CHVar:disW,disD;

LocalVarList

Var：i;

BKVar:Bpool;

whiletruedo

ifi>0then

send(disW,Bpool);

pass(disD,Bpool,i);

endif;

endwhile;

線程2有2次發(fā)信行為，向用戶端反饋可用數(shù)據(jù)塊地址時(shí)是傳遞“地址”這一數(shù)值信息，令數(shù)據(jù)節(jié)點(diǎn)開辟塊空間則是存儲(chǔ)資源使用權(quán)的轉(zhuǎn)移。

(3)線程 3. 數(shù)據(jù)節(jié)點(diǎn)

LocalVarList

Var：len,j;

BKVar:Bdisk;

while#Bdisk=0do

endwhile;

whilej=0do

endwhile;

ifBdisk==jthen

whilelen<$Bdiskthen

endwhile;

endif;

線程3有2組信息接收行為：首先從主節(jié)點(diǎn)獲得數(shù)據(jù)塊權(quán)限；其后從用戶端獲得需寫入的數(shù)據(jù)、核對(duì)寫入地址后完成操作。

后續(xù)分3部分給出各自線程的驗(yàn)證過程。系統(tǒng)的初始狀態(tài)與emp等價(jià)。

1)用戶端線程驗(yàn)證過程

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)

此處對(duì)信道狀態(tài)的更新依賴于主節(jié)點(diǎn)的驗(yàn)證過程。驗(yàn)證式⑦由RC2推出，是其他線程對(duì)信道操作的影響在全局的體現(xiàn)。驗(yàn)證式⑧依賴于主節(jié)點(diǎn)的響應(yīng)行為，在后續(xù)部分會(huì)詳細(xì)列出對(duì)應(yīng)的條件。由主節(jié)點(diǎn)的驗(yàn)證過程可知，驗(yàn)證式⑧的首次成立不會(huì)早于驗(yàn)證式⑦的首次成立。

此后為一循環(huán)，驗(yàn)證式⑦及⑧均可以成為循環(huán)體執(zhí)行前成立的狀態(tài)?，F(xiàn)以驗(yàn)證式⑦為基礎(chǔ)考慮第一次循環(huán)體執(zhí)行，有：

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

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

由于信道內(nèi)無消息可讀，在非阻塞通信的要求下，讀操作不改變?nèi)魏蜗到y(tǒng)狀態(tài)。同時(shí)由于驗(yàn)證式⑨與驗(yàn)證式⑩等價(jià)，可以構(gòu)成循環(huán)不變式。

再考慮以驗(yàn)證式⑧為前置條件的執(zhí)行過程：

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

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

后續(xù)可有如下驗(yàn)證：

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

2)主節(jié)點(diǎn)程驗(yàn)證過程

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)

初始化各變量后，線程進(jìn)入循環(huán)狀態(tài)。參考用戶端線程的驗(yàn)證過程，循環(huán)體內(nèi)可有驗(yàn)證過程如下：

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)數(shù)據(jù)點(diǎn)程驗(yàn)證過程

*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)

初始化各變量后，數(shù)據(jù)節(jié)點(diǎn)進(jìn)入循環(huán)，等待主節(jié)點(diǎn)的寫權(quán)限分配。與其他線程的循環(huán)等待相似，有效的讀信道行為對(duì)應(yīng)下列驗(yàn)證過程：

(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)

用戶端按時(shí)序提交了寫入地址和4個(gè)待寫入的數(shù)據(jù)共5條數(shù)值信息。在執(zhí)行過程中，數(shù)據(jù)節(jié)點(diǎn)無法得知信道內(nèi)尚未被讀取的信息狀態(tài)，但能在讀取地址之后確認(rèn)循環(huán)條件已不再成立。故驗(yàn)證式為循環(huán)執(zhí)行后的最終結(jié)果。

后續(xù)的驗(yàn)證過程有：

Bdisk4(emp)∧Bdisk=bd,

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

ifBdisk==jthen

Bdisk4(emp)∧Bdisk=bd,

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

其后是一個(gè)以len為循環(huán)變量的循環(huán)體。為方便起見，對(duì)循環(huán)體驗(yàn)證前先對(duì)驗(yàn)證式進(jìn)行等價(jià)變換，具體過程如下：

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)

至此可知，用戶端發(fā)起的寫請(qǐng)求得到了響應(yīng)，數(shù)據(jù)節(jié)點(diǎn)在主節(jié)點(diǎn)賦予的權(quán)限范圍內(nèi)執(zhí)行寫入，被寫入的塊的地址與主節(jié)點(diǎn)向用戶端反饋的塊地址相同，被寫入的數(shù)據(jù)與用戶端提交的數(shù)據(jù)一致，寫功能正確。該實(shí)例涵蓋了循環(huán)、通信的重要的驗(yàn)證環(huán)節(jié)，可以說明本文所提方法的有效性。

6 小 結(jié)

本文基于分離邏輯提出了一種適用于并發(fā)云存儲(chǔ)系統(tǒng)正確性驗(yàn)證的系統(tǒng)方法，在建模語言中引入新的命令和表達(dá)式以描述線程間交互行為、擴(kuò)展斷言語言，以準(zhǔn)確描述資源受限的執(zhí)行環(huán)境，并基于此完善了推理規(guī)則。驗(yàn)證實(shí)例說明本文提出方法的可行性。

本文所提邏輯能直觀描述存儲(chǔ)容量的限制、信道機(jī)制能描述權(quán)限的轉(zhuǎn)移過程，幫助驗(yàn)證者驗(yàn)證存儲(chǔ)管理行為的正確性，識(shí)別潛在的溢出和泄漏風(fēng)險(xiǎn)，滿足云存儲(chǔ)系統(tǒng)的驗(yàn)證所需。本文擴(kuò)展了塊分離邏輯的驗(yàn)證范圍，所提方法也可推廣到云存儲(chǔ)環(huán)境下的普通并發(fā)程序的正確性驗(yàn)證上，為實(shí)現(xiàn)MapReduce、Spark等并發(fā)框架下的程序驗(yàn)證提供了理論上的可能性。

未來的工作包括：①降低信道機(jī)制的復(fù)雜度，改變現(xiàn)有通過驗(yàn)證者主動(dòng)規(guī)避沖突的狀態(tài)，提升其對(duì)時(shí)序關(guān)系的描述精度；②完善所用幽靈狀態(tài)的數(shù)理基礎(chǔ)；③探究驗(yàn)證規(guī)則的可表達(dá)性、相對(duì)完備性；④擴(kuò)展并發(fā)正確性驗(yàn)證的適用范圍；⑤設(shè)計(jì)輔助驗(yàn)證工具和算法。