ロックフリーアルゴリズムとは，正確には進行性が保証されるアルゴリズムのことをいう．Compare and Swap命令(CAS)を主軸として実装する．
ロックフリーアルゴリズムにおいて，有名な問題としてABA問題がある．ABA問題の解決方法はいくつかあり，それぞれに特徴がある．今回は，タグ付きポインタとload-link/store-conditional(ll/sc)バージョンでのCASといった2つの解決方法について検証する．
最初に，ロックフリーアルゴリズムのなかで最も基本的なロックフリースタックをC言語で実装する．そして，それをPromelaでSPINのモデルとして記述する．
SPINでモデルを検証することで，それぞれの解決策の特徴を見ていく．モデル検査は，考えられる状態を徹底的に探索するため，例えばタグ付きポインタのモデルについて面白い結果が得られる．
実装したモデルや，C言語実装は以下である．
なお，atomic_compare_exchange_strong()と，CASは基本的に同じ意味で使っているが，実装側のコンテキストだと，atomic_compare_exchange_strong()という用語を使用する．
C言語バージョンでは，タグ無しとタグ付きを実装した． main関数側で，複数のスレッドを用いてpushとpopを行い，最後にその結果を評価している．
タグ無しバージョンを何度か実行すると，以下のログが出てくることがある．一方，タグ付きバージョンでは，何度か実行しても評価まで問題なく成功し，エラーログが出てくることはない．
double free or corruption (fasttop)^[[A
Segmentation fault (core dumped)
モデルの基本設計について述べる．その後，各解決策の設計に進む．
使用できるメモリを以下のように表し，メモリ領域を配列として表現した．
typedef Mem {
int data; // actual data
int next; // next pointer
int refc // reference count for detecting double free
}
Mem mem[M]; // index expresses memory addressスタック実装のためにリストを表現したいが，C言語で実装するようにやってしまうと，Promelaでの実装は難しく，またモデルとして検査すべき状態空間が大きくなりすぎてしまう．そのため，配列を用いて，限定された空間で，リストを表現することを考える．
メモリはMで指定された領域だけ存在する．Mの値の設定については後述する．配列のインデックスはメモリのアドレスと対応する．ポインタが指す先を参照する操作は，ある配列のインデックス先を参照することと対応する．変数nextはリストを表現するために使用する．
スタックは先頭を指すポインタが必要となる．これを以下のように定義した．変数headは0からM以下の数値が代入される．
typedef Lfstack {
int head; // head of lfstack, which is the mem array index.
}図で一例を表現すると以下のようになる．
head=2
| | 2 |
|--> |------|
| data |
|------| | 3 | | 1 |
| next | -> |------| |->|------|
| 3 | | data | | | data |
|------| |------| | |------|
| next | -| | NULL |
| 1 | |------|
|------|
スタックにデータを積む側の処理である．malloc()でメモリを獲得する．これはmem配列のインデックスを獲得することになる．その後，自分のpidを元にしてデータを獲得したメモリに代入する．
その後はatomic_load()とatomic_compare_exchange()によるスタックへのプッシュ処理のリトライループを行う．
proctype producer() {
int addr;
int orig;
int next;
int i = 0;
bool suc = false;
malloc(addr);
mem[addr].data = _pid + 100;
produce_again:
// lock-free push
atomic_load(orig);
mem[addr].next = orig;
compare_and_swap(orig, addr, suc);
if
:: suc == false ->
goto produce_again;
:: else -> skip;
fi;
}スタックからデータを下ろす側の処理である．atomic_load()とatomic_compare_exchange()によるスタックからのポップ処理のリトライループを行う．成功後は，メモリ領域を解放する．
proctype consumer() {
int orig;
int next;
bool suc = false;
consume_again:
// lock-free pop
atomic_load(orig);
if
:: orig == NULL -> goto consume_again;
:: else -> skip;
fi;
next = mem[orig].next;
atomic_compare_and_exchange(orig, next, suc);
if
:: suc == true ->
free(orig);
:: else -> goto consume_again;
fi;
}プロセスは，atomic_load()とatomic_compare_exchange()を利用する．これらは以下のように表現した．
inline atomic_load(_cur) {
d_step {
_cur = lfstack.head;
}
}
inline atomic_compare_and_exchange(_old, _new, _suc) {
d_step {
if
:: _old == lfstack.head ->
assert(_new != -1);
lfstack.head = _new;
_suc = true;
:: else -> skip;
fi;
}
}C言語のものとほぼ変わらないため，この段階で特筆すべき点はないだろう．構文d_stepを用いて不可分操作を表現することができる．
malloc()とfree()は以下のように表現した．
inline malloc(_addr) {
d_step {
do
:: i < M ->
if
:: mem[i].refc == 0 ->
mem[i].data = 0;
mem[i].next = NULL;
mem[i].refc = 1;
_addr = i;
break;
:: else -> skip;
fi;
i = i + 1;
:: else -> break;
od;
}
}
inline free(_addr) {
d_step {
assert(mem[_addr].refc == 1); // detector of double-free
mem[_addr].data = 0;
mem[_addr].next = NULL;
mem[_addr].refc = 0;
}
}今回は，malloc()とfree()そのものは検証の対象でないこともあり，不可分な形でなるべく簡単になるように表現した．malloc()は配列の先頭から空きスロットを探して，そのインデックスを返す．free()はmalloc()したときのインデックスを渡すだけである．
Mの値は起動するプロセスすべてがmalloc()に成功するように設定する．これにより，malloc()の失敗は考えず，モデルを単純化でき，結果の検証を行いやすくする．
タグ付きポインタは，上記の基本となるアトミック操作のモデルに以下のように変更を加えることで実現した．#ifdef TAGPで囲ったところが追加分にである．
inline atomic_load(_cur) {
d_step {
_cur = lfstack.head;
#ifdef TAGP
// tag pointer
lfstack.tag = lfstack.tag + 1;
#endif
}
}
inline atomic_compare_and_exchange(_old, _new, _suc) {
d_step {
#ifdef TAGP
if
:: mem[_old].tag != lfstack.tag ->
goto cas_end;
:: else -> skip;
fi;
#endif
if
:: _old == lfstack.head ->
assert(_new != -1);
lfstack.head = _new;
_suc = true;
:: else -> skip;
fi;
#ifdef TAGP
cas_end:
#endif
}
}ロードのたびに，メンバ変数tagをインクリメントする．CASの際には，tagが変更されていないことを確認することで，途中で他のプロセスが割り込んでいないかを検出して，ABA問題を回避する．
ll/scによるCASのエミュレートは，上記の基本となるアトミック操作のモデルに以下のように変更を加えることで実現した．#ifdef LL_SCで囲ったところが追加分にである．
inline atomic_load(_cur) {
d_step {
_cur = lfstack.head;
#ifdef LL_SC
// actually, load shall only mark. Do not overwrite it.
lfstack.mon = _pid;
#endif
}
}
inline atomic_compare_and_exchange(_old, _new, _suc) {
d_step {
if
:: lfstack.mon == _pid->
assert(_new != -1);
lfstack.head = _new;
#ifdef LL_SC
lfstack.mon = -1;
#endif
_suc = true;
:: else -> skip;
fi;
}
}タグ付きポインタよりも簡単にモデル化できる．あるプロセスが，先頭要素をロードしたときに，自分の一意の識別子である_pidを用いてマークをしておく．これが書き換わっていないかどうかを見ることでABA問題を回避する．
なお，これはll/scによるCASをPromelaで同等の表現をするようにしたものであり，実際の動作をそのままというわけではない．実ハードウェアでは排他モニタがあるメモリに対してのload後に，そのメモリ領域について更新がないかをモニタする．store時に更新がなければstoreが成功するというものである．今回は，Promelaでは_pidを用いると一意な識別ができるため，モニタの役割をこれで担った．仮に，これをC言語で行うことはできないし，pidは識別子として弱いため破綻することに注意すべきである．また，llによるモニタは，コンテキストスイッチでクリアされてしまうが，今回は簡単のため考慮しない．
バニラ状態で実行したときの結果である．エラーが検出されていることがわかる．
pan:1: assertion violated (next!= -(1)) (at depth 52)
pan: wrote lfstack.pml.trail
(Spin Version 6.5.1 -- 29 March 2020)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 172 byte, depth reached 90, errors: 1
97185 states, stored
89174 states, matched
186359 transitions (= stored+matched)
0 atomic steps
hash conflicts: 119 (resolved)
Stats on memory usage (in Megabytes):
18.537 equivalent memory usage for states (stored*(State-vector + overhead))
16.207 actual memory usage for states (compression: 87.43%)
state-vector as stored = 147 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
144.647 total actual memory usage
pan: elapsed time 0.15 seconds
pan: rate 647900 states/second
反例出力をspin -t -p lfstack.pmlで確認すると，ABA問題が起きていることが観察できる．見やすやのため，printfでログを埋め込んでいる．atomic_loadで読み込んだ値と，CASによる更新前と更新後の値を表示した．
2: atomic_load -> 1
(省略)
1: atomic_load -> 1
(省略)
2: CAS success -> 1->2
(省略)
4: atomic_load -> 2
4: CAS success -> 2->1
(省略)
1: CAS success -> 1->-1 <- ABAが起こった！
次にタグ付きポインタのほうを実行してみる．
error: max search depth too small
Depth= 9999 States= 1e+06 Transitions= 1.67e+06 Memory= 312.714 t= 1.58 R= 6e+05
Depth= 9999 States= 2e+06 Transitions= 3.45e+06 Memory= 499.628 t= 3.31 R= 6e+05
^CInterrupted
(Spin Version 6.5.1 -- 29 March 2020)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 204 byte, depth reached 9999, errors: 0
2846812 states, stored
2357688 states, matched
5204500 transitions (= stored+matched)
0 atomic steps
hash conflicts: 110442 (resolved)
Stats on memory usage (in Megabytes):
629.864 equivalent memory usage for states (stored*(State-vector + overhead))
528.884 actual memory usage for states (compression: 83.97%)
state-vector as stored = 167 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
1.930 other (proc and chan stacks)
659.589 total actual memory usage
pan: elapsed time 5.06 seconds
pan: rate 562611.07 states/second
max search depth too smallと出ており，探索が終わっていないことが分かる．Ctrl+Cで途中で探索を打ち切ったが，エラーは検出されていない．
しかし，/a.out -m100000で探索の深さを増やすとエラーが検出される．(実際には，探索の深さを増やさなくても探索を気長に待っているとエラーが検出される．)
`
Depth= 24081 States= 1e+06 Transitions= 1.69e+06 Memory= 318.595 t= 1.57 R= 6e+05
Depth= 24081 States= 2e+06 Transitions= 3.48e+06 Memory= 505.802 t= 3.26 R= 6e+05
Depth= 24081 States= 3e+06 Transitions= 5.52e+06 Memory= 694.571 t= 5.27 R= 6e+05
Depth= 24081 States= 4e+06 Transitions= 7.42e+06 Memory= 882.559 t= 7.16 R= 6e+05
Depth= 24081 States= 5e+06 Transitions= 9.47e+06 Memory= 1072.599 t= 9.33 R= 5e+05
Depth= 24081 States= 6e+06 Transitions= 1.13e+07 Memory= 1260.684 t= 11.3 R= 5e+05
Depth= 24081 States= 7e+06 Transitions= 1.32e+07 Memory= 1449.063 t= 13.4 R= 5e+05
Depth= 25670 States= 8e+06 Transitions= 1.52e+07 Memory= 1640.079 t= 15.7 R= 5e+05
Depth= 25670 States= 9e+06 Transitions= 1.71e+07 Memory= 1829.825 t= 18 R= 5e+05
Depth= 25670 States= 1e+07 Transitions= 1.91e+07 Memory= 2019.278 t= 20.3 R= 5e+05
Depth= 69805 States= 1.1e+07 Transitions= 2.12e+07 Memory= 2214.298 t= 23.1 R= 5e+05
Depth= 69805 States= 1.2e+07 Transitions= 2.32e+07 Memory= 2403.751 t= 25.6 R= 5e+05
Depth= 69805 States= 1.3e+07 Transitions= 2.51e+07 Memory= 2594.376 t= 28 R= 5e+05
Depth= 69805 States= 1.4e+07 Transitions= 2.72e+07 Memory= 2785.099 t= 30.7 R= 5e+05
Depth= 69805 States= 1.5e+07 Transitions= 2.91e+07 Memory= 2974.161 t= 33.2 R= 5e+05
Depth= 69805 States= 1.6e+07 Transitions= 3.11e+07 Memory= 3163.614 t= 35.6 R= 4e+05
pan:1: assertion violated (loop_cnt==2) (at depth 5674)
pan: wrote lfstack.pml.trail
(Spin Version 6.5.1 -- 29 March 2020)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 204 byte, depth reached 69805, errors: 1
16007272 states, stored
15089343 states, matched
31096615 transitions (= stored+matched)
0 atomic steps
hash conflicts: 4434310 (resolved)
Stats on memory usage (in Megabytes):
3541.648 equivalent memory usage for states (stored*(State-vector + overhead))
3021.979 actual memory usage for states (compression: 85.33%)
state-vector as stored = 170 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
5.341 memory used for DFS stack (-m100000)
9.182 other (proc and chan stacks)
3164.981 total actual memory usage
pan: elapsed time 35.6 seconds
pan: rate 449011.84 states/second
タグ付きポインタは，C言語ではうまくいっていたが，実際にはバグっていたのだろうか，という疑問が出てくると思う．
これは，モデル検査の面白さの一つであるかもしれない．atomic_load()とatomic_compare_exchange_strong()の間にタグが格納できる数値の幅を超えてインクリメントされ続けると，オーバフローを起こして，一周してしまうため，CASが成功してしまうケースが論理的には考えられる．これをモデル検査は拾ってこれてしまうのである．
実は，今回のタグ用の変数の型はbyteとしたが，intにするとエラーはかなり時間をかけても検出されない．逆に，bitにするとすぐにSPINはエラーを見つけてきてくれる．
これが，現実に起こり得るかという話を考えると，タグ用の変数に十分な領域をあたえてやれば，現実的には起こりえないだろう．しかし，リスクを分析するにはモデルは有用であるかもしれない．
実行結果は以下になる．エラーは検出されない．
(Spin Version 6.5.1 -- 29 March 2020)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 180 byte, depth reached 1306, errors: 0
211898 states, stored
214341 states, matched
426239 transitions (= stored+matched)
0 atomic steps
hash conflicts: 557 (resolved)
Stats on memory usage (in Megabytes):
42.033 equivalent memory usage for states (stored*(State-vector + overhead))
35.328 actual memory usage for states (compression: 84.05%)
state-vector as stored = 147 byte + 28 byte overhead
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
163.886 total actual memory usage
unreached in proctype producer
(0 of 45 states)
unreached in proctype consumer
(0 of 36 states)
unreached in init
(0 of 40 states)
pan: elapsed time 0.33 seconds
pan: rate 642115.15 states/second
ABA問題を考えると，CASとしては，通常のバージョンよりも優れたものであると言えるだろう．
ハザードポインタをモデル化して，検証すると面白そうである． また，おそらくARMのプロセッサ上でC言語実装を動作させると，タグ付きでなくともうまく動作すると推測される．なぜなら，atomic_compare_and_exchange()がll/scを用いたもので実現されているからである（少なくとも，私が知る限り）．