SML のドキュメント生成ツール SMLDoc をサルベージした
SMLDoc は SML# プロジェクトの一部として開発されていたドキュメント生成ツールです。
SMLコードのコメント中に書いた内容を、そのコメントに対応するエンティティに紐付けて表示するようなHTMLを生成します。
昔の SML# には SMLDoc が同梱されていましたが、.smi ファイルが必要になったタイミングで(?)提供されなくなっていました。
今回 SML# 0.9 から取り出してきたコードを SML/NJ と MLton でビルド出来るようにして smlsharp/SMLDoc に公開しました。
インストール
以下のようにするとビルド;インストール出来ます*1。
// MLtonの場合は // export MLB_PATH_MAP=/path/to/mlb-path-map $ make -f Makefile.(smlnj|mlton) install
Example
実際の生成例は公式サイトにあります > SMLDoc/doc/api。
自分で生成してみたい場合は smldoc-doc
ターゲットを実行するとこれと同じHTMLが doc/smldoc
以下に生成されます。
$ make -f Makefile.(smlnj|mlton) smldoc-doc
(実はサルベージした方のプロジェクトでは Basis ライブラリのエンティティにも正しくリンクできている点が違ったりします。int
型とかクリックしてみると分かります。)
使い方
コメントを書く
例えば関数のパラメータについての説明なら@param
と書いて名前と説明を書きます。
私の作っている SHA3 の実装 ではこんな風に書いてあります。
(** * Hash a string * * @params kind m * @param kind kind of hash * @param m input message string * @return hashed string *) val hashString : Sha3Kind.t -> string -> t
まぁ見たままですね。
詳しい使い方は OVERVIEW_ja.txt を見て下さい。
SMLUnit のインストールを統一して簡潔にした
SML用のユニットテストライブラリとして SMLUnit というライブラリがあります。
SML# プロジェクトの一部として開発されたようですが、現在は SML# 以外の処理系向けのコードは独立したリポジトリで管理されています。
現在対応している処理系は以下の4つです。
- SML#
- SML/NJ
- MLton
- Poly/ML
SML#については処理系のリポジトリに含まれているのでオマケです。
その他3つの処理系については対応はしていましたが、インストール方法が煩雑で手動で行う操作が多く要求されていました。
今回以下の3つのPRによって Makefile を追加、改良し、手順が統一的かつ簡潔になりました。
SML/NJ、MLton、Poly/ML いずれについても以下の形式でビルド、インストール、テストの実行が可能です。
$ make -f Makefile.[smlnj|mlton|polyml] [ smlunit-lib | smlunit-lib-nodoc | doc | install | install-nodoc | test | example ]
SML/NJ の pathconfig と MLton の mlb-path-map のエントリ追加については柔軟性が高すぎて Makefile で行う範囲を超えていると判断したため手動ですが、install ターゲットのメッセージとしてヒントを出すようにしたので考えることは減ったと思います。
SMLUnit$ make -f Makefile.smlnj install-nodoc PREFIX=~/.sml/smlnj/110.99 .. (snip) .. val it = true : bool - ================================================================ smlunit-lib has been installed to: /home/eldesh/.sml/smlnj/110.99/lib/smlunit-lib.cm Next, add an entry to your pathconfig (e.g. ~/.smlnj-pathconfig) such like: smlunit-lib.cm /home/eldesh/.sml/smlnj/110.99/lib/smlunit-lib.cm Then you can load the library like - CM.make "$/smlunit-lib.cm"; ================================================================
SMLでSHA3を実装しました
SHA(3)はNISTが定めたセキュアなハッシュアルゴリズムの標準規格です。
今回SHA2のSML実装に続きSMLでSHA3を実装し、SHA3SMLとして公開しました。
現在のところSML/NJ 110.99で動作を確認しています。
実装状況
SHA3SMLは直接FIPS 202を確認して実装しました。
以下に対応状況を示します。
SHA3にはSHA2と同じく4つの出力ビット幅によるバリエーションが用意されており、SHA3SMLはこれらには全て対応していますが、SHAKE は未実装です*1。
SHA3-224 | SHA3-256 | SHA3-384 | SHA3-512 | SHAKE128 | SHAKE256 | |
---|---|---|---|---|---|---|
実装 | ✅ | ✅ | ✅ | ✅ |
(SHAKE というのはハッシュ関数ではないものの、他の関数と同じくFIPS202で定義されておりハッシュを一般化したような関数です。)
またNISTは、ある実装がFIPS 202に適合しているかのテスト方法をSHA3VSとして公開しています。ここでは以下のような実装の制限についても定められていますが、SHA3SMLではどれも対応済みです。
✅ 空入力のサポート
✅ バイト指向入力のサポート
✅ ビット指向入力のサポート
インストール方法
ml-makedepends
を使うと依存関係が取得出来ることに気付いたので Makefile を書きました。なので普通に make install
出来ます。
ただし PATHCONFIG ファイルはどこに置くか人によるため Makefile を複雑にするより手動に任せることにしました。
$ make install PREFIX=~/.smlnj (* ..snip.. *) ================================================================ libsha3sml has been installed to: /home/eldesh/.smlnj/lib/libsha3sml.cm Add an entry to your pathconfig (e.g. ~/.smlnj-pathconfig) such like: libsha3sml.cm /home/eldesh/.smlnj/lib/libsha3sml.cm Then you can load the library like "CM.make "$/libsha3sml.cm";". ================================================================
make install
すると上記のようにメッセージが出るので(例えば)以下のように PATHCONFIG ファイルに追記します。
$ echo "libsha3sml.cm /home/eldesh/.smlnj/lib/libsha3sml.cm" >> ~/.smlnj-pathconfig
使い方
いつも通り普通に CM.make
するだけです。
$ sml - CM.make "$/libsha3sml.cm"; (* ..snip.. *) - Sha3.toString (Sha3.hashString Sha3Kind.Sha3_256 ""); val it = "A7FFC6F8BF1ED76651C14756A061D662F580FF4DE43B49FA82D80A4B80F8434A" : string
念のためsha3sumコマンドで確認します。
$ echo -n "" | sha3sum -a 256 | tr [:lower:] [:upper:] A7FFC6F8BF1ED76651C14756A061D662F580FF4DE43B49FA82D80A4B80F8434A -
一致してますね。
テスト
NISTの提供している入出力例と適合試験 CAVP のテストベクタを全てパスすることを確認しています。
手元で実行するには make test
します。
終わりに
SHA3はSHA2に比べて非常に簡単な構造で実装し易かったです。
例えばSHA2には内部的に用いるナゾの数値テーブルがビット幅ごとに用意されているんですが、SHA3にはその類いのマジックナンバーは全くありません。
また規格の文書自体もかなり読みやすく書かれていると思います。
SMLのプロジェクトとしては、NJ向けの Makefile
が書けるようになった点が収穫でした。
これで .cm/
をコピーとかする必要が無いのでユーザとしても*2大分手間が省けます。
リンク
並列ML: MaPLe v0.2 がリリースされていた
POPL 2021 の論文 Provably Space-Efficient Parallel Functional Programming が出たのに合わせて2020年末*1にMaPLe v0.2 がリリースされていました。
前回の POPL の時は aobench を動かす記事 並列ML: MaPLe で AObench を高速化 を書きました。
MaPLe(mpl) は並列実行のために改良が加えられたML処理系(いわゆる Parallel ML)の一つで、処理系の提供する並列実行用関数を使うとスレッドを良い感じに割り当ててマルチコアを使うことが出来るようになることを目論んでいます(多分)。
v0.2 で提供される主なプリミティブは以下のようなもので、
signature FORK_JOIN = sig val par: (unit -> 'a) * (unit -> 'b) -> 'a * 'b val parfor: int -> (int * int) -> (int -> unit) -> unit end
これは v0.1 と変わらず、これまでと全く同じコードが動きます*2。
改良点
v0.2 での改良点は、ヒープアロケータをスレッドスケジューラと統合したことと、メモリ使用量の上限の理論的上限を与えたことです。
v0.1 では回収出来ないメモリがスレッド内に積み上がる可能性があったのを回避出来るようになりました。
これによって論文中のベンチマークでは最大メモリ使用量が大幅に減っており、シングルスレッド実行の場合でも MLton に対して顕著に最大メモリ使用量が減っています。
並列化したことによって(無駄にメモリ使用量が膨らんで)メモリ律速になることが避けられそうですね。
ただし、替わりに(?)実行時間は数%低下しているようです。
ベンチマーク(AObench)
毎度おなじみ AObench を動かして再現実験してみます。前回と全く同じVM環境上で動かします。
実行時間
処理系 | real | user | sys |
---|---|---|---|
gcc | 0m0.870s | 0m0.876s | 0m0.004s |
mlton(20201002) | 0m1.827s | 0m1.836s | 0m0.012s |
mpl(20201216) | 0m0.477s | 0m1.855s | 0m0.017s |
MPLは前回よりやや遅くなっていますが、論文中でも実行時間は前回リリース時点に比べてやや(n < 10%)悪くなっていますので順当な結果と言えそうです。
他の処理系でもやや処理が遅くなってますのでむしろ実行環境の方が心配されますね。。。(ストレージがヘタって来てるかな…)
MDN の JavaScript building blocks を読み終えた
前回 に引き続き JavaScript の構成要素 を読みました。
- if, for, while, イベント, イベントリスナ、イベントハンドラ などが導入されました。
- 文中の練習問題はテキストエリアに入力されたコード片がインタラクティブにその場に反映されるというものなのですが、for文を書く順番によっては書いている途中でvalidなコードになって無限ループでページ全体がstuckするのはちょっと面白い*1。
- 内容は簡単ですが、説明無しに導入される単語があり相変わらず素人には勧められない。
- DOM とか Web API みたいな用語も知らないうちに導入された気がした。
- 和訳がだんだん酷くなってきてます。そろそろ怪しげな *訳し手* の能力を超えてきた感。日本語単体でもvalidな文を成してない。数学用語とかは特に酷いです。
*1:これは嫌味ではない
MDN の JavaScript First Steps を読んだ
JavaScriptを勉強することにしました。
ECMAScriptという名前で呼ばれていない時点で気にくわないものであることは確定なんですが、学ぶのが妥当という判断になってしまいました。
まずMDNのJavaScriptの第一歩という教材を一通り読んで課題をやりました。
JavaScriptについては本当に何も知らないので素人向けの文書から読んでみたんですが、流石に冗長すぎました。
以下に気になったことをメモしておきます。
- プログラミング初心者にJavaScriptを教えるという体の文章ですが、真にド素人の状態でこれを読んだとすると、相当筋の良い人でないと書いてあることを理解することは出来ないと思います。他のプログラミング言語を触ったことの無い人には薦められません。
- インクルーシブで無いです。例えば本文中に
Math クラスにはいろいろなメソッドがあるので見て下さい
というような文が書いてあります。個人的には重要視する要素ですが、頭の良い人は気にしないんじゃないかと思ってます。 - 内容が酷いです。冒頭から「この世にはコンパイル型言語とインタプリタ型言語があります」とかぶっ込んできます。mozillaの文書でこれです。絶望ですね。ただこの類いの酷さは素人の学習を今すぐ妨げるものでは無いと思います。
- 和訳が酷いです。技術的な間違いが多数あります。また原文に無い情報が追加されていたり、あったはずの情報が欠けていたりします。(良く言えば)技術文書と小説の区別が付いてない人が訳したような印象です。私も気付いたところはかなり直しました。疲れました。
並行システムの検証と実装を読んだ
序
CSP(Communication Sequential Process)というプロセス代数とそれに基づいた形式手法の本を読みました。頑張って読んだので紹介します。
CSPは並行計算をラベル付き遷移システムで表現した上で(これをプロセスという)、どのような遷移がありうるのか、プロセス間の遷移(の集合)にどのような関係(e.g. 詳細化関係)があるかを議論する枠組みです。
自動検証器の実装がいくつか知られていて、この本ではFDRを使ってモデリングと検証を行う方法が説明されています。
この本は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:ホントか?