日本ソフトウェア科学会第 37 回大会 (2020 年度) 講演論文集型システムを用いたロックフリースタックの検証
佐藤 駿太朗

住井 英二郎

ロックフリー性とは，デッドロックやライブロックが起きないという，並行システムにおいて重要な性質である．ロッ
クフリー性を検証する方法として，自然言語による非形式的な証明や，紙の上ないし定理証明支援器上の形式的な証
明の他に，軽量な形式手法とされる型システムに基づく手法があり，その実装として TyPiCal [Kobayashi] がある．
本研究では，TyPiCal を再帰型を持つセル構造で拡張して，Treiber [1986] のロックフリースタックを表現す
る．TyPiCal だけでは再帰的なプロセスのライブロックフリー性を検証できないため，TyPiCal でデッドロック
フリー性を検証し，Kobayashi と Sangiorgi [2008] のハイブリッド型システムと組み合わせてロックフリー性を証明する．その際，TyPiCal では再帰型を持つデータ構造に対する操作はプリミティブ関数として拡張する必要がある．それにともない新たに発生する制約の生成と解消を実装する．加えて，無限回のスタック操作を並行に行う場
合，ロックフリー性の定義の違いから生じる問題について考察する．

も研究されている．ノンブロッキング同期は，あるス

1 序論

レッドの遅延や失敗が，他のスレッドの実行を妨害し

1. 1 背景

ないという性質（ノンブロッキング性）を満たす同期

並行プログラミングでは，複数のスレッドから共有である [5, chapter 3]．ノンブロッキング性を満たし資源にアクセスする際，競合状態を避けるために同期つつ共有データ構造を操作するアルゴリズムをノン制御を行う必要がある．同期にはブロッキング同期とブロッキングアルゴリズムと言い，各操作について保ノンブロッキング同期がある [5, chapter 1]．ブロッ

証される性質の弱い順にオブストラクションフリー，

キング同期とは，一つのスレッドの処理を進めるため

ロックフリー，ウェイトフリーの 3 種類に分類できに，他のスレッドを遅延させる同期である [5, chapter

る [5, chapter 3]．

1]．一般に排他制御を用いた同期はこれに含まれる．

• オブストラクションフリー

明示的にロックを用いたブロッキング同期は，ロックある操作がオブストラクションフリーであるとの取得・解放のタイミングや，複数のスレッドのスケは，競合するスレッドをすべて停止させた状態

ジューリングによってはデッドロックやライブロック

で，任意の一つのスレッドのみを実行した場合を起こす．ここでデッドロックとは，完了してほしいに，有限ステップで完了するということである．

処理が完了せずに，すべてのスレッドの進行が停止す• ロックフリー

ることをいう．またライブロックとは，少なくとも一ある操作がロックフリーであるとは， 複数のス

つのスレッドが進行し続けているにも関わらず，完了

レッドがいかなるスケジューリングをされても，してほしい処理が完了しないことをいう．

それらで実行されているメソッドのうち少なくと一方，排他制御を用いない，ノンブロッキング同期も一つが， 有限ステップで完了するということである．

Shuntaro Sato, Eijiro Sumii, 東 北 大 学 大 学 院 情 報 科
学研究科, Graduate School of Infomation Sciences,
Tohoku University.

• ウェイトフリー
ある操作がウェイトフリーであるとは，複数のス

レッドがいかなるスケジューリングをされても，システムの一部の遷移を列挙して検証を試み，ロック

それらで実行されているメソッドのそれぞれが，フリー性の定義の違いにより生じる問題点について

有限ステップで完了するということである．

考察する．

ウェイトフリー性は一番望ましい性質であるが，パフォーマンスに劣る場合がある [5, chapter 3]．また，

2 準備

オブストラクションフリー性はライブロックが起きな

2. 1 Treiber のロックフリースタック

いことを保証しない．そのため，この 3 つの性質のTreiber のロックフリースタック [18] は，図 1 の擬

うち保証する性質やパフォーマンスの観点からロック

似コードで表せる．スタックは連結リストとして実装

フリー性が望ましいと考えられる [5, chapter 3]．

され，Node 構造体はリストのセルを表している．グ
ローバル変数 S の値はスタックの先頭を指すポイン

1. 2 本研究の目的と貢献

タであり，初期値として空のスタックを表す NULL が現在まで様々なロックフリーアルゴリズム [4, 13,

代入されている．

14, 18] やロックフリー性を形式的 (formal) に保証すpush 関数は，引数 v の値をスタックの先頭に追加る方法 [3, 6, 7, 9, 12, 19] が研究されてきた．既存研究する関数である．この関数ではまず，新しいセル x をにおいて，ロックフリー性を証明する方法として，自作り，v を格納する．次に，スタックの先頭を指すポ然言語による非形式的な証明や，紙の上 [3, 6] ないしインタを変数 S から読み出し，変数 t に格納する．14

定理証明支援器上の形式的な証明 [7, 19] がある．ま行目から 20 行目までは CAS (compare-and-swap)

た上記の方法以外にも，軽量な形式手法とされる型シ命令を表す atomic ブロックであり [6]，変数 S からステムに基づく手法 [9, 12] がある．定理証明支援器

再び読み出した値を変数 s に格納し，t と s の値が等（のみ）を用いる方法や，可能な遷移をすべて具体的

しいかどうか確認する．等しい場合，x の値を S に書に列挙する方法に比べ，型システムを用いる方法は，

き込み，処理を終了する．等しくない場合，ループの特に型推論により型注釈を省略できる場合，プログラ先頭である 12 行目に戻り，上の処理をやり直す．

マの負担を軽減することができると期待される．

pop 関数は，スタックの先頭要素を取り出す関数で本研究の目的は，Kobayashi と Sangiorgi のハイ

ある．スタックが空である場合，デフォルト値としてブリッド型システム [12] と Kobayashi の静的解析器

EMPTY を返す．pop は push と同じように，最初に変TyPiCal [8] を用いて，Treiber のロックフリース

数 S から読み出した値を t に格納する．そして，次タック [18] のロックフリー性を証明することである．

のセルを指すポインタを変数 x に格納する．33 行目

ハイブリッド型システムを用いてロックフリー性を検から 39 行目までは push 関数と同様に，変数 S から証するためには，「ロバストな」（すなわち，外部と通再び読み出した値が t の値と等しければ x の値を S信した際の）停止性・デッドロックフリー性・合流性をに書き込み，そうでなければループの先頭に戻る．

保証すれば十分である [12, section 3 および theorem

push 関数や pop 関数がロックフリーである直観的4.2]．そこでまずロバストなデッドロックフリー性を理由は以下である．push や pop の成否は，CAS 命令

保証するために，TyPiCal を用いて，ロックフリーの成否に対応し，CAS 命令が成功した場合は while

スタックのデッドロックフリー性を検証することにしループが終了し，操作が完了する．逆に CAS 命令がた．具体的には，再帰型を持つ連結リスト構造を用い失敗した場合は，スタックが変更されている，すなわてロックフリースタックを表現し，TyPiCal で検証

ち他のスレッドの push や pop の処理が成功したことを試みた．その際，TyPiCal では再帰型を持つデーを意味する．よって，少なくとも一つの push またはタ構造に対する操作はプリミティブ関数として定義すpop 操作は完了する．以上はどのようなスケジューリる必要があり，それにともない新たに発生した制約のングの下でも成り立つ．したがって，このスタックの生成と解消を実装した．ロバストな停止性や合流性は

実装はロックフリーであることがわかる．

struct Node {2
int data;
3
Node *next;
4 };1

TyPiCal [8] の対象言語である π 計算について説明する．π 計算とは，並行計算のモデルの一つである [15, 16]．本論文では TyPiCal の実装 [8]，ハイブ
リッド型システム [12]，デッドロックフリー性を保証

56

2. 2 TyPiCal の対象言語：π 計算

Node *S = NULL;

7する型システム [10] のそれぞれの対象言語を合わせたような π 計算を考える．

void push(int v) {9
Node *x = new Node();10
x->data = v;
11while (true) {12
Node *t = S;
13
x->next = t;14
atomic { // CAS(&S, t, x)15
Node *s = S;16
if (s == t) {17
S = x;
18
break;
19
}
}
20
21
}
22 }
8

23

int pop() {25
int ret = 0;26while (true) {27
Node *t = S;28
if (t == NULL) {29
return EMPTY;
30} else {31
Node *x = t->next;32
ret = t->data;33
atomic { // CAS(&S, t, x)34
Node *s = S;35
if (t == s) {36
S = x;
37
return ret;
38
}
39
}
40
}
41
}
42 }
24

π 計算では並行システムはプロセスとして表され，プロセスの集合は図 2. 2 のように定義される．ここでメタ変数 a はチャンネル，x や y は変数を表す．メタ
変数 v や w はチャンネルや変数，定数を含め，値を表す．プロセス 0 は何もしないプロセスを表す．プロセ
ス v!χ w. P はチャンネル v（値 v が変数 x の場合は，その変数 x に束縛されたチャンネル．以下同様）に

