日本が機械学習パラダイスなのは情報大航海プロジェクトのおかげ

人工知能じゃ〜これからはシンギュラリティじゃ〜と盛り上がっており、猫も杓子も深層学習で人工知能で人類皆失業などと楽しいお祭り、ぼくは嫌いじゃない。我々が生きていくためには金が必要なんだ。というわけで、ちょっと気になって調べたことがあったのでここに記録しておく。もしこれが知財や法曹方面の業界で有名な話だったらコンピュータエンジニアたち何やってんのという話ではある。


もともとこれが気になっていた。ので調べました。という話。


著作権法

とりあえず原文を引用しておこう。

第四十七条の七 著作物は、電子計算機による情報解析(多数の著作物その他の大量の情報から、当該情報を構成する言語、音、影像その他の要素に係る情報を抽出し、比較、分類その他の統計的な解析を行うことをいう。以下この条において同じ。)を行うことを目的とする場合には、必要と認められる限度において、記録媒体への記録又は翻案(これにより創作した二次的著作物の記録を含む。)を行うことができる。ただし、情報解析を行う者の用に供するために作成されたデータベースの著作物については、この限りでない。
(電子計算機における著作物の利用に伴う複製)

これを解釈すると日本は機械学習パラダイスだというわけだ。まあ確かにそうとしか読み取れないわけだが、本来の目的とか設立趣旨を知っておかないとあとの法解釈で死ぬだろう。というわけでヒマだしネットサーフィンをしたわけだ。この47条の7は平成21年の著作権法改正で追加された条文で、解説文書も文化庁のページからPDFながら公開されている。この解説文に

今回の著作権法改正は,議員立法や他法制定に伴う整備を除けば,平成 18 年(中略)以来の改正となるものである。改正事項は多岐に渡るため,個
別の改正事項ごとの経緯を述べるには紙幅に余裕がないが[1],全体の経緯は次のとおりである。

とあり、注釈に「 個別の改正事項ごとの検討経緯については,平成 21 年1月の著作権分科会報告書を参照されたい」とある。なので、この著作権分科会報告書を参照する。 これを見つけるのにいろいろ検索クエリを工夫した結果、文化審議会著作権分科会(第27回)議事録・配布資料を見つけることができた。で、これをみても著作権法47の7に直接関係しそうなところがない。が、つらつら見ていると次回の文化審議会著作権分科会(第28回)議事録・配布資料に、それらしきものがある。 「著作権法に関する今後の検討課題」(平成17年1月24日・著作権分科会決定)の概要とそれ以降のこれまでの審議状況というやつがそれで、これをみると4ページに

  • 概要: 画像・音声・言語・ウェブ解析技術等の研究開発における情報利用の円滑化のための法的課題の検討(知財計画2008)
  • これまでの審議状況等: 平成21年法改正案提出中(第47条の7の新設)

と書かれている(表の引用が面倒なので適当に書式を変更した)。これだ!!

というわけで、経緯が書かれているという資料1-2の文化審議会著作権分科会報告書(案)に戻ると、の第1編第3章第6節「研究開発における情報利用の円滑化について」が該当する。検討の背景の序文を引用しよう。

政府の知的財産戦略本部では、高度情報化社会の下、インターネット上の膨大な情報等から情報・知識を抽出すること等によりイノベーションの創出が促進されるとの観点に立ち、情報アクセスなどネットワーク化のメリットを最大限に活用できるような環境整備の必要性が認識されている。そして、本年6月に同本部で決定された「知的財産推進計画2008」においては、まず、それらの情報処理のための基盤的技術となる画像・音声・言語・ウェブ解析技術等の研究開発に関して、この研究開発の過程で行われる情報の利用について著作権法上の課題があることを指摘し、早急に対応すべき旨が盛り込まれたところである。

つまり知財戦略本部=政府からのお達しでイノベーションを促進するために著作権法をなんとかせいと言われているわけである。知的財産計画2008はまだ読んでないけど、それっぽい目次があるようだ。P26に

ネット等を活用して膨大な情報を収集・解析することにより高度情報化社会の基盤的技術となる画像・音声・言語・ウェブ解析技術等の研究開発が促進されること等を踏まえ、これらの科学技術によるイノベーションの創出に関連する研究開発については、権利者の利益を不当に害さない場合において、必要な範囲での著作物の複製や翻案等を行うことができるよう2008年度中に法的措置を講ずる。

情報大航海プロジェクト

