2020-12-01

並行システムの検証と実装を読んだ

序

CSP(Communication Sequential Process)というプロセス代数とそれに基づいた形式手法の本を読みました。頑張って読んだので紹介します。
CSPは並行計算をラベル付き遷移システムで表現した上で(これをプロセスという)、どのような遷移がありうるのか、プロセス間の遷移(の集合)にどのような関係(e.g. 詳細化関係)があるかを議論する枠組みです。
自動検証器の実装がいくつか知られていて、この本ではFDRを使ってモデリングと検証を行う方法が説明されています。

並行システムの検証と実装：形式手法CSPに基づく高信頼並行システム開発入門トップエスイー実践講座

作者:磯部祥尚
発売日: 2018/03/23
メディア: Kindle版

この本はCSPというプロセス代数の一種と、その理論に基づく検証手法と検査器について説明している教科書です。
トップエスイーで使っているようです。ほとんど前提知識は不要です。
読み切るとCSP(m)の簡単な構文と意味が頭に入り、実際に使える検証器であるFDR4も使えるようになります(文中で説明されるのはFDR2なので大分趣が変わりますが簡単に対応は付きます)。

書評

全体について

インクルーシブで前提知識がほとんど要らないのが良いです。Javaが読めることくらいでしょうか。
また同じ前提から導出されますが、本文中で説明する気のない無意味に高度なトピックや定理に触れたりしないのも良い点です。書いてあることは全部本の中で完結します。快適。
関連する話題として、練習問題がちゃんと練習になっており、ちゃんと解答があるのも良い点です(当たり前だとは思ってるけどこの手の教科書には期待出来ないので)。

各章について

まず5章と6章が読んでいて楽しいです。
形式的な遷移規則を使って遷移の導出をする説明がされ、詳細化関係についても定義が形式的に提示されるので分かり易いです。
またそれらを使ってどういう手順で証明をするのかについて繰り返し説明があるので、読んでちゃんと手順をなぞるだけで(大体)頭に入ります*1。
ただCSP規則(書き換え規則？)を用いた等価関係の証明については一部の規則が提示されるだけでさほど説明は無いのがやや残念でした。
(この本の主眼はFDRを用いた詳細化関係の検証なので構成上は妥当)

4, 8, 9, 10 章(全体で10章の構成)はJCSPというJavaライブラリを使ってCSPで記述したモデルをJavaで実装する方法を説明しています。
多分トップエスイーでは検証と実装が繋がっていることをちゃんと示さないといけないでしょうから仕方無いんですが、やや多いですね。
単にライブラリの使い方を説明しているわけではなく、実装するに際して発生しうる問題に対応するモデリングの方法論やテクニックが述べられてはいます。
また、タイムアウトや割り込み演算子など理論の章では扱っていないものについても適宜紹介されていて興味深いです。

が、JSCP というライブラリはメンテされているのかすらよく分からない様子で、公式サイトにもほとんどリポジトリへのリンクがあるだけです。
ライブラリという面から見ると本気で使わせるつもりがあるのか疑問という感じです。
こういう状態に加えて、理論には含まれていない実装における制約がいくつもあり(選択の可否とか送受信する値の型とか、ガードに使えるか否か、etc...) 少し読むのがツラかったです。
実装に直接対応取りたい人は興味のあるところだとは思います。

まとめ

全体として良い本です。
まず独学で読み通せるというのがポイント高いです。
また一貫して似たような例の変種を丁寧になぞって説明してくれるので、「先の例と同様なので自明。オワリ。」みたいな箇所も皆無で躓きづらいだろうと思います。

正誤表

読む過程で見つけたエラッタを書いておきます。私が読んだのは初版(2012/12/31)。

セクション	ページ	誤	正(多分)
5.3.1	p.160	次のように定義されているする	定義されているとする
5.3.1	p.163	視覚的に確認するツールPorBE	視覚的に確認するツールProBE
7.4.3	p.248	Counter(a, b) は	Counter(a, d) は
7.4.3	p.248	上司への支払い指示 tell.N と	上司への支払い指示 bill.N と
7.4.3	p.253	1番目のコイン Crypt(1) を	1番目のコイン Coin(1) を
10.2.2	p.324	length(s^t) <= Size	length(s^t) <= size

