Linearizability: A Correctness Condition for Concurrent Objects

July 17, 2021

オブジェクトを読み書きする並行プロセスの実行系列があるとき、操作がアトミックであるように観測でき、かつ、プロセスの実行を仮に直列化したときと同じ実行結果をえられる条件を示し、これを線形化可能性と呼んだ。 線形化可能性は、直列化可能性と同様に安全性の条件だが、直列化可能性にはないローカル性がある。 つまり、各オブジェクトが線形化可能かつそのとき限り、システム全体が線形化可能になる。 また、ローカル性だけでなく、ノンブロッキング性もあり、受信したリクエストの操作を保留しているオブジェクトは別オブジェクトの保留した操作の完了を待たずに自分の操作を実行できる。 ただし、そのためには、オブジェクトの任意の状態における操作の振る舞いが定義されていなければならない。

線形化可能性で発生しないことを保証できる実行系列を例示する。 下図の2つの実行系列は、並行プロセスA, B, Cがあり、オブジェクトに0か1を書き込み(W), 読み込み(R)をする。 直線は、操作の呼び出しから応答までの期間を表す。 (a)は、Aが1を読み取ったので、Bは、Aの書き込み後、Aの読み取り前に1を書き込んだという順序に整理できる。 一方、(b)は、R(1) AをみるとW(1) Bが先行するように解釈できるが、W(0) CとR(1) とをみると、その中間にあるように解釈しなければならない。 線形化可能性は、このような直列化された実行系列ではみなれない事態が起きない条件を提供する。 fig2

線形化可能性の定義に必要な用語を定義する。 システム全体の実行をhistoryとよぶ。 historyは、操作のinvocationとresponseの2種類のイベントの有限な系列からなる。 invocationを、オブジェクト\(x\), 操作名と引数\(\textit{op}(\textit{args*})\), プロセスAの組で\(<x,\textit{op}(\textit{args}^*)A>\)と書く。 responseを、終了条件を\(\textit{term}\)、結果を\(res*\)として、\(<x, \textit{term}(\textit{res*})A)>\)と書く。 responseに、オブジェクトとプロセスが同じinvocationがあるとき、responseはそのinvocationとmatchする。 Hをhistoryとして、complete(H)は、invocationとmatchするresponseからなるHの最大の部分系列をあらわす。 このとき以下の2つが成り立てば、Hはsequentialであるといい、成り立たなければconcurrentである。

H中の、プロセスPやオブジェクトxだけについての系列を、\(H\mid P\), \(H\mid x\)と書く。 あるH, H’があり、全プロセスPについて\(H\mid P = H'\mid P\)であれば、HとH’は等価である。 また、各Pについて\(H\mid P\)がsequentialであれば、Hはwell-formedである。

Historyの集合Sがあり、HがSの要素であるときHのprefixもSの要素であれば、Sはprefix-closedであるという。 あるオブジェクトのsequential historyだけからなるprefix-closed集合をオブジェクトのsequential specificationという。 各\(H\mid x\)がsequential specificationの要素であるとき、Hはsequentialかつlegalである。

\(e\)をinvocationとresponseのペアとして、Hの中で\(e_0\)のresponseが\(e_1\)のinvocationに先行する関係を、\(e_0 <_H e_1\)と書く。 \(<_H\)は反射律の成立しない半順序関係である。 Hに0以上のresponseを追加したhistoryをH’とすると、次の2つが成立するとき、Hは線形化可能である。

論文をこちらからダウンロードできます。 論文から文中の画像を引用しました。