形式化驗證工具（PAT）2PC協議學習

今天我們來看看2PC協議，不知道大家對2PC協議是不是了解，我們先簡單介紹一下。

兩階段提交協議（two phase commit protocol, 2PC）可以保證數據的強一致性，許多分布式關系型數據管理系統采用此協議來完成分布式事務。它是協調所有分布式院子事務參與者，並決定提交或取消（回滾）的分布式算法。同時也是解決一致性問題的一致性算法。該算法能夠解決很多的臨時性系統故障（包括進程，網絡節點，通信等故障），被廣泛的使用。但是，它並不能通過配置來解決所有的問題，在某些情況下，它還需要人為的參與才能解決問題。參與者為了能夠從故障中恢復，它們都使用日志來記錄協議的狀態，雖然使用日志降低了性能，但是節點能夠從中恢復。

在兩階段提交協議中，系統一般包含兩類機器（或者節點）：一類為協調者（coordinator），通常一個系統中只有一個；另一個為事務參與者（participants, cohorts或workers），一般包含多個，在數據存儲系統中可以理解為數據副本的個數。協議中假設每個節點都會記錄寫前日志（write-ahead log）並持久性存儲，即使節點發生故障，日志也不會丟失。協議中同時假設節點不會發生永久性故障而且任意兩個節點都可以互相通信。

當事務的最后一步完成之后，協調器執行協議，參與者根據本地事務能夠成功完成回復同意提交事務或者回滾事務。

顧名思義，兩階段提交協議由兩個階段組成，在正常情況下，兩個階段的執行過程如下所述：

階段1：請求階段（commit-request phase, 或者表決階段，Voting phase）

在請求階段，協調者將通知事務參與者准備提交或取消事務，然后進入表決過程。在表決過程中，參與者將告知協助者自己的決策：同意（事務參與者本地作業執行成功）或取消（本地作業執行故障）。

階段2：提交階段（commit phase）

在該階段，協調者將基於第一個階段的投票結果進行決策，提交或者取消。當且僅當所有的參與者同意提交事務協調器才通知所有的參與者提交事務，，否則協調者將通知所有參與者取消事務。參與者收到協調者發來的消息后將執行響應的操作。

協議操作流圖如下：

兩階段提交最大的劣勢是其通過阻塞完成的協議，在節點等待消息的時候處於阻塞狀態，節點中其他進程則需要等待阻塞進程釋放資源才能使用。如果協調者發生了故障，那么參與者將無法完成事務一直等待下去。以下情況可能導致節點發生永久阻塞：

如果參與者發送同意提交消息給協調者，進程將阻塞直至收到協調者的提交或者混滾的消息。如果協調器發生永久故障，參與者將一直等待，這里可以采用備份的協調器，所有參與者將恢復發給備份協調者，由它來承擔協調器的功能。

如果協調器發送“請求提交”消息給參與者，它將被阻塞直到所有參與者回復了，如果某個參與者發生永久性故障，那么協調器也不會一直阻塞，因為協調器在某一時間內未收到參與者的消息，那么它通知其他參與者回滾事務。

同時兩階段提交協議沒有容錯機制，一個節點發生故障整個事務都要回滾，代價比較大。

下面看一個例子，來說明兩階段提交協議的工作流程：

A組織B、C和D三個人去爬長城：如果所有人都同意去爬長城，那么活動將舉行；如果有一人不同意去爬長城，那么活動將取消。用2PC算法解決該問題的過程如下：

首先A將成為該活動的協調者，B、C和D將成為該活動的參與者。

階段1：

A發郵件給B、C和D，提出下周三去爬山，問是否同意。那么此時A需要等待B、C和D的郵件。

B、C和D分別查看自己的日程安排表。B、C發現自己在當日沒有活動安排，則發郵件告訴A它們同意下周三去爬長城。由於某種原因，D白天沒有查看郵件。那么此時A、B和C均需要等待。到晚上的時候，D發現了A的郵件，然后查看日程安排，發現周三當天已經有別的安排，那么D回復A說活動取消吧。

階段2：

此時A收到了所有活動參與者的郵件，並且A發現D下周三不能去爬山。那么A將發郵件通知B、C和D，下周三爬長城活動取消。

此時B、C回復A“太可惜了”，D回復A“不好意思”。至此該事務終止。

通過該例子可以發現，2PC協議存在明顯的問題。假如D一直不能回復郵件，那么A、B和C將不得不處於一直等待的狀態。並且B和C所持有的資源，即下周三不能安排其它活動，一直不能釋放。其它等待該資源釋放的活動也將不得不處於等待狀態。

