P言語の素晴らしさについて

先週Microsoft社がP言語に関するブログ記事を公開し一部界隈で話題となった。

「いまさら一文字言語かよ…」「何個目だ?」といった批判的諦念的なものから、「RustとGoとErlangの間の子みたいなのだなあ」「なんか読みにくい」といった反応が多くこの言語の重要性やインパクトに対して正しく理解しているものがあまりなかった。尊敬しているTD勢ですらあまり重要性が伝わってないようだ 1 2 。上記のブログ記事を読んだり、マニュアルを読んだらすぐ分かるようなことではあるが、日本語で解説しておこうと思う。なおいわゆる言語入門とかそういった類のものではないことをご理解いただきたい。

TL;DR

  • 並行処理や分散システムの形式証明や形式検証はそれ自体が非常に難しいことが知られていた
  • 証明や検証のツールも、実装のフレームワークも、テストのツールもあったが、形式検証と実装を同時に記述することはできなかった
  • 並行処理や分散システムのプログラムについて、形式検証と実装を同時にできるようになったのがP言語

これを読んですごさが分からなかった人は私のスライドを見てからここに戻ってくるとすごさが伝わるかも。

並行処理や分散システムの正しさを保証するのはとても難しい

そもそも人類にはマルチスレッドが早すぎたのであって、マルチスレッドプログラミングなんてものは常人がやるべきではない類のものであることは一般に知られているといっていいだろう。しかしながらCPUのクロック数IPCは頭打ちになりムーアの法則は演算コアを増やすという方向に進みつつあり、マルチスレッドプログラミング(並行処理)は、夏休みの宿題の終わっていない小中学生に対する9月1日のように差し迫ってきている。

CAS命令などの同期プリミティブが用意されている並行処理でさえその難しさが知られており、いわんや故障の含まれる分散システムをや。FLP不可能性やCAP定理といった「できない」尽くしの世界で、それでも人類はOSを発明し、RDBMSを発明し、非同期IOで動作するHTTPサーバーで日々ネットサーフィンを行い、Hadoopビッグデータを処理してきたのである。これらのソフトウェアに人類が一体どれだけのリソースを投入し、非決定論的に発生する並行バグのせいでいったいどれだけの時間と機会を失っただろうか。

手続き型のプログラミングでの正しさの保証は実践的にはまだ難しいとはいえ、多くの技術が普及しようとしている。いわゆる型推論に基づいたコンパイル時の型検査と静的リンクの強制(Haskell, OCaml)や、カリー=ハワードの同型対応を用いたプログラムの形式証明があればプログラムが正しいことを理論的に保証することができるようになった。言語仕様や処理系の実装からそういった形式証明をつけにくいプログラミング言語でも、QuickCheckを始めとしたテストパターンの網羅的な生成とエラーケースの推定をやってくれる強力なツールが登場(普及…?)している。日本語だとxuweiさんのScalaCheckの資料が非常によくできていて分かりやすい。

一方で並行処理や分散システムの正しさの保証は難しい。実装面からのテストツールはしばらく決定版がなかったが2013年のJepsenの登場によって状況は変わった。JepsenはいわゆるFault Injectionと言われる類のテストツールで、特にiptablesを操作してネットワーク分断をシミュレートするものであった。Jepsenによって Kafka, MongoDB, ElasticSearch といった多くの分散システムにバグが見つかり、それから分散システムはJepsenのテストを通ることが登竜門のようになった。ちなみにOverview of Infrastructure TestingというGoogleの記事を見てると、Googleは21世紀のかなり早い段階でネットワーク分断のFault Injectionもやっていたのだろうと推測される。実用的で著名なFault InjectionのツールとしてはChaos Monkeyがかなり早くから知られていたが、これはサービス全体に対する大規模なものであって、特定のソフトウェアを試すようなものではなかった。

他方では、分散システムのアルゴリズムプロトコル)を形式的に証明して正しさを保証しようという試みはそのもっと昔からあった。上記のMSのブログにあるTLA+SPINモデルチェッカが代表的なものだ。しかしこれらはいずれも、アルゴリズムを検証するために独自言語が必要であり、実用的なものではなかった。具体的には、これを使ってアルゴリズムが正しいことを証明できても、実際に動作するソフトウェアは別の実用的な汎用言語(CやJavaなど)で記述する必要があり、プログラムが証明された通りに実装されていることを保証する方法はなかった。ちなみに形式記述とFault Injectionの間の子としては最近、MollyNetflixで実用化されたことが話題になった。Mollyは Dedalus というDSLで記述したアルゴリズムに形式的にFault Injectionを網羅的に仕掛けてバグを出すものである。わたしは上のブログ記事で埋め込まれているPeter Alvaro のRICONでの講演を見ることができたが、これは本当に面白かった。トップレベルの研究者は話も上手くないといけない。

