4日で学ぶモデル検査 (初級編)

4日で学ぶモデル検査 (初級編) (CVS教程 (1))

4日で学ぶモデル検査 (初級編) (CVS教程 (1))

衝撃的なタイトル。モデル検査もこんな俗っぽいタイトルが付く程度に一般的なものになったのですね。科学の見事な勝利です。

本当に4日以下で読むことが出来ます。時相論理を扱っていますが、内容は非常に簡単でわかりやすい。初級編とありますが、本当に初級で、現実のシステムに応用できるまでには当然至ってませんし、本書を読んだ限りではどうやって応用するのか検討もつかないくらいです。

載っているPromelaやNuSMVのコードがあまりエレガントに感じられず、モデル検査とはこのような泥臭いものなのか、あんまりやりたいことではないなあと思ってしまいました。

中級編、上級編は果たして発売されるのでしょうか?

基盤ソフトウェア 5/15

Java仮想機械

先週はJavaのヴァーチャルマシンの話をしていた

  • -
Javaバイトコード 普通の機械語とすごく違うわけではない 最近は下火だけれどJavaバイトコードを直接実行するプロセッサを作っていた 今はどっかのメーカーに行けばあるかもしれないけれど 大々的には売れていないはず 最初は携帯電話などに売り込もうとしたのだけれど 何が悪かったのかわからないけれど ビジネス的には失敗している ただしバイトコードの全部を実際に実行できるわけではない メソッド呼び出しなど、 できなくはないのだろうけれどあまり現実的ではない そこらへんはハードウェアではやっていなかったはず 割り込みが発生してどっか飛んでいく 携帯電話のチップはコストパフォーマンスが激しい 携帯電話のプログラムは全部がJavaというわけではない そういうのもひっくるめて安く効率よく開発できないといけない Javaだけが動いてもねえ…という感じかも 元々の目論見は全部Javaでやればいいんだ、ということだったのだろうけど しかしサンは最近もまだまだ組み込みに活路を見出そうとしている
  • -
Java機械語を素直に実行するならインタプリタを作ることになる そうするとバイトコードは小さくなるけど実行性能はでない 普通の機械語だったら1サイクルで1命令 インタプリタだと100サイクルくらいかかるかもしれない 単純に100倍遅くなる Javaが登場してからわりとすぐ、 まともな速度で動かす技術(Dynamic compilation)がでてきた Java以前からあった技術 Smalltalkとか IBMが今のJavaの役目をSmalltalkで置き換えようという時期も一瞬あった 要するにCOBOLの役目を置き換えたかった 結局COBOLJavaに置き換えられつつある しかしIBMSmalltalkの会社を買収してしまったのでどうしよう?レイオフ? 結局SmalltalkJavaの開発環境とか作った 割と良く出来ていたのでそれをJavaで書き換えてEclipseができた という関連がJavaSmalltalkにはある サンはSmalltalkコンパイラを作っていたエンジニアを引き抜いて Dynamic compilationの技術を取り入れた 実行中にバイトコードをネイティブコード(x86とか)に変換(コンパイル)する コンパイルという言葉は普通人間が読めるプログラムから機械語に変換することを言うけれど 広く捉えれば機械語から機械語へもコンパイル Just-in-time ロードした後、実行が始まってからコンパイルを行う hotspot 良く実行されているところ 良く使われる回路が熱くなるから? ともかく熱くなっているメソッドをhotspotと呼ぶ 無制限にコンパイル時間をかけられない コンパイル時間を短くする必要がある 普通のコンパイルは編集した直後にやるのですごく時間がかかっても許される 最近の人はせっかちだからあまり許されないかもしれないが… Eclipseを使っていると編集しているそばからコンパイルしている すごくコンパイル時間が体感で短くなる まあ今の人でも2、3秒なら許されるのかな ネイティブコードに変換する目的は Javaを早くするためにある 早くするためにコンパイルをする しかしJITなのでコンパイル時間は実行時間に含まれている コンパイルに時間をかけすぎるとかえって遅くなってしまう いかにしてコンパイル時間を短くするか 全部をコンパイルしない 何度も実行される部分だけコンパイルする              インタプリタ コンパイル あるメソッドの実行時間     3秒    1秒                      +5秒(コンパイル時間) 実行回数1回           3     6 実行回数5回           15   5+1*5=10 良く実行されるメソッドやループの内側を探し出してコンパイルすると 多少コンパイルに時間がかかってもトータルでも短くなることが期待される しかしコンパイルの結果はディスクに保存しなければいけない メモリのオーバーヘッドも考えなければいけない 仮想記憶を使っている時など… コンパイルにはいろいろ程度がある 最適化を強力にかけるかそうでないか 普通は時間をかけてより強力な機械語を出力することが多いが あえて最適化をしないという戦略もある まず軽くコンパイル それでもインタプリタよりは早いでしょ 何度も実行されたら最適化をかける プログラムの殆どの部分は軽くコンパイルをかけていおいて ここは最適化を頑張った方がいいぞというところは時間をかけて最適化をする インタプリタをほとんど持っていなくて 最初に軽くコンパイルをかけるようなものもある JITではないものはAhead-of-time compilationと呼ぶ しかし一般的なJavaの仮想機械ではAoTは使われていない 教科書的な理由は、実行中にコンパイルした方がよく最適化されたコードが出てくる Dynamic compileの利点 良く使われてかつ短いメソッドをインライン化 分岐予測、最近はハードウェアでやるのでソフトウェアだとどうなのかちょっとわからない JavaというのはDynamicにプログラムをロードうすることができるので …という話は後にしましょう ではAhead-of-timeの欠点は? 分岐予測とかは普通のコンパイラでもプロファイルを利用すれば大丈夫 AoTが使われないのは性能云々ではなくJavaの使われ方の問題 ブラウザの中でJavaVMを動かしていてDLしてきたものを実行する、など Ahead-of-timeはサーバサイドでは悪くない クライアント側で使おうとすると起動するたびにコンパイルするのではたまらない 対話性が著しく悪い 開発する側も2回もコンパイルするのが面倒 また、セキュリティ上の立場からもよくない Officeとかも起動した直後はなんだか遅い おそらくAoTを行っているのではないか JavaVMと同じような技術を使っている
  • -
Escape Analysis x86とかのハードウェアで直接実行される機械語に変換すればまあ早くなる しかしJava言語特有の遅さというものもある JavaはCと違って高級すぎるので単純にコンパイルしただけでは あんまり早くは動かない Cでも経験のない人が書いたら遅くなってしまうかもしれない Javaだと経験のある人が頑張って書いてもあまり早くは動かない メモリ管理 Javaの場合は全てヒープ領域に割り当てる 簡単に言えばCでmallocを使って割り付けるようなもの 実行中に空いているところを探して割り付ける 動的に割り付ける  ある変数はずっと使われ続けるわけではない  使い終わったところは違う変数のために再利用  ここは使われている  ここは使われていない  そういった情報を管理する 動的に割り付けるのは結構大変 そんなに早いわけではない メモリも飛び飛びになってしまうし Cっていうのは、プログラマは偉い、何でも知っている、 というのが前提の言語なので スタック領域にメモリを割り付けるという方法も選べる スタック領域とはメソッド呼び出しの際にまとめて確保される領域 メソッドは最後に呼び出したメソッドが必ず最初に終わる メソッドが終わったらまとめて解放する これならフラグメンテーションが発生しないしすごく高速に管理できる 続きは来週