這是一個關於ZooKeeper正在使用的全序廣播協議(Zab)的簡短概述。它在概念上很容易理解,也很容易實現,而且提供很高的性能。在這篇文章裏,咱們會呈現ZooKeeper在Zab上的需求,也會展現這個協議該如何使用,而後咱們整體概述一下這個協議是如何工做的。html
1. 簡介node
在雅虎(Yahoo!),咱們開發了一款叫作ZooKeeper[9]的高性能高可用的協做服務,它容許大規模的應用羣執行協做任務,好比Leader選舉、狀態傳播和會合(rendezvous)。該服務實現了一個層級的數據結點空間——znodes,客戶端能夠用它來實現本身的協做任務。咱們已經發現這個服務有很強的性能擴展性,所以它很容易就知足雅虎的網絡規模,關鍵任務的產品需求。ZooKeeper放棄了鎖,經過實現了無等待(wait-free)的共享數據對象,並保證在這些對象上的操做是有序的,以此來代替鎖。客戶端充分利用這些保障來實現本身的協做任務。通常而言,一個引出ZooKeeper的主要緣由就是,對於應用來講,保持更新操做的有序性比其餘特定的協做技術更加劇要,好比阻塞。web
集成到ZooKeeper裏的是一個全序的廣播協議:Zab。有序的廣播是實現咱們的客戶端保障的關鍵,同時它也須要在每一臺ZooKeeper服務器上維護ZooKeeper的狀態副本。這些副本經過使用咱們的全序廣播協議來保持一致性,好比使用複製狀態機[13]。這篇文章主要關注ZooKeeper在該廣播協議上的需求以及對它實現的一個概述。算法
一個ZooKeeper服務一般由3到7臺機器組成。咱們的實現支持更多機器,可是3到7臺機器能夠提供足夠的性能與彈性。一個客戶端鏈接提供服務的任意一臺機器,並始終能得到ZooKeeper狀態的一致性視圖。這個服務最多能夠容忍在2f+1臺服務器中有f臺出現故障。數據庫
使用ZooKeeper的應用數量很是普遍,而且同時有成千上萬個客戶端併發地訪問它,因此咱們須要有高的吞吐量。咱們爲了知足讀寫操做比例大於2:1的場景而設計ZooKeeper,可是咱們發現ZooKeeper的高寫吞吐量使得它也能勝任一些寫主導的工做。ZooKeepr經過在每臺服務器上的ZooKeeper狀態副原本提供高吞吐量的讀服務。所以,經過添加機器能夠提高容錯率和讀吞吐量,可是不能提高寫吞吐量。相反地,它反而由於廣播協議而受限,因此咱們須要一個高吞吐量的廣播協議。apache
圖1展現了ZooKeeper服務的邏輯組成部分。讀請求由包含ZooKeeper狀態的本地數據庫提供服務。寫請求由ZooKeeper請求轉化成冪等(idempotent)事務,並經過Zab發送,而後再生成響應。許多ZooKeeper寫請求是有條件限制的:api
一個znode只能在它沒有子結點的狀況下被刪除安全
一個zonde能夠用一個名字加一個序號來建立服務器
對數據的修改只能在指望的版本下進行網絡
甚至一些沒有條件限制的寫請求修改了元數據(meta data),好比版本序號,從某種程序上說這不是冪等的。
經過單一的服務器,也就是Leader來發送全部的更新請求,咱們能夠把非冪等的事務轉化爲冪等事務。在這篇文章裏,咱們用事務(transaction)來表示冪等的請求。Leader能夠執行這個轉換,由於它有數據庫副本將來狀態的完美視圖,而且能夠計算出新記錄的狀態。冪等事務就是這個新狀態的一條記錄。ZooKeeper充分利用冪等事務的方面不少已經超出本文範疇,可是事務的冪等性容許咱們放鬆廣播協議在恢復過程當中的排序需求。
2. 需求
咱們假設有一組實現並使用了原子廣播協議的進程集合。爲了保證在ZooKeeper中能正確轉換成冪等請求,那麼同一時刻只能有一個Leader,因此咱們強制規定在協議實現中,只有這樣一條進程。咱們在展現該協議更多細節時再深刻地討論它。
ZooKeeper在廣播協議中定義了以下需求:
可靠交付(Reliable delivery):若是一個消息m在一臺服務器上被交付,那麼它最終將在全部正確的服務器上被交付。
徹底有序(Total order):若是一個消息a在消息b以前被一臺服務器交付,那麼全部服務器都交付了a和b,而且a先於b。
因果有序(Causal order):若是消息a在因果上先於消息b而且兩者都被交付,那麼a必須排在b以前。
爲了保證正確性,ZooKeeper額外地須要以下前置屬性(Prefix property):
前置屬性:若是m是Leader L交付的最後一條消息,那在m以前L提出的消息都必須已交付。
須要注意的是,一條進程可能被選舉屢次,可是因爲這前置屬性,每一次都會被當成不一樣Leader。
在下面三條保證的前提下,咱們能夠保持ZooKeeper數據庫副本的正確性:
可靠性和全序性保證全部副本有一致的狀態。
因果有序保證了從使用Zab的應用的角度來看狀態是正確的。
Leader以收到請求的前提下向數據庫提出更新。
觀察到在Zab中有兩種因果有序關係很重要:
若是有兩條消息a和b,它們是經過同一服務器發送的,而且a在b以前提出,那麼咱們說a在因果上先於b。
Zab假設同時只有一個Leader能夠提交提案。若是Leader變化了,任意先前提出的消息在因果上先於新的Leader提出的消息。
因果衝突示例
爲了展現違反第二條因果關係會出現的問題,咱們來看看下面的場景:
一個ZooKeeper客戶端C1請求設置znode結點"/a"的值爲1,這會轉化成一條消息w1,內容包括("/a", "1", 1),這個元組表明路徑,值和znode的版本。
而後C1請求設置結點"/a"的值爲2 ,這會轉換成一條消息w2 ,內容爲("/a", "2", 2)。
L1提出並交付w1 ,可是在它故障以前,只將w2發佈給它本身。
一個新的Leader L2接管了系統。
一個客戶端C2請求設置結點"/a"的值爲3,這是在版本1的條件下,因此會轉化爲一條消息w3 ,內容爲("/a", "3", 2)。
L2提出並交付w3。
在這個場景中,客戶端接收到了一個對w1成功的響應,可是因爲Leader故障了,對w2收到一條錯誤響應。若是最終L1恢復,又從新得到了Leader的地位,而後嘗試交付w2提案,客戶端請求的因果順序會被破壞,副本的狀態也會出現錯誤。
咱們的故障模型是帶狀態恢復的崩潰模式(crash-fail)。咱們不假設有同步時鐘,可是咱們假設服務器能用差很少的速率感知時間的流逝(咱們使用超時來派發故障)。組成Zab的進程有一個持久化的狀態,因此進程能夠在故障後重啓並經過持久狀態進行恢復。這就意味着一個進程可能只有部分有效的狀態,好比丟失最近的事務,或者更嚴重的,進程可能有早前沒被交付而如今應該丟棄(skipped)的事務。
咱們可以處理f個故障,但咱們也必須處理對應的恢復故障,好比電源中斷。爲了從這些故障中恢復,咱們在消息交付以前,須要將它們保存在多數(Quorum)磁盤的磁盤媒介中。(一些非技術性、實際的和操做導向的緣由使咱們沒有將像UPS設備、冗餘/專用網絡設備和NVRAMs設備加入咱們的設計中。)
雖然咱們假設沒有拜占庭錯誤, 但咱們確實會在協議內部處理消化數據的污染。咱們也給協議包添加了額外的元數據(metadata),用來進行正確性檢驗。若是咱們發現數據被污染或者正確性檢驗失敗,咱們會停止這個服務進程。
因爲運行環境的獨立實現和協議自己的實際問題,咱們發現實現一個徹底的拜占庭容錯的系統對咱們的應用來講是不切實際的。研究也代表爲了得到徹底可靠的獨立實現須要不止程序資源(programming resources)[11]。迄今爲止,咱們產品的大部分問題,要麼是影響全部副本的實現bug,要麼是在Zab實現範疇之外的問題,可是又影響着Zab,好比網絡的錯誤配置。
ZooKeeper使用了一個內存數據庫,而且將事務日誌和週期性的數據庫快照(snapshot)保存到磁盤當中。Zab的事務日誌也兼作了數據庫寫前(write-head)事務日誌,因此一個事務只會往磁盤當中寫入一次。因爲數據庫是一個內存數據庫,而且咱們使用千兆網卡接口(gigabit interface cards),因此寫操做的性能瓶頸就在於磁盤的I/O。咱們採有批量寫的方式下降磁盤I/O瓶頸,這樣咱們能夠在一次向磁盤的寫操做中記錄多條事務。這個批量操做是在副本實現層面而不是在協議層面,因此這個實現和消息打包(message packing)[5]對比更相似於分組提交(group commits)[4, 6]。咱們選擇不用消息打包以下降延遲,可是在批量的磁盤I/O中仍然得到了很高收益。
咱們的帶狀態恢復的故障模型意味着,當一個服務器恢復時,它會去讀它的快照,並重播那些在快照以後交付的事務。所以,在原子廣播(atomic broadcast)的恢復期間,並不須要保證一次性交付。咱們使用冪等事務意味着一條事務的屢次遞交沒有問題,只要能保持重啓的順序。這是寬鬆的全序需求。具體地,若是a是在b以前被交付的,以後因故障致使a再次被交付時,b也將在a以後從新交付。
咱們還有其餘的操做需求:
低延遲(Low latency):ZooKeeper在衆多應用中被普遍使用,咱們的用戶指望有低的響應時間。
爆發性高吞吐量(Bursty high throughput):使用ZooKeeper的應用通常進行讀導向的工做,可是偶爾錯誤的激進配置出現致使大量寫吞吐峯值。
平滑故障處理(Smooth failure handling):若是一個不是Leader的服務器故障,而且仍有多數服務器能正常工做,那麼服務就不會中斷。
3. 爲何開發新的協議
可靠的廣播協議能根據應用的需求能夠呈現不一樣的語義。好比,Birman和Joseph提出兩個原語(primitives),ABCAST和CBCAST,這分別知足了所有有序和因果有序[2]。Zab也提供了因果有序和徹底有序的保證。
對於咱們的狀況,有個好的候選算法是Paxos[12]。Paxos有不少重要的屬性,好比無論故障進程有多少仍能保證安全性,而且容許進程崩潰和恢復,在必定實際的假設下,它能在三次通訊步驟以內提交一個操做。咱們觀察到存在一些實際的假設可讓咱們簡化Paxos算法並且能得到很高的吞吐量。首先,Paxos能容忍消息的丟失和亂序,經過使用TCP進行服務器之間的通訊,咱們能夠保證交付的消息以FIFO(先進先出)的順序進行,這就使得咱們能夠在服務器進程有多個提案消息時也能知足每一個提案的因果有序。可是Paxos並不直接保證因果有序由於它沒有需求FIFO的通道( channel)。
Proposer是Paxos中爲不一樣實例提出value值的代理。爲了保證進度,必須只有一個Proposer提出提案,不然Proposer可能會在一個給出實例中不斷競爭下去。這樣一個有效的Proposer就是Leader。當Paxos從一個Leader故障中恢復過來,新的Leader要保證全部被部分交付的消息要所有交付,而後恢復從舊的Leader中止的那個序號開始提出提案。多個Leader爲一個給定實例提出提案會形成兩個問題。首先,提案可能會衝突,Paxos使用選票(ballot)去派發和解決衝突的提案。其次,這樣的話就不可以知道一個給定序號被提交了,進程須要能獲得哪一個value值被提交的信息。Zab經過保證一個給定的提案編號只有一條提案消息來避免這兩個問題。這就排除了選票的需求並簡化了恢復過程。在Paxos中,若是一個服務器認爲本身是Leader,那麼它就會用一個更高的選票去從上一個Leader當中取得Leader地位。然而,在Zab中,一個新的Leader在多數服務器放棄上一個Leader以前不能得到Leader地位。
一個能夠得到高吞吐量的方法就減小每一次廣播的協議消息的複雜度,好比使用FSR協議(Fixed-Sequencer Ring)。使用FSR協議,即便系統增加了,吞吐量也不會降低,可是延遲會有所增加,所以不適用於咱們的環境。虛擬同步(Virtual synchrony)在羣組穩定了足夠長的時間也能夠提供高的吞吐量[1]。可是,任一服務器故障都會致使服務的重配置,這就致使了在這樣的重配置過程當中有短暫的服務中斷。另外,在這樣系統裏,一個故障監視器(failure detector)須要監視全部服務器。這樣一個故障監視器的可靠性對重配置的穩定性和速度來講就顯得很是重要。Leader導向協議(Leader-based)一樣也依賴故障監視器來保證活性,可是這樣一個故障監視器一次只監視一臺服務器,那就是Leader。在咱們接下來章節的討論中,咱們不爲寫操做使用固定的多數集和羣組,而且當Leader沒有故障時就能保證服務的可用性。
咱們的協議有固定的計數器(sequencer),根據Defago et al.的分類[3],就是咱們說的Leader。這樣一個Leader經過一個Leader選舉算法被選舉出來,並與大多數服務器進行同步,這些服務器叫Follower。因爲Leader須要管理給全部Follower的消息,考慮到這個協議使用固定計數器的決定不能在組成這個系統的服務器之間公平地分配負載。咱們接受這個方法,有如下幾個緣由:
客戶端能夠鏈接任一服務器,服務器要能在本地提供讀操做,並保持與客戶端的會話(session)信息。這個對於Follower進程的額外負擔(不是Leader進程),可讓負載更均勻地被分發。
服務器數量的影響比較小。這意味着網絡通訊的上限不會成爲能夠影響固定序列協議的瓶頸。
實現更復雜的方法沒有必要,由於簡單的實現能夠提供足夠性能。
好比擁有一個可移動的計數器,提高了實現的複雜度,由於咱們必需要處理一些如token丟失的問題。一樣,咱們在通訊歷史的基礎上移除這些模型,好比發送者導向模型(sender-bassed),以此來避免這些協議引發的二次消息複雜度。最終一致性協議也有一樣的問題[8]。
使用一個Leader須要咱們從Leader故障中恢復以保證進度。咱們使用一些視圖變化相關的技術,好比Keidar and Dolev協議[10]。不一樣於他們的協議,咱們不使用羣組通訊來操做。若是一個新的服務器加入或者離開(可能由於崩潰),咱們不會引起一個視圖變動,除非那是一個表明Leader崩潰的事件。
4. 協議
Zab協議包括兩個模式:恢復(recovery)和廣播(broadcast)。當服務啓動或者在Leader故障之後,Zab過渡到恢復模式。在一個Leader出現而且有多數服務器與它進行同步後,恢復模式結束。同步包括保證Leader和新的服務器保持一致的狀態。
當Leader有了多數已同步的Follower,它就能夠開始廣播消息。就像咱們在簡介當中提到的,ZooKeeper服務使用一個Leader來處理請求。Leader就是那個經過初始化廣播協議來處理廣播的服務器,其餘除了Leader之外的服務器要發送消息的話得先把它發送給Leader。經過從恢復模式選出來的Leader看成處理寫請求和協調廣播協議的Leader,咱們消除了從寫請求Leader到廣播協議Leader的網絡延遲。
若是一個Zab服務器在Leader的廣播階段上線,這個服務器會以恢復模式啓動,查找並與Leader進行同步,而後纔開始參與消息廣播。服務會保持在廣播模式直到Leader故障或者它再也不具備多數集合的Follower。任意Follower的多數集對Leader來講都是足夠的,這樣服務就能保持活躍。好比,一個Zab服務由3臺服務器組成,其中1臺是Leader,另外2臺是Follower,而後系統進入廣播模式。若是其中一個Follower死亡,也不會形成服務中斷,由於Leader仍然具備一個多數集。若是這個Follower恢復而另外一個死亡,那樣也不會形成服務中斷。
4.1 廣播
在原子廣播協議運行時咱們使用的協議叫作廣播模式,就像一個簡單的二階段提交(two-phase commit)[7]:Leader提出一個請求,收集投票,最後提交。圖2闡述了咱們協議的消息流。咱們能簡化二階段提交協議由於咱們沒有中斷(aborts),Follower要麼接受Leader的提案,要麼放棄這個Leader。沒有中斷也意味着咱們能夠在多數服務器迴應(ack)時當即提交,而不用等到全部服務器響應。這個簡化的二階段提交它本身是不能處理Leader故障的,因此咱們會添加恢復模式去處理Leader故障。
這個廣播協議使用FIFO(TCP)通道進行全部通訊。經過使用FIFO通道,維持有序保證就顯得很是簡單。消息經過FIFO通道被順序地派發,只要消息能以它們被接收到的順序被處理,順序就能保證。
Leader爲被交付的消息廣播一個提案。在發起一條提案消息以前,Leader爲它分配一個單調遞增的惟一id,叫作zxid。由於Zab保證了因果有序,發送的消息也會在它們的zxid上保持有序。經過將包含信息的提案附着到每一個Follower的輸出隊列中,並經FIFO通道發送給Follower,以此來進行廣播。當一個Follower收到一個提案,會將它寫入磁盤,若是有可能的話就批處理它們,而後當提案寫到磁盤媒介時發送迴應給Leader。當一個Leader從多數Follower中收到迴應(ACK)時,它會廣播一條提交(COMMIT)指令而後在本地提交消息。當Follower從Leader處收到提交(COMMIT)指令時也提交消息。
注意到若是Follower之間互相廣播ACK的話,Leader並非必定要發送COMMIT指令。這個改動不只會提高網絡負載,它也須要比簡單星狀拓撲(simple star topology)更完整的通訊圖,星狀拓撲從TCP鏈接的角度來看更容易管理。保持這個圖而且追蹤ACK信息,在咱們的實現中認爲這是不可接受的複雜度。
4.2 恢復
這個簡單廣播協議在Leader故障或者失去多數的Follower前都能良好工做。爲了保證進度,一個選舉新Leader和使全部服務器進入正確狀態的恢復過程就顯得頗有必要。對於Leader選舉,咱們須要一個高成功機率的算法以保障活性。這個Leader選舉協議不止讓Leader知道本身是Leader,也要讓多數服務器贊成這個決定。若是一個選舉階段不能正確完成,服務器不會進行下一步工做,它們最終會超時,而後從新開始Leader選舉。咱們有兩種不一樣的Leader選舉實現。若是還存在多數運行正常的服務的話,最快的Leader選舉只須要幾百毫秒就能完成。
在恢復階段完成過程的一段時間裏,會有一些提案正在被傳送。這些提案的最大值是個可配置選項,但默認值是1000。爲了保證這個協議在Leader故障時也能正常工做,咱們須要兩個具體的保證:咱們不會忽略(forget)任何已遞交的消息,也不會保留已經跳過(skipped)的消息。
若是一條消息在一臺機器被交付,那麼就應該在全部機器上被遞交,哪怕那臺機器出現故障。這種狀況很容易出現,若是Leader提交了一條消息而後在COMMIT指令到達其餘機器前出來故障,如圖3所示。由於Leader提交了這條消息,客戶端應該已能在這條消息中看到事務的結果,因此該事務最終要發送給全部其餘服務器,所以客戶端才能看到一個一致的視圖。
相反地,一條跳過的消息要保持被跳過。一樣這個狀況也很容易出現,若是Leader生成了一個提案而後在任何人看到以前就出現了一些故障。好比在圖3 ,沒有其餘服務器看到編號爲3的提案,因此在圖4中,當服務器1從新上線並從新集成到系統中時,它須要保證把編號3的提案丟棄。若是服務器1成爲新的Leader,並在消息100000001和100000002被提交後提交消息3,這就違反了咱們的順序保證。
經過對Leader選舉協議的簡單調整就能解決記住已交付消息的問題。若是這個Leader選舉協議保證新的Leader具備多數服務器中最高的提案編號,那麼新選出來的Leader就會擁有全部已提交的消息。在提出新提案消息以前,新選出來的Leader要保證全部記錄在它事務日誌中的消息已經被提出並被多數服務器經過。注意到新的Leader是處理最高zxid的服務器進程剛好是一個優化,這樣新選出來的Leader不須要從Follower羣組中找到哪一個擁有最高的zxid,而且去拉取(fetch)丟失的事務。
全部正常運行的服務器要麼是一個Leader,要麼就是這個Leader的Follower。Leader保證它的Follower能看到全部提案,而且全部已經過的提案都被交付。它經過把新鏈接的Follower還沒看到的PROPOSAL指令放到隊列裏,而後將這些提案到最新提案的COMMIT指令也放到隊列中來實現這個目的。當全部這樣的消息都放到隊列中後,Leader將Follower添加到之後的PROPOSAL和ACK的廣播列表。
跳過那些被提出可是沒有被交付的消息一樣也很容易處理。在咱們的實現中,zxid是個64位(64-bits)的數字,其中低32位(32-bits)看成一個簡單的計數器。每一條提案增長那個計數。高32位表明輪次(epoch)。每次新的Leader選出,它會從它日誌中最高的zxid裏提取出輪次,增長輪次,並用新輪次和計數0組成的zxid。使用輪次去標記Leader的變動而且讓多數服務器認爲一臺服務器是當前輪次的Leader,可讓咱們避免多個Leader使用同一個zxid提出不一樣提案的狀況。使用這個模式的其中一個好處就是咱們能跳過當Leader故障時的一些實例,所以能夠加速和簡化恢復過程。若是一臺服務器重啓並帶着一條沒被交付的上輪消息,它不能成爲一個新的Leader,由於任一多數服務器集,都有一個具備新輪次,即有更高的zxid的提案的服務器。當這個服務器以Follower的身份鏈接,Leader檢查Follower的最大提案輪次的最後提交的消息,並讓Follower清空它的事務日誌(也就是忽略)直到當前輪次。在圖4中,當服務器1鏈接上Leader,Leader告訴它從事務日誌中清除提案3。
5. 結束語
咱們快速地實現這個協議,而且在生產環境上證實了它的強健性(robust)。更爲重要的是,咱們也實現了的高吞吐量低延遲的目標。因爲特殊的4倍於數據包傳輸的延遲與服務器的數量無關,在非飽和(non-saturated)的系統中,延遲以毫秒計。爆發性負載也獲得適當的處理,由於當收到多數提案的迴應時,消息就會被提交。緩慢的服務器不會影響爆發性吞吐量,由於快速的多數服務器能夠在不包括慢速服務器的前提下響應消息。最後,因爲Leader一收到多數Follower迴應就提交消息,因此只要大多數和機器運行正常,Follower故障並不會影響性能甚至是吞吐量。
因爲該協議的高效實現,咱們有一個實現系統達到了每秒數萬到數十萬操做,讀寫工做負載比例達到2:1甚至更高。這個系統是目前在生產環境中使用,而且它是用於大型應用的,好比雅虎crawler和雅虎廣告系統。
致謝
咱們要感謝審稿人的寶貴意見,感謝Robbert van Renesse在關於Zab的離線討論中幫咱們闡明瞭幾個觀點。
6. 引用文獻
[1] K. Birman and T. Joseph. Exploiting virtual synchrony in distributed systems. SIGOPS Oper. Syst. Rev., 21(5):123–138, 1987.
[2] K. P. Birman and T. A. Joseph. Reliable communication in the presence of failures. ACM Trans. Comput. Syst., 5(1):47–76, 1987.
[3] X. D ́efago, A. Schiper, and P. Urb ́an. Total order broadcast and multicast algorithms: Taxonomy and survey. ACM Comput. Surv., 36(4):372–421, 2004.
[4] D. J. DeWitt, R. H. Katz, F. Olken, L. D. Shapiro, M. R. Stonebraker, and D. Wood. Implementation techniques for main memory database systems. SIGMOD Rec., 14(2):1–8, 1984.
[5] R. Friedman and R. van Renesse. Packing messages as a tool for boosting the performance of total ordering protocols. In HPDC, pages 233–242, 1997.
[6] D. Gawlick and D. Kinkade. Varieties of concurrency control in ims/vs fast path. IEEE Database Eng. Bull., 8(2):3–10, 1985.
[7] J. Gray. Notes on data base operating systems. In Operating Systems, An Advanced Course, pages 393–481, London, UK, 1978. Springer-Verlag.
[8] R. Guerraoui, R. R. Levy, B. Pochon, and V. Quema. High throughput total order broadcast for cluster environments. In DSN ’06: Proceedings of the International Conference on Dependable Systems and Networks, pages 549–557, Washington, DC, USA, 2006. IEEE Computer Society.
[9] http://hadoop.apache.org/zookeeper. Zookeeper pro ject page, 2008.
[10] I. Keidar and D. Dolev. Totally ordered broadcast in the face of network partitions. In D. R. Avresky, editor, Dependable Network Computing, chapter 3, pages 51–75. Kluwer Academic, 2000.
[11] J. C. Knight and N. G. Leveson. An experimental evaluation of the assumption of independence in multiversion programming. IEEE Trans. Softw. Eng., 12(1):96–109, 1986.
[12] L. Lamport. The part-time parliament. ACM Trans. Comput. Syst., 16(2):133–169, 1998.
[13] F. B. Schneider. Implementing fault-tolerant services using the state machine approach: a tutorial. ACM Comput. Surv., 22(4):299–319, 1990.