少し話を戻して、並行処理のプログラム(いわゆるマルチスレッドで動作するプログラム)の正しさを検証する方法で私が一番良く知っているのはErlangのQuickCheckが持っているPULSEだ。これは相互作用する2つのFSMを並べて状態とメッセージの組み合わせを網羅的に試してRaceが起きる条件を絞り出していくというものだ。他にも eqc_statemなど素晴らしいツールがあるので、ErlangやElixir使いでRace conditionに悩んでいる諸君がいたら是非使うべきだ。決して値段は安くはならしいが、本番で競合で悩むくらいならこれをサクッと買った方がよい。Erlang以外の処理系でここまで踏み込んだものはあまり知らない。もっともそこまで必要ないという話かもしれないが… 他の言語なり処理系だと、GoのRace detectorClangのThread Sanitizerくらいが有名だろうか。僕も詳しくないので教えてほしい。まあDTraceやBPF, ClangのXRayを使えばどうにでもなるという話かもしれないが、どのツールも私のような凡人に無理じゃないかと思う。

おわかりだろうか。これだけ日進月歩で研究と実践の歴史が積み重ねられてなお、 1) 分散システムや並行処理を形式検証するDSL, 2) Fault Injectionしてみて動くかどうか確かめてみるテストフレームワーク, 3) とりあえずトレース仕掛けてじっと様子を睨む といった方法くらいしかないのである。ここに颯爽とP言語が登場するのである。

P言語そのものについて

実はP言語は先々週登場したわけではなく、2012年には存在が公表され2013年にはPLDIに論文が登場した。さらに昨年10月にはソースコードが公開された。余談だが、実は遅くとも2014年にはCodePlexでコードが公開されており、たとえば "a1cd6fa" は完全に一致している: Codeplex, GitHub。じゃあ一体このInfoQの記事は何だったのか。このInfoQではP言語で書いたコードをZingという謎システムに入れて検証できるようにしたと書いてある。今年の記事では、P言語からC#の形式検証用のコードを吐いてツールに食わせることができると書いてある。2012年からいろいろあったんだね…

P言語のどこがすごいかというと、P言語でシステムを書くと、本番で動作する分散システムのC言語でのプログラムと、形式検証ツールに食わせるためのC#のプログラムが同時に生成されるのである。このP言語のコンパイラツールチェインが正しく作られている限りにおいては、形式検証済みの分散システムを本番で使うことができるのである。理論的にはバグがないというやつである。ネットワーク分断も死んだふり故障も(もしかしたら、書き方によってはビザンチン故障も)もう恐れなくてよいのである。TLA+は僕にはちょっと難しいのだけど、僕がもし次に分散システムを手作りする必要があったら、まず最初にP言語での実装を検討するだろう。なのでまずはMacPortsで使えるようになってくr(軟弱

ここまで来ると、Rust的なメモリ管理とか、Go的な軽量プロセスや、Erlang的な状態遷移マシンの記述なんていうのはモダンなシステム実装言語にはあって当たり前で、そこからもう一歩進んで何があるかが決め手になるということが分かる(もちろんRustやGoが劣っているということではなく、他によいところがある)。

ちなみに、この手のものは実はP言語とは違うMicrosoftの別チームが同様のものを出している。その名もIronFleet だ(よくわからない日本語解説よくわかる解説)。カタログスペックのコンセプトは、実は全く同じだ。何だか強そう。著者の名前を見比べるとわかるが、P言語とは全く別のチームだ。キャンパスが違うんだろうか、仲はいいのか悪いのか、実績からいうとP言語の方が強そうだよなとか、いろいろ妄想できてなんか楽しい^^;

レポジトリをもうちょっとうろうろすると、入門PPTがなんとそのまま入っていて(ノ∀`)アチャーと思ったがその内容が思ったよりすごい。なんとHololensやOfficeでも使われているというのだ。実績も十分だ。こんなすごい言語が使われているAzureやWindowsを使ってみたくなるね^^;

f:id:kuenishi:20170525081934p:plain

参考

P.S. とりあえずMacOSでの最初のビルドは見事にコケた。Sierra 10.12.5, commit 601520c8, monoとcmakeはMacPortsから。
P.S. mono >= 4.5 が必要だと id:matarillo さんにブコメで教えてもらった。
P.S. コメントで本文は形式的証明と形式検証を混同していることを指摘していただいた。その辺りは割り引いて理解していただけると助かる。
P.S. プログラムと検証を一致させる試みは何もPやIronFleetが初めてなわけではなく先行者がいることもコメントで指摘いただいた。割り引いて読んでくれ。
P.S. TD勢に対する煽りが少し攻撃的だったのでマイルドな表現に修正した。