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の最初のイベントがinvocationである。
各invocationの直後のイベントはmatchするresponseである。ただし、最後のinvocationにmatchするresponseがなければ、そのinvocationの直後のイベントは問わない。

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は線形化可能である。

complete(H’)と等価なlegal sequential history Sが存在する。
\(<_H\subseteq <_S\)

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