障害モデルは、証明や設計においてどのような異常が発生し得るかを規定する。「1つの障害に耐えられる」というプロトコルは、障害の種類、永続化の仮定、通信条件、障害ドメインと組み合わされて初めて意味を持つ。プロセスの終了、データディスクの喪失、片方向のパケット損失、ノードによるメッセージの偽造は、すべて異なる事象である。
ノードはどのように失敗し得るか
モデル 許容される動作 設計上の関心事
Crash-stop ノードが停止した後は実行しない 残りのメンバー間で安全性と進行をどのように維持するか
Crash-recovery ノードが停止した後、再起動可能 どの履歴を永続化すべきか、どのように再参加するか
Omission メッセージの送信漏れ、受信漏れ、処理漏れ リトライ、重複排除、タイムアウト、再送
Byzantine プロトコル違反の任意の動作(異なる相手に対して異なる主張を含む) 認証、競合証拠、ビザンチン耐性プロトコル
厳密な用法では、Fail-stop は他のノードが停止を確実に識別できるというより強い仮定を含み、crash-stop と同義として常に扱えるわけではない。非同期ネットワークでは、停止したプロセスを極めて遅いプロセスと区別できない場合がある。
Crash-stop の純粋なモデルでは、ノードが回復した後に何を保存するかについて言及しないことがあるが、これは実際のサービスが永続性を必要としないことを意味しない。停電後の再起動で確認済みデータを保持する必要がある製品は、追加のストレージと復旧要件を提示している。
Crash-recovery:コミットメントの忘却自体がプロトコルエラー
Raft ノードが再起動後、自身の任期で誰に投票したかを忘れると、再度投票してしまう可能性がある。Paxos acceptor が既に発行した Promise を忘れると、拒否することを約束した古い提案を受け入れてしまう可能性がある。したがって、永続化はユーザーデータだけでなく、将来の動作を制約するプロトコルの履歴も保存する必要がある。
また、「OSキャッシュへのデータ書き込み」と「障害後の永続化要件を満たすこと」を区別する必要がある。ディスク、コントローラ、ファイルシステムの実際の保証は、障害モデルの一部である。古いノードIDと空のデータディレクトリを持つ新しいマシンを無条件で元のノードの正常な回復として扱うことはできない。
1回の障害で、なぜ2人の候補者が過半数を獲得できるのか
3人の投票者 A、B、C がおり、ログはどちらも最新であると考える。任期 7 で A が自身に1票を投じ、B が A に賛成を返信したため、A は A+B の2票を獲得する。B の投票がメモリにのみ記録され、返信後かつ永続化前に障害が発生した場合、回復時に B は既に A に投票したことを忘れる可能性がある。その後、C が同じ任期で自身に1票を投じ、B が C に賛成すると、A+B と B+C の2つの選挙過半数が存在することになる。
2つの過半数は依然として交差するが、問題は交差点である B が、自身の将来の動作を制約する状態を保持しなかったことにある。したがって、「過半数は必ず交差する」という命題は、「交差するメンバーが投票ルールを違反しないこと」と組み合わされて初めて、完全な安全性の推論となる。
誤った返信順序:過半数は交差するが、交点は自身の投票を忘れた
B が A に投票
メモリ内のみの記録
A への返信到達
A+B が過半数に
B が障害復旧
永続状態には投票記録なし
B が再び C に投票
B+C も過半数に
正しい順序:term/votedFor を記録 → 永続化完了 → 返信
すべてのリクエストは任期 7 にあり、候補者のログも同様です。問題は復旧後の重複投票です。
以下では、永続状態を不変のタプルとして簡略化する。durable=False は意図的に誤った早期返信をシミュレートしており、再起動は永続タプルからのみ復旧する。永続化の順序に焦点を当てるため、すべてのリクエストはログの新規性による資格チェックを通ると仮定し、コードは完全な RequestVote を実装しない。
class Voter :
def __init__ ( self ) :
self . stable = ( 0 , None )
self . reboot ( )
def reboot ( self ) :
self . term , self . voted_for = self . stable
def request ( self , term , candidate , durable = True ) :
if term < self . term :
return False
if term > self . term :
self . term , self . voted_for = term , None
if self . voted_for not in ( None , candidate ) :
return False
self . voted_for = candidate
if durable :
self . stable = ( self . term , self . voted_for )
return True
broken = Voter ( )
assert broken . request ( 7 , " A" , durable = False ) broken . reboot ( )
assert broken . request ( 7 , " C" )
safe = Voter ( )
assert safe . request ( 7 , " A" )
safe . reboot ( )
assert not safe . request ( 7 , " C" )
assert safe . request ( 7 , " A" ) assert safe . request ( 8 , " C" ) safe . reboot ( )
assert not safe . request ( 7 , " A" )
実際の実装では、これらの状態に依存する応答を送信する前に、プロトコルが要求する永続的なストレージの更新を完了させる必要がある。永続化は完了したが応答が失われた場合、リトライは古い決定を見ることになる。応答が既に送信されたが決定が失われることを許容すると、他のノードは復旧後に成立しなくなったコミットメントに基づいて行動を続ける可能性がある。これらの2つの障害位置における安全性の意味は異なる。Raft Figure 2:応答前に永続状態を更新
タプルの代入は復旧の境界を表現するためのものであり、ファイルシステムの fsync、原子性書き込み、または停電動作を検証するものではない。実際の障害テストでは、プロセス、カーネル、またはマシン全体がどの時点で障害を起こしたか、およびどのストレージ層がデータを保持しているかを明確にする必要がある。
ビザンチン障害:認証は誠実さを意味しない
認証されたノードであっても、A には値 X を、B には値 Y を主張する可能性がある。署名はメッセージの送信者を証明するが、送信者がプロトコルを自動的に遵守させるものではない。実装ミス、メモリ破損、または侵入により、ノードの動作が単純な停止モデルを超えてしまう可能性がある。
古典的な PBFT は、その非同期安全性と最終的な進行に必要な条件下で、f 個のビザンチン障害に耐えるために少なくとも 3f+1 個のレプリカを使用する。直感的には、2f+1 のクォーラム2つは、3f+1 個のノードの中で少なくとも f+1 個で交差し、その中に少なくとも1つの誠実なノードが含まれる。しかし、安全性は誠実なノードがプロトコルの投票およびロックルールを遵守することに依存する。
これは、同期、認証、信頼できるハードウェアなどのモデルすべてにおける統一されたノード数の下限ではない。2f+1 と 3f+1 を比較する際には、仮定を明確にする必要がある。非ビザンチン多数派コンセンサスでは、交差するノードがプロトコルを遵守すると仮定されるのに対し、ビザンチンモデルでは、交差部分が嘘をつくノードだけで構成されるのを防ぐ必要がある。
1つのノードとの交差が、なぜビザンチンモデルでは不十分なのか
3ノード A、B、C のうち、2つの2票集合 {A,B} と {A,C} の交差は A だけである。A が B には X の署名を、C には Y の署名を行える場合、両側は異なる2つの身份の署名を取得できる。認証はこの交差点を誠実なものにはしない。
古典的な 3f+1 構成は、より大きな交差によって最大 f 個の非誠実メンバーを相殺する。集合の大きさから導かれる:
|Q1 ∩ Q2| ≥ |Q1| + |Q2| − N = 2(2f+1) − (3f+1) = f+1。
交差点に f 個の悪いノードがすべて含まれていたとしても、少なくとも1つの誠実なメンバーが残る。以下の表は数式を展開し、「レプリカ数」、「証拠の閾値」、「障害予算」の口径が混同されていないかを確認しやすくしている。
f レプリカ数 3f+1 クォーラムサイズ 2f+1 最小交差 最小誠実交差
1 4 3 2 1
2 7 5 3 1
3 10 7 4 1
from itertools import combinations
assert ( set ( " AB" ) & set ( " AC" ) ) - { " A" } == set ( )
for f in ( 1 , 2 , 3 ) :
n , q = 3 * f + 1 , 2 * f + 1
quorums = [ set ( c ) for c in combinations ( range ( n ) , q ) ]
smallest = min ( len ( a & b ) for a in quorums for b in quorums )
assert smallest == f + 1
assert smallest - f >= 1
この列挙は集合条件のみをチェックするものであり、PBFT の実装や安全性証明ではない。完全なプロトコルでは、フェーズ、ビュー、シーケンス番号を区別し、誠実なノードがいつ投票し、いつロックし、リーダー交代時にどの証拠を継承するかを規定する必要がある。任意の 2f+1 個のメッセージを取得してコミットを宣言することはできない。異なるビューや異なるログ位置の署名を組み合わせても、同じ決定の有効な証拠は形成されない。PBFT のサービス保証とモデル
交差するノードは、すべての悪いノードを排除するのに十分か?
ここには2種類の交差数がある:あなたが選択した2つの集合が実際に交差する数と、集合の大きさだけを知っている場合に最小保証される交差数である。プロトコルは後者の保証を必要とする。なぜなら、各ラウンドでどのノードが返信するかを事前に指定できないからである。以下では N=7 を固定する。両側でそれぞれ5つのノードを選択する場合、最小交差は3であり、最大2つの非誠実メンバーを差し引いても、少なくとも1つの誠実なメンバーが残る。
h m i n = max ( 0 , ∣ Q 1 ∣ + ∣ Q 2 ∣ − N − f )
図を準備しています 再読み込み
交差するノードは、すべての悪いノードを排除するのに十分か? 2つの集合の最小交差は max(0,∣Q₁∣+∣Q₂∣−N) である。最大 f 個のメンバーが非誠実な場合、誠実な交差の下限はさらに f 減じられ、0 に切り捨てられる。
{"id":"quorum-honest-intersection","title":"交差するノードは、すべての悪いノードを排除するのに十分か?","summary":"2つの集合の最小交差は max(0,∣Q₁∣+∣Q₂∣−N) である。最大 f 個のメンバーが非誠実な場合、誠実な交差の下限はさらに f 減じられ、0 に切り捨てられる。","height":1000,"html":"<h2 data-i18n=\"heading\"></h2><p class=\"intro\" data-i18n=\"intro\"></p><p class=\"hint\">Q₁</p><div id=\"q0\" class=\"choices\"></div><p class=\"hint\">Q₂</p><div id=\"q1\" class=\"choices\"></div><div id=\"overlap\" class=\"track\"></div><div class=\"control\"><label for=\"faults\" data-i18n=\"f\"></label><output for=\"faults\" id=\"faults-value\"></output><input id=\"faults\" type=\"range\" min=\"0\" max=\"3\" value=\"2\" step=\"1\"></div><div class=\"metrics\"><div><span data-i18n=\"actual\"></span><strong id=\"actual\"></strong></div><div><span data-i18n=\"lower\"></span><strong id=\"lower\"></strong></div><div><span data-i18n=\"honest\"></span><strong id=\"honest\"></strong></div></div><div id=\"formula\" class=\"formula\"></div><div class=\"copy\"><p id=\"explanation\" role=\"status\"></p><p class=\"reserve\" aria-hidden=\"true\" data-i18n=\"yes\"></p><p class=\"reserve\" aria-hidden=\"true\" data-i18n=\"no\"></p></div><details class=\"scope\"><summary data-i18n=\"scopeLabel\"></summary><p data-i18n=\"scope\"></p></details>","css":".intro{margin:8px 0 18px;color:var(--muted);font-size:14px}.caption,.hint{font-size:12px;color:var(--muted);margin-top:12px}.control{display:grid;grid-template-columns:minmax(0,1fr) auto;gap:6px 12px;align-items:center;margin:14px 0;font-size:13px}.control label{font-size:13px}.control output{color:var(--accent);min-width:5em;text-align:right;font-variant-numeric:tabular-nums}.control input{grid-column:1/-1;width:100%;margin:0}.presets{display:flex;gap:4px;align-items:stretch}.presets button{flex:1 1 0;min-width:0;overflow-wrap:anywhere;font-size:13px}.actions{display:flex;gap:8px;flex-wrap:wrap;margin:14px 0}.actions button{flex:1;min-width:0;font-size:13px;min-height:42px}.copy{display:grid;font-size:14px;margin:16px 0}.copy>*{grid-area:1/1;margin:0}.reserve{visibility:hidden}.scope{margin-top:14px;color:var(--muted);font-size:12px}.scope summary{padding:8px 0;cursor:pointer}.scope p{margin-top:10px}.two{display:grid;grid-template-columns:repeat(2,minmax(0,1fr));gap:12px;margin:16px 0}.card{border:1px solid var(--rule);border-radius:9px;padding:14px;min-width:0}.card header{font-size:14px;font-weight:600;margin-bottom:10px}.card button{font-size:12px;width:100%;min-width:0}.card small{display:block;font-size:12px;color:var(--muted)}.card code{font-size:12px;overflow-wrap:anywhere}.metrics{display:grid;grid-template-columns:repeat(2,minmax(0,1fr));gap:12px;margin:16px 0}.metrics>div{border-left:2px solid var(--accent);padding-left:10px;min-width:0}.metrics span{display:block;min-height:3.2em;color:var(--muted);font-size:12px}.metrics strong{font-size:23px;display:block;font-weight:500;overflow-wrap:anywhere;font-variant-numeric:tabular-nums}.formula{border-top:1px solid var(--rule);padding-top:12px;margin-top:14px;font-size:13px;font-variant-numeric:tabular-nums;overflow-wrap:anywhere}.value{font:500 20px var(--viz-font-ui)}.legend{display:flex;flex-wrap:wrap;gap:6px 14px;font-size:12px;color:var(--muted);margin:12px 0}.legend span:before{content:'';display:inline-block;width:8px;height:8px;border-radius:2px;background:var(--accent);margin-right:6px}.legend .second:before{background:var(--second)}.check{display:flex;align-items:center;gap:8px;font-size:13px;margin:12px 0}.check input{width:16px;height:16px;flex-shrink:0;accent-color:var(--accent)}select,input[type=text],input[type=number]{background:var(--paper);color:var(--ink);font:inherit;font-size:13px;padding:10px;border:1px solid var(--rule);border-radius:7px;max-width:100%;min-width:0}select{width:100%;min-height:42px}.band{height:20px;display:flex;background:var(--surface);border-radius:4px;overflow:hidden}.band i{height:100%;display:block;background:var(--accent);transition:width .25s}.band i.second{background:var(--second)}button:disabled{cursor:default}.status{font-size:13px;min-height:4.8em}.mono{font-family:var(--viz-font-mono);font-variant-numeric:tabular-nums}.muted{color:var(--muted)}\n@media(max-width:480px){.two{gap:8px}.card{padding:12px 9px}.actions button,.presets button{font-size:12px}.metrics strong{font-size:20px}.metrics{gap:8px}}\n@media(prefers-reduced-motion:reduce){*,*::before,*::after{transition:none!important;animation:none!important}}\n.track-row{margin:16px 0}.track-row>span{display:block;font-size:12px;color:var(--muted);margin-bottom:7px}.track{display:flex;gap:5px;min-width:0}.cell{flex:1;min-width:0;min-height:48px;border:1px solid var(--rule);border-radius:5px;background:var(--surface);display:flex;align-items:center;justify-content:center;text-align:center;padding:5px 3px;font-size:12px;overflow-wrap:anywhere;font-variant-numeric:tabular-nums}.cell.on{background:var(--accent-soft);border-color:var(--accent)}.cell.gold{background:var(--second-soft);border-color:var(--second)}.cell.empty{border-style:dashed;color:var(--muted)}.cell.error{border-color:var(--second);text-decoration:line-through}.choices{display:grid;grid-template-columns:repeat(4,minmax(0,1fr));gap:6px;margin:14px 0}.choices button{min-width:0;padding:10px 4px;font-size:12px;overflow-wrap:anywhere}.choices button[aria-current=true]{border-color:var(--accent);background:var(--accent-soft)}.relation{display:grid;grid-template-columns:minmax(0,1fr) 28px minmax(0,1fr);align-items:center;gap:6px;margin:12px 0}.relation .cell{min-height:72px}.relation>i{text-align:center;font-style:normal;color:var(--accent)}.readout{font-size:13px;white-space:pre-line;min-height:6.4em;overflow-wrap:anywhere}.plot{position:relative;border-left:1px solid var(--rule);border-bottom:1px solid var(--rule);padding:8px 0;margin:18px 0}.plot-row{height:28px;position:relative;margin:4px 0;background:var(--surface)}.plot-row i{position:absolute;inset-block:5px;background:var(--accent);min-width:2px;transition:width .2s,left .2s}.plot-row b{position:relative;padding:4px 6px;font:11px/28px var(--viz-font-ui);background:var(--paper);border-radius:3px}.axis{display:flex;justify-content:space-between;font-size:11px;color:var(--muted)}\n\n/* Action labels must remain readable across locales and narrow embeds. */\n.actions{display:grid;grid-template-columns:repeat(2,minmax(0,1fr));gap:8px}\n.actions button{overflow-wrap:anywhere;white-space:normal;min-height:58px;padding:8px}\nbutton{overflow-wrap:anywhere}\n@media(min-width:640px){.actions{grid-template-columns:repeat(3,minmax(0,1fr))}}\n\n.metrics span{overflow-wrap:anywhere}\n\n.choices{grid-template-columns:repeat(7,minmax(0,1fr))}.metrics{grid-template-columns:repeat(3,minmax(0,1fr))}.metrics span{min-height:5.4em}","js":"const $=s=>document.querySelector(s);const set=(id,v)=>$('#'+id).textContent=v;const t=k=>viz.t(k);function cells(id,values){$('#'+id).replaceChildren(...values.map(v=>{const e=document.createElement('div');e.className='cell '+(v.cls||'');e.textContent=v.text;e.title=v.title||v.text;return e;}));}function pressed(mode){document.querySelectorAll('[data-mode]').forEach(e=>e.setAttribute('aria-pressed',String(e.dataset.mode===mode)));}let qs=[new Set([0,1,2,3,4]),new Set([2,3,4,5,6])];for(let q=0;q<2;q++)for(let i=0;i<7;i++){const b=document.createElement('button');b.textContent='ABCDEFG'[i];b.dataset.node=i;b.onclick=()=>{qs[q].has(i)?qs[q].delete(i):qs[q].add(i);draw();};$('#q'+q).append(b);}function draw(){const a=qs[0].size,b=qs[1].size,f=+$('#faults').value,x=[...qs[0]].filter(i=>qs[1].has(i)).length,lo=Math.max(0,a+b-7),honest=Math.max(0,lo-f);set('faults-value',f);set('actual',x);set('lower',lo);set('honest',honest);set('formula','max(0, '+a+' + '+b+' − 7 − '+f+') = '+honest);cells('overlap',Array.from({length:7},(_,i)=>({text:'ABCDEFG'[i],cls:qs[0].has(i)&&qs[1].has(i)?'gold':'empty'})));qs.forEach((set,q)=>$('#q'+q).querySelectorAll('button').forEach(e=>e.setAttribute('aria-pressed',String(set.has(+e.dataset.node)))));set('explanation',t(honest?'yes':'no'));}$('#faults').oninput=draw;draw();","audio":false,"strings":{"actual":"実際の交差","f":"最大非誠実メンバー f","heading":"交差するノードは、すべての悪いノードを排除するのに十分か?","honest":"誠実な交差の保証下限","intro":"ノードをクリックして、2つの証拠集合をそれぞれ選択してください。故障予算を調整し、実際の交差数と最悪ケースの下限を照合してください。","lower":"同じ大きさの任意の集合の交差下限","no":"下限が0:人数だけでは交差に誠実なメンバーが含まれることを保証できない。","reset":"リセット","scope":"7つのノードを固定し、集合条件のみを検証します。誠実な交差は、同じビュー、位置、フェーズのプロトコルルールに従う必要があります。これは完全な PBFT シミュレーションではありません。","scopeLabel":"モデル範囲と規約","yes":"下限が0より大きい:交差箇所には必ず誠実なメンバーが存在し、その投票を制約するプロトコルルールが必要。"}}
ネットワーク分断:方向性と規模は2つの次元
分断により、ノードは実行を継続できるが、必要なメッセージを交換できなくなる。対称的な分断は両方向に影響を与えるものを指し、非対称的な分断は一方の方向は通るがもう一方は通らないものを指す。これは「均等分割」や「1つのノードの孤立」によって定義されるものではない。
5ノードが 3 + 2 に分断:片側のみが過半数を持つ
A
B
C
D
E
3票:クォーラムを形成
2票:クォーラムを形成不可
少数側の旧リーダーが在任中と思っていても、新たなコミットは正当化されません。
固定されたメンバー集合において、互いに素な2つの分断がどちらも厳密な過半数を含むことはあり得ない。3+2 の分断において、過半数側のノードがすぐに健全であるとは限らない。再選挙が必要であったり、低速ディスクや過負荷の影響を受けたりする可能性がある。2+2+1 に分断された場合、どの側にも過半数はない。
ブレインシュラウド(脳分裂)は、本来唯一であるべきサービスの権威に複数の実際の書き込み者が現れることを指す。合法なマルチマスターシステムは並行書き込みを許可し、競合処理を定義しており、複数の書き込み者が存在するからといってプロトコルの失敗と見なすべきではない。シングルマスターシステムでは、クォーラム、任期、または外部フェンシングを通じて、期限切れの書き込み者が効果を引き続き引き起こすのを阻止する必要がある。
時間モデル:どのような条件下で進行が保証されるか
同期モデルでは、関連する処理と通信に既知の上限が存在すると仮定する。非同期モデルではそのような速度の上限は提供されない。部分的同期モデルでは、何らかの最終的な安定条件下で、十分な時間的制約を獲得できることを許容する。これらはプロトコルの推論における仮定であり、「データセンター内ネットワーク」を同期、「公開ネットワーク」を非同期と呼ぶだけの単純なものではない。
FLP は、1つのプロセスの障害を許容する完全な非同期モデルにおいて、決定論的なコンセンサスがすべての許容される実行で終了することを保証できないことを示している。これは、コンセンサスが安全性を実現できないと言っているわけでも、Raft や Paxos が実際の安定したネットワークで動作できないと言っているわけでもない。エンジニアリングプロトコルは通常、安全性ルールを維持し、利用可能なクォーラム、最終的に安定した通信、ランダム化、または障害検出の仮定の下で進行を追求する。Gilbert と Lynch による不可能性結果の考察
タイムアウトは証拠であり、ノード死亡の証明ではない
応答がタイムアウト内に届かない場合、それは相手側の障害、ネットワークの混雑、ローカルのスケジューリング停止、または応答の損失によるものかもしれない。リクエストが相手側で既に有効になっている場合、タイムアウト後のリトライは重複実行を引き起こす可能性がある。障害検出、ビジネスリトライ、および引き継ぎの権限は、それぞれ個別に設計する必要がある。
タイムアウトが短すぎると、ロングテールレイテンシがリトライや選挙を増幅し、逆に負荷を高める。長すぎると、回復が遅れる。エンドツーエンドのレイテンシ分布、停止、許容される偽陽性、および回復目標に基づいて設定し、過負荷時にはリトライを制限する必要がある。P99 などの統計値は観測サンプルを反映したものであり、将来のレイテンシの硬い上限ではない。
φ-accrual などのプローバーは、ハートビート間隔を疑念の度合いに変換し、連続的な証拠を表現するのに役立つ。しかし、それでも完璧な障害判定を提供するものではない。具体的な推論については障害検出 を参照。
関連する障害:レプリカ数は障害ドメインに取って代われない
3台のマシンが同じ電源、スイッチ、または同じソフトウェア欠陥を共有している場合、同時に失敗する可能性がある。レプリカを異なる障害ドメインに分散させることで、ある種の関連リスクを低減できるが、共通の制御平面、証明書の期限切れ、または誤ったリリースによる共通障害を排除することはできない。
バックアップとレプリケーションも異なる。誤った削除は、すべてのレプリカに正しくレプリケートされる可能性がある。履歴データの復旧を目的とする場合、バックアップ、保持、および復旧検証を別途定義する必要があり、「3つのレプリカがある」ということですべてのデータ保護要件を満たすものではない。
設計と検証のクイックリファレンス
書き込み成功後に、どのデータを失うことを許容し、どのノードまたはストレージ障害に耐えるか?
再起動時にどのプロトコル状態を保持し、ディスクを失ったノードはどのように再参加するか?
ネットワークは片方向の障害、遅延、重複、および分断復旧を考慮しているか?
クォーラムがない場合、どの操作を待機させ、拒否するか、または古い状態での読み取りを許可するか?
古いプロセスが復旧した後、実際のリソースはどのようにして期限切れの権限を拒否するか?
安全性チェックは異常な実行をカバーしているか、回復の進行には明確な前提条件があるか?
これらの質問は、障害注入シナリオに直接変換できる。応答前後の障害、永続化後の停電、旧リーダーの隔離後の復旧、遅延された重複リクエスト、およびメンバー変更中のノード再起動などである。期待される結果は、「最後にサービスが起動した」ことをチェックするだけでなく、不変条件と回復条件として記述されるべきである。
参考
Keywords: crash-stop, crash-recovery, fail-stop, Byzantine, partition, partial synchrony, FLP, safety, liveness