Linearizability from 並シス本
Part 1, Correctness
Chapter 2, Linearizability
avashe.iconひたすら必要な定義を重ねる章、頑張って耐えたい
2.1. Introduction
線型可能性 (Linearizability) はshared object implmentationsにおける正確さ(Correctness)の指標
FIFO queueを用いて説明される
$ Enq(a): キューに$ aを挿入
$ Deq(): キューの先頭から要素を取り出す、空ならば$ nilを返す
FIFO queueは直列であるならば操作ごとにステートと入出力が定まる
複数のプロセスから操作しても何らかの直列な操作列のように振る舞うとき、それを線型的であると呼ぶ
Serializabilityの議論の上では実時間中のプロットやLinearization Pointのような概念は存在せず、ただ「複数の操作の間のその並び替えは合法か否か?」を読み書きの依存関係に絞って議論する。
時間軸のどこにプロットされるかを議論するのがLinearizability
2.2 The Players
(定義) 計算の実行者をプレイヤーと定義する
プレイヤーは実行とその履歴に関わる
プレイヤーは大別してプロセスとオブジェクトの2つに別れる
プロセスは有限な$ n個の集合であり、$ p_1,...,p_nと表記する
プロセスはローカル変数にアクセスできることに加え、共有オブジェクト(shared objects)を操作できる
単にこれをオブジェクトと呼ぶ
オブジェクトは同期的に操作する必要がある
(定義) プロセス$ p_iによるオブジェクト$ Xに対する命令 $ opを2つのイベントでモデル化する
命令を呼び出すイベントを$ inv \lbrack X.op \enspace \mathrm{ by } \enspace p_i \rbrack で示す
命令を終了するイベントを$ resp \lbrack X.op.res \enspace \mathrm{ by } \enspace p_i \rbrack で示す
これは前者のinvに対応する
あらゆるプロセスとオブジェクトの関係は可視的なイベントで表現される
呼び出し、命令の応答などがそれに当たる
(定義) それら可視的イベントを履歴(history)と呼ぶ
履歴は平行システムの上で起きる観測可能なイベント列で表現される
(仮定) 各プロセスは独立しており直列であることを仮定する
(定義) 命令の応答が帰ってこない限り次の命令が呼び出せない性質を直列(Sequential)であると呼ぶ
一つの命令は一度に1つのオブジェクトしか操作できない
本書はこの状況における並行性について考察する
(定義) オブジェクトは同一性(identity)を有する
avashe.iconidentityで調べるとこう出てくるけど、私は個体識別性の方がわかりやすい
(定義) オブジェクトは型を有する
複数のオブジェクトは同一の型になりうる
(仮定) 本書では簡便化のため1つのオブジェクトにつき1つの型に限定する
現実には継承やサブタイピングによって複数の型を持ちうる
(定義) オブジェクトの型は3つの要素で定義する
1. オブジェクトが取りうる状態の集合
2. 1.の状態をオブジェクトを通じて操作する命令の集合
命令はあくまでオブジェクトへ作用し、結果として状態が移りうる
3. Sequential specification
a sequential specification that describes, for each operation of the type and every state, the effect this operation produces when it is applied to the object in that state (in the absence of concurrency).
avashe.icon伝わるけどもはや数式書けって感じの文章、誰か良い感じに訳して
avashe.icon既存の訳語はわからん
オブジェクトを固定し、あらゆる状態と命令の組合わせ全体を見たときに言える性質を指している
後に全域(total)という用語がでてくるので、分かりにくければpartial functionとかtotal functionみたいな性質のことを考えると思考の一助になりそうだけど、命令は関数ではないので注意
We say that the type exports its operations.
型が決まれば命令とその性質が定まることを「型が命令をエクスポートする」と呼ぶ
原義に合わせて「運び出す」とか良さそう
日本語だと生成されたり、導かれたり、要請されるやつ
(仮定) 本書ではオブジェクトの型のSequential specificationは 全域(total)であると仮定する
avashe.icon例外とか強制的にクラッシュする例も考えられるけど、理論を構成する上では一旦置いておきますという意味かと
$ Deq()の定義のように、状態がemptyでもnilを出すなどで壊れないように解釈する
あらゆる状態のオブジェクトについて、ある命令を適用した結果、その命令に固有の応答と状態が帰ってくるならば、そのオブジェクトの型は決定性を有する
型が決定性を有するならば、その型の全ての命令が決定性を有する
命令に対して結果(応答と状態)が複数ありうる型は非決定性を有する
特に結果の数が有限である型は有限非決定性を有する
(仮定) 本書における非決定性の命令は全て有限であると仮定する
(定義) ある型やオブジェクトにおける、命令呼び出しとその応答が交互に続く列の集合もSequential specificationと定義する
言葉の濫用っぽいがすまんな(著者
avashe.icon私の解釈で補足すると
例えば有限非決定ミーリマシンを考え、それが受理する言語の集合を考えてみよう 但し言語だと状態の列とかになっちゃうので、記録する要素を「選択した遷移関数」、「遷移関数に渡された入力」、「遷移時の出力」の直積とすればよい
舞台となるミーリマシンの上でこれら要素に注目したとき、生じうる列の集合がその型のSequential specificationとなる
全域かつ有限非決定性を仮定しているのでこの集合が成り立つ
例1: (多分状態が)非有界なFIFOキュー
このオブジェクトの型からは$ Enq(a)と$ Deq()の組み合わせからなるSequential specificationが生成される
古典的なproducer/consumer 同期問題に該当する
(定義) 例2: Read/Write オブジェクト(レジスタ)
共有されたリソース(メモリやディスク)に対し、読み書きするようなモデル
しばしば言われる通り本書でもこれらをレジスタと呼ぶ
古典的なreader/writer同期問題に該当する
レジスタの型では以下の命令を考えられる
入力を伴わない$ read() 命令
応答として最後の$ write(v)命令の入力$ vを返す
ある入力$ vを伴う$ write(v)命令
応答として命令の完了を示す$ okを返す
Sequential specificationとして$ read()と$ write(v)からなる列の集合が生成される
レジスタの実装は次の章で議論する
複数のプロセスとオブジェクトによる相互作用をイベントによる全順序集合$ Hでモデル化する
(定義) イベントを要素とする全順序集合$ Hを履歴(history)あるいはトレース(trace)と呼ぶ
同時に起こるイベント群の順序は任意となる
$ H間の全順序関係を$ <_Hで示す
イベントは以下の要素からなる
オブジェクト名
プロセス名
命令名
その命令に用いられた入出力のパラメータ
(定義)$ Hの内、$ p_iに注目した履歴をローカル(local)な履歴と呼び、$ H|p_iで表す
$ H|p_iis a projection of $ H on process $ p_i
$ p_iが関与した履歴のサブシーケンスになる
(定義) 二つの履歴$ H, H'が等しいことを以下のように定義する
$ H = H' := \forall i.\enspace H|p_i = H|p_i
(定義) 全ての$ p_iにおける履歴$ H|p_iが直列であるならば、$ Hは well-formed である
命令の完全性について
(定義) 履歴がある命令の呼び出しとその応答、両方のイベントを含んでいるならば、その命令は履歴内において完全(complete)であると呼ぶ
(定義) 履歴に命令の呼びだしがあり、対応する応答が無い場合、その命令は履歴内において待機している(pending)と呼ぶ
履歴の完全性について
(定義) 待機している命令が無い履歴は完全である
(定義) 待機している命令がある履歴は不完全(incomplete)である
システムが不整合な状態でクラッシュした状況は不完全な履歴としてモデル化できる
直列であることからプロセスは待機している命令を最大1つしか持てないことに注意せよ
履歴$ Hはその構造上、命令に関する非反射-反順序関係(irreflexive partial order)を誘導(induce)する
avashe.icon$ H上に定義される反順序関係において、反射律を非反射律に置き換えたものを指す
数学のwebページは数学の知識を仮定してくるために、C++の仕様として解説してくれるページの方が丁寧になってる現象ウケますね
avashe.icon お前前後で全順序集合な履歴とか言ってる癖にどっちやねん
後述の「重複(並行)する命令」が無ければ全順序集合になる
命令が重複する場合、同時に起こる命令があるため順序が付けられない要素が生じ、非反射-反順序関係に「なりうる」(ここが"induce"要素)
(定義) 履歴$ Hにおいて、命令$ opが命令$ op'に先立つ(precedes)ことを$ (op \rightarrow_H op')で示し、
$ (op \rightarrow_H op') := (resp \lbrack op \rbrack <_H inv \lbrack op' \rbrack )
と定義する
where
$ op = X.op1() \enspace \mathrm{by} \enspace p_i
$ op' = Y.op2() \enspace \mathrm{by} \enspace p_j
(定義) $ \neg(op \rightarrow_H op')かつ $ \neg(op' \rightarrow_H op)であるとき、命令$ opと$ op'は重複する(overlap)、または並行する(concurrent)と呼ぶ
定義からして重複する命令は常に二つ以上である
(定義) 直列な履歴(Sequential history)を以下のように定義する
1. 最初のイベントが呼び出しである
2. (最後のイベントを除く)各呼び出しイベントの直後に、対応する応答イベントが続く
3. (最後のイベントを除く)各応答イベントの直後に、何らかの呼び出しイベントが続く
「最後のイベントを除く」(except possibly the last)のは不完全な履歴との定義の兼ね合い
直列でない履歴は並行な(concurrent)履歴である
直列な履歴では命令が重複しえない事から、$ Hが直列な履歴であるなら$ \rightarrow_Hは全順序である
厳密に言えば、あるオブジェクトの型のSequential specificationとは、そのオブジェクトから生成できる直列な履歴の集合のことである
(定義) 直列な履歴$ Hが適法(legal)であるとは、$ Hに含まれる各オブジェクト$ Xについて、$ H|Xが$ XのSequential specificationに含まれることである
ここから述べる線形可能な履歴とはここまでに述べたSequential specificationと関係があるため、ここで二つの間を取り持つ定義を行っておく
2.3. Linearizability