TLで「Is Parallel Programming Hard, And, If So, What Can You Do About It?」 https://www.kernel.org/pub/linux/kernel/people/paulmck/perfbook/perfbook.html という本がおもしろそう、というのがまわってきた。
こういう本には珍しく形式検証を扱っている章があり、SpinLockのモデルをPromelaでコードを書いてSpinでモデル検査を行っていた。 ただそのコードがあまりいけてない書き方だったので、自分で書き直してみた。
以下のコードが書き直した内容。inline lockの中に全部いれてしまえるのならそれでいいし、active [N] proctypeで並列数を調整している。
bit mutex = 0; int sum; inline lock() { do :: 1 -> atomic { if :: mutex == 0 sum++ mutex = 1 sum-- break :: else fi } od } inline unlock() { mutex = 0 } active [3] proctype locker() { do :: lock() unlock() od }
spinはDebian系ならapt-get install spinで入れられる。
早速実行してみる。 全部で51状態、error: 0なので正しく出来ていそうだ。
$ spin -a lock.spin
$ gcc -o pan pan.c
$ ./pan
(Spin Version 6.4.6 -- 2 December 2016)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 36 byte, depth reached 43, errors: 0
51 states, stored
94 states, matched
145 transitions (= stored+matched)
17 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.003 equivalent memory usage for states (stored*(State-vector + overhead))
0.290 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
unreached in proctype locker
lock.spin:29, state 21, "-end-"
(1 of 21 states)
pan: elapsed time 0 seconds
すごい今更だけど、これってSpinLockとSpin model checkerがかけた高等なギャグなのでは…？