w を送信した後，P を実行する．プロセス v?χ y. Pはチャンネル v から受信した値を y に束縛した後，Pを実行する．アノテーション χ は ◦ か • であり，アノ
テーションがついている送受信が成功してほしい（◦）
か，そうでないか（•）というプログラマの意図を表す．アノテーション χ が ◦ であるとき，プレフィック
ス v!χ w ないし v?χ y がマークつき (marked) であるという．プロセス (P | Q) は P と Q を並列に実行する．プロセス ∗P は無限個の P の並列実行（複製）を表す．プロセス (νa)P は P において a がフレッシュであることを表す．プロセス if v then P else Q はv が true のとき P ，false のとき Q を実行する．プ
ロセス let x = e in P は，式 e を評価した値を x に束縛した後，P を実行する．本論文では [8, 10] と同様に，let を用いて式の評価を明示し，送受信 !, ? の対象および if の条件部分は値（変数の場合を含む）に限定している．ただし，実際にプロセスの例を書く
際は，しばしば let を展開した略記を用いる．
η

ラベルつき遷移関係 P −→ Q は，プロセス P が，
ラベル η が表す動作を行なってプロセス Q に遷移することを表す．例えば，プロセス P がそのプロセス内部で送受信を行い，プロセス Q に遷移するとき，ラベτル τ を用いて，P −→ Q と書く．ラベルつき遷移関ττ∗係 −→ の反射的推移的閉包を −→ と書く．また，プη

図1

ロックフリースタックの擬似コード

τ∗

ロセス P に関して，P −→ Q や P −→ Q となるよητ∗

うな Q が存在するとき，それぞれ P −→ や P −→

::=

0

(inaction)|χv! w. P

(output)|v?χ y. P(input)|(P | Q)(parallel composition)|∗P(replication)

|

(νa)P

(restriction)|

if v then P else Q(conditional)|

let x = e in P

(evaluation)e (expressions)::=true | false | x | a | ⟨e1 , e2 ⟩ | proj 1 (e) | proj 2 (e)v, w (values)::=

true | false | x | a | ⟨v1 , v2 ⟩P (processes)

図2

TyPiCal の対象言語：π 計算と書く．ラベルつき遷移関係の定義は [10–12] などを参照されたい．

ここで遷移列が full であるとは，遷移列が無限であるか，これ以上遷移できないプロセスで終わることをいう．また，遷移列が strongly fair であるとは，

2. 3 ロックフリー性の定義

直観的には，同一のトップレベルの入出力プレフィッ

プレフィックスがトップレベルにあるとは，その送受クスの組が無限回出現しないことをいう [12, p. 9]．

信が他の送受信や複製の下にないことをいう（複製のデッドロックフリー性と強いロックフリー性の違い

下のプレフィックスは遷移が進めば複製の外に出てくは，ライブロックの有無である．未完了の送受信がるので，議論を簡単にするために省いている）[12, p.

ある場合，デッドロックフリー性はプロセスが更に τ

8]．

遷移することのみを保証し，ロックフリー性はその特定義 1 (デッドロックフリー性 [12, Deﬁnition 2.6])定の送受信が有限回の τ 遷移で成功することを保証

プ ロ セ ス P が デッド ロック フ リ ー で あ る と は ，

する．

τ

∗

P −→ Q なるすべての Q に対して，マークつき

1. 1 節で示した [5] でのロックフリー性の定義と，プレフィックスが少なくとも一つ Q のトップレベル

本節で示した [12] でのロックフリー性の定義は異なっτにあるとき，Q −→ が成り立つことをいう．

ている．[5] の定義は，どのようなスケジューリング

ロックフリー性を定義する際，一つ一つのマークつにおいても，ある少なくとも一つの操作が完了するこきプレフィックスの成否を追跡する必要がある．プロとを意味しているが，[12] の定義は，strongly fair な

セス P 中のトップレベルのプレフィックスのアノテー

スケジューリングの下で，すべての操作がいずれ完了

ション ◦ をどれか一つだけ □ に書き換えたプロセスすることを意味している．したがって，無限個の操作の集合を，P のタグづけ (tagging) という．また，送（例えば push(1)，push(2)，. . . ）を並行に行う場合，

信と受信の少なくとも一方に □ がついているような

前者では（たとえ strongly fair なスケジューリング

τ 遷移を −−→ と書く．

の下でも）一部の操作（例えば push(奇数) のみ）し

定義 2 (強いロックフリー性 [12, Deﬁnition 2.8])

か成功しない可能性がある一方，後者では（strongly

プロセス P が強いロックフリー性を満たすとは，

fair なスケジューリングを仮定すれば）すべての操作

τ□

τ

∗

P −→ Q なるすべての Q に対して，Q のタグづけに属するそれぞれのプロセスの遷移列のうち，full かτ□

つ strongly fair であるすべての遷移列が，遷移 −−→を含んでいることをいう．

がいずれ成功する．

∆ |=RD P

Erase(∆) |=RTer P

Erase(∆) |=RConf P

nocap(∆)∆ ⊢SLT P
図3(SLT-Hyb)

ハイブリッド型システムのための型つけ規則

2. 4 デッドロックフリー性を保証する型システム

刻 t1 以前に行われている必要があるからである．

本研究が用いるデッドロックフリー性を保証する型

また，ある送受信の obligation to が他の送受信のシステム [10, 11, 17] は，π 計算の単純型システムに，

capability tc で遅延されている場合，to > tc という順

usage と obligation level，capability level を導入し序関係が生じる．例えば，プロセス x?z. y!0 | y?z ′ . x!0て拡張した型システムである．型の集合は以下のようにおいて，x の usage を ?tt01 | !tt23 （ただし前述の制に定義される．

約より t0 ≤ t3 かつ t2 ≤ t1 ），y の usage を ?tt45 | !tt67

τ (types) ::= bool | τ1 × τ2 | chan(τ, U )（ただし t4 ≤ t7 かつ t6 ≤ t5 ）とする．y!0 は x?z のチャンネル型 chan(τ, U ) は，τ 型の値を usage U にあとにあるため，t1 < t6 という制約が生じる．また，

従って送受信するチャンネルの型を表す．

x!0 が y?z ′ のあとにあるため，t5 < t2 という制約がusage とはチャンネルがどのように送受信に使われ生じる．これらの制約から，t1 = t6 = t5 = t2 = ∞るかを表した式であり，以下のような抽象構文で定義となる（ただし ∞ < ∞ は成り立つとする）．つま

される．

り，受信 x?z や y?z ′ は成功しない可能性があること

U ::= 0 | αttco . U | (U1 | U2 ) | . . .
α ::= ! | ?

がわかる．
さらに，[10] の型システムでは，usage と obligation

ここで，! は送信を表し，? は受信を表す．また，tolevel，capability level に加えて，チャンネルが作成

は obligation level，tc は capability level を表し，そされた順序を表す関係 ≺ を導入している．型環境 Γ

れぞれ自然数か ∞ である．obligation level と capa-とチャンネルの順序関係 ≺ のもとでプロセス P に型

bility level は，直観的には時刻に対応する．αttco のがつくとき，P はデッドロックフリーである．詳細

obligation level to は，時刻 to までに，その送信または [10, section 3] を参照されたい．

は受信を行わなければならないことを表す．ただし，

to = ∞ のときは，送受信を行わなくてもよいこと

2. 5 ハイブリッド型システムを表す．また，capability level tc は，その送信また強いロックフリー性を保証するハイブリッド型シス

は受信を行なったら時刻 tc までに成功することを表テム [12] は，強いロックフリー性を保証するハイブ

す．ただし，tc = ∞ のときは，成功することを保証

リッドでない（完全に静的な）型システム [9] に，図しない．

3 の型つけ規則を追加した型システムである．型環

あるプロセスがデッドロックフリーであることを保境 ∆ はプロセス P に自由出現する名前に関する仮定証するためには，各チャンネルがデッドロックしないを表す（Erase は型の中の usage を消去する）．前提

ように使われることを，以下のように usage を通し∆ |=RD P ，Erase(∆) |=RTer P ，Erase(∆) |=RConf Pて確認すればよい．

は，それぞれロバストなデッドロックフリー性，ロバ

まず，ある送信（または受信）が成功するためには，

ストな停止性，ロバストな合流性を表す．ロバストな

それ以前の時刻に，対応する受信（または送信）が行

性質（停止性，デッドロックフリー性，合流性のいずわれる必要がある．例えば，プロセス x!0 | x?y におれか）とは，大まかには，任意のプロセス Q と並列

ける x の usage !tt01 | ?tt23 では，capability level t1 のに実行しても，P がその性質を満たすことを意味す

送信 ! に対応する受信 ? の obligation level t2 は，t1

る．Q は任意のため，∆ はいかなる capability も含以下である必要がある．なぜなら直観的には，送信がまないとする（nocap(∆)）．ただし，5 節で検証する

時刻 t1 までに成功するためには，対応する受信が時

ロックフリースタックのシステム全体は自由な名前を1*makeCell?r.

2

new readData in new readNext in new writeData in new writeNext in3

let quad = makeQuadruple (readData, readNext, writeData, writeNext) in4

