Linearizability
線形化可能性と訳される概念．
要旨
SerializabilityだけをトランザクションのCorrectness Conditionにすると実際のアプリにとっては不十分であることがある． Serializabilityとは別に，新たなCorrectness Conditionとして Linearizabilityというものを定義し，
この両者をともに満たすときスケジュールがStrict Serializableである，とする．
以後のトランザクション手法は$ Linearlzable \wedge Serializable な手法にすると良いでしょう，という論文．
定義
Linearizabilityの定義
「単一のオブジェクトに対する単一の操作が，何らかの順序(例えば，real-time order)を反映してスケジュールされること」
$ w_0(x_0) w_1(x_1)として，real time orderで$ w_0(x_0) \leq w_1(x_1)ならばよし
より詳細な定義は論文にある
Serializabilityの定義
「複数のオブジェクトに対する複数の操作が，単一のオブジェクトに対する単一の操作として扱えること」
i.e., 命令の全順序集合であるスケジュール$ Sから，トランザクションの全順序 $ Mを得られること
Strict Serializability ( Serializable かつ Linearizable) の定義
"A history is serializable if it is equivalent to one in which transactions appear to execute sequentially, i.e., without interleaving. A (partial) precedence order can be defined on non-overlapping pairs of transactions in the obvious way. A history is strictly serializable if the transactions’ order in the sequential history is compatible with their precedence order."
つまり，$ SがSerializableであるとき得られる$ Mに対するさらなる制約がLinearizability．
説明すると，
$ trans(S)のそれぞれのpair $ T_i, T_jについて，
$ Sにおいてconcurrentならば，$ Mにおける順序は問わない
$ Sにおいてnot concurrentならば，何らかのreal time constraintに従う
Let $ S be a schedule such that there exists a version order $ \ll such that $ MVSG(CP(S), \ll) is acyclic.
Thus, we can generate $ M, a total order of transactions by topologically-sorting of MVSG.
Linearizability is the condition of the order in $ M.
The formal definition of linearizability for a given schedule $ S and a total order of transactions $ M is following:
$ \forall p_i \forall q_j(((p_i \in op(T_i) \land q_j \in op(T_j)) \land p_i <_S q_j)) \Rightarrow T_i <_M T_j\ where <_M \in M, <_S \in S
ここでは「何らかのreal time constraint」を「スケジュール$ Sの命令順序」と仮定しているのに注意．
言い換えると．「何らかのreal time constraint」をどう定義するかによってStrict Serliazabilityの定義は変わる
たとえば分散システムならスケジュールされた順序と実時間の対応が簡単にとれるわけではないので，定義は変わる
以上．
以下は勉強していたときのメモ．
二つの条件からなる．
1. 一つのオブジェクトに対する単一の操作を命令列として，一本の線にプロットできること
つまり命令を実行した瞬間を一点に定められること
2. 命令を実行した際のReal Time orderに準じた順序であること
こっちが本命．
1. を拡張して，複数のオブジェクトへの複数の命令列を，linearizableにするということを考える
まずSerializableにするだけで，複数のオブジェクトへの複数の操作を，一つのオブジェクトに対する単一の操作として，一点に定めることができる． Serializabileであれば，命令列を，「システムに対するトランザクション処理の全順序」に還元できる
$ H = w_1(x)r_2(x)w_3(y)r_4(y)...のようなHistoryも，$ T1 \to T2 \to T3 \to T4といったSerialization Orderに還元できる
加えて，2. の Realtime orderに準じる，ということを実現する．
Serializableであることに加えて，「Commit OrderとSerialization Orderを一致させる」ことが求められる．
つまり $ Serialziable \subset Linearizableである
Concurrency controlの手法によって異なるが，どの手法も必ずSerialization Pointがある．
このSerialization Pointの順序が，Real Time Orderと前後するのはSerializableでは可．
これをRealtime orderと一致させるということ．
ではトランザクションのReal time orderとは何か?
複数の命令が実行されているのだからbegin-endの間が実行期間である．これは一点に定められない
このbegin-endがinterleaveしていない場合real time orderが明にあるということになる
interleaveしているものはserializableの範疇で自由
not linearizableな例
$ H1 = w_1(x_1) c_1\ r_2(x_0) c_2
Serializableではある．
論文を読んだ
よりformalな記述があった
Formally, an execution of a concurrent system is modeled by a $ history, which is a finite sequence of operation $ invocation and $ responseevents.
...
A response $ matches an invocation if their object names agree and their process names agree.
invocationとresponseは，トランザクションでいうとこのbegin/commitにあたる．
If $ His a history, $ complete(H) is the maximal subsequence of $ Hconsisting only of invocations and matching responses.
A history $ H is $ sequential if:
(1) The first event of H is an invocation.
(2) Each invocation, except possibly the last, is immediately followed by a matching responce.
Each response is immediately followed by a matching invocation.
A history that is not sequnetial is $ concurrent.
いわゆるserialと同義...と思うが(2)がよくわからない．
Each response is immediately followed by a matching invocation.
ってどういうことだろう？responseが先に来ることがあるのか