自作言語 Orphos の実装 Mullos を支える(予定の)言語実装技術(2018)

この記事は、言語実装 Advent Calendar 2018の23日の記事だ。

自作言語 Orphos (おるぽす)の実装 Mullos (むっろす)を支える(予定の)技術のうち、言語実装と関係の深いものを雑多に紹介する。 本当は紹介したうえで「こちらが実践例になります」とやりたかったのだがさっぱり実践できていない。まあ年末年始進めよう。

最適化とコード生成

最適化とコードジェネレータにはLLVMを使う。その理由は、

呼び出し規約

デフォルトの呼び出し規約として、cc 11(HiPEの呼び出し規約)を使う。

LLVM Language Referenceに書かれている呼び出し規約のうち、 cc 10(GHCの呼び出し規約)とcc 11(HiPEの呼び出し規約)は末尾呼び出しをサポートしていて、かつCallee savedなレジスタがない。 cc 10は引数の数に制限があり、浮動小数点数を渡せないらしいので、cc 11の方を選ぶ。

Callee savedなレジスタがないことの利点の一つとして、例外の送出がスタックポインタをずらしてジャンプするだけですむ。 OCamlもこの恩恵を受けているらしい

OrphosにはOCaml Multicore風のAlgebraic Effect Handlerを入れる。 Algebraic Effect Handlerの機構は再開可能な例外機構みたいなものなので、例外とか継続的なものの高速化は重要だ。 ワンショットの継続の実装の参考にするためにBoostのfcontext(アセンブラで実装された、ucontextに似たAPI)の 実装を眺めてみたのだが、 レジスタの保存・復元が行われていた。 ジャンプを実行する関数の呼び出し規約をcc 11にすれば、退避は呼び出し側でLLVMが行ってくれる。 呼び出し側で使われていないレジスタがあれば退避をスキップできる。

型パラメータの実装

C++のテンプレートのように、LLVMのlinkonce_odrというLinkage Typeをつけた関数を型パラメータごとに生成する。 また、型クラスの実装も暗黙引数1とかにせずに、静的に解決して直接呼び出しする。

性能もさることながら、いったん特殊化してしまえば、具象型だけ考えればよくなるのでコード生成の実装も簡単になるのではないかと思っている。 コンパイル時間やコードサイズは長期的な課題とする。

GC

デフォルトで正確なGCを行う。

保守的GCはデータ構造がGC-robustかどうか気にしないといけない。 GC-robustでないデータ構造をつくってしまうと、制限なしのリークが起きる可能性がある。 たとえば無限リストをキューとして使っていると、その途中のノードをにせポインタが指していてリークしたら、それから先の無限リストが無限にリークする!  書き手に気をつけさせるのは望ましくないので、言語としてGC-robustでないデータ構造を作れないようにするべきだが、その気はない。 正確なGCをするしかない。

スタックの走査・リロケーション

正確なスタック走査・リロケーションのため、LLVMのGC機構を使う。 シャドウスタックとSafepointsのふたつのGC機構が候補になる。

シャドウスタック

スタックに配置したポインタ(へのポインタ)のリストを管理する。 スタックを走査するときはリストをたどれば良いし、リロケーション時にはスタック上のポインタを更新すれば良い。

LLVMにはシャドウスタックを実現するためのサポートがある。 対象にしたい関数にgc "shadow-stack"をつけておき、 イントリンシック関数@llvm.gcrootでスタック上のポインタへのポインタをマークする。 するとグローバル変数のllvm_gc_root_chainでスタック上のポインタへのポインタのリストが管理される。 マルチスレッド(Orphos言語にはファイバー的なものを入れたいので、マルチファイバー)に対応するためには llvm_gc_root_chainをスレッドローカル変数かローカル変数にする必要がありそうなど、いろいろと手を入れる必要がありそうだが、いちから実装するよりは楽だろう。

LLVMのもうひとつのGCサポートであるStatepointsのドキュメントには、 gcrootの機構には歴史的関心しか残されていないが、例外としてシャドウスタックの実装はサポートされるとある

Statepoints

スタックマップをつくるらしい。 AzulのなプロプライエタリなJVMのLLVMベースの高性能JITコンパイラFalconで使われているらしいので、速いのだろう。

OCamlのGCもスタックマップを使っているらしいので[要出典]、OCamlと性能で競争するためにはこちらを使いたいところだが、 あまりサンプルコードが見つからないしドキュメントに There are a couple places where bugs might still lingerとあるなど 面倒なので長期的目標とする。

ヒープの分離

ファイバーごとにヒープを分離する。 他のファイバーにメッセージを送るときにはコピーが行われる。

ファイバーが終了すればヒープごと解放できるので、短命なファイバーならGCなしで完了できるだろう(リージョンみたいなものだ)。 また、ファイバーごとにGCのアルゴリズムを変えられるようにできるので、パフォーマンスチューニングの余地が増えるという利点もある。

巨大なバイナリなどをいちいちコピーすると遅いので、 ポインタを含まない大きな(ページサイズ以上とか)オブジェクトは独立したヒープに確保して、 何個のファイバーから参照されているかの参照カウントを管理するようにする。

Semispace copying GC

ファイバーごとにヒープを分離することにより、semispaceなコピーGCが充分実用的になるかもしれない。 GCが他のファイバーを止めないし、GC中のファイバーのぶんしかメモリ使用量が2倍にならない。

自動定理証明

型クラスの法則の検査

Orphos言語に実装したい型クラスの機能として、

がある。 4つ目のlawのチェックのために定理証明器のZ3を使う。 コンパイラはZ3を使ってlawの反例を探し、見つけたら警告を出す (警告ではなくコンパイルエラーということにしてしまうと、互換性のため、時間のかかるチェックを打ち切るわけにはいかなくなるし、すべてのOrphos処理系でチェックの実装が必須になってしまう)。

Z3のC APIには証明に使う時間やリソースの制限を指定する機能があったはずなので(今ちょっと探したら見つからなかった。まあなんとかなるだろう)、その閾値をコンパイラオプションで指定するようにする。 CIでビルドするときだけ閾値を上げて高性能ハードウェアで殴るとか、安定版リリース前に閾値を上げて時間で殴るという運用が可能だろう。

ふるい型(refined type)

Int > 0みたく型に制約をつける(集合をふるいにかける)らしい。 これもZ3で殴って警告を出す機能にしたい。

type-systems/refined-types
ふるい型の検査をZ3などのSMTソルバで行う実装例。

レベルベースの型推論

sound_lazy.mlを参考にレベルベース型推論を実装する。

How OCaml type checker works – or what polymorphism and garbage collection have in common
前述のsound_lazy.mlが載っている記事。
OCaml でも採用されているレベルベースの多相型型推論とは
去年の言語実装Advent Calendarの記事。 レベルベースの型推論が紹介されている。

おわり

ブログ復活させたばかりでコメントシステムをまだつけてないので、何かあったらマストドンアカウントまで。


  1. 実は言語実装Advent Calendar 2016の17日にImlicit Calculusという題名で予定を入れている(最初はたしかTruffleについて書くとしていて、その後変えた)のだが、未だに書いていない(すみません…)。Orphosでは暗黙引数自体は実装しないつもりだが、型クラスの理解にかかわるのでいずれ論文をちゃんと読んで記事を投稿するつもり。 [return]