r!quad | new data in new next in data!0 | next!null5| *readData?r. data?v. (r!v | data!v)| *readNext?r. next?v. (r!v | next!v)| *writeData?(v2,r). data?v1. (r!0 | data!v2)| *writeNext?(v2,r). next?v1. (r!0 | next!v2)

6
7
8

図4

makeCell

含まず，型環境も空としてよい．そのような場合，ロバストな性質は通常の性質と同様である．

ンネル r を受信し，上述の 4 つのチャンネルを組と し て r に 返 信 す る サ ー バ で あ る ．†1 こ の サ ー

ここでいう合流性とは概ね以下の意味である

バ は チャン ネ ル r を 受 信 し た 後 ，ま ず readData，[12, Deﬁnition 3.8]．プ ロ セ ス P が 部 分 的 な 合 流

readNext，writeData，writeNext の 4 つのフレッ

τ,S1

η,S2

性を持つとは，P1 ←−−− P −−−→ P2 ならば常に，
η,S

τ,S

シュな チャン ネ ル を 作 成 す る ．次 に ，プ リ ミ ティ

12
η = τ ∧ S1 = S2 であるか，P1 −−−→≡
←−−−
P2 であ

ブ関数 makeQuadruple を用い，この 4 つのチャン

ることをいう．ここで，S1 ，S2 はその遷移に関わっ

ネ ル を 組 に し て ，チャン ネ ル r に 送 信 す る ．チ

たチャンネルの集合を表す [12, p. 18]．プロセス P

ャン ネ ル data と next は ，セ ル の 要 素 と ，次 のがロバストな合流性を持つとは，任意の閉じた代入 σ

セ ル を 指 す ポ イ ン タ を そ れ ぞ れ 保 持 す る チャン

η1ηkについて，σP −→ · · · −→ Q ならば常に，Q が部分ネルである．*readData?r...と*readNext?r...は，的な合流性を持つことをいう．

返 信 用 の チャン ネ ル r を 渡 さ れ た ら ，そ れ ぞ

規則 (SLT-Hyb) は，上述の仮定が成り立てば，プ

れ data ま た は next か ら 値 を 取 り 出 し て ，r に

ロセス P はロックフリーであり，P が（他の必ずし渡 す と と も に ，再 び data ま た は next に 戻 す．

も停止しないプロセスに対して）strongly fair にス*writeData?(v2,r)...と*writeNext?(v2,r)...は，ケジュールされれば，∆ に含まれる obligation を果それぞれ data または next に書き込む値と，処理がたす，ということを主張している．この規則の正し完了したことを通知するチャンネルの組を受け取る．

さ（健全性）は，直観的には以下のように理解でき

そして data または next から値を取り出し，r に通る．まず，ロバストな停止性より，プロセス P の遷知を行うとともに，data または next に新しい値 v2

移列は有限である．すると，ロバストなデッドロック

を渡す．

フリー性 [12, Deﬁnition 3.7] より，P は少なくとも

図 5 は push 関数を π 計算で表現したプロセスであ

1 回は obligation を果たせる状態になる．よって，ロる．このサーバは全体的動作としては，スタックに追

バストな合流性から，P は必ず obligation を果たす．

加する値 value と，処理が完了したことを知らせるためのチャンネル reply を受け取って，スタックに

3 ロックフリースタックの π 計算での表現

値 value を追加した後，reply に 0 を送信する．詳2. 1 節で紹介したロックフリースタックを π 計算で細としては，まず 2 行目で makeCell に送信したチャ表現するためには，まず，Node 構造体のようなセルンネルから 4 つ組 quad を受け取る．それから 5 行

をプロセスで表現する必要がある．セルを表現するプ目でセルに value を格納する．6 行目以降は図 1 のロセスには，セルが保持する値と次のセルのポインタ

擬似コードの while ループに対応する．擬似コードを読み書きするために，4 つのチャンネルを用意する．
図 4 のプロセス*makeCell?r...は返信用のチャ†1 本論文ではしばしば π 計算のプロセスを，TyPiCalの実装に近い具体文法を用いて表す．

1*push?(value, reply).

2

new ref in makeCell!ref. ref?quad.

3

let writeData = third quad in

4

let writeNext = fourth quad in5

new a in writeData!(value, a). a?l.

6

new while in while!reply| *while?r. stack?t. ( stack!t| new a in writeNext!(t, a). a?l. lock?l.
stack?s. ( stack!s| if s = tthen stack?u. ( stack!quad | lock!0 | r!0 )else ( lock!0 | while!r )))

7
8
9
10
11
12

図5

1
2
3
4
5
6
7
8
9
10
11
12
13

push

*pop?reply.
new while in while!reply| *while?r. stack?t. ( stack!t| if s = nullthen r!0
else let readData = first t in
let readNext = second t in
new a in readData!a. a?v.
new b in readNext!b. b?x.
lock?l. stack?s. ( stack!s| if s = tthen stack?u. ( stack!x | lock!0 | r!v )else ( lock!0 | while!r )))

図6

pop

における atomic ブロックはグローバルなチャンネル

して 0 を送信する．全体の流れは，push 関数の表現

lock に値を送受信することで実現し，while ループと同様である．

は再帰的なプロセスで表している．返信用のチャン

ロックフリースタックに push や pop を無限回行う

ネル reply をチャンネル while に渡している理由は，クライアント側のプロセスは図 7 のようになる．pop

デッドロックフリー性を保証する型システムにおけでは，返信用のチャンネル r を pop に送信し，r からる reply への送信の obligation を，ループを繰り返

v を受信する．push では，スタックに追加する値と，すたびに受け渡しするためである．

処理が完了したことを伝えるチャンネル r を組にし

図 6 は，ロックフリースタックの pop 関数を π 計て送信し，r から受信を行う．

算で表現したプロセスである．このプロセスは，チャ

上述のロックフリースタックのサーバとクライア

ンネル pop から返信用のチャンネル reply を受け取

ントの π 計算での表現は，1. 1 節の意味ではロックフ

り，スタックの先頭の要素を reply に送信する．ス

リーだが，定義 2 の意味での強いロックフリー性はタックが空（null）である場合は，デフォルトの値と満たさない．なぜならば，無限個のクライアントのう*(new r in pop!r. r?rep) | *(new r in push!(1,r). r?rep)
図7

無限個のクライアント

P0≜(νr)(push!⟨1, r⟩. r?rep)Q0≜(νr)(pop!r. r?rep)

System≜(νmakeQuadruple, push, pop, stack, lock)(stack!null | lock!0 | ∗Push | ∗Pop | P0 | Q0 )図8

ロックフリースタックのシステム全体（push と pop が 1 回ずつの場合）

P0 | Q 0| stack!quad | lock!0
P7 | Q 0| stack!quad | lock!0P0 | Q 2| stack!quad | lock!0

P11 | Q0
| lock!0
P16 | Q0
| stack!quad’ | lock!0

P7 | Q 2| stack!quad | lock!0
P11 | Q2
| lock!0

P0 | Q12| lock!0
P7 | Q12| lock!0

P0 | Q17| stack!null | lock!0

P11 | Q12
| lock!0
P12 | Q12

P11 | Q13

P16 | Q12
| stack!quad’ | lock!0

P11 | Q17
| stack!null | lock!0

P16 | Q14

P12 | Q17

P16 | Q 1
| stack!quad’ | lock!0

P 1 | Q17
| stack!null | lock!0

P16 | Q2
| stack!quad’ | lock!0

P7 | Q17| stack!null | lock!0

P16 | Q17
| stack!quad | lock!0

P16 | Q17
| stack!quad’ | lock!0
図9

クライアントの状態遷移

ち，一部（例えば「奇数番」）のクライアントのみがめである．一方，定義 2 を弱め，すべての Q についそれぞれ有限時間で操作を完了し，他（例えば「偶て，−−→ を含む遷移列が存在するという弱いロック数番」）のクライアントは永久に操作を完了しないよ

フリー性は満たされる．

うな，full かつ strongly fair な遷移列が存在するたτ□push 操作や pop 操作が有限回のシステムであれば，

makeQuadruple :chan(chan(int, !), ∗!) ×chan(chan(quad t, !), ∗!) ×chan(int × chan(int, !), ∗!) ×chan(quad t × chan(int, 1), ∗!)−→ quad t

first :

quad t −→ chan(chan(int, !), ∗!)second :quad t −→ chan(chan(quad t, !), ∗!)third :

quad t −→ chan(int × chan(int, !), ∗!)fourth :quad t −→ chan(quad t × chan(int, !), ∗!)図 10

プリミティブ関数の型

強いロックフリー性を満たす．例えば push と pop を

pop の処理が任意に進んでいる（0 ≤ j ≤ 17）．

それぞれ 1 回ずつ並行に行うロックフリースタックの0 ≤ i ≤ 16 ∧ j = 17： pop が完了した後（j = 17），

システム全体は図 8 のように表される．ここで Push

push の処理が任意に進んでいる（0 ≤ i ≤ 16）．

と Pop はそれぞれ，図 5 の push サーバと，図 6 の