基於此，后來有人提出了三階段提交協議，在其中引入超時的機制，將階段1分解為兩個階段：在超時發生以前，系統處於不確定階段；在超時發生以后，系統則轉入確定階段。

2PC協議包含協調者和參與者，並且二者都有發生問題的可能性。假如協調者發生問題，我們可以選出另一個協調者來提交事務。例如，班長組織活動，如果班長生病了，我們可以請副班長來組織。如果協調者出問題，那么事務將不會取消。例如，班級活動希望每個人都能去，假如有一位同學不能去了，那么直接取消活動即可。或者，如果大多數人去的話那么活動如期舉行（2PC變種）。為了能夠更好地解決實際的問題，2PC協議存在很多的變種，例如：樹形2PC協議（或稱遞歸2PC協議）、動態2階段提交協議（D2PC）等。

好了，說了這么一大段協議的東西，我們接下來看看在PAT里面怎么實現這樣的協議。

//Two Phase Commit Protocol (TPCP)

#define N 2; //number of pages
enum {Yes, No, Commit, Abort}; //constants
//channel result 0;
//channel inform 0;
channel vote 0;
var hasNo = false;
 
//The following models the coordinator 
Coord(decC) = (|||{N}@ request -> Skip); 
              (|||{N}@ vote?vo -> atomic{tau{if (vo == No) {hasNo = true;}} -> Skip}); 
              decide -> 
              (([hasNo == false] (|||{N}@inform.Commit -> Skip); CoordPhaseTwo(Commit)) [] ([hasNo == true] (|||{N}@inform.Abort -> Skip); CoordPhaseTwo(Abort)));
CoordPhaseTwo(decC) = |||{N}@acknowledge -> Skip;

//The following models a page
Page(decP, stable) = request -> execute -> (vote!Yes -> PhaseTwo(decP) [] vote!No -> PhaseTwo(decP));
PhaseTwo(decP) = inform.Commit -> complete -> result.decP -> acknowledge -> Skip
                         [] inform.Abort -> undo -> result.decP -> acknowledge -> Skip;
//定義這個alphabet有什么用呢？
#alphabet Coord {request, inform.Commit, inform.Abort, acknowledge};
#alphabet Page {request, inform.Commit, inform.Abort, acknowledge};

System = Coord(Abort) || (|||{N}@Page(Abort, true));
Implementation = System \{request, execute, acknowledge, inform.Abort, inform.Commit, decide, result.Abort, result.Commit};

#assert System deadlockfree;
#define has hasNo == 1;
#assert System |= [](has -> <> undo);
#assert System |= [](request -> <> undo);

Specification = PC(N);
PC(i) = [i == 0](|||{N}@complete -> Skip)
        []
        [i > 0]    (vote.Yes -> PC(i-1) [] vote.No -> PU(i-1));
PU(i) = [i == 0](|||{N}@undo -> Skip)
        []
        [i > 0](vote.Yes -> PU(i-1) [] vote.No -> PU(i-1));
#assert Specification deadlockfree;
#assert Implementation refines Specification;

代碼里面的參與者是pages，這里有兩個人參與者。

枚舉類型給了4個變量，Yes，No，Commit，Abort。值分別為0,1,2,3，Yes和No表示參與者返回給協調者的信息，如果都是YES（0），那么協調者就會確認（Commit，值為2），如果有一個參與者返回的是No（1），協調者就會讓參與者回滾（Abort，值為3）。接下來定義一個通道（channel）vote，接下來定義一個變量（hasNo），表示這個參與者返回給協調者的信息里面是不是有No。

下面來對協調者進行建模：

Coord(decC) = (|||{N}@ request -> Skip); 
              (|||{N}@ vote?vo -> atomic{tau{if (vo == No) {hasNo = true;}} -> Skip}); 
              decide -> 
              (([hasNo == false] (|||{N}@inform.Commit -> Skip); CoordPhaseTwo(Commit)) [] ([hasNo == true] (|||{N}@inform.Abort -> Skip); CoordPhaseTwo(Abort)));
CoordPhaseTwo(decC) = |||{N}@acknowledge -> Skip;

首先，協調者先向參與者發送請求，讓參與者提交，然后協調者通過vote這個通道收到消息，然后如果收到的消息里面有No就把hasNo置為true。然后來做決定，然后是一個選擇，每個選項前面有一個需要滿足的條件（[hasNo==false]或者[hasNo=true]),當hasNo為false時，說明每個參與者都返回給協調者Yes，那么協調者就會確認（Commit），然后開始第二階段。第二階段就是收到來自參與者的答復。

