この章では並行オブジェクトの correctness と progress を規定する様々な方法を学ぶ。
correctness の3つタイプ
- Quiescent consistency
- 弱い制約。ハイパフォーマンスを必要とするシステムに使える
- Sequential consistency
- 強い制約。ハードウェアメモリのような低レベルのシステムに役立つ
- Linearizability
- 強い制約。linearizable なコンポーネントから構成される、高レベルのシステムに役立つ
ブロッキングとノンブロッキングの progress の実装による違いの話もやる。
並行オブジェクトの correctness が意味するのは？
- Fig. 3.1 の並行FIFOキューは排他制御しているので correct と判断できる。
- Fig. 3.2 は A, B, C が同時にアクセスしている例。ロックがあるので操作がシーケンシャルに呼ばれる。
- Fig. 3.3 はロックを使わない並行FIFOキューの実装。
single-enqueuer/single-dequeuer なら correct と言えるが説明は簡単じゃない。
確かに、メソッドレベルでロック使えば簡単だけど、アムダールの法則を忘れずに。
並行オブジェクトを規定して使えるようになりましょう。
オブジェクトのメソッドのふるまいを記述する方法は formal spec から plain English まで様々。
APIドキュメントはよく使われる。
事前条件、事後条件、副作用の書き方のスタイルは sequential specification と呼ばれ、
シングルスレッド（シーケンシャル）では機能するけど、マルチスレッドだと破綻する。
複数スレッドのメソッド呼び出しがオーバーラップするので、同じメソッドを同時に呼び出した時や、
状態を変更するような別々のメソッドが呼ばれることがある。
並行オブジェクトがどうふるまうかの直感を鍛える一つの方法は、 単純なオブジェクトを含む並行計算の例を直感と照らし合わせること。
メソッド呼び出しは、invocation と response の間にはインターバルがあり、 並行処理ではメソッド呼び出しがオーバーラップしうる。
invocation して response がまだのメソッドは pending の状態と呼ぶ。
Fig. 3.4 はレジスター（読み書きのメモリ領域）に同時に書き込んで、書き込みが混ざる例、
これは、許容できないので、以下の原理を提起している。
Principle 3.3.1.
メソッド呼び出しは、起こった順番に１つずつ起きるように見えなくてはいけない
これだけでは役に立たない。 （例：順次実行だとしても、read が常にオブジェクトの初期状態を返すことを許容する）
pending の状態のメソッド呼び出しがない場合（アクセスがない時）、 オブジェクトが quiescent （休止）であると呼ぶ。
Principle 3.3.2.
休止期間で区切られたメソッド呼び出しは、リアルタイム順で作用されるように見えなくてはいけない
例えば、AとBが同時にxとyをFIFOに入れて、休止期間後 C が z を入れる場合、 x と y の順番は予測できないが z が x, y の後であることは明らか。
これら二つを合わせて quiescent consistency と呼ぶ。
砕けて説明すると、休止状態になるまでに実行された呼び出しは、 その完了した呼び出しのどれかの順次実行パターンと等価。 例としては、Chapter 1 の共有カウンター、椅子取りゲーム。
quiescent consistency はどのくらい同時実行を制限するのか？ 何も制限しない。
- メソッドが全ての状態に対して定義されるなら total、一部なら partial
- 無制限の FIFO キューの場合、enq は total、deq は partial（nonempty の時しか作用が定義されない）
どの同時実行でも、total メソッドの pending invocation は quiescently consistent なレスポンスがある。 レスポンスが何であるか分かるのは簡単と言っているのではなく、correctness の条件がそこに立ちはだかることはないと言っている。
ノンブロッキング特性
quiescent consistency は nonblocking correctness の条件であることを Section 3.6 で明らかにする。
Compositionality
correctness property P が compositional とは、システム内のオブジェクトがいつでも P を満たすときに、 システム全体が P を満たす場合。
Compositionality は大規模システムには重要。コンポーネント単位で正しさを保証すればよくなりお互いに実装を気にしなくて良い。
quiescent consistency は compositional。
Fig. 3.5 は共有メモリにシングルスレッドで 7 を書いて -3 を書いて、読むと 7 が返ってくる例。 最後に書いたのが読めないような挙動を、許容できないアプリはある。
この例ではプログラム順に作用していないのが問題なので、以下の原理を提起している。
Principle 3.4.1.
メソッド呼び出しはプログラム順に作用するように見えなくてはいけない
この原理は、純粋な逐次計算は期待通りにふるまう事を保証してくれる。
3.3.1 と 3.4.1 を合わせて sequential consistency となる。
これは、同時実行するメソッド呼び出しが、プログラム順と同じ順に逐次実行する順番があること。
この条件を満たす順番は一つとは限らない。
Fig. 3.6 では以下の二通りのプログラム順が考えられるが、どちらも sequential consistent。
A enq(x) → B enq(y) → B deq(x) → A deq(y)B enq(y) → A enq(x) → A deq(y) → B deq(x)
sequential consistency と quiescent consistency は比較できない。
sequential で quiescent でないのもあるし（休止期間の保証ない）、その逆もある（プログラム順の保証でない）。
最近のマルチプロセッサのアーキテクチャでは、メモリの読み書きは sequentially consistent ではない。
- 複雑な方法で並べ替えしている
- 正しくメモりに読み書きができるように、アーキテクチャはメモリバリアなどの特殊な命令を提供している
- 従って、オンデマンドに sequentially consistent を実装している
Fig. 3.7 は sequential consistency は満たすが、直感に反する例。
A enq(x) と B enq(y) はプログラム順では関係ないので並び替えていい。
ノンブロッキング特性
sequential consistency は quiescent consistency と同じようにノンブロッキング。
Compositionality
sequential consistency は compositional ではない。
Fig. 3.8 の例で、p と q は以下のように並び替えれば sequential consistent だが、
- B p.enq(y) → A p.enq(x) → A p.deq(y)
- A q.enq(x) → B q.enq(y) → A q.deq(x)
プログラム順と組み合わせるとループになっている。
- A p.enq(x) → A q.enq(x) → B q.enq(y) → B p.enq(y) → A p.enq(x)
sequentially consistent は compositional でない欠点があるので、以下の制約を考える。
Principle 3.5.1.
それぞれのメソッド呼び出しは、invocation と response のどこがで即座に作用するように見えなくてはいけない
これは、メソッド呼び出しのリアルタイムのふるまいが保たれることを意味していて、 linearizability と呼ぶ。
linearizability は sequnetially consistent だが逆は違う。
通常は、線形化の場所はメソッドが作用を起こす部分。
ロックを用いた実装だと、クリティカルセクションだし、ロックがない場合は他のメソッド呼び出しから見える部分に作用を起こす場所。
composition が重要でないハードウェアメモリとかでは Sequential consistency は良い方法。
対して、Linearizability は、コンポーネントを組み合わせて作る大規模なシステムには良い方法。
linearizability の正式な定義を考えましょう。
quiescent consistency と sequential consistency は exercise で！
並行システムを History でモデル化（H と表記）
- History : invocation と response の有限シーケンス
- SubHistory : History のサブシーケンス
メソッド呼び出しは <x.m(a∗) A> で表現する。
- x: オブジェクト
- m: メソッド
- a*: 引数リスト
- A: スレッド
レスポンスは <x : t(r∗) A> で表現する。
- x: オブジェクト
- t: OK もしくは、例外名
- r*: 戻り値リスト
- A: スレッド
メソッド呼び出しは、invocation と response のペア。
- pending : invocation の response がない状態
- H の extension : H のいくつかの pending invocations に response を付け足したもの。（3.6.1 で詳しく）
- complete(H) : pending している invocation を取り除いたもの。
- Sequential : H のメソッド呼び出しがオーバーラップしていない
- H|A : H からスレッド A だけ抜き出したもの
- H|x : H からオブジェクト x だけ抜き出したもの
- Equivalant : 二つのヒストリーのスレッド単位でのヒストリーが一致
- Well-formed : スレッド単位でのメソッド呼び出しが Sequential
- Legal history : H|x が sequential spec を満たしている
どんな partial order → も total order < に拡張できる。すなわち、
Fact 3.6.1.
→ が X の partial order なら、X には x → y なら x < y になる total order “<” が存在する
- m0 precedes m1 : メソッドコール m0 が m1 の開始前に終了していること。 すなわち m0 の response が m1 の invocation の前。
- m0 →H m1 : H で m0 precedes m1 の時（→H が partial order である証明は exercise で！） H が Sequential なら →H は total order。
- m0 →x m1 : H|x で m0 precedes m1
基本ルールは、一つのメソッド呼び出しが別の呼び出しより precedes している時、前の呼び出しは後の呼び出しの前に作用している。
逆に、二つのメソッドがオーバーラップしていて、順序が曖昧な時は、都合良く並び替えていい。
Definition 3.6.1.
H が linearizable とは、H' の extention であり L1, L2 を満たす legal sequential history S が存在する
L1: complete(H') が S と equivalent
L2: m0 →H m1 の時 m0 →S m1 も真
S を H の linearization と呼ぶ（H は複数の linearization を持つこともある）。
H の extention H' は、他のメソッドに影響を与える呼び出しで response がないものは response を付け足す。
Fig 3.9 で enq(x) は deq(x) に影響があるので response を付け加えるように extend する。
L2 は H の順序が保存されていることを言っている。
Linearizability は compositional。
Theorem3.6.1.
それぞれの x に対して H|x が linearizable の場合（かつ、その場合に限り）H が linearizable
Proof:
only if の部分は excercise で！
それぞれの x で H|x の lineralization を選択する。
Rx を lineralization を構成するのに足した resoponse の集合とし、→x を対応する linearization 順とする。
H' を H に Rx を足したヒストリーとする。
H' のメソッド呼び出しの数の帰納法で証明。
メソッド呼び出しが 1 つの場合は明らか。
メソッド呼び出しが 1 より大きい K より小さいの全ての H で成り立つと仮定。
H'|x の最後のメソッド呼び出し m を考える（m →H m' となる m' はない）。
H' から m を取り除いたヒストリーを G' とする。
m は最後なので、H' は G�' · m と equivalent。
帰納法の仮定から、G' は linearizable な sequential history S' があるので、
H' と H は linearizable な S�' · m がある。
Compositionality はモジュール化して組み立てられるから重要。
Noncompositional な並行システムは、全てのオブジェクトを集中型のスケジューラに頼るか、
スケジューリングプロトコルに準拠させるようにオブジェクトに新しい制約を課す必要がある。
Linearizability はノンブロッキング。 すなわち total method の pending invocation は他の pending invocation の完了の待ちを必要としない。
Theorem 3.6.2.
inv(m) を total method の invocation とする。
<x inv P> が linearizable history H の pending invocation の場合、
H · <x res P> が linearizable である response <x res P> が存在する。
Proof:
S を H の任意の linearization とする。
S が <x inv P> のレスポンス <x res P> を含む時、S は H · <x res P> の linearization なので OK。
そうでない場合、S は linearization が pending invocations を含まない定義から <x inv P> を含まない。
メソッドは total なので、legal である S' = S · <x inv P> · <x res P> を満たす <x res P> が存在する。
S' は H · <x res P> の linearization なので、 H の linearization。
linearizability のみでは total method の pending invocation を持つスレッドをブロックしないことを意味。
もちろん、linearizability の実装次第では、ブロッキング（デッドロックも）は起こりえる。
この定理は、linearizability が concurrency と real-time が重要なシステムにとって役立つことを言っている。
ノンブロッキング特性は、意図したブロッキングを妨げるものではない。
例えば、空の FIFO に deq した時に enq を待ちたい場合。 deq の spec には partial とし、空のキューの状態は定義しない。 この場合の自然な解釈としては、メソッドで定義された状態になるまで待つこと。
Linearizability のノンブロッキング特性は、どんな pending invocation も適切なレスポンスを返すことを示しているが、そのレスポンスの計算の仕方については言及していない。
Fig 3.1. のロックを使った空のキューに、A が enq(x) の途中で停止した場合、B の deq() はどうなるか？
ノンブロッキングの場合は、x か exception を返すことを保証するはずだが、B はロックがとれないので A を待ち続ける。
これはブロッキングであり、一つのスレッドの予期しない遅延が他のスレッドの progress を妨げる動作である。
マルチプロセッサでは予期しない遅延はよく起こる。コンピュータや OS によって値は異なるが
- キャッシュミス: 百サイクル
- ページフォルト: 数百万サイクル
- OSのプリエンプション（コンテキストスイッチ）: 数億サイクル
定義
- メソッドが wait-free : メソッド呼び出しが有限のステップで終了する
- bounded wait-free : ステップの数に制限（スレッド数に依存）がある（ex. Chapter 2 の doorway）
- population-oblivious : アクティブスレッド数にパフォーマンスが依存しない wait-free のメソッド
- オブジェクトが wait-free : オブジェクトの全メソッドが wait-free
- クラスが wait-free : クラスの全インスタンスが wait-gree
wait-free であることは、ノンブロッキングの一例。
Fig. 3.3 のロック使わないキューは wait-free（説明略）。
wait-free は止まらないので魅力的だけど、効率が悪いので、ノンブロッキングより弱くて良い場面もある。
lock-free は、基本 wait-free だが、一部 starve するスレッドもある特性。
wait-free は lock-free だが、逆は成り立たない。
実際問題 starvation が滅多に起こらないケースは多いので、遅い wait-free より、速い lock-free が魅力的。
wait-free と lock-free のノンブッキング特性は、 システムがスレッドをどうスケジュールしても処理が進むことを保証する。
Chapter 2 のブロッキングでの deadlock-free と starvation-free は プラットフォームが保証する場合のみ保証され、原則的に、全てのスレッドが クリティカルセクションから離れることを OS が保証する時の役立つ。
メソッドがロックベースの同期に依存しているクラスは、 せいぜい dependent progress properties しか保証できない。
ロックベースは避けるべき？ 必ずしもそうではない。
クリティカルセクションの真ん中でのプリエンプションはまれなので dependent blocking progress conditions はノンブロッキングとは区別できない。 プリエンプションが頻繁に起こったり、遅延のコストが高い場合はノンブロッキングを考えるのが懸命。
obstruction-free（妨害しない）の定義。
Definition 3.7.1.
独立で実行しているどんなポイントからも有限のステップで終了する場合のメソッドを obstruction-free と言う。
obstruction-free は、一部のスレッドの急な遅延に対して、全てのスレッドがブロックされるわけではい。
lock-free は obstruction-free だが、逆は違う。
obstruction-free アルゴリズムはロックの利用を排除するが、複数のスレッドが並行して進行することを保証しない。
多くの OS が公平を無視して採用しているアプローチで、一つのスレッドだけ不公平にスケジュールされる。
実際は問題なく、obstruction-free は同じ共有オブジェクトのメソッドを呼んでいる、衝突したスレッドのみの中断を必要とする。
obstruction-free アルゴリズムを利用する簡単な方法は back-off メカニズムを導入すること。
- 衝突を検知したスレッドは、前のスレッドが終了する時間を与えるために停止する 詳しくは Chapter 7 で。
並行オブジェクトの実装のための progress 条件の選択は、アプリの要件とプラットフォームの特徴に依存する。
完全な wait-free と lock-free progress は良い理論的な特性があり、どんなプラットフォームでも働き、
ミュージックやテレビゲームなどのようなインタラクティブアプリに役立つ real-time 保証を提供してくれる。
obstruction-free, deadlock-free, starvation-free はプラットフォームに依存するが、シンプルで効率的な実装の余地がある。
Java は共有オブジェクトの読み書きの linearizability、sequential consistency を保証しない。
理由は、コンパイラの最適化に合わないから（いくつか例）。
Java のメモリモデルは relaxed model
- プログラムの sequentially consistent 実行が一定のルールに従う場合、 relaxed model での実行は sequentially consistent (？？)
Fig. 3.10 は有名なシングルトンのダブルロックだが間違い。
Line 5 で初期化してアサインしているけど、 Java のメモリモデルではこのステップは out-of-order なので、 初期化の途中の状態でアサインされて、他のプログラムに見えることがある。 各スレッドが共有メモリのオブジェクトのワーキングメモリを持っていて フィールドの読み書きはキャッシュされて伝搬しない。
一般的な synchronization は原子性や排他制御を意味するが、 Java ではワーキングメモリと共有メモリの一致させることを意味する。 Synchronization イベントは linearizable。
synchronized で排他制御できる。
field への全てのアクセスが同じロックで守られていたら、フィールドへの読み書きは linearizable。
ロックを取得、解放したタイミングでメモリが同期される。
Volatile フィールドも linearizable。
ロックみたいにフィールドへの読み書きが共有メモリと同期される。
x++ のような複数の読み書き処理は atomic ではないので java.util.concurrent.atomic など使って排他制御する。
final フィールドは、コンストラクタがルールに従えば synchronization なしで正しく初期化、公開される。
this 参照はコンストラクタが完了する前に渡してはいけない。
Fig. 3.12 は、コンストラクタで this を EventSource に渡しているよくない例。
まとめると、フィールドへの読み書きは volatile にするか、 読み書きへのアクセスを一つのロックで排他制御すると linearizable。
どの progress 条件がアプリに適切？
アプリの要件とプラットフォームしだい。
でも、同じオブジェクトでもメソッドが違うと progress が異なることも。
どの correctness 条件がアプリに適切？ アプリの要件次第。
Italy in the 1920s. According to Mussolini
"the ideal citizen is intelligent, honest, and Fascist. Unfortunately, no one is perfect"
linearizable ハードウェア、linearizable データ構造で良いパフォーマンスは理想だが難しい。
にも関わらず、この本の残りの部分で、理想への多くのチャレンジを示しています。