7 ≤ i ≤ 11 ∧ 2 ≤ j ≤ 12： push と pop が 1 回目のpop サーバを表している．また，P と Q はそれぞれ，

stack?t を実行後，lock?l をとる以前まで進ん

push を行うクライアントと，pop を行うクライアン
トを表している．

でいる．

11 ≤ i ≤ 16 ∧ j = 12： push が先に lock?l でロッ

後者のシステム全体の状態遷移を列挙する．stack にクを取得し（i = 12），push が完了する（i = 16）．

何らかの quad が出力されている状態から，push と pop

i = 16 ∧ j = 12, 13, 14, −1： push が 完 了 し た 後をそれぞれ 1 回ずつ並行に行うクライアント P0 | Q0

（i = 16），pop がロックを取得し（j = 13），（および，そのときの stack と lock への出力プロセ

スタックの先頭が変わっているため，競合を検出ス）の状態遷移図を図 9 に示す（それら以外のプロセ

して再試行を行う（j = 2）．

スは変化しないので省略する）．この図では 1 ステップi = 11 ∧ 12 ≤ j ≤ 17： pop が先に lock?l でロック

以上の遷移を ↠ で表している．push を行うクライアを取得し（j = 13），pop が完了する（j = 17）．

ントの状態を Pi (i = 0, 1, . . . , 16, −1) で表し，pop を

i = 11, 12, 13, −1 ∧ j = 17： pop が 完 了 し た 後行うクライアントの状態を Qj (j = 0, 1, . . . , 17, −1)（j = 17），push がロックを取得し（i = 12），で表すことにする．Pi および Qj の具体的な定義はスタックの先頭が変わっているため，競合を検出それぞれ付録 A と B に示す．push と pop を行うク

して再試行を行う（i = 7）．

ライアントが並行に実行されている状態 Pi | Qj を考えると，i と j の値の組が取りうる範囲とその理由は以下のとおりである．

0 ≤ i ≤ 16 ∧ 0 ≤ j ≤ 2： push 処 理 が 任 意 に 進 み（0 ≤ i ≤ 16），pop 処理は 1 回目の stack?t
以前まで進んでいる（0 ≤ j ≤ 2）．

0 ≤ i ≤ 7 ∧ 0 ≤ j ≤ 17： pop 処 理 が 任 意 に 進 み（0 ≤ j ≤ 17），push 処理は 1 回目の stack?t
以前まで進んでいる （0 ≤ i ≤ 7）．

i = 16 ∧ 0 ≤ j ≤ 17： push が完了した後（i = 16），

4 TyPiCal の拡張とデッドロックフリー性の検証
4. 1 再帰型を持つ 4 つ組プリミティブの追加
本節では，3 節で述べた π 計算におけるロックフ
リースタックの表現のデッドロックフリー性を TyP-

iCal で検証する．図 4 の 4 つ組 quad で表現されるセルは，次のセルへのポインタ（writeNext の第 1 引
数 v2 および readNext の返り値）を持っているため，再帰型を必要とする．TyPiCal ではユーザは新たな再帰型を定義することができないため，TyPiCal の実装に新たな再帰型と，それを用いるプリミティブ関

1

new makeCell in new push in new pop in

数を追加した．具体的には，再帰型を持つ 4 つ組を2

new stack in new lock in

作る関数 makeQuadruple と，その要素を取り出す関3

stack!null | lock!0

数 first, second, third, fourth を追加した．

| (*makeCell??r . . . . )5 | (*push?r. . . . )6 | (*pop?r. . . . )7 | *(new r in pop!!r . r??rep)
8 | *(new r in push!!(1,r) . r??rep)

4 つ組 quad の型 quad t の定義は，チャンネルのusage の部分を除くと次のとおりである．
quad t ≜ µα.
chan(chan(int))

4// readData× chan(chan(α))// readNext

× chan(int × chan(int))// writeData× chan(α × chan(int))// writeNext
4 つ組のそれぞれのチャンネルの usage を含む型を考えると以下のようになる．
readData: chan(chan(int, !), ∗!)readNext:chan(chan(quad t, !), ∗!)writeData:chan(int × chan(int, !), ∗!)図 11

TyPiCal での検証結果の一部

バはデッドロックフリーであることがわかる．8 行目の push 操作についても同様である．

push および pop 操作が有限回の場合も同様である．

5 ロックフリー性の検証
本節では，まず図 8 の，有限回の操作に対するロッ

writeNext : chan(quad t × chan(int, !), ∗!)以上を踏まえると，追加するプリミティブ関数の型はクフリースタックのロックフリー性を考える．図 8 の

図 10 のようになる．

システムは，4. 2 節のとおりデッドロックフリーであ

これらのプリミティブ関数を追加した結果，新たなり，さらに図 9 のとおり停止性も成り立つ（デッド形の制約が発生したため，それを解消する方法を実装

ロックフリー性も図 9 から確認することもできる）．

した．具体的には，subusage 制約 U1 ≤ U2 において，

したがって，図 8 のシステムはロックフリーであると従前の TyPiCal では U1 は usage 変数 α に限られていえる．

いたが，今回の拡張により新たに U1 が !ttoc . 0, ∗!ttoc . 0,

一方，図 7 の，無限回の操作を行うロックフリース(!ttoc . 0), ↑t (∗!ttoc . 0) のケースも発生したため，本研

タックは，状態数が無限になるため，図 9 のように究で必要となった，U2 に ? が出現しないケースについすべての遷移を列挙することは容易でない．そこで，て，subusage の定義に従い制約の解消を実装した．具push サーバおよび pop サーバは図 3 のハイブリッド

体的には，条件 cap ! (U1 ) ≤ cap ! (U2 ) [10, Deﬁnition

型システムで追加された型つけ規則を用い，サーバ以35, 3.]（他の条件は自明）から，capability level に関外の部分は従来のロックフリー性を保証する完全に静する制約（それら自体は既存）を生成する関数を実装

的な型システム [9] を用いて型つけすることを考えるした．

（ [12, Example 3.12] と同様）．

↑t

図 3 の規則では，ロバストなデッドロックフリー

4. 2 TyPiCal での検証結果

性，ロバストな合流性，ロバストな停止性を示す必要

TyPiCal に，無限回の push および pop 操作を並がある．まず，4. 2 節のように，TyPiCal が実装し行に行うロックフリースタックのプロセスを入力したているデッドロックフリー性を保証する型システムで結果の出力を図 11 に示す．!!や??は，その送受信の型つけが成功すれば，ロバストなデッドロックフリー

成功が保証されている（マークつきである）ことを表性も成り立つことが知られている [12, Theorem 3.9]．

す．pop 操作を行うクライアント側のプロセス（7 行（サーバの）ロバストな停止性は，外部との送受信は目）において，処理が終わった通知を必ず受け取れる

有限回である前提なので [12, Deﬁnition 3.6]，スタッことが保証されている（x??rep）．つまり，pop サー

ク操作が有限個の場合と同様に成り立つ．
問題は（サーバの）ロバストな合流性である．ハイブリッド型システムでいう合流性は 1 ステップでの合操作が完了することのみを主張している．無限個の流性という定義 [12, Deﬁnition 3.8] なので，そのま

push 操作や pop 操作がある場合（あるいは無限にスまでは成り立たない．1 ステップでの合流性を要求す

レッドを生成できるシステムの場合），fair なスケ

る理由は，ある遷移列で obligation が果たされれば，

ジューリングを仮定しなければ，すべてのスレッドが同じ obligation がすべての遷移列で果たされること途中までしか実行されず，いずれの操作も永久に完了を示す際，前者に含まれる遷移は，後者にも含まれる

しない可能性があるので，後者のロックフリー性は明ことを示すためである [12, Lemma C.1]．1 ステップ

らかに成り立たない．

ではなく複数ステップでの合流性に弱めることも可能
だが，fairness の前提を適用するため，同じ遷移が先

6 関連研究頭に来る（enable されている）必要がある．

すでに述べたロックフリーアルゴリズム [4,13,14,18]

そのように合流性の条件を弱めても，本論文のようなロックフリースタックのサーバでは，例えば lockや，ロックフリー性を保証する型システム [9, 12] 以
外に以下のような研究がある．

や stack の受信後，直ちに送信は行えないので，成り

Hoﬀmann ら [6] はロックフリー性の定義を形式化立たない．実際，無限個の push 操作や pop 操作を並して，それを検証するための分離論理の拡張を提案

行に行う場合，push のみが実行され続けて，pop がし，Treiber のロックフリースタックのロックフリー

永久に実行されない可能性があるので，ロックフリー

性を紙の上で形式的に証明した．

性が成り立たない．これは 2. 3 節すなわち [12, p. 9]

Jia ら [7] は，“read, compute and update” というでいう strongly fair な遷移を前提にしても，push の形をしたアルゴリズムのソースコードに補助変数をみが実行されている場合，図 6 の 3 行目の stack?t

割り当てることによりロックフリー性を検証する手法に対応する図 5 の 3 行目の stack!t および 10 行目を提案した．具体的には，共有データへの書き込みがの stack!s が，push 操作のたびに複製されて異なる