こんどは情報大航海プロジェクトについて見てみよう。検索したら平成19年の「情報大航海プロジェクト」についてという資料がみつかった。平成19年は2007年だ。まあパワーポイントなのでポンチ絵なのだが、P3には「制度・環境」と題して「プライバシー、著作権を始めとする制度的課題について、法改正やルール整備等の所要の手当てを処置」と書かれている ((ちなみにP4には将来のIT化社会の未来像みたいなのが語られているが、なんだか昔も今も似たようなことやっとるんだなあと感慨に浸ることができる名文である)。さらに、2008年のJapioの雑誌?機関紙?には「情報大航海プロジェクト2年度目を迎えて」という文章が寄稿されている。これを見ると

今後web情報における現在の検索エンジンにとどまらず新サービスが開拓される実情について、文化庁・経産省で大航海プロジェクトにも参加するベンチャー企業への共同ヒアリングを実施、文化庁へのパブコメにも意見を提出、著作権審議会法制小委員会にて著作権法改正の方針が固まったことは、こうした利用が可能となっている諸外国並に日本の法的環境が進捗するだけではなく、さらにどのような環境を整備していくのかに内外関心を集めることになるであろう。

と書かれており、情報大航海プロジェクトの関係者が文化庁に働きかけたことがわかる。だってここをクリアしないと検索エンジンも作れないもんね。当時某プロジェクトで微妙に検索エンジン経由でそういう噂も聞いていたので、まあそうなるわなー。当時は役人仕事しろって思うけど、今思うとお役所頑張ったな!と感慨深いものがある。

改正著作権法の解説から合わせて考えると、まず検索エンジンがクローリングして集めたWebサイトや文章、音声、動画などのデータを検索エンジン事業者がそのまま国内で保存していたら著作権法上の複製にあたりそうだから、ちょっと法律関係をちゃんと整備しないといけなくなった…おそらく2006とか2007年の情報大航海プロジェクトの企画時にはわかっていたことだと思う。当時すでに国産の検索エンジンは何社もあったわけだし(当時の事業者は基本的にクロールしたデータはインデックス作成後すぐに消していたようなので、心配はしていたがそんなに問題にはなっていなかった?)。ところがグーグルが登場して技術の流れが変わって法整備ちゃんとしようということになったので、政府にプロジェクト関係者が働きかけて法改正に持っていったものと推測できるわけだ。

改正著作権法の解説

情報大航海プロジェクトと改正著作権法の関連を示すものとしては、改正著作権法の解説というページからリンクされている解説が非常にわかりやすい。公式見解ではないと前置きしつつも、どう考えても全員関係者です、という非常に味わい深い資料なのであるが、6-20をみると面白い。

法47条の7により認められる複製等によって情報解析を行い、その結果を他人に提供するサービスを実施したいと考えているが、どのようなサービスであれば問題ないか。

という問題だ。深層学習関係に敷衍すると、GANによる自動生成なんかが主に関係するだろう。ここでは、『ネガティブ4割、ポジティブ6割」は、上記の「情報解析結果のデータ」に』と書かれているように、別の記号やキーワードなどに抽出された統計情報ならOKとしか書かれていない。そして、49条で「第47条の7に定める目的以外の目的のために、同条の規定の適用を受けて作成された二次的著作物の複製物を用いて当該二次的著作物を利用した者」は、「当該二次的著作物の原著作物につき第27条の翻訳、編曲、変形又は翻案を行つたものとみなす」と書かれている。GANによる生成は統計情報の抽出なり利用を人間は全くやってないので、はてこれは新たなグレーゾーンなのでは…と心配できたりするわけである。

もちろんほとんどのケースでは元のデータが分からないくらい多くミックスされているわけで、人間の全ての創作活動が既存の作品の模倣とアレンジ、組み合わせであると主張する立場からはコンピュータと人間がやるのでは大差ないという話になるかもしれない。あるいは、創作側が「人間に見せるのはOKだがコンピュータに見せるのはNGだ」と言ってしまえば話はそれで終わるかもしれない。

まあそもそも件の記事の上野達弘氏は経歴をみるに文化審議会著作権分科会の小委員会を何度も歴任しているし、知財戦略本部にもおられたようなのでどうみても関係者(か、限りなく現場に近い)だったのであろう。知ってる人は知ってる話というだけの話だ。

まとめ

  • 著作権法47の7は2008年の政府の知財戦略の成果のひとつであり、たまたまそこにあったわけじゃない
  • 改正に関する経緯を追っていくと情報大航海プロジェクトの働きかけがあったことが分かる
  • あれくらい大きなプロジェクトであれば法改正もできるということだ!!感謝しよう!!敬え!!
  • とはいえ深層学習を応用した生成系のタスクについては著作権的に悩ましいところもまだありそう


参考

  • 高田寛, 情報大航海プロジェクトと検索エンジンの法的問題についての-考察, 比較法制研究(国士舘大学)第31号(2008)129-168

消すだけなのに rm -rf がいっつも長くて待ちきれない問題

今時のファイルシステムはみんなジャーナルもってて何かあったときにそこからリカバリする仕組みになってるので、当たり前といえばそうなんだけども。

(TODO: ここにファイルシステムのツリー+ジャーナルのポンチ絵を手描きでも何でも描く)

ご本尊のデータのツリーと何らかのWALを1セットで持っておくのはRDBだろうがファイルシステムだろうがそうは変わらない、で、削除についても並行制御をうまくやるために削除フラグをログに入れておいてあとで本尊のデータを整理するというのが基本的な設計になる。そこで私は立ち上がった(TL;DR: 特にオチとかはないです)。

で色々調べてみた結果、結論は既存のファイルシステムはよくできているということだった。何かしら高速化を期待された場合はちょっと次回以降をお待ちいただきたい(調べることが多すぎて飽きたともいう)。

ベースライン測定とか

まず1バイトのコンテンツを持ったファイルを大量に作る。

深さ4幅32なので 32^4 = 1048638 個のファイルが33284のディレクトリの下にできたことになる。論理値でいえば1MBほどだが、ディレクトリやファイルなどのオーバーヘッドの方が大きいだろう。それでもRAMが32GBあるマシンで実験したのでファイル実体のディスクアクセスは全てディスクキャッシュに乗る。おそらくWALの書き込みが支配的になるだろう。で、このファイルとディレクトリを消す方法はざっくりインターネットを調べると簡単なものは3つくらいみつかる。それに一つ我流を追加。

  1. rm(1) を使う方法: "rm -rf " とやるだけ。実はこれがかなりよくできていて速い。
  2. xargs(1) と rm(1) を使って並列化する方法: "ls | xargs -n 1 -P 8 rm -rf" などとやるだけ。rm(1)が速くできている上に並列化されて実時間はかなり速くなる。ただしコンテキストスイッチはまあまあ増える。
  3. find(1) を使う方法: "find -delete" とやるだけ。これで 以下が全部消される。いまのところこれが rm(1) よりも速いといわれている。
  4. C++17のstd::experimental::filesystem::remove_allを使う方法

この4つを /usr/bin/time で測ってみる。スペックは家のデスクトップDebianの /dev/sdc1 上に作ったXFSディレクトリである。このためだけに作ってあった。user, sys は秒、realは時:分である。

user sys real voluntary cs CPU
rm -rf 0.37 20.42 1:58 5327 17%
xargs 1.05 42.80 0:28 1151757 155%
find 0.52 20.82 1:23 942 25%
prm 4.59 46.35 1:24 1251687 60%

想定の通り最も短時間で前処理が終わるのは xargs(1) を使った方法だった。しかしシングルスレッドで最速だと思われた rm(1) よりも find(1) が速いのは意外だった。そこで strace(1) の結果を比較してみる。 これは、さきほどの実験コマンドで /usr/bin/time の代わりに "strace -c -f" とつけてやるだけである。まず rm -rf の結果がこちら

$ strace -c rm -rf tree
% time     seconds  usecs/call     calls    errors syscall
------ ----------- ----------- --------- --------- ----------------
 99.04    0.193423           0   1082401           unlinkat
  0.31    0.000614           0    101475           getdents
  0.25    0.000488           0    304425           fcntl
  0.18    0.000351           0     67650           openat
  0.10    0.000189           0    101481           close
  0.07    0.000133           0     67653           fstat
  0.05    0.000099           0     33825           newfstatat
...

で、find(1) の結果がこちら。

$ strace -f -c  find tree -delete
% time     seconds  usecs/call     calls    errors syscall
------ ----------- ----------- --------- --------- ----------------
 99.10    0.190004           0   1082401           unlinkat
  0.24    0.000469           0     67650           getdents
  0.23    0.000436           0    304426           fcntl
  0.13    0.000258           0     33825           openat
  0.13    0.000241           0     67650           newfstatat
  0.12    0.000235           0    135311           close
  0.04    0.000086           0     33834           fstat
...

xargs(1) の結果は rm -rf のものとそう変わらなくて(xargsのwait4(2) が必然的に待ち合わせなのでほとんどの時間を占めている)、30分違ったのはどうしてかなあというところではある。また、99%の時間を使っているはずの unlinkat(2) のシステムコールですら 0.19秒で、wallclock time には全く追いつかない。strace(1) のマニュアルを見ると"On Linux, this attempts to show system time (CPU time spent running in the kernel) independent of wall clock time." と書かれていて、system time が出てもよさそうなもんであるが…という謎に当たる。 xargs(1) で並列化した rm が速くて自作で並列化した prm.cc がどうして遅いのかは

$ strace -f -c /home/kuenishi/path/to/prm tree
% time     seconds  usecs/call     calls    errors syscall
------ ----------- ----------- --------- --------- ----------------
 85.01   57.128000     2197231        26         6 futex
 10.46    7.032312           6   1082401     33825 unlink
  2.21    1.484577          22     67652           getdents
  1.90    1.278376           1   2164802           lstat
  0.33    0.219737           6     33825           rmdir
  0.03    0.019788           1     33832           open
  0.03    0.017729           1     33832           close
  0.02    0.016686           0     33833           fstat
...

としてみればわかるように、 unlink(2) がちょうどディレクトリの個数だけ失敗していて、さらに lstat(2) も大量に呼ばれていることから、ああこの辺だなあとすぐに想像がつく。余談なので深くは追わないが、実際に GCC のSTL実装では簡単にポータブルに作ることを意識していて性能とかそういうことは微塵もなさそう。

このベースライン測定で分かるのは以下

  1. シングルスレッドで動くものだとざっくり1.5 ~ 2時間、マルチスレッドで速く動くものなら30分くらいかかる
  2. システムコールの使い方が下手だとそもそも並列化の恩恵つきでも赤字
  3. どうやら unlinkat(2) をちゃんと使うと速いらしい
  4. userとsysを全部足してもwallclockに追いつかないので、どこで時間が溶けているのか分からない

プロファイル(on CPU)

さてここからが本番である。strace(1)をしても何で時間が溶けているのかよくわからない。こりゃ、削除を速くするとかそれ以前に謎が多いゾ…?という話である。CPUインテンシブなジョブではないので、ふつうのプロファイリングをしてもダメだろうなあというのが容易に想像できる。そこで我らがperf(1)先生の登場だ。perf先生のすごいところは動作中のプロセスもアタッチして覗けるところなのだが、バッチプログラム相手だともっと簡単に起動できる。

実際の測定は簡単で、

$ sudo perf record -F 99 -a -g -- rm -rf tree
$ sudo perf script > out.perf

などとすれば、秒間99のレートでプロセスのスタックをすっぱ抜いてチェックできる。それをこうして…

$ ./stackcollapse-perf.pl out.perf > out.folded
$ ./flamegraph.pl out.folded > out-rm-single.svg
$ firefox out-rm-single.svg

こうじゃ!

f:id:kuenishi:20171006182347p:plain

"rm -rf tree" の代わりに "ls | xargs -P 8 rm -rf" でやったやつもあるよ!

f:id:kuenishi:20171006182505p:plain

どちらの図もほとんどの時間を unlinkat(2) が使っていることが分かる。これは strace の結果とも矛盾しない。で、そのなかでも "vfs_unlink" と "xfs_fs_destroy_inode" がものすごく時間を使っていることがわかる。ちょっとだけLinuxのコードを読んだのだけど、中で沢山ロックをとって、スピンロックも沢山あって、それから inode エントリを書き換えたりして、それをジャーナルに流している?っぽい処理が沢山ある。それから kthread の方で "xlog_iodone" がCPUを使っていることもわかる。しかしながら CPU使用率が 17% しかない( perf は実行中のプロセスに対してしかスタックをぶち抜かない)ので、これでは全体の実行時間の 17% くらいしか説明できない。

プロファイル (off CPU)

で、IO待ちのプロセスのスタックを抜くにはperfでは不足で、Linuxの eBPF というのを使う。iovisorという便利なツールキットがあるので、そいつをさくっと入れる。

# echo "deb [trusted=yes] https://repo.iovisor.org/apt/xenial xenial-nightly main" >> /etc/apt/sources.list.d/iovisor.list
# apt update
# apt install bcc-tools

これは特定にCPUを見てくれるとかはしなくて、OS内のプロセスで特定の状態にいるやつを拾ってくる。状態一覧はカーネルのヘッダをみると

$ grep TASK_ /usr/src/linux-headers-4.9.0-3-common/include/linux/sched.h  | grep define
#define TASK_RUNNING            0
#define TASK_INTERRUPTIBLE      1
#define TASK_UNINTERRUPTIBLE    2
#define __TASK_STOPPED          4
#define __TASK_TRACED           8
#define TASK_DEAD               64
#define TASK_WAKEKILL           128
#define TASK_WAKING             256
#define TASK_PARKED             512
#define TASK_NOLOAD             1024
#define TASK_NEW                2048
#define TASK_STATE_MAX          4096

などとなっているので、IO待ちの TASK_INTERRUPTIBLE をみるために

$ /usr/share/bcc/tools/offcputime -f 20 --state 2 > out.offcpustack

と仕掛けておく。別のコンソールで素早く

$ time ./coreutils-8.26/src/rm -rf tree

として、コマンドが返ってきたら offcputime もさくっととめる。こいつをグラフにするには

$ ./flamegraph.pl --color=io < out.offcpustack > offcpu-2a.svg

などとすると、こんな感じで

f:id:kuenishi:20171006184650p:plain

TASK_INTERRUPTIBLE状態のプロセスのスタックを秒間20で覗いたときの集計結果を見ることができる。でもカーネル分からないのでウ~ン…となっちゃうけど、やっぱり "xlog_write" という名前からしてXFSのジャーナル書くところで時間を食っているように見えなくもない(心眼)。これは負荷がないときと比較しないといけないんだろうなーと思ったけど、なぜか僕のメモはここで途絶えている。カーネルスレッドって誰が起動してるんだろね…

結論

  • perfやiovisorを使ってon-CPUとoff-CPUのFlameGraphを描いてみた
  • XFSやrm(1)はよくできている
  • それはそれとして unlinkat(2) のシステムコールに縛られたファイルシステムはインターフェースからして改善の余地があるのではないか

想像するに、rm で消しに行ったけどシステムコールから返ってくるには何らかの待ち(おそらくはXFSのジャーナルにwrite)をしないといけないのだけど、それは非同期でやっているので on-CPU のグラフには出てこないし、 off-CPU のグラフのどこに出てくるかをちゃんと調べないとよくわからない。Kernel tracing は難しい。第二部に続く(かもしれない)。

UNIX Filesystems: Evolution, Design, and Implementation (Veritas)

UNIX Filesystems: Evolution, Design, and Implementation (Veritas)

おまけ: 環境構築

manpagesを入れる

$ sudo apt install man-db

perfなどのツールを入れる

$ sudo apt-get install linux-perf strace build-essential perf-tools-unstable
$ sudo perf test

これで(ほとんど)全ての項目がOkになるようにしておくこと。

デバッグシンボルつきの rm(1) を作る

$ apt-get source coreutils
$ cd coreutils-x.yy
$ CFLAGS="-g3" ./configure
$ make -j8
$ src/rm -h

書評: ビッグデータを支える技術

Googleを支える技術 ?巨大システムの内側の世界 (WEB+DB PRESSプラスシリーズ)で著名な西田さんの著書である。とても先見性のある本で、当時は仕事でもあったからとてもお世話になった。その西田さんの新作だというし、最近はもういろいろビッグデータのソフトウェアとミドルウェアがありすぎてワケの分からないことになっていると思ったので、知識を整理するためにサクッと購入。

ビッグデータを支える技術―刻々とデータが脈打つ自動化の世界 (WEB+DB PRESS plus)

ビッグデータを支える技術―刻々とデータが脈打つ自動化の世界 (WEB+DB PRESS plus)

本書の冒頭でも触れられているが、昨今ではありとあらゆるソフトウェアがオープンソースで公開されているし、詳しい情報はほぼすべてインターネットで公開されているから、この本はカタログ的にさまざまな概念や製品を紹介していき、個別に深く解説することはしないと注意されている。まさにそれこそが本書の価値で、元エンジニアで昨今のビッグデータの潮流を知りたい課長、部長級の管理職や、現場でビッグデータを前に呆然としているエース級のフルスタックエンジニアが知識の補完を行う用途にピッタリである。次点で向いている用途としては、これからビッグデータの赤い荒波に乗り出していこうと考えているエンジニアや営業職にとっても、業界を俯瞰して全体図を把握するにはよい(当然コレだけではダメで、そこから自分の得意分野を深掘りしていかなければならないだろう)。ビッグデータのことが分からない、という人は必読の一冊だ。

私自身はこの業界にもう10年近くいることになるので、おおよその概観を脳内に持っているつもりだったが、思った以上にビジネスインテリジェンスとかETLとかバッチとかに多様な世界があって、いろいろあるらしいなあということをざっと確認できたのでよかった。以下は、自分の専門分野で気になったところの指摘をささやかながらしておこうと思う。ちょっと忌々しい指摘ではあるが、これで本書の価値が損なわれるわけではないのでお間違いのなきよう。

10/6追記: YARNとLXCに関して - 「ビッグデータを支える技術」補足 にて捕捉いただいた。この捕捉を読んでから、以下のコメントは割り引いて読んでいただきたい。

Apache Mesos について @ P119

119ページのカラムで「Mesosによるリソース管理」と題してApache Mesosの紹介をしているのだが、2017年の本にしては情報が古い。まず出だしの「MesosはOSレベルの仮想化技術を用いており、YARNと比べると…」という話からしてアレでして、YARNもMesosもリソース制限は基本的にcgroupを使っているわけなのでそんなに変わらない。Namespacesの利用があるかどうかは異なるかもしれないが、それはリソース制御ではなくIsolationなのでちょっと違う。また「Dockerと同じくLinuxコンテナ(LXC)が用いられ」というのは明らかに誤り。遅くても1.0の時点でサポートされているコンテナエンジンはDockerかMesos独自のエンジンであり、LXCは一年以上前から利用していない。DockerもLXCは既に利用しておらず、LinuxのNamespacesを利用している。

またその後の解説でMesosにData localityがなく、一方でYARNにはあるのでYARNの方が優れていると解説されている。確かにMapReduceなどのLocality機能と親和性が高い機能がYARNだとスムーズに動作するらしいが、Mesosの2 level scheduler という思想に基づけば入力データのHDFS上の位置をみつつLocality awareに作るのはフレームワーク側の仕事である。テクニカルには、多数のOfferを抱えておけばIPアドレスは分かるので、フレームワーク側でデータの位置と割り当てられたリソースをマッチングしてスケジュールすることが可能。むしろYARNみたいに中央集権的にスケジューリングするよりも、Mesos用にスケジューリングアルゴリズムを自律的に使い分ける方が便利なケースもあるだろうから、Data localityがあるから優れていると一方的に評するべきではない。それでも、On the flyですぐLocalityを考慮してジョブを動かせるのは便利だけど、それは計算フレームワーク側が対応してるかどうかの問題じゃないかと思う。もちろんYARNの方が対応してるソフトウェアは多いと思うが、それは個別のソフトウェアの話だろう。

分散システムという言葉について

また、本書の全体を通して「分散システム」という言葉が定義なしに使われていて、都度どのような故障モデルや通信モデルを備えているのか、合意の基準は何なのかが引っかかる。

特にP150では「TCPではメッセージにシーケンス番号を付けますが、分散システムではシーケンス番号はあまり使われません」と表記していて、続く文章で欠番のないシーケンス番号の発行は(いわゆる故障あり非同期通信モデルでは)現実的に難しいためと解説している。たしかにトランザクションIDやTCPのシーケンス番号、REDOログなど欠番があったときに途中のメッセージを待つ必要がある場合には、要件を満たすシーケンス番号を発行することが技術的に難しい(Twitter の Snowflake などはあったが、それだけでクラスタを一つ組まなければならない)ので「使われません」という表現になる。なる、が、非常にこれはミスリーディングで、我々がシステムで依存しているPaxos, Zab, Raft といった分散合意プロトコルは欠番を許容するシーケンス番号を順につけていって、プロトコルの正しさはその順序性に依存しているのである。Raftはシーケンス番号の欠番を許さないが、欠けたデータを復元する手順を持っている。

この言い回しが紛らわしいのは「分散システムでは」の主語が大きいことに由来しているので、もっと限定的に書くべきであった。そもそもこの文章はストリーム処理における "at least once" の解説に含まれている場面であって、冗送排除の文脈であって欠損メッセージの検出ではない。したがって同じメッセージには同じIDがついているだけで十分で、送信側が受信側からAckを確認するまで再送し続ければ at least once は達成できる。つまり欠損の検出が不要なわけで、シーケンス番号じゃなくてもいい…シーケンス番号はよく使うんだよ…という主張だ。「あまり使いません」というミスリードは不要だったのではないかという話。

最近のBashoのニュースの「買収」という言葉はちょっと違う(追記あり)

PublickeyというIT界隈でわりと影響力のあるサイトで分散型NoSQLデータベースの「Basho」をギャンブルサイトの「Bet365」が買収。全製品のオープンソース化を表明という記事が公開された。しかしながらこの記事は若干の誤りを含みつつミスリードが多かったのでここで指摘していきたいと思う(この記事の公開後に修正あり)。今北産業の方々は末尾のまとめをご覧いただきたい。

www.publickey1.jp

なお私は 2016年3月までBashoの日本法人の被雇用者であり機密情報を一部知る立場であったが、ここでは公開情報だけをもとに解説する。また現在は一連の関係者との公的な関係は一切なく利害関係にないことを明記しておく。つまり外野で野次馬です。

基本的な指摘事項

Bet365を表現するのに「ギャンブルサイト」という言葉は一般的ではない、きちんとした会社である(対応済み)

はてブでブックメーカーをギャンブルサイトといえば確かにそうだけど。というコメントがついている通り、Bet365は伝統的なブックメーカーのオンライン版であると表現するのが正しい。「アメリカの大統領選挙やゲームの大会、アカデミー賞の授賞者や次のジェームズ・ボンドを演じる役者等もブッキングの対象になる」とあるように、イギリスではプレミアリーグから何から何までギャンブルの対象にすることが法律で認められている。飲み屋でよくある「アイツが明日遅刻するのに10ポンド賭けてもいいぜ」みたいなのが大っぴらにできるというわけだ。日本では賭博行為は一部の公営のものだけが認められており、その他の賭博は全て違法である。日本語で「ギャンブル」というときはネガティブな文脈で出ることが多く、関連付けて記述されたものはよい迷惑であろう。

こちらの解説にもあるようにBet365はきちんとした歴史ある会社で知名度も高い。

BET365とは1974年から続く超老舗ブックメーカーで、 現在は、全世界200ヵ国に500万人の顧客がいる と言われている大手メーカーです。
イングランドプレミアリーグ(イギリスのトップリーグ)、ストークシティのユニフォームスポンサーを務めるなど、名実ともに信頼ある大企業です。

しかるにPublickeyではタイトルからしてミスリーディングであり、Riakというソフトウェアの将来が怪しいギャンブル企業に買われてしまってどうなってしまうのか分からない…といったことを示唆する記事になっている。もちろん本文にそういった記述はないが、日本での賭博行為に対する一般的なイメージからいって先入観をもって読まれることは確実であろう。

したがって、新野さんは何よりもそれを予め防ぐような書き方をすべきであったと思います。訂正入りました

Riakを始めとするBashoの製品は「ほとんど」がそもそもオープンソースソフトウェアであった(対応済み)

記事には「Bet365のCTOが、Bashoの全製品をオープンソース化すると宣言」という見出しがあり、この曖昧な記述ではBashoの製品がプロプライエタリであるかどうかはっきりしない。全製品をオープンソース化という表現は、全製品がクローズドソースであったことを強く示唆する書き方であり、Riakというソフトウェアの正しい理解を妨げると思う。もともとRiakはOSS版とプロプライエタリ版があり、OSS版では一部機能が実装されていないという差があっただけのことだ。それはPublickeyの以前の記事(Amazon S3互換、Yahoo! Japanも採用した分散オブジェクトストレージのRiak CSがオープンソースで公開 - Publickey)でもある程度触れられていると思ったのだが、ここの記述は簡素に過ぎると思う。

OSS版との機能差は主に以下である。

  1. データセンター間レプリケーション
  2. SNMP/JMXによる監視機能

SNMPなどはまあオマケで、基本的にこのデータセンター間レプリケーションが目玉であったため、ここだけはソースコードは公開されていなかった。OSS部分は実に膨大で、ソフトウェアの機能でいうと9割以上はOSSとして公開されていたといっていい。いちおうここに機能差の表がある(が、いつまで残っているかはBet365次第だろう)

Bashoの資産はソースコードだけではないし、全ての資産を買収したわけでもない(対応済み)

Bashoの資産は商用版のソースコードだけでなく、他にも多くのものがある。

  1. 既存アカウントとのサポート契約
  2. basho.com のドメインと関連するインターネットサービス( *.basho.com のWebサイトや riak-users などのML
  3. GitHubアカウントや、Bashoが持っていた各種データ、ログ、ビルド関連のツールやサーバーなど
  4. Riakの商標権

たとえばRiakのドキュメント docs.basho.com はしばらく前から利用できなくなっていたし、 RiakのカンファレンスRICONのサイト ricon.io も今はアクセスできくなっている。RiconはRiakに限らない分散システムのカンファレンスを標榜していて、Riakに限らず分散オタクたちのハードコアなカンファレンスとして有名であった(こういうやつ)。まあGitHubアカウントやいろいろな性能や試験などのソフトウェアに関するデータはそのうち出てくるかもしれないし、Bet365が不要だと判断して破棄するかもしれない。

なかんづく重要なのはRiakの商標権で、これについてスレッドでも盛り上がっていた。商標権を確保しているといないとではOSSとしてのRiakの使いやすさが大きく違う。もちろん商標がなくてもライセンスで認められているのでOSSとしてソフトウェアを利用し続けることはできるが、Riakそのものを使ってビジネスをすることが難しくなるし、OSSとして好ましい状態ではない。Hudsonのことを覚えておられる読者諸賢も多いのではないだろうか?

最後の問題点は既存アカウントとのサポート契約だ。Bet365の人からのメールにも "Basho's remaining assets (except support contracts)" と明記されている。つまり厳密には「Bet365とBashoは、Bashoの資産をすべてBet365が買収することで合意」という表現も誤っている。

私の推測では、Bet365の動機はこの商標権とデータセンター間レプリケーションなのではないかと思う。データセンター間レプリケーションは長年の大型クラスタでの無停止運用にも耐えた実績があり、こちらをうまくコミュニティで共同でメンテナンスすることで使い続けたいという意図がOSS化の背景にあると想像している。

「買収」の背景: これはいわゆる普通のスタートアップの買収とは違う

さてRiakやBashoという名前、昨年はほとんどインターネット上で見かけることもなかったと思う。今年に入ってからはめっきり動きがなくなり"Will the last person at Basho please turn out the lights?" と、その消えっぷりに疑問を持つ人が多くいたくらいだ。これが 7/13 で、その月末には End of the road for Basho: Court puts biz into receivership • The Register という記事が出ており、 "filed for receivership in early July after Basho defaulted on payments" と書かれている。つまり資金繰りができなくなって7月にreceivership状態になった(何と訳すのがよいか知らないが「管財申請」とか財産管理状態ということだろう)。Wikipediaによると破産すらできない状態ということらしい。こうなると具体的にどういうプロセスを経ていくのかは詳しくはないので分からないが、こういう状態であるから、いわゆるスタートアップの買収とは異なり人もモノもないので、二束三文の価格だったのだろうと容易に推測できる。つまりBashoに投資した投資家は大損こいたわけである(あれ、Receivershipになったということは投資家には二束三文どころか1セントも戻らないということ?アメリカの制度詳しくないので誰かに教えてほしい)。これは救済とは呼べない。

実際に世界中のオフィスが閉鎖され、ほとんどの従業員が既に解雇されており、Bashoの良心たるMvMが Basho closed とメッセージを発信していた。さてこれで困るのは大規模なRiakクラスタを抱えるユーザーたちである。データセンター間レプリケーションを除くほぼ全ての機能はソースコードが公開されているからすぐには困らないものの、ソフトウェアをメンテナンスしながら使い続けるか、他のソフトウェアに移行するかを選ばなければならない。後者は基本的に黙って去るので、特にインターネット上で観測できない。前者はBet365を筆頭に、BashoとRiakの技術を高く買っているところが集まったようだ。6月にはErlang Solutionsが商用サポートの検討を始め、8月の時点で商用サポートが行われることがアナウンスされた。- Erlang SolutionsのRiakページ によるとRiak CSもサポート対象のようだ。おおお。。。

NHSは商用版に諦めをつけ始めたのか、データセンター間レプリケーションのミドルウェアをRabbitMQを使って作ってしまったようだ(公開直後にBet365のニュースを知って驚いたともコメントしている)。

Riakはこれからどうなるのか?

コミュ二ティでは、Bet365、Erlang Solutions, NHS を中心にメンテナンスが続けられていくだろう。公開予定の商用版コードについてはApache 2ライセンスが支持されているようだ。その場合、Bashoなき今、著作権者は誰になるのだろうか? 素直に Apache 財団に送ってもよいと個人的には思うが、みんなJIRA嫌いだったしなあ…CNCFってこともないだろうしな…

商用サポートについては、アナウンス通りTI Tokyoという東京の会社がサポート契約を買い取っており、既存顧客のサポートはそちらでErlang Solutionsと共同で行われる模様だ。
あとのことは分からない。

まとめ

  • Bet365は「ギャンブルサイト」ではなく伝統的なブックメーカーであり、合法で社会的に認められた事業である
  • 「全製品をオープンソース化」ではなく、これまでプロプライエタリだった部分を公開するとBet365が宣言した
  • Bashoの資産はソースコードの他にもいろいろあって一番不安視されていたのが商標権
  • これはいわゆる普通のスタートアップ買収とは異なるものであるが「救済」という言葉も少し違うと思う

追記: その後コメントをいただき、記事が修正された。時間をみるにわたしが記事を公開した直後の対応だったようだ。

参考

Replication (Lecture Notes in Computer Science)

Replication (Lecture Notes in Computer Science)

Real World HTTP ―歴史とコードに学ぶインターネットとウェブ技術

Real World HTTP ―歴史とコードに学ぶインターネットとウェブ技術

ハイパフォーマンス ブラウザネットワーキング ―ネットワークアプリケーションのためのパフォーマンス最適化

ハイパフォーマンス ブラウザネットワーキング ―ネットワークアプリケーションのためのパフォーマンス最適化

2017年冬〜春アニメまとめ

概要

冬は「この素晴らしき世界に祝福を!2」「CHAOS;CHILD」くらいしか面白いものがなくて不作であった…と思ったら、あとで追いついた幼女戦記がここ一番の出来だった。。春は完走は多かったものの「有頂天家族2」が突出していてベルセルク2期は安定、次点は「つぐもも」か。

リアルタイムではないが2017年上半期に後から完走したものとして「響け!ユーフォニアム」2期、東京喰種√A、青の払魔師、この素晴らしき世界に祝福を!、SAOおよびSAO2、有頂天家族1期、幼女戦記Charlotteなどが高評価だった。

個別

昨年秋アニメも残していないものがいくつかあったので合祀。面白いところはネタバレしないように気をつけています。

  • 無星: 見る価値がない。一応完走
  • ★: 一度は見ておいた方がよい
  • ★★: もう一度見返しておきたい
  • ★★★: 他人に自信をもって勧めたいレベル

幼女戦記 ★★★

前世紀の魔法大戦物だけど、転生もの。空戦の描写はハリウッド的で迫力があってSEもよい。なんとも言えぬ閉塞感の中でとにかく勝ちまくるのが非常に気持ちがよい。帝国が滅ぶところが全然想像できない。アニメでは時間が足りなかったが、漫画だとすれ違いが強調されていてこれは別にまた面白い。2017年上半期個人的No.1をあげたい。

eYe's 【通常盤】

eYe's 【通常盤】


オープニングテーマが非常に気に入ったのでアルバムを買ったら、Re:ゼロでもいくつか曲提供している人たちだった

ゼロから始める魔法の書

傭兵とゼロの魔法の国のお話。国が案外小さいのと、ゼロの魔術師団があまり賢くなくて悲しい。傭兵のハイパー超人クライミング技術はすごいんじゃないかと思う。

終末何してますか?忙しいですか?救ってもらっていいですか?

ようわからんかった…原作みたら面白いと思えるのかもしれないけど、ファンタジー度が高くて俺には難しそう。ヒロインが14、15歳なのに結婚とかいうのもちょっとオッサンにはきつい。

ソートオラトリア ダンまち外伝

ダンまちが面白かっただけにちょっと残念。59階層に着いて終わりで、アイズの正体は生い立ちに切り込んでからが面白そうなのだけど、2期がちょっとなさそうな感じ…

有頂天家族2 ★★★

一家の心温まるドタバタ喜劇に、天狗親子の確執と愛情を織り交ぜてより面白くなった。

有頂天家族 ★★★

一家の心温まるドタバタ喜劇。ウィットのある会話と話のおかしさと家族の絆がとてもよい。優しくなれるお話

有頂天家族 (幻冬舎文庫)

有頂天家族 (幻冬舎文庫)

武装少女マキャベリズム

武闘派学園ハーレムもの。

ベルセルク2期 ★★

安定。断罪の塔編終了後から

ロクでなし魔術講師と禁忌教典

肌の露出多い以外はなかなか面白い魔法学園もの。主人公がやる気がないっていう典型的なところが感情移入できてすばらしい。結局アカシックレコードのカケラも出てこなかったが、二期は厳しそう。

つぐもも ★★

軽快でテンポのよい定番コメディ。戦闘シーンはまあまあ迫力があるし、主人公の成長もよい。今思ったけど、かなり「かんなぎ」にクリソツじゃね…?

この素晴らしい世界に祝福を!2 ★★

安心してゲラゲラ笑いながら見れるのでよい

この素晴らしい世界に祝福を! ★★

ゲラゲラ笑いながら見れるのでよい

CHAOS;CHILD

妄想科学ADVっていうけど全然科学的じゃなくて悲しい。10年前のテキストゲーをみているよう

風夏

ひたすらだるい、人気絶頂のアイドルと幼馴染で三角関係とか30過ぎたオッサンにはきつい少年誌ファンタジー。そんな簡単にベース覚えたり作曲したりできるわけねえだろ!

ガンダムTHE ORIGIN IV ★

UC最初のモビルスーツ戦のやつ。まあこれはガンダム税なので…

響け!ユーフォニアム2 ★★★

前期は地方予選。全国大会まで行って…部活する女子高生がどんどん成長していくのがよい。

響け!ユーフォニアム ★★★

とにかくみんなかわいい。部活する女子高生の機微がこれでもかと描かれていて(当時理解できなかったのが)つらい。

鉄血のオルフェンズ2期 ★

ガンダム税とられましたって感じ…ラスタルエリオンがそのままってのはどーも納得いかないですね

終末のイゼッタ

なんか考え方が封建っぽい、魔法戦闘のシーンはかっこいいのだけど、幼女戦記を見てしまった今では非常に色あせてみえる。

双星の陰陽師

陰陽師幽霊戦闘、体の一部が人間じゃなくなった変態系の中学生〜高校生の成長モノ。長かった、普通に分かりやすく少年誌でよいはなし。

セイレン

9話までみたけどだる過ぎて切った。ストーリーはともかく作画崩壊が多くて原作の魅力が台無しなのでは。原作みてないけど。

非リアルタイム

dアニメストアで配信された過去の作品を少しずつ見ていく。

Charlotte ★★★

面白くて一気に見てしまった。展開がベタで分かりやすいのだけど、友利がかわいい(そればっかりだけど)のでつい見てしまう。途中で出てきた華僑系っぽいマフィアはえらく中途半端で弱かったり、1年かそこら?で世界中の能力者から能力を奪うなんてできるのか?それだとせいぜい数千人くらいしか能力を奪えない気がするのだけども。

結城友奈は勇者である

まあまあいい話だったけど、最後の出来事(大赦が勇者を解放したアレ)だけがどうしてもわからない。女の子に「うおおおおおおおおおおおお!!!!」って言わせるのを楽しむやつ。

未確認で進行形 ★★

日常系なんだけど小紅がとにかくかわいい。前半だるいけど後半からテンポ上がって飽きなくなる。

ソードアート・オンラインII

GGO編とエクスカリバー編。詩乃がとにかくかわいいが、展開が1期に比べてちょっと平凡というかスリルに欠ける。スリル要素が少数の悪役に絞られてしまったところが厳しいか。

ソードアート・オンライン ★★

最強主人公モノはやっぱり定番で王道。SAO編はやっぱり命がかかっているというスリルがあって非常によかったが、ALO編はヒールを倒すだけの話になってしまってちょっと残念。あと、2年も寝たきりで意識のない人間はもっとやつれてると思うゾ。

青の祓魔師 ★★

少年誌らしい、飽きさせない展開でつい最後まで観てしまった。

東京喰種√A ★★★

漫画も :re まで全部読んでしまった。喰種という天敵が人間社会に潜伏してるというそのプロットがすでにずるい。登場人物がみんなキャラが立ってて、いくらでも四コマ漫画が書けるみたいだ。

氷菓 ★★

ウィットに富んだ謎解きの話。しかし高校生にしては教養ありすぎじゃないか?!えるの作画がときどき「あざといなー」と思いながらもついつい見てしまった。

トリニティセブン

ラッキースケベ学園ハーレム異世界転生もの。敵役との妙な馴れ合いとか、モブの命が軽すぎるとかいろいろ感情移入しにくい要素があった。

東のエデン劇場版 Paradise Lost

記憶を取り戻して母親を探したり。ラストは納得行かない展開だけど、Juisだけはかわいい。100億円使って日本をよくするという話、ニーチェ的な超人論に持ち込んでいて既視感満載だったのでちょっと楽しめなかった。いやそんなに単純じゃねーから…というのは野暮。

東のエデン劇場版 The King of Eden

記憶をなくしてリセットされたところから。ニューヨーク編

東のエデン

巷で言われてるほど…って感じだった。アニメで完結せず劇場版に続く

完走できず

sin 七つの大罪

魔導学園HxH枠。マリアが可愛くてみていたが、巨乳はそんなに好きじゃないしHxH以上にストーリー皆無だった。

ガリレイドンナ

時間切れ。ガリレイの秘密はまあよいが、それにしても科学まわりのファンタジープロットがいささかお粗末。

BanG Dream!

切った。アニメは最高につまらなかったがゲームが出て売れていると聞いて、ああ俺はお呼びではなかったのかと得心した。

グラスリップ

PAworksということで期待しながら半年くらいかけて少しずつみていたがついに断念(2017/6/7)。岡田麿里路線を目指してみたようが狂気とインパクトに欠ける

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勢に対する煽りが少し攻撃的だったのでマイルドな表現に修正した。

一次情報を確認しなければ信頼性のある記事にはならない

こんばんは、やっと先週ガノンの打倒という宿願を果たし、ハイカラシティからもいささか足が遠のいてしまった私であるが、なんとか季節の変わり目にも風邪を引かずに過ごせている。読者諸賢はいかがお過ごしだろうか。はや4ヶ月、1年の1/3が過ぎてしまったが、先日の大🔥炎🔥上🔥騒🔥ぎで2017年のクラウドを何だか占い損ねた件を覚えておられるだろうか。これが公共のメディアに書く価値があるどころか、記事で取り上げられた会社の名誉や主張を歪曲しかねないものであったことを。

本日、友人に教えられ、同じ記者が同様に見過ごせない記事を書いたことを知ったので、いっそ皿まで、いやとりあえず再度批評することとしたい。それがこれである。リンクを踏んでPVに貢献することは結構だが、後悔するのでやめておいた方がよい。

it.impressbm.co.jp

リンク先を読んでない方は、次の指摘からもおおよそのクオリティがおわかりいただけるだろう。

この平氏を直接は私は存じ上げないが、Redhat Linuxに非常に精通しており、恵比寿でコンピュータ・ソフトウェアに関する仕事をしているということは事実のようだ。

AWSとの戦略的提携を発表、OpenShift Container PlatformからAmazon Redshift、Amazon AuroraなどAWSのマネージドサービスがダイレクトに利用可能に

これが平氏の指摘であるが、AWSRedhatはもともと戦略的提携をしており、双方の公式発表をみても Red Hat and AWS Extend Strategic Alliance to Package Access to AWS Services Within Red Hat OpenShift , Red Hat and AWS Extend Strategic Alliance to Package Access to AWS Services Within Red Hat OpenShift と、いずれも "Extend Strategic Alliance" という表現を使っている。これは、素直に英語を読めば「もともと戦略的提携をしていたが、提携を拡大しOpenShiftからAWSを使えるようになった」という話になる。まったく提携していなかった2社が提携を始めるわけではないので、これではニュースバリューを偽って誇張している表現である。

これまでどのような提携をしていたかは、Redhatが出しているフォローアップの記事 AWS and Red Hat -- Digging a little deeper を見ればすぐに分かる。本文の早い時点で "March 2010 was an exciting month in the collaboration history of Red Hat" (2010年3月はRedhatの歴史上とてもエキサイティングな月だった)と書かれており、ここからAWSRedhatの提携が始まったことがわかる。具体的にはEC2のMarketPlaceでRedhatサブスクリプションつきのイメージが買えるようになったのだと記憶している。こちらの記事 - AWS Partner SA ブログ: AWS上のRHELのサポート体制とアップデートサーバー は2015年であるが、その内容がわかりやすく日本語で書かれている。また、今回の提携拡大の伏線としては Deploy Red Hat OpenShift on Amazon Web Services | AWS Partner Network (APN) Blog が分かりやすい。AWSが大好きな顧客の声を汲むなら、「ここまで来てるんならもういっそAWS隠蔽して適当に使えるようにしてくれよ!」だろう。

次はこちらだ。

コンテナベースでクラウドネイティブなアプリケーション開発環境「Red Hat OpenShift.io」を開発者向けに無償提供

OpenShift.io The Gathering – Summit 2017 – Developer Tools, Overview and Roadmap Part I には、

OpenShift.io is the next generation OpenShift platform, based on OpenShift 3, for building and running applications in the cloud.

と書かれている。ここで重要なのは "building and running applications" という部分で、正確に訳すなら「アプリケーションの開発と実行」である。つまり、OpenShift platformはアプリケーションの開発環境と実行環境を兼ね備えたものであり、開発環境だけのものではない。この記事を丁寧に読んでいけば、OpenShift(コンテナのオーケストレーション技術)がどのようなものかはすぐに分かるだろう ( 新野さんの記事も非常に分かりやすい )。2017年のクラウドを占ったときの「これからはDevOpsがクラウドで重要になる」というフワッとした指摘を奇しくも裏付けた形になり、それをベースに記述を肉付けしたら伏線を拾ったもっとよい記事になったであろうに、勿体ない。

Disney、Pixarなどのユースケースに見るOpenStackおよびコンテナ関連のビジネスの拡張

これは、どうしてこういう表現になるのか分からない。残念ながら私も現地には行っていないので分からないが、おそらく Disney Studios and Pixar use OpenShift to accelerate the delivery of platforms and services のセッションを指しているのだろうと思うが、少なくともOpenStackという文字は文中になく、むしろOpenShift推しなのが分かるだろう。また、セッションの検索 をしてみても、OpenStackは32件、OpenShiftは95件のセッションがマッチした。これをみても分かるようにOpenStackは下火で、OpenShiftとコンテナオーケストレータの採用が拡大している傾向の方がニュースとしては正確である。ひょっとしてOpenShiftとコンテナとOpenStackの関係が理解されていないのでは…とうっかり疑ってしまうので、その関係がよく整理されている OpenStack、Docker、OpenShiftの関係を理解する! レッドハット朝活セミナーのご紹介 | RED HAT OPENEYE を紹介しておこう。

そして、推測にみちたこの文章

今回、その距離を一気に縮める提携を発表したことは、AWSと近しい関係を構築するほうがメリットが大きいと判断したといえる。

は、「ただのパートナー→戦略的提携」という前提にもとづいているが、もともと戦略的提携していたのだからこの文章はほとんど意味がない。私の考えでは、今回のサミットで特に距離を縮めたということは別になくて、その傍証として、キーノートにAWSからの有名人(例えばWerner VogelsやHamilton)どころか、誰もキーノートで話していないことを挙げておこう。しかも、セッションスピーカーで検索してもAWSのスピーカーが3人しか見つからなかったことも付け加えておこう。

で、「プライベートクラウドパブリッククラウドの境界線がより曖昧になっている流れ」とは一体何なのか。ハイブリッドクラウドユースケースが増えていることを指すのだろうか。境界線が曖昧とは一体どういう意味なのだろうか。少なくともシステムの管理主体と利用者がはっきりしている限りは境界線が明確にあると思うのだが、考えれば考えるほど意味がわからない。

次は「エンタープライズ企業によるDockerの採用が増えるにしたがい、オープンソースコミュニティを重視するスタイルをビジネスと両立させることが難しくなってきたのも事実だ」という表現だ。何が難しいのだろうか。私は仕事で体感したから知っているが、難しい理由は具体的にはモノによって様々に異なっており一般論として述べるにはまだ十分早いと思う。なぜなら直後に記事でべた褒めしているRedhatサブスクリプションモデルで成功しているからだ。

いちおうDocker CEO 退任の挨拶から以下の文を引用しておこう。

Docker has the potential to become not only one of the most enduring technology companies, but also a transformational platform, technology, and movement; I can’t think of a better or more qualified individual to lead us to that future than Steve.

オープンソースソフトウェアでビジネスをするのは難しいということであるが、さてここでCrunchBaseのランキングを指摘しておこう。この記事で取り上げた Docker (26位) よりも Hortonworks (152位) よりも、第2のRedhatに近い存在がいる。 "Open Source" "Enterprise Software" でカテゴリを any 検索するとすぐに出てくる、12位の、先日IPOしたヤツである。

f:id:kuenishi:20170509235744p:plain

まあこのランキング、IPOしてるしてないとかゴッチャだしRedhatは登場しないし、IBMがかなりの下位だったりと独自のランキング手法であるが、今調べたら時価総額で3.5倍程度差がついているこの会社をスルーしてHortonworksを取り上げるのは数字上はかなりアンフェアだと私は思う。ちなみに、150位くらいまでに出てくるOSS企業は MongoDB (56位), Pivotal (128位), Elastic (168位), Databricks (182位), あたりがある。