http://research.microsoft.com/en-us/um/people/lamport/pubs/time-clocks.pdf の要約。
著者はレスリー・ランポート (Leslie Lamport), 1978年。
分散アルゴリズムの書籍や論文でお馴染みの、分散システムにおけるイベント群の順序や時刻の概念を説明している論文。
!
が先頭についている箇所は、要約者による(いい加減な)注釈。
! 資料作成の便宜上、記号や記法が、元論文と若干異なることがあるので注意。
! 後半の要約はだいぶ怪しい...
時間の概念は、思考の際の基礎となるもの:
- これは「イベント群の発生順序」というより基本的な概念から派生している
- e.g., 「ある物事Aが3:15に発生した」という場合、以下の順序でイベント群が生じている:
-
- 時計が3:15を刻む
-
- Aが発生
-
- 時計を3:16を刻む
-
- e.g., 「ある物事Aが3:15に発生した」という場合、以下の順序でイベント群が生じている:
- システムについて考える際に、イベント群の順序の概念、を用いることは普通
- e.g., フライト予約システムの例
- 「そのフライトが満杯になる 前 は、予約は成功すべき」
- e.g., フライト予約システムの例
ただし、分散システムのイベント群について考える場合には、注意が必要。
分散システム:
- 空間的に分離されたプロセス群から構成される
- メッセージ交換によって、互いに通信を行う
- 例:
- a) インターネットで接続されたコンピュータ群
- b) 単一のコンピュータ:
- CPU、メモリ、I/Oチャンネルを、それぞれ別のプロセス、として見ることが可能
- c) マルチプロセスプログラム
- => プロセス間のメッセージ(i.e., 情報・知識)の転送遅延が無視できないなら、そのシステムは分散している、と言える
- 本論文の主関心は
a)
だけど、内容的には(上述のような)より一般的な範囲に適用可能- ! 実際、並列アルゴリズムに関する書籍である『The Art of Multiprocessor Programming』でも似たような話題が出てくる
- ! 命令同士のhappened-before的な関係(半順序)やその全順序付け(linearize)は、並列アルゴリズムを考える際にも重要な概念
- ! マルチコア環境では、CPUキャッシュの影響で、メモリへのWRITE命令が即時に他のスレッドに伝わる保証がないので、その点で分散していると言える(気がする)
- 保証がない、というかラグ(遅延)がある (全てのREAD/WRITE命令の前後にバリアを挟めば別だけど)
- スケーラビリティを上げたり、最適化(reorder,cache)の余地を増やそうとすると、分散システムのモデルに近づいていく、といった方が適切?
分散システムでは「どちらのイベントが先に発生したか」を断定するのが不可能なことがある:
- イベント群の
happened-before
関係は、半順序にしか成り得ない - この事実(およびそれが示唆すること)を理解していないために発生した問題を(著者は)しばしば見かけた
本論文では、
-
happened bofore
関係によって定義された半順序(および論理時計)、について議論し、
-
- それを一貫性のある全順序に拡張する分散アルゴリズムを提示する。
- 得られた全順序は、分散システムにおける同期問題を解決するために利用可能
-
- その後に、この順序付けで生じ得る問題(i.e., ユーザが奇妙に感じるシステムの振る舞い)を説明し、
-
- その解決策として、物理時計(およびその同期方法)、を導入する。
「イベントaがイベントbよりも早い時刻に発生したなら、前者は後者に先行(happened-before)する」という表現はよく見かけるもの:
- 実際には、時刻(time)は、システム内で観察可能なイベント群を用いて定義されなければならない
- 物理時刻(physical time)を使うなら、実時計(real clocks)をシステムが含んでいる必要がある
- ただしそれが利用可能な場合でも、時計の精度や同期を完全にすることは不可能、という問題が残る
- => 上の問題を避けるために、物理時計を使わずに
happened before
関係を定義する
対象となるシステムのより正確な定義:
- プロセスの集合から構成
- 各プロセスはイベント列から形成される
- イベントの粒度はアプリケーション依存 (e.g., サブプログラム、単一のCPU命令)
- メッセージの送受信もイベントの一つ
happened before
関係の定義:
->
と表記- 定義:
-
- aとbが両方との同じプロセス内でのイベントで、aがbの前に出現しているなら
a -> b
- aとbが両方との同じプロセス内でのイベントで、aがbの前に出現しているなら
-
- aがあるメッセージの送信イベントで、bはそのメッセージの受信イベントなら
a -> b
- aがあるメッセージの送信イベントで、bはそのメッセージの受信イベントなら
-
a -> b and b -> c
ならa -> c
-
a -/-> b and b -/-> a
なら、aとbは__並行__、となるa -/-> a
は常に成立するものとする- =>
->
は、システム内のイベント群の(irreflexiveな)半順序、となる
この関係は、空間・・時間ダイアグラム、として図示可能
- 図1
- 横が空間、縦が時間
- 点がイベント
- 矢印の向き(or 真上)を辿っていくことで
happend before
関係にあるイベント群が把握可能
- 矢印の向き(or 真上)を辿っていくことで
happened before
関係の別解釈:
a -> b
なら「aはbに因果的に影響を与え得る」といえる- aはbに対して、情報を伝えることが可能なため
- 実際に因果関係にあるかどうかは
->
だけでは不明 - ! 以降では「aはbに対して因果的に先行している」という表現を用いることがある
a -/-> b
なら互いに独立しており、因果的な影響を与え合うことは不可能
システムに時計を導入する:
- 抽象的な観点では、時計は各イベントに何らかの数値を割り当てる方法、に過ぎない
- その数値は、イベントの発生時刻を表現している
本節で扱う時計の定義:
C[i]
: プロセスP[i]
にローカルな時計(を表す関数)C[i]<a>
で、P[i]
内の任意のイベントaに数値(i.e., 時刻)を割当可能
C
: システム全体の時計の集合C<b>
で、システム内の任意のイベントbに、数値を割当可能- bが
P[j]
のイベントならC<b> = C[j]<b>
- => 物理時刻に対する仮定は一切無いので
C[i]
は__論理時計__ - => 実際のタイミングメカニズムを使わずに、カウンタによって実現可能
時計の正当性条件:
- 物理時刻を正しさの論拠とすることはできない (正確な物理時計が必要となるので)
happened before
関係に基づいた、以下のClock Condition
を使用する:- 全てのイベントa,bに対して
if a -> b then C<a> < C<b>
が成立- => 「aがbよりも前に発生したなら、前者はより早い時刻を有しているべき」という条件
- 次の二つの条件が満たされていればOK:
C1
: プロセスP[i]
内で、aがbよりも前に発生したならC[i]<a> < C[i]<b>
C2
:P[i]
がaで送信したメッセージをP[j]
がbで受信したならC[i]<a> < C[j]<b>
- 全てのイベントa,bに対して
- 注意: 逆は成立しない
- より早い時刻を有しているイベントが、因果的に先行しているとは限らない
- 図1の例:
- p2とp3は両方共、q3に対して並行
- 逆が成立するためには
C(p2) = C(p3) = C(q3)
が要求されるけど、それはC(p2) < C(p3)
の要求と矛盾する
- ! 時刻から
happend before
関係を求めたいなら、ベクトルクロックを用いる必要がある
図の空間・時間ダイアグラムに時刻を付与したのが図2:
- 点線が
Clock Condition
を満たす時計の時刻(tick)- ! 下から二番目の点線の必要性がいまいち不明
- それを時刻ベースに並び替えたものが図3
- 物理時刻の概念を導入しない限りは、図2と図3のどちらがより良い表現かを決定することはできない
この論理時刻を実現するための方法:
- 各プロセスは、以下の方法で、自分のローカル時計
C[i]
の値を管理するIR1
: プロセス内の時計の調整方法 (C1に対応)- 各イベント発生後に時計の値をインクリメントする
IR2
: プロセス間の時計の調整方法 (C2に対応)-
- メッセージmの送信の際には、その時点の時刻Tmを一緒に乗せる
-
- 受信側は
max(Tm, ローカル時刻)
を、新しいローカル時刻とする
- 受信側は
-
- => この方法で
Clock Condition
は満たされる
TODO: 整理
Clock Condition
を満たす時計システムを用いて、イベント群に全順序を付与することが可能:
=>
関係:- 次のどちらから成立するなら
a => b
となる:- i)
C[i]<a> < C[j]<b>
- ii)
C[i]<a> = C[j]<b> and P[i] -< P[j]
- i)
- =>
-<
は競合を解消するための任意の関数 (e.g., プロセスIDの比較)
- 次のどちらから成立するなら
=>
は、->
の素直な拡張:->
で順序付け可能なものはそのまま->
で並行なイベント群は、Clock Condition
を満たす範囲で任意に順序付け- =>
=>
は一意ではなく、許容される複数の全順序があり得る- 時計システムと
-<
次第 - なお
->
は、システム内のイベント群に対して一意に定まる
- 時計システムと
全順序があると、分散システムを実装する上でとても便利:
- 実際、論理時刻システムを作る理由は、全順序が欲しいから
相互排他(mutex)問題の例で、全順序の使い方の例を示す:
- ! mutex自体の説明は省略
- 以下の条件を満たす解法がほしい:
-
- ロックを獲得可能なのは、一度に一人のみ
-
- 獲得順は、リクエストの発行順(
->
)を反映 (順序制約; 並列なものの順序は任意)
- 獲得順は、リクエストの発行順(
-
- いつかは獲得可能
- => 今回の話題に関していえば
2)
が重要
-
- これはnon-trivialな問題:
- 代表プロセス(i.e., スケジューラ)を用意した中央制御では不十分
- 例:
-
P[0]
を代表プロセスとする
-
P[1]
がロック獲得リクエストをP[0]
に送信
-
P[1]
が別のメッセージをP[2]
に送信
-
P[2]
は、その受信を受けて、P[0]
にロック獲得リクエストを送信
-
P[0]
が、P[2]
からのリクエストを受信して、ロックを許可
-
P[0]
が、P[1]
からのリクエストを受信
- => ロック獲得順番が、リクエストの発行順を反映出来ていない
-
- ! "causal delivery"と組み合わせれば、代表プロセスモデルでも解決可能
- 本論文内の解法はより強いもの
- この問題は全順序配信を利用すれば解決可能:
-
- ロックの獲得および解放メッセージをブロードキャストする
-
- 各プロセスは、ロックの獲得・解放順に対して合意(全順序がある)ので、それに従って処理を進めるだけ
- => 各プロセスがローカルの知識のみで、処理可能なので、分散アルゴリズム
-
- 全順序ブロードキャストの実現方法:
-
- 各プロセスはローカルのキュー(優先度付きキュー)を管理
- 順番は
=>
によって決定する
-
- メッセージ(with 時刻)を受信したら、ackメッセージ(with 時刻)を返す
-
- 以下の条件が満たされれば、そのメッセージの順番は(そのプロセスにとって)確定している
- 全てのプロセスに対して、そのメッセージの時刻よりも、時計が進んでいることが確認できた場合
- 各プロセスは、(ローカルに)受信したメッセージ群の時刻から判断可能
- ! 進行性(liveness)を保証するためにackが必要
- ! 通信チャンネルはFIFOを仮定?
-
- 順番が確定したメッセージは、先頭から順番に処理する
-
全順序配信を使えば、任意の同期問題が解決可能:
- 全順序配信は合意問題と同じ表現力
- ! 参考: 『Communication and Agreement Abstractions for Fault-Tolerant Distributed Systems』
ただし、プロセスの失敗には弱い:
- 全員がアルゴリズムに参加することが必須
- ひとつの失敗で崩れる:
- ! 『Impossibility of Distributed Consensus with One Faulty Process』が詳しい
- => 非同期分散システムの本質的な特性
- 失敗を扱うためには、物理時刻の概念が必要
- ! 正確には(?)失敗検出器が必須 (同期システムならそれがただ(?)で手に入る)
- ! 『Impossibility of Distributed Consensus with One Faulty Process』が詳しい
=>
による順序付けだけだと、システムが"奇妙な振る舞い"を取ることがある:
- 例:
-
- ユーザAが、要求Aを、コンピュータAに対して発行
-
- ユーザAは、ユーザBに電話して、別の要求の発行を依頼
-
- ユーザBは、要求Bを、コンピュータBに対して発行
- => 要求Bの時刻が、要求Aの時刻よりも小さくなることが、普通にあり得る
- ユーザAからしたら、先に発行したはずの要求が、後で処理されているように見える
- => ユーザAとユーザBの間の通信が、システムの外部で発生しているのが原因
-
- LET:
F
は、システム内のイベントの集合 - LET:
F~
は、外界も含めたイベントの集合 - LET:
~>
は、F~
に対するhappend before
関係 - 上の現象は
A ~> B
だけど、A -/-> B
なために発生する
二つの対策がある:
-
- 外部の時間を明示的に導入する
- 上の例だと、ユーザAは、要求Aを発行した際にその時刻を受け取り、ユーザBにそれより後の時刻付きの要求の発行を依頼する
- => 奇妙な振る舞い、を回避するのは利用者側の責任
- ! システム内部の時刻を一貫して使用するアプローチ
-
- 次の
Strong Clock Condition
を満たす時計システムを構築する
Strong Clock Condition
:F
内の任意のa,bに対してif a ~> b then C<a> < C<b>
が成立
Clock Condition
よりも強く、論理時計だけでは満たせない条件- => 物理時計を導入する
F~
を物理的な時間・空間が関係するリアルなイベント群、と仮定- 物理時計を用いることで、どのように・どの程度、奇妙な振る舞いが回避可能か、を次節で扱う
- ! システムの内部と外部で共通の時刻(物理時刻)を使用するアプローチ
- ただし、それをシステムから利用するには、物理時計を通す必要があり、そこには誤差がズレがある
- (一つのプロセス内での)時刻と時計の間のズレ、と、時計間のズレ
- 次の
TODO: 整理
物理時計の導入:
- 「物理時刻
t
に、時計C[i]
の値を取得する」をC[i](t)
と表記する - この時計(時計システム)は、以下の二つの制約を満たす必要がある:
- PC1: 全てのiに対して
|dC[i](t)/dt - 1| < k
となるk << 1
が存在するdC[i](t)/dt
は、時計の、物理時刻に対する進行レート- 「物理時刻の(物理時間に対する)の誤差に上界がある」という条件
- 典型的な水晶時計では
k =< 10^(-6)
程度
- PC2: 全てのi,jに対して
|C[i](t) - C[j](t)| < e
が成立- 「プロセス間の時計のズレには上界がある」という制約
- => 異なるプロセス間の時計が、同じレートで進む保証は無いので、何らかの同期メカニズムが必要(後述)
- PC1: 全てのiに対して
- 仮定:
- 時計の値は、前方に飛ぶことはあっても、逆戻りはしない (単調増加)
誤差(i.e., k
とe
)が、どの程度小さければ「奇妙な振る舞い」を防げるか:
- そのためには
Strong Clock Condition
がF~
で満たされている必要がある - 前提:
F
でClock Condition
を満たす時計はあるものとする- => 異なるプロセス間のイベントのみを考慮すればOK
- LET:
M
は、F~
におけるメッセージ転送時間の下限a ~> b
が成立する場合、aの発生時刻をtとすると、bの発生時刻はt + M
以降になる- 光速とプロセス間の距離(の最短)を使えば、常に計算可能
- => ただし、実際のシステムでは、これよりずっと大きな値になるのが普通
- ! 以降の考え方としては「情報の伝達に時間が掛かるなら、時計に多少の誤差があっても大丈夫」的なもの
- 極端な例としてもし
M
の値が0なら、完全に誤差のない時計が必要になる
- 極端な例としてもし
- 「奇妙な振る舞い」を防ぐためには、任意のi,j,tに対して、以下が満たされる必要がある:
C[i](t + M) - C[j](t) > 0
:- 変形:
C[i](t + M) > C[j][t]
- 以下のように解釈すると分かりやすい:
C[j](t)
は、メッセージ送信時の(送信側の)時刻C[i](t + M)
は、メッセージ受信時の(受信側の)時刻の下限- =>
メッセージ受信時刻の下限 > メッセージ送信時刻
- => つまり「依存関係にあるイベント同士で時刻の逆転が起きてはいけない」といっているだけ
- TODO: 転送遅延分だけ、プロセス間の時計がズレても大丈夫、という話が図があった方が分かりやすい
- MEMO:
P[i]
が物理時間=10の時に、メッセージをP[j]
に送信したとする- その際の時計の値は、
P[i]
で10,P[j]
で0、だったとする - 転送遅延が11の場合には
メッセージの時刻=10 < P[j]の時刻=11
となるので問題なし - !
P[j]
の時計が進んでいる分にも問題なし
- その際の時計の値は、
- MEMO:
- 変形:
- 上の制約をPC1およびPC2と組み合わせると
k
およびe
の上限が得られる:- NOTE:
k
は単一プロセス内での時計の誤差の上限、e
はプロセス間の時計のズレの上限 - PC1は
C[i](t + M) - C[i](t) > (1 - k)M
を示唆する:- => "M物理時間経過時に、プロセス内では最低でも(1 - k)Mだけ時計が進む"
- PC2から、以下の不等式が成立すれば、上の条件が満たされることが分かる:
e / (1 - k) =< M
:- =>
プロセス間のズレの最大値 / 時計の最小進行率 =< 最小転送遅延
- "転送遅延分はズレでも良いよ"と"時計の進行速度には差があるよ"の組み合わせ
- =>
- => これが成り立つなら「奇妙な振る舞い」は発生しない
- NOTE:
PC2を保証するためのアルゴリズム:
- プロセス間の時計のズレを蓄積させないための方法
- TODO
- MEMO:
- あるメッセージの正確な転送時間が分かれば、それを元に二プロセス間の時計の(受信時点では)正確な同期を取ることは可能
- ただし"正確な転送時間"は分からないのが普通なので、それよりは小さい、何らかの最小転送遅延、の値を使用して同期を取る
- その最小転送遅延と実際の転送遅延の差が、プロセス間の時計の誤差となる
- ! 転送遅延には上限がある必要がありそう
- 時計の調整アルゴリズム自体はIR1およびIR2とほぼ同様 (特殊化)
上のアルゴリズムがPC2条件を満たすために利用可能なことの説明:
- TODO
- MEMO:
- すごく雑に言えば「全てのプロセス間で、定期的に通信が発生するなら、いつかは同期するでしょ」的な話(だと思う)
TODO: 整理
- 物理時刻を導入しましょう
C[i](t)
で、物理時刻のt
の時計C[i]
を読みだす- 便宜上、クロックは(離散的なtickではなく)連続的な値であるものと仮定する
- TODO: "more precisely"
dC[i]/dt
は、t
時点でのクロックのレートを示す- C[i]が真の物理クロックであるためには、近似的に正しいレートで走る必要がある
- つまり
dC[i]/dt ~= 1
が全てのt
に対して成立する必要がある - より正確には、次の条件が満たされていることを仮定する:
- PC1: 以下を満たす定数
k << 1
が存在する- 全ての
i
に対して|dC[i]/dt - 1| < k
- 全ての
- 典型な水晶時計では
k =< 10^-6
- PC1: 以下を満たす定数
- 複数プロセス間の物理時計に対する制約も必要 (近似的に同期している必要がある)
- PC2: 全ての
i,j
に対して|C[i](t) - C[j](t)| < e
が成立する e
は十分に小さな定数- 図2の例: PC2は横線の高さが
e
以下であることを要求する(?)
- PC2: 全ての
- ドリフトの話:
- 複数のプロセスの時計が違うレートで進むことは普通なので、差が蓄積していくことがある
- PC2が常に満たされるようなアルゴリズムを開発する必要がある
- その前に、まずは
k
とe
の値をどの程度小さくすれば、特異な振る舞いを防げるのかを見ていく- システム
~f
: 関連する物理イベントが発生するシステム。ここでStrong Clock Conditionが満たされる必要がある - 仮定: 前提とするシステム内の論理時計はClock Conditionは満たしいている
~f
内で因果関係にあるイベント同士に関してStrong Clock Conditionが成り立つことを保証する- 異なるプロセス間のイベントのみを考慮すればOK
- LET:
m
- イベント
a
が物理時間t
で起こったとする - 別のプロセスで
a -> b
を満たすイベントb
が発生したとする b
の発生時刻はt + m
以降- 言い換えると「
m
はプロセス間の最小転送時間よりも小さな値」となる - プロセス間の距離と光の速さを使って求められるよ云々
- => 実際には
~f
での転送方法に応じて、もっとずっと大きな値になるでしょう
- イベント
- システム
- 特異な振る舞い、を防ぐための方法:
- 任意の
i,j,t
に対して、以下を確実にする必要がある:C[i](t + m) - C[j](t) > 0
- =>
C[i](t + m) > C[j](t)
C[j](t)
は、"メッセージ送信時のクロック"C[i](t + m)
は、"メッセージ受信時のクロックの下限"- => つまり"依存関係にあるイベント同士で(物理)クロックの逆転が起きない"ことの保証
- ! 図を書きたいかも
- これをPC1およびPC2と結合すると
k
とe
の適切な値が得られる- 仮定: クロックがリセットされる場合には、逆戻りはしない
- PC1は
C[i](t + m) - C[i](t) > (1 - k)m
を示唆する- !
k
は単一のクロックのレートのズレの上限値 - => つまり"m物理時刻経過時に、同じプロセス内の論理時刻は最低でも(1 - k)m進む"といっているに過ぎない
- !
- PC2からは以下が成立すれば
C[i](t + m) - C[j](t) > 0
といえることがわかるe/(1 - k) =< m
- =>
プロセス間のクロックの最大誤差 / クロックの最小進行度 =< 最小転送時間
- => "転送時間分だけはずれても良いよ" + "クロックの進行速度自体に差があるよ"の組み合わせ
- => プロセス間で許容される(i.e, 因果時刻が逆転しない)ズレに、クロック自体の進行の振れ幅を考慮したもの
- ! 図を書きたいかも
- => 上の不等式が満たされれば、特異な振る舞い、は発生し得ない
- ! 外部システムでの情報伝達遅延が減るほど、システム内部の物理時計の同期精度がシビアになる
- 任意の
- PC2(i.e., プロセス間のズレ幅)を保証するためのアルゴリズム:
- LET:
m
を物理時刻t
に送信され、t'
に受信されたメッセージ、とする - LET:
vm = t' - t
: メッセージmのトータル遅延- この値が何かは、プロセスの受信側は知らない (物理時刻に直接アクセスはできないため?)
- しかし、受信プロセスは
0 =< Mm =< vm
となるような最小遅延Mm
を知っているものと仮定する - LET:
gm = vm - Mm
: 予測不可遅延 - IR1とIR2を物理クロック用に特殊化する:
- IR1':
- TODO
- 物理クロックを反映した値だよ、的な話
- IR2':
- a) 送信側
- P[i]が物理時刻tにメッセージmを送ったとする
- mは
Tm = C[i](t)
を含む
- b) 受信側(受信時)
- Pjがメッセージmをt'に受信した
C[j](t') = max(C[j](t' - 0), Tm + Mm)
を実行C[j](t' - 0) = lim{g->0} C[j](t' - |g|)
- a) 送信側
- IR1':
- プロセスは自分のクロックと受信メッセージのタイムスタンプだけ知っていれば良いよ
- 便宜上の仮定: イベントはひとつの時間内に完結する、別々のイベントは別々の時間に発生する
- IR1'とIR2'は、IR1とIR2の特殊化なので、もともとのClock Conditionは保持しているよ
- 実際のイベントは有限の尺だから、アルゴリズムの実装は問題ないよ
- 実装上の関心となりえるのは、離散クロックのtickがC1を満たすに足るに十分な頻度であるか、どうか
- LET:
- 上のクロック同期アルゴリズムがPC2条件を満たすために使えることを示す:
- 仮定:
- プロセス群は有向グラフで記述される
- メッセージの送信元から送信先に対して、有効エッジ(アーク)が存在する
- "T秒毎に、アーク上をメッセージが送信される"という、もし以下がなら (英語がいまいち読み取れていない)
- 任意のtに対して、PiがPjに対して、最低でもひとつのメッセージを、tからt+Tの物理時刻の間、に送信しているなら
- 直径: 任意の2つのプロセスを結ぶパスの最短ホップ数
- 次の定理は、システムが最初に開始した際に、クロックが同期された状態になるまでの経過時間の上限を示している
- 仮定:
- 強く接続されたプロセス群のグラフ
- 直径はd
- IR1'とIR2'に従う
- 仮定:
- 任意のメッセージm(
Mm =< M
が成立。Mは任意の定数)とt => t0
に対して、以下が成立する: - a) PC1が成立
- b) 定数Tとgが存在する
- T秒毎に、予測不可遅延がg以内のメッセージが、全てのアーク上で送信される
- 任意のメッセージm(
- then:
- PC2が全ての
t >= t0 + Td
に対して、e ~= d(2kT + g)
で満たされる - where
m + g << T
が想定される
- PC2が全ての
- ! 後で復習
- この定理の証明はすごく難しいので、付録に回すよ
- 良い参考論文があるよ
- 軽い紹介と本節の新規性に関して
- 仮定:
- 仮定:
TODO: 整理
- "happen-before"の概念を見てきた
- 分散マルチプロセスシステムにおけるイベント群の順序の不変項の定義
- => これが満たされないと整合性が崩れる
- 半順序から全順序への変換アルゴリズム
- 全順序を使って、同期問題を解決する例の提示
- 全順序だけだと、ユーザの視点からは奇妙な振る舞い、となることがある
- 同期された物理時刻の利用
- どの程度厳密に同期可能かの定理の紹介
- 分散システムでは、イベント群は半順序でのみ認識可能なのを知ることは重要
- このアイディアが任意のマルチプロセスシステムを理解するために有用であると信じている
- 問題を解くための方法とは別に、マルチプロセスの基本的な問題を理解することは助けになるはず
省略