成功した場合には補助変数の値をインクリメントし，

出現とみなされるため，pop 操作の成功が保証されな

失敗した場合には，他のスレッドにより補助変数の値

いからである．[12, p. 9] のような fairness の定義をがインクリメントされている（他のスレッドが書き込変更し，送受信の組ではなく stack?t のような受信みに成功している）ことを確認する．これにより，ス（ないし送信）のみに注目して成功を保証するようなレッドが 1 つずつ減っていくことや，プログラム全

スケジューリングの定義は今後の課題である．そのよ

体の停止性を議論している．また，その手法を自動証

うに定義を変更すれば，前述の obligation がすべて

明ツール Cave として実装し，ロックフリーなスタッの遷移列で果たされることや，ひいては push サーバ

クやキューのロックフリー性を証明した．

や pop サーバのロックフリー性も証明できる可能性がある．

π 計算でのスタックの表現を [12, Example 3.12] の二分探索木のように根本的に変更すれば，ハイブリッ

Pinto [1] は，Total-TaDA という，ノンブロッキン
グなプログラムの停止性を証明する分離論理の拡張を提案し，それを用いてロックフリーなスタックやキューの紙の上での証明を行なった．

ド型システムでロックフリー性を保証することも可

佐久間 [19] は，Hoﬀmann らの分離論理の拡張に能である．本研究では，共有メモリを用いた Treiber

基づき，Treiber のスタックの push のロックフリーのロックフリースタックを π 計算で表現してロック

性を，Coq を用いて検証した．

フリー性を検証することを試みた．

2. 3 節で述べたとおり，1. 1 節でいうアルゴリズ
ムのロックフリー性は，2. 3 節のプロセスのロック
フリー性 [12, Deﬁnition 2.8] と異なり，fair なスケ
ジューリングを仮定しない一方，少なくとも 1 つのこれらと比較すると本研究は，既存の型システムを用いた部分については，分離論理の拡張に基づく証明
より簡便な検証が可能であった．

7 結論と今後の課題
本研究では，π 計算のプロセスのロックフリー性を型システムにもとづき検証するツールである TyP-

iCal を，再帰型を持つセル構造で拡張して Treiberのロックフリースタックを表現し，そのデッドロック
フリー性を検証した．デッドロックに限らないロック
フリー性は，有限回のスタック操作についてはハイブ
リッド型システム [12] を用いて検証した．無限回の並行なスタック操作の場合は，そもそもロックフリー
性が成り立たない一方，fairness の仮定を変更すれば証明できる可能性を示唆した．また，ハイブリッド型システムでロックフリー性を検証する際に必要な停止性は，本研究ではすべての遷移列を列挙して検証したが，ツールによる自動化や型システム [2] の利用も考えられる．
謝辞 TyPiCal やハイブリッド型システムに関する質問にご回答くださった小林直樹氏に深謝します．本
研究は JSPS 科研費 JP15H02681，JP20H04161 の助成を受けたものです．

参 考 文 献[ 1 ] da Rocha Pinto, P.: Reasoning with time anddata abstractions, PhD Thesis, Imperial College
London, UK, 2016.
[ 2 ] Deng, Y. and Sangiorgi, D.: Ensuring termination by typability, Inf. Comput., Vol. 204,
No. 7(2006), pp. 1045–1082.
[ 3 ] Gotsman, A., Cook, B., Parkinson, M. J., andVafeiadis, V.: Proving that non-blocking algorithms don’t block, Proceedings of the 36th ACM
SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages, POPL 2009, Savannah,
GA, USA, January 21-23, 2009, Shao, Z. and
Pierce, B. C.(eds.), ACM, 2009, pp. 16–28.
[ 4 ] Harris, T. L.: A Pragmatic Implementation ofNon-blocking Linked-Lists, Distributed Computing,
15th International Conference, DISC 2001, Lisbon,
Portugal, October 3-5, 2001, Proceedings, Welch,
J. L.(ed.), Lecture Notes in Computer Science,Vol. 2180, Springer, 2001, pp. 300–314.
[ 5 ] Herlihy, M. and Shavit, N.: The art of multiprocessor programming, Morgan Kaufmann, 2008.
[ 6 ] Hoﬀmann, J., Marmar, M., and Shao, Z.: Quantitative Reasoning for Proving Lock-Freedom, 28th
Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA,
June 25-28, 2013, IEEE Computer Society, 2013,

pp. 124–133.
[ 7 ] Jia, X., Li, W., and Vafeiadis, V.: Proving
Lock-Freedom Easily and Automatically, Proceedings of the 2015 Conference on Certiﬁed Programs
and Proofs, CPP 2015, Mumbai, India, January
15-17, 2015, Leroy, X. and Tiu, A.(eds.), ACM,
2015, pp. 119–127.
[ 8 ] Kobayashi, N.: TyPiCal: A Type-Based Analyzer for the Pi-Calculus, http://www-kb.is.s.
u-tokyo.ac.jp/~koba/typical/.
[ 9 ] Kobayashi, N.: A Type System for Lock-Free
Processes, Inf. Comput., Vol. 177, No. 2(2002),
pp. 122–159.
[10] Kobayashi, N.: A New Type System for
Deadlock-Free Processes, CONCUR 2006 - Concurrency Theory, 17th International Conference,
CONCUR 2006, Bonn, Germany, August 2730, 2006, Proceedings, Baier, C. and Hermanns,
H.(eds.), Lecture Notes in Computer Science,Vol. 4137, Springer, 2006, pp. 233–247.
[11] Kobayashi, N., Saito, S., and Sumii, E.: An
Implicitly-Typed Deadlock-Free Process Calculus,
CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA,
August 22-25, 2000, Proceedings, Palamidessi,
C.(ed.), Lecture Notes in Computer Science,Vol. 1877, Springer, 2000, pp. 489–503.
[12] Kobayashi, N. and Sangiorgi, D.: A hybrid typesystem for lock-freedom of mobile processes, ACM
Trans. Program. Lang. Syst., Vol. 32, No. 5(2010),
pp. 16:1–16:49.
[13] Michael, M. M.: High performance dynamic
lock-free hash tables and list-based sets, Proceedings of the Fourteenth Annual ACM Symposium on
Parallel Algorithms and Architectures, SPAA 2002,
Winnipeg, Manitoba, Canada, August 11-13, 2002,
Rosenberg, A. L. and Maggs, B. M.(eds.), ACM,
2002, pp. 73–82.
[14] Michael, M. M. and Scott, M. L.: Simple, Fast,and Practical Non-Blocking and Blocking Concurrent Queue Algorithms, Proceedings of the Fifteenth
Annual ACM Symposium on Principles of Distributed Computing, Philadelphia, Pennsylvania,
USA, May 23-26, 1996, Burns, J. E. and Moses,
Y.(eds.), ACM, 1996, pp. 267–275.
[15] Milner, R.: Communicating and mobile systems- the Pi-calculus, Cambridge University Press, 1999.
[16] Sangiorgi, D. and Walker, D.: The Pi-Calculus a theory of mobile processes, Cambridge University
Press, 2001.
[17] Sumii, E. and Kobayashi, N.: A Generalized
Deadlock-Free Process Calculus, Electron. Notes
Theor. Comput. Sci., Vol. 16, No. 3(1998), pp. 225–
247.
[18] Treiber, R. K.: Systems Programming: Coping
With Parallelism, Technical report, IBM Almaden
Research Center, 650 Harry RoadSan Jose, California, 1986.

[19] 佐久間亮: ロックフリーアルゴリズムの形式的検証,
修士論文, 情報科学研究科, 東北大学, 2018.

A push クライアントの状態
1

P0 =

2

new r in push!(1, r). r?rep

3
4

P1 =

5

new r in r?rep| (new ref in makeCell!ref. ref?quad’.
let writeData = third quad’ in
8
let writeNext = fourth quad’ in
9
new a in writeData!(value, a). a?l.
10
new while in while!reply
11| *while?r. stack?t. ( stack!t12| new a in writeNext!(t, a). a?l. lock?l.
13
stack?s. ( stack!s14| if s = t
15then stack?u. ( stack!quad’ | lock!0 | r!0 )16
else ( lock!0 | while!r ))))
6

7

17
18

P2 =

19

new r in new ref in

20

r?rep

| (new readData in new readNext in new writeData in new writeNext in
let quad = makeQuadruple (readData, readNext, writeData, writeNext) in23
r!quad | new data in new next in data!0 | next!null24| *readData?r. data?v. (r!v | data!v)
25| *readNext?r. next?v. (r!v | next!v)
26| *writeData?(v2,r). data?v1. (r!0 | data!v2)
27| *writeNext?(v2,r). next?v1. (r!0 | next!v2))
28 | (ref?quad’.
29
let writeData = third quad’ in
30
let writeNext = fourth quad’ in
31
new a in writeData!(value, a). a?l.
32
new while in while!reply
33| *while?r. stack?t. ( stack!t34| new a in writeNext!(t, a). a?l. lock?l.
35
stack?s. ( stack!s36| if s = t
37then stack?u. ( stack!quad’ | lock!0 | r!0 )38
else ( lock!0 | while!r ))))
21
22

