「Is Parallel Programming Hard, And, If So, What Can You Do About It?」のSpinLockのPromelaのコードを書き直してみた
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がかけた高等なギャグなのでは…？
SpinlockのExponential Backoff実装について
SpinLockのExponential Backoffアルゴルズムの実装を少し調べた.
ParkingLot (WebKit,C++)
https://webkit.org/blog/6161/locking-in-webkit/ という素晴らしいブログ記事で spinning という節で触れている. どうやら JikesRVM というJVM実装に由来するようだ.
また本文中で Intelのpause命令に触れている箇所 があるが, どうも思うような性能が出なかったようだ. ParkingLotのSpinLockではマイクロベンチで性能のよかったsched_yieldを使った実装になっている.
Finally, it’s clear that the x86 pause instruction is not useful for our spinlocks. Intel shows that it is a speed-up, but we cannot confirm their claim.
parking_lot (Rust)
spinwait というところで実装されている.
Rustの実装ではIntelのpause命令を用いている.
corssbeam-channel (Rust)
crossbeam-channelでは parking_lot のspinwaitは使わず独自で実装している. といっても spin_loop_wait はx86のpause命令を使っているし yield_now は sched_yield なのでカウンタの値による分岐が違っているくらい.
どうやら parking_lot でされている話が元で実装されているようだ. https://github.com/Amanieu/parking_lot/issues/43
本家の方は追随しないのだろうか.
DockerとD言語のイメージ
そろそろDockerをまじめにやらないといけなくなってきた。D言語は飾りです。
まずは試す
準公式？のDockerイメージがあるのでpullしてくる。
$ docker pull dlanguage/dmd (...)
README にあるとおりに試す、ファイル名だけかえて hello.d というファイルを作成しておく。
Dockerfileの内容をみるとベースはUbuntu16.04だった。
コマンドを試すと、あっさりと動いた。
$ docker run --rm -ti -v $(pwd):/src dlanguage/dmd dmd -run hello.d Hello
イメージのサイズをみると614MBほど。
$ docker images| grep dlang dlanguage/dmd latest 51a13a70578f 3 weeks ago 614MB
生成した成果物をローカルに残したかったら -w オプションを使う。
ここでは生成したバイナリはrootユーザ権限で作成されている、カレントのユーザに変更したければ --user $(id -u):$(id -g) をつける。
$ docker run --rm -ti -v $(pwd):/src -w /src dlanguage/dmd dmd -c hello.d $ ls -a ./ ../ hello.d hello.o
dubを使ったビルドもできる。
$ dub init -n dockertest && cd $_ (...) $ docker run --rm -ti -v $(pwd):/src -w /src dlanguage/dmd dub build --build=release Performing "release" build using dmd for x86_64. dockertest ~master: target for configuration "application" is up to date. To force a rebuild of up-to-date targets, run again with --force. $ ls dockertest* dub.json source/ $ ./dockertest Edit source/app.d to start your project.
ひとこと
Dockerに対してまだどういう使い方するのかいいのかイメージが沸いてない部分がある。(Dockerだけに、ね)
DCDのめも
多くの言語と同じようにD言語にもコード補完ツールがあり、DCDという。
コード補完ツールは基本の仕組みはほぼほぼ同じなのだが、それなりに個性があったりする。
例えばコンパイラがライブラリとしてパーサを提供していてそれを使っているもの(RustのracerやGoのgocode、Nimのnimsuggest)、別にあるパーサライブラリを使っているもの(Pythonのjediが使っているparso)といった違いがある。DCDは後者に属しており、dsymbol/dparseというライブラリを使っている。このあたりのライブラリをまとめて作っているのがhackerPilot氏である。
DCDの特徴として
- クライアント-サーバモデル、クライアントがコマンドを投げてサーバが結果を返す仕組み
- 通信はUNIXドメインソケット通信(posix)かTCPソケット通信(Windows)
- 通信のメッセージはMessagePackにより圧縮されている
- 補完以外にもddocの情報をとってこれるようになっている
- 補完候補を探す対象モジュールをパスを追加することで増やすことができる(減らすことは現状できないようだ)
- サーバ側ではidentifierやモジュール名をキャッシュする仕組みがある
などが挙げられる。
あとDCDは機能的には結構シンプルで、racerやnimsuggestのようなgoto-definitionの機能はない。tagsでいいじゃんということだろうか。
※追記
company-dcdはgoto-definitionの機能を持っていて、どうやってるのだろうと思ったが dcd-clinet --symbolLocationでうまいこととれるようだ。getSymbolsByTokenChainあたりを読めばわかりそうだがめんどくさくなったので打ち止め。
Dで生成したバイナリ自身のシンボルをみる
完全ではないが、モジュール情報や関数名や型情報などは .symtab をみればとれる。もう少しまじめにsections_elf_shared.dを読めば意味のあるものになるかもしれません。
import core.demangle; import std.algorithm : map; import std.file : thisExePath; import std.format : format; import std.range : walkLength; import std.stdio; import elf; void main() { auto bin = thisExePath; ELF elf = ELF.fromFile(bin); ELFSection s = elf.getSection(".symtab"); writeln(" Symbol table .dynsym contains: ", SymbolTable(s).symbols().walkLength()); writefln("%-( %s\n%)", SymbolTable(s) .symbols() .map!(s => "%s\t%s\t%s".format(s.binding, s.type, demangle(s.name)))); }
今回はelf-dというライブラリを使用している。これはELFフォーマットのパーサ+一部DWARF(.debug_abbrevとか.debug_lineとか)あたりをサポートしている、Dでは貴重な静的ライブラリを扱うためのライブラリなんですがDWARF対応が中途半端なので本格的にごにょごにょやろうと思うと.debug_infoというかcompilation unitsを自前でがんばる、みたいになるのでかなりめんどくさい。Rustはgoblin/gimli-rsあってこのへんやるのに向いてるような気がする。Sentryとかでも利用実績あるしなあ。。
D言語の数値まわりの字句解析のはなし
仕様はここにある https://dlang.org/spec/lex.html#Integer
これをみると、 0b_ はBinaryIntegerとして表現可能なリテラルとなる。
import std.stdio; void main() { writeln("0b_: ", 0b_); writeln("0b________: ", 0b________); // _ がいくつあってもよい }
結果は _ が何個あっても0になる。
(dmd-2.076.1)$ rdmd bin.d 0b_: 0 0b________: 0
しかし、 BinaryIntegerは 0b だけでも評価できてしまう。そのためこんなコードもコンパイルが通ってしまう。
import std.stdio; void main() { writeln("0b: ", 0b); writeln("0buL: ", 0buL); }
結果はやはり0となる。
(dmd-2.076.1)$ rdmd bin.d 0b: 0 0buL: 0
また、 0x_ は HexadecimalInteger として表現できないリテラルであるが、実際にはコンパイルできてしまう。
import std.stdio; void main() { writeln("0x_: ", 0x_); }
0b_ 同様、結果は値0となる。
(dmd-2.076.1)$ rdmd hex.d 0x_: 0
こちらも 0x や 0xuL のようなコードが実行できる。
import std.stdio; void main() { writeln("0x: ", 0x); writeln("0xuL: ", 0xuL); }
結果:
(dmd-2.076.1)$ rdmd hex.d 0x: 0 0xuL: 0
社内勉強会でD言語とマイコンのはなしを発表した
Q&A
- 組込みでDを使うメリットがあまりなかった、Rustのほうが筋がいいのでは？
- たしかにそうなんですよね
- Cのライブラリを使わなかったのはなぜ？
- プリプロセッサマクロがふんだんに使われているので、どうせなら全部自前で実装したほうがはやかった
雑談
ちょっと話をどうふるべきか迷った感がある。メモリ安全も例外もラインタイムも標準ライブラリもない状態なのでエレガントにコードが書けるよ、みたいなのに全般的にふるべきだった気が。やはり文字列ミックスインは強力。
GC
そもそもGCは組み込み向きではないので、どうしたものかな。組込み向けのGCを作ればいいんじゃないか、という話があるがなんにせよ優先度は下がりそう。
例外
クラスベースの例外システムはほんとうに欲しいものなんだろうか。 それと例外の実装そのまま流用するのはdruntimeのオレオレ実装にしろucontext(3)にしろsetjmp(2)/longjmp(2)にしろaltstackを用意して、という話なので組込みと相性悪いんじゃないかと思っている。 assertくらいはほしくて、ユーザ定義な例外ハンドラに飛ばせるように、というイメージ。
ランタイム
GCも例外もランタイムなのだが。。まあdruntimeをそのままもってくるのはできないという話。少なくとも__tls_getaddr相当のものを実装する必要がある。libcに依存してしまえばいいのでは、というのもあるがその場合でもdruntime側にそうとう手を入れる必要があるので、なんともなあ。。
標準ライブラリ
標準ライブラリはアーキテクチャサポートの問題、libc依存の問題、バイナリサイズの問題、だいたいの実装でヒープが必要(これは実装すればいいだけ)な問題がある。全部サポートする気はないけどstd.mathはほしい。