*1:ホントか？

2020-08-20

SML#のDockerイメージが全種揃った

SML docker

eldesh/smlsharp で公開しているSML#のdockerイメージがあります。
最近必要になってバージョン1 系列(1.0.0, 1.0.1, 1.0.2, 1.0.3, 1.1.0)を追加しました。

今月初め頃 0.90 をビルドしてあったため、
これで現時点でのリリースを全種揃えたことになりました。

2020-07-26

SML/NJのdockerイメージをマルチアーキテクチャ対応した

SML docker

私が個人的に管理しているsml/njのdockerイメージを linux/amd64 と linux/386 のマルチアーキテクチャ対応しました。

以下のページでタグを確認すると、linux/amd64 と linux/386 という種類が表示されると思います。

> eldesh/smlnj/tags

使用方法

使用するにはそれぞれのアーキテクチャのLinuxホストから任意のイメージをpullするだけ、つまり普通に使うだけです。
amd64版の方は全て 32/64bit モード両方でビルドしてありますので、sml -32(or -64) とすることで32bitモードでも使うことができますが、これは非ネイティブ動作(らしい)なので注意です*1。

仕組み

docker registry は、各イメージ名に manifest というメタデータを関連付けており、ここに対応アーキテクチャ(やプラットフォーム)も含まれています。
ですので docker cli から適切なアーキテクチャを指定すればそのレイヤーがダウンロード出来るというワケです。

以下のように確認出来ます。(manifest は実験的な機能なので明示的に有効にしてやる必要があります。)

$ DOCKER_CLI_EXPERIMENTAL=enabled docker manifest inspect eldesh/smlnj:latest
{
   "schemaVersion": 2,
   "mediaType": "application/vnd.docker.distribution.manifest.list.v2+json",
   "manifests": [
      {
         "mediaType": "application/vnd.docker.distribution.manifest.v2+json",
         "size": 1157,
         "digest": "sha256:86983a83d1ef042bd3dbc1e013dad7845a566dc2afc3e52c17582f993a626af7",
         "platform": {
            "architecture": "386",
            "os": "linux"
         }
      },
      {
         "mediaType": "application/vnd.docker.distribution.manifest.v2+json",
         "size": 1158,
         "digest": "sha256:6d93f94070bf7877595f143f7f2ae7b3488e3740b2da35db17362a614f310a05",
         "platform": {
            "architecture": "amd64",
            "os": "linux"
         }
      }
   ]
}

*1:これに注意すべき人存在する気がしないけど

2020-06-09

SMLUnitをPoly/MLに対応した

SML PolyML

SMLUnitというSML用ユニットテストライブラリをPoly/ML5.8から使えるようにしました。
makeと上手く連携するMakefileが書けたので満足です。
ブランチはここ> https://github.com/eldesh/SMLUnit/tree/support/polyml *1

使い方はReadmeに書いたけど、Poly/MLの機能の解説もしつつここにもまとめておこう。

使い方

まずREPLでの使い方。

Poly/MLは PolyML.make: string -> unit という関数にディレクトリ名を与えると、そのディレクトリ以下の ml_bind.ML みたいな名前のファイルを探してきて読み込みます。
さらに ml_bind.ML の中で structure, signature, functor に言及すると、それらと同名のファイルを探してきて読み込みます。
ちゃんとmakeなので(？)2回目以降は前回読んだ時から更新されたファイルだけ読み込んでくれるので便利です。

SMLUnit$ poly --eval 'PolyML.suffixes := ".sig"::(!PolyML.suffixes)'
> PolyML.make "src/main";
Making main
Making SMLUnit
..
structure SMLUnit: SMLUNIT
val it = (): unit

--eval には PolyML.make が探すファイル名の拡張子を追加するコードを渡しています。
こうしておくと未知のシグネチャ名に言及したときに .sig ファイルも探してくれます。

ビルド

SMLUnitはユニットテストライブラリなので当然他のライブラリからも参照したいですね。
でも実はPolyML.makeは、その時点でのカレントディレクトリからの相対パスでファイルを探すので*2、無関係なディレクトリから参照しづらいという問題があります。
そこでコンパイルした結果をモジュールエクスポートという機能を使って書き出しておきます。