39
40

P3 =

41

new r in new ref in42

new readData in new readNext in new writeData in new writeNext in

43

r?rep

| (new data in new next in data!0 | next!null45| *readData?r. data?v. (r!v | data!v)
46| *readNext?r. next?v. (r!v | next!v)
47| *writeData?(v2,r). data?v1. (r!0 | data!v2)
48| *writeNext?(v2,r). next?v1. (r!0 | next!v2))
49 | (let writeData = third quad’ in
50
let writeNext = fourth quad’ in51
new a in writeData!(1, a). a?l.
new while in while!reply
5253| *while?r. stack?t. ( stack!t54| new a in writeNext!(t, a). a?l. lock?l.
55
stack?s. ( stack!s56| if s = t
57
then stack?u. ( stack!quad’ | lock!0 | r!0 )58
else ( lock!0 | while!r ))))
44

59
60

P4 =

61

new r in new ref in new a1 in

62

new readData in new readNext in new writeData in new writeNext in

63

r?rep

| (new data in new next in data!0 | next!null| *readData?r. data?v. (r!v | data!v)
66| *readNext?r. next?v. (r!v | next!v)
67| *writeData?(v2,r). data?v1. (r!0 | data!v2)
68| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
69| data?v1. (a1!0 | data!1))
70 | (a1?l.
71
new while in while!reply
72| *while?r. stack?t. ( stack!t73| new a in writeNext!(t, a). a?l. lock?l.
stack?s. ( stack!s74
75| if s = t
76
then stack?u. ( stack!quad’ | lock!0 | r!0 )77
else ( lock!0 | while!r ))))
64
65

78
79

P5 =

80

new r in new ref in new a1 in81

new readData in new readNext in new writeData in new writeNext in

82

r?rep

| (new data in new next in next!null| *readData?r. data?v. (r!v | data!v)
85| *readNext?r. next?v. (r!v | next!v)
86| *writeData?(v2,r). data?v1. (r!0 | data!v2)
87| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
88| (r!0 | data!1))
83
84

89
90
91
92
93
94
95
96

| (a1?l.
new while in while!reply| *while?r. stack?t. ( stack!t| new a in writeNext!(t, a). a?l. lock?l.
stack?s. ( stack!s| if s = tthen stack?u. ( stack!quad’ | lock!0 | r!0 )else ( lock!0 | while!r ))))

97
98

P6 =

99

new r in new ref in new a1 in100

new readData in new readNext in new writeData in new writeNext in

101

r?rep

| (new data in new next in next!null| *readData?r. data?v. (r!v | data!v)
104| *readNext?r. next?v. (r!v | next!v)
105| *writeData?(v2,r). data?v1. (r!0 | data!v2)
106| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
107| data!1)
108 | (new while in while!reply
109| *while?r. stack?t. ( stack!t
110| new a in writeNext!(t, a). a?l. lock?l.
111
stack?s. ( stack!s112| if s = t
113
then stack?u. ( stack!quad’ | lock!0 | r!0 )114
else ( lock!0 | while!r ))))
102

103

115
116

P7 =

117

new r in new ref in new a1 in

118

new readData in new readNext in new writeData in new writeNext in

119

r?rep

| (new data in new next in next!null121| *readData?r. data?v. (r!v | data!v)
122| *readNext?r. next?v. (r!v | next!v)
123| *writeData?(v2,r). data?v1. (r!0 | data!v2)
124| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
125| data!1)
126 | (new while in127| *while?r. stack?t. ( stack!t128| new a in writeNext!(t, a). a?l. lock?l.
129
stack?s. ( stack!s130| if s = t
131then stack?u. ( stack!quad’ | lock!0 | r!0 )132
else ( lock!0 | while!r )))133| stack?t. ( stack!t120

| new a in writeNext!(t, a). a?l. lock?l.
stack?s. ( stack!s| if s = tthen stack?u. ( stack!quad’ | lock!0 | r!0 )else ( lock!0 | while!r ))))

134
135
136
137
138
139
140

P8 =

141

new r in new ref in new a1 in

142

new readData in new readNext in new writeData in new writeNext in

143

r?rep

| (new data in new next in next!null| *readData?r. data?v. (r!v | data!v)
146| *readNext?r. next?v. (r!v | next!v)
147| *writeData?(v2,r). data?v1. (r!0 | data!v2)
148| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
149| data!1)
150 | (new while in151| *while?r. stack?t. ( stack!t152| new a in writeNext!(t, a). a?l. lock?l.
153
stack?s. ( stack!s154| if s = t
155then stack?u. ( stack!quad’ | lock!0 | r!0 )156
else ( lock!0 | while!r )))157| ( stack!quad158| new a in writeNext!(quad, a). a?l. lock?l.
159
stack?s. ( stack!s160| if s = quad
161
then stack?u. ( stack!quad’ | lock!0 | r!0 )162
else ( lock!0 | while!r ))))
144

145

163
164

P9 =

165

new r in new ref in new a1 in new a2 in

166

new readData in new readNext in new writeData in new writeNext in

167

r?rep

| (new data in new next in next!null169| *readData?r. data?v. (r!v | data!v)
170| *readNext?r. next?v. (r!v | next!v)
171| *writeData?(v2,r). data?v1. (r!0 | data!v2)
172| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
173| data!1
174| next?v1. (a2!0 | next!v2))
175 | (new a in new while in176| *while?r. stack?t. ( stack!t
177| new a in writeNext!(t, a). a?l. lock?l.
178
stack?s. ( stack!s168

| if s = t

179

then stack?u. ( stack!quad’ | lock!0 | r!0 )

180
181
182
183
184
185
186
187

else ( lock!0 | while!r )))| ( stack!quad| a2?l. lock?l.
stack?s. ( stack!s| if s = quadthen stack?u. ( stack!quad’ | lock!0 | r!0 )else ( lock!0 | while!r ))))

188
189

P10 =

190

new r in new ref in new a1 in new a2 in

191

new readData in new readNext in new writeData in new writeNext in

192

r?rep

| (new data in new next in| *readData?r. data?v. (r!v | data!v)
195| *readNext?r. next?v. (r!v | next!v)
196| *writeData?(v2,r). data?v1. (r!0 | data!v2)
197| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
198| data!1
199| (a2!0 | next!quad))
200 | (new while in201| *while?r. stack?t. ( stack!t202| new a in writeNext!(t, a). a?l. lock?l.
203
stack?s. ( stack!s204| if s = t
205then stack?u. ( stack!quad’ | lock!0 | r!0 )206
else ( lock!0 | while!r )))207| ( stack!quad208| a?l. lock?l.
stack?s. ( stack!s209
210| if s = quad
211
then stack?u. ( stack!quad’ | lock!0 | r!0 )212
else ( lock!0 | while!r ))))
193
194

213
214

P11 =

215

new r in new ref in new a1 in new a2 in

216

new readData in new readNext in new writeData in new writeNext in

217

r?rep

| (new data in new next in| *readData?r. data?v. (r!v | data!v)
220| *readNext?r. next?v. (r!v | next!v)
221| *writeData?(v2,r). data?v1. (r!0 | data!v2)
222| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
223| data!1

218
219

| next!quad)
225 | (new while in
226| *while?r. stack?t. ( stack!t
227| new a in writeNext!(t, a). a?l. lock?l.
228
stack?s. ( stack!s229| if s = t
230
then stack?u. ( stack!quad’ | lock!0 | r!0 )231
else ( lock!0 | while!r )))| ( stack!quad232
233| lock?l.
234
stack?s. ( stack!s235| if s = quad
236
then stack?u. ( stack!quad’ | lock!0 | r!0 )237
else ( lock!0 | while!r ))))
224

238
239

P12 =

240

new r in new ref in new a1 in new a2 in241

new readData in new readNext in new writeData in new writeNext in

242

r?rep

| (new data in new next in244| *readData?r. data?v. (r!v | data!v)
245| *readNext?r. next?v. (r!v | next!v)
246| *writeData?(v2,r). data?v1. (r!0 | data!v2)
247| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
248| data!1
249| next!quad)
250 | (new while in251| *while?r. stack?t. ( stack!t
252| new a in writeNext!(t, a). a?l. lock?l.
253
stack?s. ( stack!s| if s = t
254
255
then stack?u. ( stack!quad | lock!0 | r!0 )256
else ( lock!0 | while!r )))257| (stack!quad258| stack?s. ( stack!s259| if s = quad260
then stack?u. ( stack!quad’ | lock!0 | r!0 )261
else ( lock!0 | while!r ))))
243

262
263

P13 =

264

new r in new ref in new a1 in new a2 in265

new readData in new readNext in new writeData in new writeNext in

266

r?rep

267

