val it: α → α = fun

Unisonの人の論文。Unisonてのはファイルとディレクトリ構造の同期を行うツールで、この論文はUnisonの定式化を行うというもの。
http://www.cis.upenn.edu/~bcpierce/papers/unisonspec.pdf

まずは関連研究との比較でこれが結構面白い。言うまでもなく、同期に関する既存研究はいっぱいある。だがほとんどのツールではoperationalな意味論から同期を定義している、ってのがこの論文の指摘。operationalというのは、ファイルを編集したとか、移動したとか、作ったとか消したとか、そういうファイルシステム上のオペレーションがわかっていて、それをどう順序付けるかというもの。だけどUnisonではこのアプローチを採用しない、というかできない。

なぜか。Unisonが独特なのは、複数の動作環境をはじめから念頭に置いていることと、ユーザレベルのプログラムとして動作すること。例えばファイルシステムの機能として組み込むことなく、ユーザが適当に起動して同期することを目指す。したがってポータビリティは高いが(WindowsとLinuxの間での同期とかもできる)、ファイルシステムの内部構造に深く根ざした処理は行えない。つまり、operationalな意味論は適用できない。ユーザがツールを起動した時点でわかるのはその時点でのファイルシステムの中身だけで、あとはせいぜい前に実行したときに保存してたデータぐらいしかない。そこで、最後に同期したときのツリーの中身と、その時点でのふたつのツリーの中身だけから可能な限りの同期を目指す。どうするか、という問題設定なわけだ。

4章でファイルシステムツリーの概要、5章でマージとコンフリクトの形式的な定義が説明されている。てことでここがこの論文の核心部だけど、ここはくだくだと説明するのは厄介ですね。まあ割と直感的な定義です。6章で、5章の形式的な定義から言えることが書いてあって、まあなんにもしないってのも同期のひとつだよねとか、最大限同期するとすると、同期のとり方はひとつに定まるよねとか、そういうことが説明されている(最大限の同期が存在してただひとつに定まるというのは、同期するときにはとても大事な性質だと思うので、この証明は大事。まあproof sketchしか書いてないんですが……)。

7章は、6章までの形式的な定義をOCamlの参照実装として作りましたという話で、まあ普通。説明はかなり簡略で、詳しい説明は付録の方に書いてある感じ。しかも、どうやってOCamlの実装が形式的定義にきちんと従っているかの確認は、頑張りましたというぐらいだし……。

8章が面白い。7章は抽象的なツリーに対する同期の参照実装なので、実世界で動作する本物のUnisonとはかなり違う。Fully specifying and verifying a real-world system program of Unison’s size and complexity—i.e., proving that the actual codebase meets its specification—would be a superhuman task.だそうです。で、どういう所がいかに難しいかをくだくだと説明しています。たとえば、参照実装は関数的で、例えば前のファイルシステムの中身が完璧にわかるし、後までずっと参照できるし、新しいツリーは元のツリーと無関係に構築できるけど、現実的にはin-placeにツリーを書き換えるしかないとか、そういう感じのことね。

9章はメタデータの扱い。ファイルは中身だけじゃなくてパーミッションとかいろいろあるよねと。いろんなやり方があるけど、ディレクトリの子要素としてファイルがあるみたいに、「パーミッション」のようなメタデータ用の特別なパス名があることにしてファイルの子ノードにメタデータを持ってくると、ツリーの同期として等価に扱えるよねとかそういうことが書いてある。ただ参照実装はそんな風にはなってないので、たぶん後で思いついたのかもね。

最後の11章は将来の方向性で、いろんなことが書いてあるけど、個人的に面白かったのはHarmonyというやつで、ファイルシステム以外の、XMLみたいな構造データも変更操作できるよね……という。

個人的には、こういうのの形式的定義とかって半分自己満足みたいなもんかなと思うけど、既存研究との差異がきちんとあって、Unisonのデザインの指針がきちんとあった上での形式化をしてて、modeling gapがちゃんと書いてあるあたりはなかなか面白いなあと思いました。