SMLUnit$ make -f Makefile.polyml
echo "" | poly -q --error-exit --eval 'PolyML.suffixes := ".sig"::(!PolyML.suffixes)' \
        --eval 'PolyML.make "src/main"' \
        --use export.sml \
        --eval 'PolyML.SaveState.saveModule ("libsmlunit.poly", SMLUnit)'
Making main
Making SMLUnit
..
Created structure SMLUnit

デフォルトターゲットをmakeすると、PolyML.SaveState.saveModuleを使ってSMLUnitの公開するモジュールが ./libsmlunit.poly に書き出されます。
このファイルは普通にREPLからも読めますのでライブラリのデバッグなどに便利です*3。

> PolyML.loadModule "./libsmlunit.poly";
signature ASSERT =
  sig
..
signature TESTRUNNER =
  sig type parameter val runTest: parameter -> Test.test -> unit end
val it = (): unit

(他ライブラリからの)使い方

Poly/MLでプログラムの最終結果(実行ファイル)を得るには、まずPolyML.export: string * (unit -> 'a) -> unitという関数に適切なオブジェクトファイル名とエントリーポイントになる関数(要はmain関数)を渡します。
その際あらかじめ依存しているライブラリ(libsmlunit.poly)をロードしておきます:

> PolyML.loadModule "/path/to/libsmlunit.poly"; (* 依存している SMLUnit を読み込む *)
> PolyML.make "hoge/src"; (* 利用側のコードを読み込む *)
> PolyML.export ("libhoge.o", Main.main); (* main: unit -> unit をエクスポート *)

そしてエクスポートしたオブジェクトファイルをpolycコマンドでリンクして完了です。

$ polyc -o hoge libhoge.o
./hoge
..

*1:まだ先にやりたいことがあってマージはしてない

*2:これは今読んでいるファイルからの相対パスに修正するべきだと思う

*3:この形式でビルドされるライブラリが存在すれば。。。

2020-02-23

SML# 版 AObench をMassiveThreadsで高速化

SML

前回*1はちょっとケチが付いてしまいましたが、今回めげずに AObenchSML の SML# 版に MassiveThreads による並列化版を追加しました。
シングルスレッド版と並列化版を両方実行します。
並列forを実装して並列ML: MaPLe で AObench を高速化で作ったものと全く同じコードで動くようにしました。

パフォーマンス

私の環境で一番良かった並列化パラメータでの結果を載せます。

環境: Linux(amd64) VMWare 4core 8GB MEM

	real	user	sys
sml#(シングルスレッド)	0m13.872s	0m9.969s	0m1.442s
sml#(4プロセス並列化版)	0m5.739s	0m19.625s	0m1.978s

2.4倍に速くなりました。ちゃんと並列化できてるようですね。

並列化の粒度調整

MaPLeと同じくSML#の場合もプロセス数と粒度をそれぞれ指定する必要がありました。
よさそうな組み合わせを探したときのログを簡単に可視化したものを以下に示します*2。

AObench SML# 3.5.0 MassiveThreads 並列化版のパフォーマンスグラフ — AObench SML# 3.5.0 MassiveThreads 並列化版のパフォーマンス

x軸が MYTH_NUM_WORKERS で y軸が粒度(1スレッド内で何行計算するか)、カラーバーは実行時間(秒)です。
並列度が高くても粒度が大きすぎるとパフォーマンスが劣化していることが分かりますね。今回のケースではコアと同数のプロセス、2行(512ピクセル)分の粒度がもっとも良かったようです。

終わり

今回のケースでは(エンジニア的センスで)適当に指定してもシングルスレッド版より遅くなることはあまり無さそう
とりあえず粒度を小さくしておいても問題無さそうなので手軽に使えそう
- MaPLe版である程度調整済みだったので無駄な試行が少なかったのもある
実験中パフォーマンスのばらつきが結構あったのはparfor内でjoinしているのが遅いのかも知れない

*1:SML#のプログラムにMassiveThreadsのオプションを付けるとパフォーマンスが低下する

*2:各頂点間の平均を取ってる色らしいので本当はあんまり良くない

2020-02-17

SML#のプログラムにMassiveThreadsのオプションを付けるとパフォーマンスが低下する

SML

SML# には最初からユーザレベルの細粒度スレッドライブラリ MassiveThreads のラッパーが提供されています。
Myth ストラクチャを使ってプログラムを書き、環境変数 MYTH_NUM_WORKERS で仕様コア数を指定するようです。
> 11.2 MassiveThreadsを用いた細粒度スレッドプログラミング‣ Chapter 11 SML#の拡張機能：マルチスレッドプログラミング ‣ Part II チュートリアル ‣ プログラミング言語SML#解説

この環境変数を通常のシングルスレッド向けの AObenchSML で設定みたところ、パフォーマンスが 60% ほど低下しました。

$ time ./aobench-smlsharp aobench-smlsharp.ppm

real	0m11.233s
user	0m9.969s
sys	0m1.417s

$ time MYTH_NUM_WORKERS=0 ./aobench-smlsharp aobench-smlsharp.ppm

real	0m18.210s
user	1m10.984s
sys	0m2.163s

4コアの環境で実行しています。user(CPU時間)ではちょうど 18.210s * 4 ≒ 1m10.984s ですね。
ランタイムの何かが無駄に同期しているんでしょうか？謎です。

2020-02-13

並列ML: MaPLe で AObench を高速化

SML

POPL2020 で新しい並列ML(MaPLe)(略称: MPL)の提案がありました。
正確に言うと言語の提案じゃ無くて、「並列プログラムの性質を表す(良い)性質 Disentanglement Property を提案したので、その良さ(= 並列プログラムの実行効率)を示すための処理系を作って公開しました」というモノ。

(珍しいことに)あっさり手元で動いたので AObench-SML に追加してベンチマークを取ってみました。
ただしこの処理系の持つ並列プリミティブは正しく使わないとクラッシュするので実用するものではありません*1。

AObench はピクセル毎に並列化しやすく、ループ毎に配列の互いに異なる領域に書き込むアルゴリズムなのでMPL(というかDisentanglement)の役立つ形の処理にかなりよくマッチしています(多分)。

ベンチマーク結果

実際のベンチマーク結果を以下に示します。

Linux(amd64) VMWare 4core 8GB MEM

処理系	real	user	sys
gcc	0m0.732s	0m0.718s	0m0.012s
mlton	0m1.589s	0m1.579s	0m0.008s
mpl	0m0.398s	0m1.523s	0m0.016s

MPLについてはユーザがプロセス数を指定する必要があるため、以下のようにコア数と同じ procs 4 を指定しています。
(後ろの 4 は後述する並列粒度指定。実験的に求めた値。)

./aobench-mpl @mpl procs 4 set-affinity -- aobench-mpl.ppm 4

この処理系は MLton を拡張して実装されているので並列化しない場合は素の MLton と同じパフォーマンスが出ます。
今回はちょうど(プロセス数と同じ)4倍速になってますね。

変更箇所

主な変更箇所を解説します。

まず以下の部分。
ライン毎のループを ForkJoin.parfor に換えています。粒度とループ範囲を与えるだけで並列化完了です。
この粒度は上で示したコマンドライン引数から渡される 4 で、この範囲(つまり f n .. f (n+3) を実行する範囲)では各スレッド内でシーケンシャル実行されます。
ここで渡す関数が並列実行されます。

<       for {begin=0, limit=h, step=succ} (fn y=>
---
>       ForkJoin.parfor grain (0, h) (fn y =>
>         let val drand48 = mk_rand (48271 + y) in

for から parfor への変更だけだと乱数生成の部分がスレッド間で共有されてしまい速度が出ませんでした*2。
そのため以下のようにクロージャを作る関数を定義し直して使用するようにしました。

<   local
<     val rand = Random.rand (48271, Option.getOpt (Int.maxInt, 1073741823))
<   in
<   fun drand48 () = Random.randReal rand
<   end
---
>   fun mk_rand seed =
>     let
>       val rand = Random.rand (seed, Option.getOpt (Int.maxInt, 1073741823))
>     in
>       fn () => Random.randReal rand
>     end