| (new data in new next in| *readData?r. data?v. (r!v | data!v)

268

| *readNext?r. next?v. (r!v | next!v)
270| *writeData?(v2,r). data?v1. (r!0 | data!v2)
271| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
272| data!1
273| next!quad)
274 | (new while in275| *while?r. stack?t. ( stack!t
276| new a in writeNext!(t, a). a?l. lock?l.
stack?s. ( stack!s277
278| if s = t
279
then stack?u. ( stack!quad | lock!0 | r!0 )280
else ( lock!0 | while!r )))281| (stack!quad’’282| if quad’’ = quad283
then stack?u. ( stack!quad’ | lock!0 | r!0 )284
else ( lock!0 | while!r )))
269

285
286

P14 =

287

new r in new ref in new a1 in new a2 in288

new readData in new readNext in new writeData in new writeNext in

289

r?rep

| (new data in new next in| *readData?r. data?v. (r!v | data!v)
292| *readNext?r. next?v. (r!v | next!v)
293| *writeData?(v2,r). data?v1. (r!0 | data!v2)
294| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
295| data!1
296| next!quad)
297 | (new while in298| *while?r. stack?t. ( stack!t| new a in writeNext!(t, a). a?l. lock?l.
299
300
stack?s. ( stack!s301| if s = t
302then stack?u. ( stack!quad | lock!0 | r!0 )303
else ( lock!0 | while!r )))304| ( stack!quad’’ | stack?u. ( stack!quad’ | lock!0 | r!0 ) ))

290
291

305
306

P15 =

307

new r in new ref in new a1 in new a2 in308

new readData in new readNext in new writeData in new writeNext in

309

r?rep

| (new data in new next in
311| *readData?r. data?v. (r!v | data!v)
312| *readNext?r. next?v. (r!v | next!v)
313| *writeData?(v2,r). data?v1. (r!0 | data!v2)
310

| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
315| data!1
316| next!quad)
317 | (new while in318| *while?r. stack?t. ( stack!t
319| new a in writeNext!(t, a). a?l. lock?l.
320
stack?s. ( stack!s321| if s = tthen stack?u. ( stack!quad | lock!0 | r!0 )322
323
else ( lock!0 | while!r )))324| ( stack!quad’ | lock!0 | r!0 ))

314

325
326

P16 =

327

new r in new ref in new a1 in new a2 in

328

new readData in new readNext in new writeData in new writeNext in(new data in new next in| *readData?r. data?v. (r!v | data!v)
331| *readNext?r. next?v. (r!v | next!v)
332| *writeData?(v2,r). data?v1. (r!0 | data!v2)
333| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
334| data!1
335| next!quad)
336 | (new while in337| *while?r. stack?t. ( stack!t338| new a in writeNext!(t, a). a?l. lock?l.
339
stack?s. ( stack!s340| if s = t
341
then stack?u. ( stack!quad | lock!0 | r!0 )342
else ( lock!0 | while!r )))
343
| O
329
330

344
345

P−1 =

346

new r in new ref in new a1 in new a2 in347

new readData in new readNext in new writeData in new writeNext in

348

r?rep

| (new data in new next in| *readData?r. data?v. (r!v | data!v)
351| *readNext?r. next?v. (r!v | next!v)
352| *writeData?(v2,r). data?v1. (r!0 | data!v2)
353| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
354| data!1
355| next!quad)
356 | (new while in357| *while?r. stack?t. ( stack!t358| new a in writeNext!(t, a). a?l. lock?l.

349
350

359

stack?s. ( stack!s360| if s = t

361

then stack?u. ( stack!quad’ | lock!0 | r!0 )362

else ( lock!0 | while!r )))363| while!r ))B pop クライアントの状態
1

Q0 =

2

new r in pop!x . r?rep

3
4

Q1 =

5

new r in r?rep| (new while in while!reply| *while?r. stack?t. ( stack!t8| if s = null
9
then r!0
10
else let readData = first t in
11
let readNext = second t in12
new a in readData!a. a?v.
13
new b in readNext!b. b?x.
14
lock?l. stack?s. ( stack!s15| if s = t
16then stack?u. ( stack!x | lock!0 | r!v )17
else ( lock!0 | while!r ))))
6
7

18
19

Q2 =

new r in r?rep| (new while in22*while?r. stack?t. ( stack!t23| if s = null
24
then r!025
else let readData = first t in26
let readNext = second t in27
new a in readData!a. a?v.
28
new b in readNext!b. b?x.
29
lock?l. stack?s. ( stack!s30| if s = t
31then stack?u. ( stack!x | lock!0 | r!v )32
else ( lock!0 | while!r )))33| (stack?t. ( stack!t34| if s = null
35
then r!036
else let readData = first t in37
let readNext = second t in
20

21

new a in readData!a. a?v.

38
39

new b in readNext!b. b?x.

40

lock?l. stack?s. ( stack!s41| if s = t

42then stack?u. ( stack!x | lock!0 | r!v )43else ( lock!0 | while!r )))))

44
45

Q3 =

new r in r?rep| (new while in48*while?r. stack?t. ( stack!t49| if s = null
50
then r!051
else let readData = first t in52
let readNext = second t in53
new a in readData!a. a?v.
54
new b in readNext!b. b?x.
55
lock?l. stack?s. ( stack!s56| if s = t
57
then stack?u. ( stack!x | lock!0 | r!v )58
else ( lock!0 | while!r )))59| ( stack!quad
60| if quad = null
61
then r!062
else let readData = first quad in63
let readNext = second quad in64
new a in readData!a. a?v.
65
new b in readNext!b. b?x.
66
lock?l. stack?s. ( stack!s67| if s = quadthen stack?u. ( stack!x | lock!0 | r!v )68
69
else ( lock!0 | while!r ))))
46

47

70
71

Q4 =

72

new r in r?rep| (new while in*while?r. stack?t. ( stack!t75| if s = null76
then r!077
else let readData = first t in78
let readNext = second t in79
new a in readData!a. a?v.
80
new b in readNext!b. b?x.
81
lock?l. stack?s. ( stack!s82| if s = t7374then stack?u. ( stack!x | lock!0 | r!v )83

else ( lock!0 | while!r )))84
85| r!0)

86
87

Q5 =

88

new r in| (new while in90*while?r. stack?t. ( stack!t| if s = null
91
92
then r!093
else let readData = first t in94
let readNext = second t in95
new a in readData!a. a?v.
96
new b in readNext!b. b?x.
97
lock?l. stack?s. ( stack!s98| if s = t
99then stack?u. ( stack!x | lock!0 | r!v )100else ( lock!0 | while!r )))
101
| O)
89

102
103

Q6 =

104

new r in r?rep| (new while in106*while?r. stack?t. ( stack!t107| if s = null
108
then r!0
109
else let readData = first t in110
let readNext = second t in111
new a in readData!a. a?v.
112
new b in readNext!b. b?x.
lock?l. stack?s. ( stack!s113
114| if s = t
115
then stack?u. ( stack!x | lock!0 | r!v )116
else ( lock!0 | while!r )))117| ( stack!quad118| new a in readData!a. a?v.
119
new b in readNext!b. b?x.
120
lock?l. stack?s. ( stack!s
121| if s = quad
122
then stack?u. ( stack!x | lock!0 | r!v )123else ( lock!0 | while!r ))))
105

124
125

Q7 =

126

new r in new readData in new readNext in new writeData in new writeNext in127

new a in r?rep

| (new data in new next in data!1 | next!quad’’129| *readData?r. data?v. (r!v | data!v)
130| *readNext?r. next?v. (r!v | next!v)
131| *writeData?(v2,r). data?v1. (r!0 | data!v2)
132| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
133| data?v. (a!v | data!v))
134 | (new while in
135*while?r. stack?t. ( stack!t| if s = null
136
137
then r!0
138
else let readData = first t in139
let readNext = second t in140
new a in readData!a. a?v.
141
new b in readNext!b. b?x.
142
lock?l. stack?s. ( stack!s143| if s = t
144then stack?u. ( stack!x | lock!0 | r!v )145else ( lock!0 | while!r )))146| ( stack!quad147| a?v.
148
new b in readNext!b. b?x.
149
lock?l. stack?s. ( stack!s150| if s = quad
151
then stack?u. ( stack!x | lock!0 | r!v )152else ( lock!0 | while!r ))))

128

153
154

Q8 =

155

new r in new readData in new readNext in new writeData in new writeNext in156

new a in r?rep| (new data in new next in next!quad’’| *readData?r. data?v. (r!v | data!v)
159| *readNext?r. next?v. (r!v | next!v)
160| *writeData?(v2,r). data?v1. (r!0 | data!v2)
161| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
162| (a!1 | data!1))
163 | (new while in164*while?r. stack?t. ( stack!t165| if s = null
166
then r!0
167
else let readData = first t in
168
let readNext = second t in169
new a in readData!a. a?v.
170
new b in readNext!b. b?x.
171
lock?l. stack?s. ( stack!s172| if s = t
157

158

then stack?u. ( stack!x | lock!0 | r!v )173else ( lock!0 | while!r )))

174
175
176

| ( stack!quad| a?v.

177

new b in readNext!b. b?x.

178

lock?l. stack?s. ( stack!s179| if s = quadthen stack?u. ( stack!x | lock!0 | r!v )else ( lock!0 | while!r ))))

180
181
182
183

Q9 =

184

new r in new readData in new readNext in new writeData in new writeNext in

