『Linearizability: A Correctness Condition for Concurrent Objects』

定義 (形式的なの書いてないけど)

history

処理の開始 (invocation) と終了 (response) の列

プロセスAがオブジェクトxに対して処理Opを開始

プロセスAのオブジェクトxに対する処理が結果Termで終了

処理は終わってなくてもいい

対応する開始と終了の間に他のイベント (開始、終了) が間に挟まっていてもいい

同じプロセスのイベントが挟まっていいかどうかは不明 (Aの開始、Aの開始、みたいに)

↑ 挟まってよさそう。history はただの inv と res のイベント列で、どんな列かは規定していない

同じプロセスのイベントが挟まったらだめなやつは well-formed な history と呼ぶ (後述)

history H の subhistory

H の部分列

complete(H)

H のなかの、対応する response がない invocation を取り除いた history

history H が sequential

最初のイベントが invocation である

invocation の直後に対応する response がくる

ただし最後は invocation で終わってもいい

history H が concurrent

H は sequential ではない

process subhistory H | P

H からプロセス P のイベントだけを取り出した history

object subhistory H | x

H からオブジェクト x のイベントだけを取り出した history

二つの history H, H' が equivalent

forall P, H | P = H' | P

history H が well-formed

forall P, H | P が sequential

以降、この論文に出てくる全ての history は well-formed だと仮定

object subhistory については規定しない

operation

invocation と、対応する response のペア

operation e に対して、inv(e) と res(e)

e0 が e1 の中にある (e0 lies within e1)

inv(e1), inv(e0), ..., res(e0), res(e1) のように、開始と終了のなかに収まっている

inv(e1) と inv(e0) が隣り合っていなければいけないかどうかは不明

history の集合 S が prefix-closed

S 中の全ての history H について、H の全ての prefix が S に含まれる

single-object history

一つのオブジェクトに対するイベントしかないような history

あるオブジェクトの sequential specification

そのオブジェクトの single-object で sequential な history の prefix-closed な集合

sequential history H が legal

すべての object x に対して、object subhistory H | x が x の sequential specification の要素

value

history 終了時の object の state のこと

事前条件と事後条件を記述するのに使う

sequential specification を作るため

operation が total

事前条件がない

total function 的な意味での total

operation が partial

事前条件がある

partial function 的な意味での partial