下面是對參與者進行建模：

Page(decP, stable) = request -> execute -> (vote!Yes -> PhaseTwo(decP) [] vote!No -> PhaseTwo(decP));
PhaseTwo(decP) = inform.Commit -> complete -> result.decP -> acknowledge -> Skip
                         [] inform.Abort -> undo -> result.decP -> acknowledge -> Skip;

參與者收到請求，然后開始執行然后進入選擇，要么回復給協調者Yes，然后進入第二階段，要么回復No，進入第二階段。

第二階段就是要么收到確認要么收到回滾，確認之后就是完成，然后進行相應的結果處理，然后給協調者一個答復。收到回滾后就開始回滾，然后對相應的結果進行處理，然后給協調者一個答復。

下面是定義了程序的變量集合：

#alphabet Coord {request, inform.Commit, inform.Abort, acknowledge};
#alphabet Page {request, inform.Commit, inform.Abort, acknowledge};

其實這一個我也不知道是什么意思。

First of all, alphabet of processes are calculated only when it is necessary, which means, only when a parallel composition is evaluated. 
This saves a lot of computational overhead. Processes in a large number of models only communicate through shared variables. 
If no parallel composition is present, there is no need to evaluate alphabets. 
We remark that when there is no shared abstract events, process P ||| Q and P || Q are exactly the same. Therefore, we recommend ||| when appropriate. 
When a parallel composition is evaluated for the first time, the default alphabet of each sub-process is calculated (if not manually defined). 
The procedure for calculating the default alphabet works by retrieving all event constituting the process expression and unfolding every newly-met process reference. 
It throws an exception if a process reference is met twice with different parameters (which probably indicates the unfolding is non-terminating). 
In such a case, PAT expects the user to specify the alphabet of a process using the following syntax,

#alphabet P {...};

where P is process name and {...} is the set of events which is considered its alphabet. Notice that the event expressions may contain variables. 

 翻譯過來就是：

首先，僅當必要時才計算出進程的字母表，這意味着只有當並行組合被評估時。
這節省了大量的計算開銷。大量模型中的進程只能通過共享變量進行通信。
如果不存在平行組合，則不需要評估字母。我們說當沒有共享抽象事件時，進程P ||| Q和P || Q完全一樣。
因此，我們推薦|||適當時候當首次評估並行組合時，會計算每個子進程的默認字母表（如果沒有手動定義）。
計算默認字母表的過程通過檢索構成過程表達式的所有事件並展開每個新滿足的過程引用。
如果一個進程引用被兩次不同的參數（這可能表示展開是不終止的），它會拋出異常。
在這種情況下，PAT希望用戶使用以下語法來指定進程的字母表，

#alphabet P {...};

其中P是進程名稱，{...}是被認為是其字母表的事件集合。請注意，事件表達式可能包含變量。

大概就是說這個字母表是可以自己指定，如果自己不指定那么PAT就會自動生成一個字母表。指定字母表有一個好處就是當程序比較復雜時，PAT就只是照着指定的字母表運行。

然后接下來就是整個系統，整個系統就是協調者和參與者的並發。

接下來Implementation表示在System的基礎上隱藏一些行為。

下面就是一些驗證：

首先驗證System會不會不死鎖。

然后定義了has 變量為 hasNo==1;意思就是hasNo為true，也就是說參與者有回復No的，由此可以看出

#assert System |= [](has -> <> undo);

是正確的，因為有人回復No，那么就會回滾。

下面這個驗證是不正確的，因為協調者讓參與者commit，但是不一定會回滾。

#assert System |= [](request -> <> undo);

接下來是一個行為，

Specification = PC(N);
PC(i) = [i == 0](|||{N}@complete -> Skip)
        []
        [i > 0]    (vote.Yes -> PC(i-1) [] vote.No -> PU(i-1));
PU(i) = [i == 0](|||{N}@undo -> Skip)
        []
        [i > 0](vote.Yes -> PU(i-1) [] vote.No -> PU(i-1));

這個行為大家看看是什么意思，有點復雜，我也不想解釋了。

接下來是兩個驗證：

#assert Specification deadlockfree;
#assert Implementation refines Specification;

這兩個驗證都是正確的。至於為什么正確我也不想解釋了，因為這一塊我不是太懂。