185

new a in r?rep| (new data in new next in next!quad’’| *readData?r. data?v. (r!v | data!v)
188| *readNext?r. next?v. (r!v | next!v)
189| *writeData?(v2,r). data?v1. (r!0 | data!v2)
190| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
191| data!1)
192 | (new while in
193*while?r. stack?t. ( stack!t194| if s = null
195
then r!0
196
else let readData = first t in197
let readNext = second t in198
new a in readData!a. a?v.
199
new b in readNext!b. b?x.
200
lock?l. stack?s. ( stack!s201| if s = t
202
then stack?u. ( stack!x | lock!0 | r!v )else ( lock!0 | while!r )))203
204| ( stack!quad205| new b in readNext!b. b?x.
206
lock?l. stack?s. ( stack!s207| if s = quad
208
then stack?u. ( stack!x | lock!0 | r!1 )209
else ( lock!0 | while!r ))))
186

187

210
211

Q10 =

212

new r in new readData in new readNext in new writeData in new writeNext in

new a in new b in r?rep| (new data in new next in next!quad’’215| *readData?r. data?v. (r!v | data!v)
216| *readNext?r. next?v. (r!v | next!v)
217| *writeData?(v2,r). data?v1. (r!0 | data!v2)
213

214

| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
219| data!1
220| next?v. (b!v | next!v))
221 | (new while in222*while?r. stack?t. ( stack!t223| if s = null
224
then r!0
225
else let readData = first t in
let readNext = second t in
226
227
new a in readData!a. a?v.
228
new b in readNext!b. b?x.
229
lock?l. stack?s. ( stack!s230| if s = t
231
then stack?u. ( stack!x | lock!0 | r!v )232
else ( lock!0 | while!r )))233| ( stack!quad234| b?x.
235
lock?l. stack?s. ( stack!s236| if s = quad
237
then stack?u. ( stack!x | lock!0 | r!1 )238
else ( lock!0 | while!r ))))
218

239
240

Q11 =

241

new r in new readData in new readNext in new writeData in new writeNext in242

new a in new b in r?rep| (new data in new next in244| *readData?r. data?v. (r!v | data!v)
245| *readNext?r. next?v. (r!v | next!v)
246| *writeData?(v2,r). data?v1. (r!0 | data!v2)
247| *writeNext?(v2,r). next?v1. (r!0 | next!v2)| data!1
248
249| (b!quad’’ | next!quad’’))250 | (new while in251*while?r. stack?t. ( stack!t252| if s = null
253
then r!0
254
else let readData = first t in255
let readNext = second t in256
new a in readData!a. a?v.
257
new b in readNext!b. b?x.
258
lock?l. stack?s. ( stack!s259| if s = t
260
then stack?u. ( stack!x | lock!0 | r!v )261
else ( lock!0 | while!r )))262| ( stack!quad
243

263
264
265
266
267

| b?x.
lock?l. stack?s. ( stack!s| if s = quadthen stack?u. ( stack!x | lock!0 | r!1 )else ( lock!0 | while!r ))))

268
269

Q12 =

270

new r in new readData in new readNext in new writeData in new writeNext in

new a in new b in r?rep| (new data in new next in273| *readData?r. data?v. (r!v | data!v)
274| *readNext?r. next?v. (r!v | next!v)
275| *writeData?(v2,r). data?v1. (r!0 | data!v2)
276| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
277| data!1
278| next!quad’’)279 | (new while in280*while?r. stack?t. ( stack!t281| if s = null
282
then r!0283
else let readData = first t in284
let readNext = second t in
285
new a in readData!a. a?v.
286
new b in readNext!b. b?x.
287
lock?l. stack?s. ( stack!s288| if s = t
289
then stack?u. ( quad | lock!0 | r!v )290else ( lock!0 | while!r )))291| ( stack!quad292| lock?l. stack?s. ( stack!s| if s = quad
293
294
then stack?u. ( stack!quad | lock!0 | r!1 )295
else ( lock!0 | while!r ))))
271

272

296
297

Q13 =

298

new r in new readData in new readNext in new writeData in new writeNext in299

new a in new b in r?rep| (new data in new next in| *readData?r. data?v. (r!v | data!v)
302| *readNext?r. next?v. (r!v | next!v)
303| *writeData?(v2,r). data?v1. (r!0 | data!v2)
304| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
305| data!1
306| next!quad’’)307 | (new while in
300
301

308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323

*while?r. stack?t. ( stack!t| if s = nullthen r!0
else let readData = first t in
let readNext = second t in
new a in readData!a. a?v.
new b in readNext!b. b?x.
lock?l. stack?s. ( stack!s| if s = tthen stack?u. ( stack!x | lock!0 | r!v )else ( lock!0 | while!r )))| ( stack!quad| stack?s. ( stack!s| if s = quadthen stack?u. ( stack!quad | lock!0 | r!1 )else ( lock!0 | while!r ))))

324
325

Q14 =

326

new r in new readData in new readNext in new writeData in new writeNext in

327

new a in new b in r?rep| (new data in new next in| *readData?r. data?v. (r!v | data!v)
330| *readNext?r. next?v. (r!v | next!v)
331| *writeData?(v2,r). data?v1. (r!0 | data!v2)
332| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
333| data!1
334| next!quad’’)335 | (new while in336*while?r. stack?t. ( stack!t337| if s = nullthen r!0
338
339
else let readData = first t in340
let readNext = second t in341
new a in readData!a. a?v.
342
new b in readNext!b. b?x.
343
lock?l. stack?s. ( stack!s344| if s = t
345
then stack?u. ( stack!x | lock!0 | r!v )346
else ( lock!0 | while!r )))347| ( stack!quad’348| if quad’ = quad349
then stack?u. ( stack!quad | lock!0 | r!v )350
else ( lock!0 | while!r )))
328
329

351
352

Q15 =

353

new r in new readData in new readNext in new writeData in new writeNext in

new a in new b in r?rep| (new data in new next in356| *readData?r. data?v. (r!v | data!v)
357| *readNext?r. next?v. (r!v | next!v)
358| *writeData?(v2,r). data?v1. (r!0 | data!v2)359| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
360| data!1| next!quad’’)361
362 | (new while in363*while?r. stack?t. ( stack!t364| if s = null
365
then r!0366
else let readData = first t in367
let readNext = second t in368
new a in readData!a. a?v.
369
new b in readNext!b. b?x.
370
lock?l. stack?s. ( stack!s371| if s = t
372
then stack?u. ( stack!x | lock!0 | r!v )373
else ( lock!0 | while!r )))374| stack!quad’
375| stack?u. ( stack!quad | lock!0 | r!1 )))
354

355

376
377

Q16 =

378

new r in new readData in new readNext in new writeData in new writeNext in

new a in new b in r?rep| (new data in new next in381| *readData?r. data?v. (r!v | data!v)
382| *readNext?r. next?v. (r!v | next!v)| *writeData?(v2,r). data?v1. (r!0 | data!v2)
383
384| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
385| data!1
386| next!quad’’)387 | (new while in388*while?r. stack?t. ( stack!t389| if s = null390
then r!0391
else let readData = first t in392
let readNext = second t in393
new a in readData!a. a?v.
394
new b in readNext!b. b?x.
395
lock?l. stack?s. ( stack!s396| if s = t
397
then stack?u. ( stack!x | lock!0 | r!v )
379

380

else ( lock!0 | while!r )))

398
399

| ( stack!quad | lock!0 | r!1 ))

400
401

Q17 =

402

new r in new readData in new readNext in new writeData in new writeNext in

new a in new b in r?rep| (new data in new next in
405| *readData?r. data?v. (r!v | data!v)| *readNext?r. next?v. (r!v | next!v)
406
407| *writeData?(v2,r). data?v1. (r!0 | data!v2)
408| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
409| data!1
410| next!quad’’)411 | (new while in412*while?r. stack?t. ( stack!t413| if s = null
414
then r!0415
else let readData = first t in416
let readNext = second t in417
new a in readData!a. a?v.
418
new b in readNext!b. b?x.
419
lock?l. stack?s. ( stack!s420| if s = t
421
then stack?u. ( stack!x | lock!0 | r!v )422
else ( lock!0 | while!r )))
423
| O)
403

404

424
425

Q−1 =

426

new r in new readData in new readNext in new writeData in new writeNext in

new a in new b in r?rep| (new data in new next in429| *readData?r. data?v. (r!v | data!v)
430| *readNext?r. next?v. (r!v | next!v)
431| *writeData?(v2,r). data?v1. (r!0 | data!v2)
432| *writeNext?(v2,r). next?v1. (r!0 | next!v2)
433| data!1
434| next!quad’’)435 | (new while in436*while?r. stack?t. ( stack!t437| if s = null
438
then r!0439
else let readData = first t in440
let readNext = second t in
441
new a in readData!a. a?v.
442
new b in readNext!b. b?x.
427

428

443

lock?l. stack?s. ( stack!s444| if s = t

445

then stack?u. ( stack!x | lock!0 | r!v )446

else ( lock!0 | while!r )))447| while!r ))