2006-07-04
森見登美彦, 太陽の塔. [ISBN4-10-129051-2]
私は招き猫に問いかけた。
恋したごときで何を威張るか。恋する者はそんなに偉いか。
「僕の２０歳の日々が美しかったなんて誰にも言わせない」と言ったのは誰だったか [google] 。人並みに明るい青春を予感していた若者達は，その予感に反し灰色の青春が眼前に広がっていくのを見るにつれ，自らの背負う運命が世間のそれとは大きく異なることを知る。そこで普通ならば，少しでも人並みの幸せを手にしようともがき苦しむものを，誇り高き魂を持つ彼らは，世間と決別し，ありふれた幸せと決別し，他の様々なものとも決別し，ただ己の妄想力のみを手に，同じ志を持つ者と共に孤高の存在を目指し，暴走する。
ともすれば偏屈な人々の繰り広げる独り善がりな行為の顛末になってしまおうものが，ここまで清々しく感じられる痛快な物語となっているのは一体何故だろう。ひとえに彼らの生き様は美しく哀しい。何故人は，己の生きたいように生きることができないのだろう。己の愚かさを世間に転嫁し，己の醜さに目を瞑り，ただ己の信ずるままにその道を突き進むも，時折顔を覗かせる弱さと幸せへの未練が，不意に彼らを失意の底へと突き落とす。彼らほどの潔さをもってしてもなお，幸せとは暖かく捨て難いものであるに違い無い。失意の中で悩み苦しむ彼らの姿を見るとき，読者は彼らの隠された人間性を密かに感じることだろう。
（とか言う適当な感想はさておき，恋愛と青春の素晴らしさを，まったく素晴らしくない例をもって示すとこうなる，という愉快な小説。一点だけ注意としては，まかりなりにも『ファンタジーノベル大賞受賞作』であるということを覚えておかないと，たまに思い出したように挿入されるファンタズムに面食らうことになる。その点は心しておいた方が良い。）
2006-07-05
Image from Defence Review
Defence Review の記事によると，先月７日，ペンシルバニアは Action Manufacturing Company において，フル・オートマティック散弾銃 AA12 を利用して１２口径榴弾 FRAG-12 を射撃する試験が行われた [DefenceReview] 。試験結果は良好であり， AA12 と FRAG-12 の組み合わせが有効なものであることを示した。
記事に添付された映像を観てみると，これが非常に印象的な威力を持つ組み合わせであることが分かる。毎秒６発という従来の散弾銃には有り得ない連射性能の高さと，鉄板をも打ち砕く榴弾の破壊力の凄まじさには，空恐ろしいものを感じる。
AA12 (Auto Assault-12) は Military Police Systems 社によって開発されたフル・オートマティック式１２口径散弾銃である。旧式の軍用散弾銃 AA-12 (Atchisson Assault-12) [Guns] や USAS-12 [Guns] をベースとしているが，そこからの変更点は 188 箇所にも上り，リコイルスプリングを除いてはほぼ別物に仕上がっているというのが実情であるとされる。この辺りの開発経緯については Soldier of Fortune 誌の記事に詳しい [Military.com] 。
AA12 の特徴は，連射性能の高さと，メンテナンスの易さ，リコイル（反動）の小ささにある。これらの特徴については，別の記事に添付された映像を観てみると分かりやすい [DefenceReview] 。２０発ドラム形弾倉をあっと言う間に撃ち尽くしてしまうほどの連射性能の高さは，マシンガンならぬ「マシン・ショットガン」の異名を与えられる所以でもある（もっとも，あれだけ大きな弾倉に２０発しか入っていないというのも驚きだが……）。また，長大なリコイルスプリングを用いることにより実現された "Constant Recoil" 技術は，反動の小ささという点において過去のフルオート火器と一線を画す。散弾銃と言うとただでも反動が大きそうだが，これを片手で撃つことさえ可能になっている。
また， AA12 の紹介記事では，必ずと言ってよいほど FRAG-12 が併せて紹介されている。 FRAG-12 は Experimental Cartridge Company および Action Manufacturing 社によって開発された１２口径榴弾である [DefenceReview] 。１２口径３インチ長の一般的な薬莢の中に，推進剤，安定翼，１９ミリ弾頭が搭載されており， 200 m 先の目標までを狙うことができる。弾頭には榴弾，対人榴弾，徹甲弾の３種類が存在し，徹甲弾を用いれば 0.5 インチの厚さの鉄板をも貫くことが可能とされる [USMC] 。これらの弾頭を用いることにより，例えば軽車両に致命傷を与えることが可能になるなど，主に都市戦において様々な威力を発揮するものと考えられている。
2006-07-06
capsule - FRUITS CLiPPER [yamaha] [capsule]
半年に１枚のペースでコンスタントにアルバムをリリースし続ける capsule. その律儀なリリース間隔もさることながら，音楽性の面でも変化を続ける姿勢は，通算７枚目となるこのアルバムでも強かに示されている。これまでの capsule を象徴していた「キュートな感じ」「ポップな感じ」「レトロ・フィーチャーな感じ」は徐々に薄れつつあり，よりダンス・ミュージック的な力強さ，シンセティックな冷たさを備えたキャラクターへと変貌を遂げようとしている。
Sound & Recording 誌７月号に掲載された中田ヤスタカ氏へのインタビュー記事によれば，今作の制作工程は全て氏の自宅スタジオにおいて完結されている。また，ミキシングやマスタリングについても氏が単独で行っていることや，殆どのトラックはソフトウェア音源によって構成されていることなども明かされている。 DAW 環境の充実した現代にあっては，このような制作スタイルを採ることも理論上可能であるが，メジャーアーティストでここまで徹底しているケースは珍しいのではないかと思われる。
capsule の楽曲に見られる過剰なほどの音圧への偏重は，前作 "Lounge Designers Killer" から特に強く感じられていたが，それが氏のワンマン制作スタイルによって実現されているという事実は，妙に納得させられるところがある。スペクトルを隙間無く埋め尽くすかの如く緻密に組み立てられたミキシングは，まるでよく出来た工業製品のような隙の無さを醸し出している。恐らく，専業のエンジニアの手を介した場合，ここまで自我の感じられるマスタリングを行うことは躊躇われてしまうのではないかと思われる。
COPTER4016882 - perfect joke [contemode]
中田ヤスタカ氏率いる contemode レーベルに所属の COPTER4016882. 子洒落て澄ました雰囲気は capsule にも通じるものがあるが，こちらはもっと素っ気無く，いい意味で華やかさが無い。内に秘めたる過激さや繊細さを微かに匂わせながらも，どこか力の抜けた感じのある自然体の楽曲群は，聴いていて心地が良い。３分程度の曲ばかりなので，気付くといつの間にか聴き終わっている。そんな感覚も，今更ながら新鮮に感じられる。
2006-07-07
石田敦子，アニメがお仕事！ [amazon]
物作りの仕事に長く係わっていると，いつの間にか自分が得体の知れない理屈にばかり囲まれてしまっていることに気付く。「ＸＸはＸＸだからＸＸすべきである」。「ＸＸはＸＸだからＸＸすべきではない」。趣味ではなく仕事なのだから，理屈に従わなくてはならない場面もあることは分かっている。しかし，そういった理屈だけから導き出された答えは作り手の自我に欠けており，まるで魂が抜け落ちてしまったような面白味の無い代物になってしまう。創造とは本来，人間の自由意志 [skepdic] によって為されるべきものではないだろうか？ 理屈とは創造を補助するための術であって，それ自体が何かを生み出すものとは違うのではなかろうか？ 論理的な導出とは，知識と判断力さえあれば誰にでもできる，最も単純な「やりかた」であることを忘れてはならない。ある作品を他の作品とは異なる唯一無二の存在たらしめるのは，作り手の自我の力に他ならないと信じている。
「創ること」，それ自体が楽しかったし，それが楽しいことには今も変わりがない。楽しいからこそ「創ること」を仕事にしたのに，なぜかその仕事が最大の障害となって，自分と「創ること」の間に深い溝を作り出してしまう ― 石田敦子の「アニメがお仕事！」は，アニメーション業界に飛び込んだ若き姉弟の生活を軸として，そんな「創ることが仕事」にありがちな矛盾を描き出す。柔らかな絵柄に反して内容はシリアスであり，ある面では現実の冷酷さを描きながらも，ある面では「創ること」の純粋な喜びを描く。作者の人生経験を反映した部分が大きいのか，その描写にはある種の凄みさえ感じられる。
余談になるが，石田敦子作品においては時折，先程まで主人公的な存在だった男性キャラが，何かの理由で急に堕落する瞬間があり，その突き落としぶりが非常に恐ろしい。全体的に女性キャラの方が冷静な視点を持っているという点も，（青年誌の作品にあっては）ユニークに感じられる。
2006-07-12
Image from EDN article
いわゆる「メモリエラー」と呼ばれる現象は，「恒久的な回路の損傷」と「単発的なビットの反転」の２種類に大別される。前者はハードエラー (hard error) と呼ばれ，後者はソフトエラー (soft error) [Wikipedia] と呼ばれる。
メモリがソフトエラーを起こす原因は幾つか挙げられるが，そのうちの主なものとしてアルファ線・中性子線の影響が指摘される [EDN] [ZeroSoft] 。
ソフトエラー研究の初期の段階（1970 年代）においては， DRAM チップのパッケージ内に含まれるウラニウム 238 やポロニウム 210 等の放射性物質がソフトエラーを引き起こしているものと考えられていた。これらの放射性物質はアルファ崩壊に伴ってアルファ粒子を放出する。アルファ粒子は電荷を持っており，これが PN 接合の空乏層 [Wikipedia] を通過すると電流に乱れが生じる。アルファ線は透過力が非常に弱いため，パッケージ外からの影響を考慮に入れる必要は無いが，パッケージ内に発生したアルファ線が内部回路に影響を与えることは十分にありうる。
アルファ線によるソフトエラーを防ぐには，パッケージに用いられている素材から放射性物質を取り除くか，放射性物質をメモリセルから遠ざけるようにすればよいと考えられる。しかし実際には，そのような対処を行ってもソフトエラーが解消されることは無かった。
1980 年代に入ると，宇宙線に起因する中性子線がソフトエラーを引き起こしていることが明らかになってくる。この調査は IBM の James F. Ziegler を中心としたチームによって大規模に行われた。旧世代のハードウェアを対象とした調査ではあるが，宇宙線とソフトエラーの相関性や，航空機内における宇宙線の影響などを本格的な実地調査によって検証した貴重な資料であり，今もなお参考になる点が多い [IBM] 。
高エネルギーの宇宙線（多くが陽子によって構成される）が大気に入射すると，大気中の原子核との相互作用から様々な種類の粒子が生成される（空気シャワー） [甲南大] 。このうち，中性子とパイ中間子のみがソフトエラーを引き起こす原因になりうる。これらの粒子はアルファ粒子とは異なって電荷を持たないが，シリコン原子と衝突することにより重イオンとアルファ粒子を生成する。その衝突から引き起こされる電流の乱れは，前述のアルファ線の場合と比較しても強力な影響を持つと考えられている。
中性子線による影響のやっかいな点として，透過力の高さが指摘される。中性子線は，アルファ線とは異なって非常に高い透過力を持っており，例えば厚さ 1.5m のコンクリート壁をも透過することができる。前述の IBM の調査においては，中性子線による影響を完全に遮断する目的から，厚さ 20m もの岩盤に覆われた貯蔵庫の中に測定機材を設置するという試みが行われている。
中性子線による影響は，デバイスの存在する地理的な位置によってその強さが異なってくる。例えば，中性子線は大気によって一部遮られている（大気層による遮蔽効果は厚さ 4m のコンクリート壁に相当する）ため，標高の高い位置にあるほど中性子線の束密度は高くなる。その影響から，飛行機に乗っている間などは，地上にいる場合と比較して，ソフトエラーの発生率が 100 倍から 800 倍にも高まるとされる。
また，中性子線の発生源となる宇宙線は，地球の磁場による遮蔽効果を受けており，その効果は赤道に近づくほど強くなる。その影響から，緯度の高いロンドンにおいては，赤道付近と比較して，ソフトエラーの発生率が 1.3 倍ほどに高まるとされる。
ソフトエラーの発生率は，一般に「時間あたりの故障量」 ― FIT (Failure In Times) によって表される。時間の単位としては 10 億 (109) 時間が用いられ， 1Mbit あたりの FIT という形で記述されることが多い。
[Tezzaron] によれば， 2004 年の時点では 1,000 から 5,000 FIT/Mbit 程度のエラー発生率が妥当な数値であったとされている。この 1,000 FIT/Mbit とは，実際にどの程度の発生率なのだろうか？ 例えば 256Mbit のメモリを搭載した携帯電話ならば，半年に 1 回程度の確率でソフトエラーを引き起こすことになる。これが 1GB のメモリを搭載した PC になると， 5 日に 1 回の確率にまで高まる。更に飛行機の中などになると，約 100 倍の 100,000 FIT/Mbit 程度にまで高まると考えられるから， 512MB のメモリを搭載したノート PC を持ち込んだとして， 2.4 時間に 1 回の確率でソフトエラーを引き起こすという勘定になる。
2006-07-13
Sudhakar Govindavajhala, Andrew Appel. Using Memory Errors to Attack a Virtual Machine. IEEE Symposium on Secutiry and Privacy. May 2003.
Java のセキュリティモデルは， Java 言語の型安全性 (type safety) の上に成り立っている [Sun] 。この型安全性は， Java の言語仕様によって保証されている（と考えられている）。しかし，その型安全性を何らかの手段によって破ることができれば，そこからセキュリティモデル全体を突き崩すことが可能になると考えられる。 Govindavajhala らは，メモリのソフトエラーを利用することによって，この型安全性を破ることが可能であると指摘する。
原理は簡単で，次のような２種類のクラスを用いる。
class A { A a1; A a2; B b; A a4; A a5; int i; A a7; };
class B { A a1; A a2; A a3; A a4; A a5; A a6; A a7; };
クラス A のインスタンスはたった一つのみ生成し，あとはひたすらクラス B のインスタンスをメモリ内に敷き詰める。このとき，クラス A に対する参照は，すべて「たった一つのインスタンス」を指すようにする。準備が済んだならば，何らかの原因によってソフトエラーが発生するのを待つ。上手くいけば，「たった一つのインスタンス」を指す参照（ポインタ）にエラーが発生し，メモリ内に敷き詰められたクラス B のインスタンスのいずれかを指すようになってくれるかもしれない。
Image from Govindavajhala's paper
これで Java の型安全性は破られたことになる。あとは，クラス A のメンバ変数 i を駆使すれば，好きなアドレスのメモリを書き換えることが可能になる。そこからセキュリティ関連のコードを書き換えることも可能であると考えられるから，この時点で既に Java のセキュリティモデルは崩壊したものとみなすことができる。
Govindavajhala らは，実際に IBM Java 2 RE と Sun Java 2 RE の２種類のランタイム環境に対して攻撃を行い，その両者において攻撃を成功させている。この攻撃は Java コード内から確保することのできるメモリ容量が大きいほど成功しやすくなるが，もしその容量が小さいと，攻撃が成功するよりも前に VM （ないしはホスト OS） にとって重要な領域の方が破壊されてしまう可能性が高くなる。その「勝率」は，実験に用いられた 1GB メモリの Linux マシンにおいて 71% 程度であると算出されている。
実験においては，自然発生的なソフトエラーを待つわけにもいかず，人為的にソフトエラーを発生させる方法が用いられた。とは言っても，中性子によるソフトエラーを人為的に発生させるには粒子加速器が必要となってしまう。さすがにそれは無理があるので， 50W 電球を使ってメモリを暖めるという地味な方法が採られた。
Image from Govindavajhala's paper
この実験では，実際に 71% に近い確率で攻撃が成功することが確認された。つまり， 50W 電球さえあれば，攻撃対象に物理的損傷を与えること無くハックが可能であることが実証されたことになる……それに実用性があるかどうかはさておき。
この論文は，個人的な談話を参考資料に挙げるなど，論文の体裁として少し危うい部分があり，果たしてどの程度本気で書かれているのか量りかねるものがある。それはともかくとして，型安全性を主軸とした検証系を用意することによってコードの信頼性を保証するという手法に対し，限定的ながらも反証を提示することができたものと考えられる。今後 .NET Framework などが浸透することによって仮想マシンを主体とした環境が整ってくるに従い，このような攻撃手法がその存在意義を強めていくのではないかと思われる。
註： 2003 年の論文であるため，現在は既に対策が施されている可能性もある。その点は確認していない。
2006-07-14
Maged M. Michael. Scalable Lock-Free Dynamic Memory Allocation. In Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, pages 35-46, 2004.
昨今の多くの CPU には "compare-and-swap" (CAS) と呼ばれる類の命令が用意されている [Wikipedia] 。これは，比較とスワップ（あるいは代入）をアトミック（不可分）に実行するというものであり，次のような擬似コードによって表される（[Michael] より引用）。
CAS(addr, expval, newval) atomically do
if (*addr == expval) {
*addr = newval;
return true;
}
else return false;
この挙動を一言で表せば，「知らぬ間に値が変えられている場合は代入を失敗させる」というようなものになるだろうか。この命令を利用することによって，様々な処理をアトミックに実行することが可能となる。例として以下に「アトミックなインクリメンタ」の実装を示す（[Michael] より引用）。
AtomicInc(addr)
do {
oldval = *addr;
newval = oldval + 1;
} until CAS(addr, oldval, newval);
同様にして，セマフォやミューテックスのような同期機構も実装することができる。
通常，ある処理をマルチスレッドに対応させるには，システムのサービスとして用意された同期機構を利用することになるが，この CAS 命令を直接に用いれば，いわゆる "lock-free" な実装を実現することができる。 [Wikipedia] からのリンクには，それらの例が幾つか示されており参考になる。
この論文は， CAS 命令を用いることにより同期機構を一切利用しないメモリアロケーターの実装が可能であることを示している。同期機構を用いないことによって，マルチプロセッサ環境におけるスケーラビリティが向上するほか，シングルプロセッサ環境においてもレイテンシの軽減が果たされるものと考えられる。
論文中では，従来の手法との比較のために， libc の標準アロケーター， Hoard アロケーター [Hoard], ptmalloc アロケーター [Gloger], それにこの "lock-free" アロケーターを用いた場合のベンチマークの取得が行われている。その結果として，従来の手法よりも「プロセッサを増やした場合のパフォーマンスの向上」が高くなる傾向にある（つまり，スケーラビリティが高い）ことが確かめられている。
Image from Michael's paper
また，シングルプロセッサ環境の場合にも，従来の手法では同期機構を用いることのオーバーヘッドからレイテンシが高まっていたのに対し， "lock-free" アロケーターにおいてはオーバーヘッドが最小限に保たれており，レイテンシも軽減されていることが確かめられている。
2006-07-20
プログラマ的数学観
Norman Megill. Metamath: A Computer Language for Pure Mathematics. 序説より "A Non-Mathematician's Quest for Truth" ― 「非数学者による真理の探究」
大学に戻って３年ないしは６年を費やし数学の学位を取得すれば，それら（註：種々の数学定理の証明）を理解することができるのではないかと感じられるかもしれない。しかし，そのような行為はキャリアにそぐわないだろうし，人生における他の様々な物事ともそぐわないだろう。また，実利的な意義を見出すこともできない。そこで，近道を探すことにする。コンピュータ・プログラムに対してよくやるように，道程をその始まりに向かって一歩一歩，理解できるところまで遡っていくのだ。 （中略） まず最初に本の序説を読み，何が前提知識とされているのかを調べる。同じような調子で２・３冊の本を遡っていけば，遂には「始まり」と思われる場所 ― 算術の公理 (axioms of arithmetic) へと辿り着くことができるだろう。「なるほど！」 純朴にも，こう考えるかもしれない 「これこそ始まりの場所に違いない。すべての数学的知識の源泉なんだ。」
数学者から見た現実
萩谷昌己．エッセイ「形式化願望」より．
例えば、δεによる極限の定義から連続関数に関する様々な定理が極めて形式的な推論によって導かれることを学んだ学生が、その推論の過程を完全に形式的に書き下して、さらに、各々の推論ステップに間違いのないことをコンピュータ・プログラムによってチェックしたい、と思ったとしよう。もちろん、そんなことを思う奴は数学者としてのセンスはゼロである。数学者になろうなどとは考えず、別の道を歩むのがよいだろう。
還元主義
コンピュータ・プログラムの世界には，ある種の「厳密さ」 (rigour) が確かに存在すると感じられることがある。どのように外見が曖昧模糊としたものでも，それを地道に細かく分割していけば，最終的にアセンブリという単純化された世界へと辿り着くことができる。その世界においては，すべての物事が明快かつ厳密に進行する。その働きには誰にも疑いの持ちようが無い。そして，すべてのコンピュータ・プログラムは，そのような単純化された世界の出来事に還元することができるのだという「信念」が，プログラマとしての精神構造の重要な部分を形成しているように思われる。
だからプログラマは，数学の世界に際してもそのような接し方ができるに違いないと期待してしまうのではないだろうか。
断続的にしろ多くの年月をプログラミングに費やしてきた。プログラミング言語のことであれば，その規則の有り様について疑問を差し挟む余地も無く理解している。その規則は緻密であり，なおかつ水晶の如く明らかである。その規則にさえ従えばプログラムは動き，従わなければ動かない。プログラムの複雑さは問題ではない。そのような複雑さは極めて単純な断片へと分解することが可能であり，究極的には，何らかの機能を実行するために動き回るただのビット群として認識することができる。プログラムによっては，このような認識に至るまでに途方もない努力が必要とされることもあるが，何か特定の部分のみに注目するならば，その他の部分がどのように動いているか知る必要も無かったりする。さて，数学も斯くの如くあるべきではないだろうか？ （同じく Metamath 序説より）
実際には，そのような接し方をすることはできない ― できたとしても，とても実用のレベルで当てになるものではない。数学における様々な理論は集合論の上に組み立てることができるのだという事実を知ったとしても，そのことをコンピュータ・プログラムにおけるアセンブリの類推として見ることは難しい。ましてや，数学の世界における「厳密さ」など，探せば探すほどその姿が見えなくなってしまう幻のような存在に思えてならない。
形式主義
しかし，コンピュータ・プログラムの世界さえも，その理論面に注目すると，途端に「厳密さ」が霞んできてしまう。例えば，あるプログラムが与えられたときに，そのプログラムが正常に動作することを「厳密に」確かめることはできるだろうか？ あるいは，あるプログラムが与えられたときに，そのプログラムの意味するところ（意味論的内容）を「厳密に」述べることはできるだろうか？ これらの問題を，何らかの処理系に入力（コンパイル）して実証するのではなく，純粋に理論的な側面から捉えようとすることは非常に難しい。
例えば， Java の型システムの健全性 (soundness) を証明しようという試み [Drossopoulou1] [Drossopoulou2] [Drossopoulou3] などは，却ってプログラミング言語の非健全性を暴いているように思えてならない。
これが Java のプログラム？ Image from [Drossopoulou3]
Sophia Drossopoulou, Susan Eisenbach. Java is Type Safe - Probably. 「Java は型安全である ― 恐らくは」．
Tobias Nipkow, David von Oheimb. Javalight is Type Safe - Difinitely. 「Javalight は型安全である ― 絶対に」．
Java のサブセットを定義し，そのサブセットに関して健全性を証明することは既にできているようだが，それを「実世界のJava」にまで拡張することは到底不可能であるように思われる。いくらサブセットに関して型安全性を主張することができても，いわゆる「Saraswat のバグ」 [Saraswat] [戸沢] のように「実世界のJava」に固有の問題を攻撃されてしまえば意味が無い。
あれほど「水晶の如く明らか」であったコンピュータ・プログラムの世界も，ここでは複雑な理論の上にようやく成り立っている危うい存在に過ぎない。あるいは，外見上成り立っているように見えるのも，その実は既に崩れかけているのかもしれない。そのことを厳密に確かめることは極めて難しい。そのような曖昧さ・不完全さからは，どうあっても，到底逃れることはできない。
2006-07-21
Bruce L. Jacob, Trevor N. Mudge. A look at several memory management units, TLB-refill mechanisms, and page table organizations. In Proceedings of the 8th International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 295-306. October 1998.
近代的な OS においてはプロセッサに実装された仮想記憶 (virtual memory) の機構を用いることによって柔軟なメモリ管理やメモリ保護が実現されている。しかし，仮想記憶の運用には一定のオーバーヘッドが伴うものと考えられる。特に，アドレス空間の高速な変換を担う TLB (Translation Lookaside Buffer) [MYCOM] の管理には，比較的高いコストが要されることが知られている。
Jacob らはシミュレータを利用して様々なアーキテクチャの様々なコンフィギュレーションにおける仮想記憶のオーバーヘッドを計測した。その結果，それまでは全体の 5% から 10% 程度と考えられていた仮想記憶のオーバーヘッドが，実は 10% から 20% にも及んでいることが示された。
仮想記憶の運用においてオーバーヘッドが生じる要因は，いわゆる「TLB ミス」にあるとされる。通常，プロセッサの TLB には数十から数百の変換エントリが格納されているが，この中に必要なエントリが含まれていなかった場合は，主記憶上に格納されたページテーブルエントリ (PTE) を TLB にロードしなければならない。もしここで当該エントリがキャッシュメモリ上に無ければ，そのロードを待つために非常に大きな遅延が発生することになる。また，ここでキャッシュが汚されることによって発生しうる副次的なオーバーヘッドも考慮に入れなければならない。
このような TLB の更新処理は， Intel の x86 アーキテクチャにおいてはハードウェアによって実装されているが，他のアーキテクチャにおいてはソフトウェアに委ねられていることが多い。この場合は， TLB ミスが発生すると同時に割り込みが要求され，所定の割り込みハンドラへと処理が飛ばされることになる。そのハンドラが命令キャッシュ上に無ければ，やはりロードのために非常に大きな遅延が発生することになる。また，割り込みによるパイプラインの停止・破棄なども発生しうる。もちろん， TLB を更新する処理自体の負荷も考慮に入れなければならない。この負荷は，システムが採用している仮想記憶方式の複雑さ次第では，比較的高い負荷となることも考えられる。
ソフトウェアが単一のアドレス空間上で動作している限りでは， TLB の更新頻度は低く抑えられる。ただし近代的な OS においては，それぞれ異なるアドレス空間を持つ多数のプロセスが短時間に切り替わりながら動作しており，しかもそれらのプロセスが専用のアドレス空間を持つカーネルに対して頻繁にアクセスを行っている。ゆえに TLB は相当に酷使されることになる。
Jacob らは考察の結論として，仮想記憶を運用すること自体のオーバーヘッドが 5% から 10% 程度， TLB 更新のための割り込み処理によるオーバーヘッドが 5% から 10% 程度，キャッシュが汚されることによるオーバーヘッドが 5% から 10% 程度あり，これらをすべて合わせて 10% から 20% 程度のオーバーヘッドになりうることを示している。ちなみに，実験の対象となったアーキテクチャの中では， TLB 更新処理がハードウェア化されている x86 アーキテクチャが最も良好な結果を導き出している。
これらのオーバーヘッドは，プロセッサが高速化するほど相対的に高まるものと考えられる。この論文が 1998 年に発表されたものであることを考えると，最新のプロセッサにおいては更に高いオーバーヘッドが生じている可能性がある。この事実は，仮想記憶という機構の有り様を考え直す動機となっている。例えば Microsoft が研究を進めている "Singularity" プロジェクト [Microsoft] などは，ハードウェアによるメモリ保護をもはや過去のものとする試みとして非常に興味深く感じられる。
2006-07-26
Mark Aiken, Manuel Fähndrich, Chris Hawblitzel, Galen Hunt, James Larus. Deconstructing Process Isolation. In Microsoft Research Technical Report MSR-TR-2006-43. 2006.
一般的なオペレーティング・システムにおいては，プロセスの隔離 (isolation) を実現するために，仮想記憶やメモリ保護，特権レベルなどのハードウェア機能が用いられている。これに対し Microsoft が研究を進めている Sigularity システム [Microsoft1] においては，ソフトウェアを基盤としたプロセスの隔離が図られている。プロセスの隔離をハードウェア上の機能からソフトウェア上の機構へと移すことによって，ハードウェア側の保護機能に付随するオーバーヘッドの回避や，より厳密なレベルでの信頼性の保証などが可能になると考えられている。
この論文では，ハードウェアによって隔離されたプロセスを hardware isolated process (HIP) と呼び，それと対比させる形で，ソフトウェアによって隔離されたプロセスを software isolated process (SIP) と呼んでいる。
Singularity システムにおいては，ハードウェア機能に頼らない形でのプロセスの隔離を実現するために，型安全な言語のみが用いられる。型安全な言語とは，例えば Java や C# のことを指しており， C や C++ などはこれに含まれない。実際には「型安全な中間言語」が用いられることになるから，例えば MSIL (Microsoft intermediate language) を用いるならば C# の他に Visual Basic や Iron Python も使用可能というように，ある程度の言語の選択肢は与えられることになる。現状の Singularity システムにおいては MSIL と Bartok コンパイラ [Microsoft2] の組み合わせが用いられているが，将来的にはより高い信頼性と汎用性を得るために typed assembly language (TAL) [Cornell] が導入される予定であるとされる。
このような前提により， Singularity 向けのアプリケーションは，信頼無し (untrusted) ではあっても安全 (safe) であることが保証される。一方，システム内部にアクセスするコードは全て信頼 (trusted) されていなければならない。システムから提供されるコードのみがこれに分類され，型安全性では保証することのできないレベルまで安全性が確かめられたものになっている。 Singularity システムはアプリケーションのインストール時に静的型検証を行い，そのコードが安全であることを確認したのちに，信頼されたコードの組み込み（リンク）を行う。アプリケーションは信頼されていないが，安全であるがゆえに信頼コードを迂回してシステム内部にアクセスすることができない。それでいて，システム内部にアクセスするコードはアプリケーション内部に直接組み込まれるため，ほとんどオーバーヘッドを伴わない形になる。これは安全性と高速性を両立した非常に合理的な解決法であると言える。
ソフトウェアによるプロセスの隔離にひとたび成功したならば，ハードウェア側の保護機能を用いる必要性はほとんど無くなる。もはや仮想メモリは不要であり，特権レベルの区分も不要となる。実際にこの論文の検証においては，仮想メモリの機能を無効化し，特権レベル０ (Ring 0) のみを用いるというコンフィギュレーションが試されている。このようなコンフィギュレーションにおいては，仮想メモリの管理を行う必要が無くなり，特権レベルの切り替えを行う必要も無くなる。これらのオーバーヘッドは他プロセスやカーネルとのやりとりを行う際に発生するものであるため，これらのやりとりを特に多く行うアプリケーションにおいては高速化の効果が期待できることになる。また，アドレス空間が単純化することによる TLB ミスの減少という効果も考えうる。
この論文では，各種方式におけるパフォーマンスの比較を行うために， SIP と HIP を様々な形で織り交ぜたコンフィギュレーションを用いてのベンチマークが行われている。その結果を覗いてみると，「メモリページの確保」や「プロセスの生成」といったシステムコール類のマイクロベンチマークにおいて 2 倍から 10 倍ものパフォーマンスの向上が得られていることが分かる。また，実物大のアプリケーションを走らせた場合のマクロベンチマークにおいては，コンパイラのような独立傾向の高いアプリケーションの場合には約 2.5% の向上に留まったものの， SPECWeb のような複合傾向の高いアプリケーションにおいては 30% 以上もの向上が得られている。これは，型安全性の確認に伴う実行時オーバーヘッドが 4.5% 程度であることを考慮すると，若干低速化する可能性をはらみつつも，高速化する可能性は相応に大きいと考えることができる。
2006-07-31
Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A Realistic Typed Assembly Language. In the 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25-35. May 1999.
Typed assembly language (TAL) は RISC 命令セットに基づいた静的型付き言語である。型安全な低レベル言語という意味では Java 仮想マシン言語 (JVML) に近い位置付けになるが， JVML よりも厳密な形式化がなされており，なおかつ汎用性に富んでおり，それでいてターゲット言語（アセンブリ）に近いという特徴を持つ。この論文では IA32 アーキテクチャをターゲットとした派生言語 TALx86 を構築することにより， TAL が実際に応用可能な技術であることを示す。
まず始めに Morrisett らは JVML の問題点を指摘している。
形式モデルの構築と共に言語仕様の策定が行われ，なおかつターゲット言語に極めて近い表現を持つ TAL は，これらの問題を解決することができると考えられている。 Morrisett らは実際に Windows および Linux 上で動作する TALx86 ソース検証器およびリンク時検証器を実装し，これを Cornell 大学サイト内において公開している [TAL] 。また同時に， TALx86 向けの高級言語 Popcorn （型安全なC言語拡張）と SCHEME-- （Scheme のサブセット実装）を開発しており，高級言語への応用が現実的なものであることを示している。ちなみに， TALx86 のアセンブリ・ソースは MASM (Microsoft Macro Assembler) との互換性が保たれており，専用のアセンブラが用意されているのは MASM に存在する１行あたりの文字数制限を回避するためでしかないとされている。
Image from Morrisett et al.
TAL は証明付きプログラム (proof-carrying code; PCC) を実現する技術のひとつとして， PCC の話題と併せて言及されることが多い [塚田] 。つまるところ，近代的なオペレーティング・システムが抱えるセキュリティ上の諸問題を解決するために，このような技術が重要になると考えられている。また， Microsoft の Singularity プロジェクトの研究にも見られるように，ソフトウェアの安全性を静的に証明する手立てを用意することは，実行時パフォーマンスの面から見ても有意義なものであると考えられている [Singularity] 。
このような話題に触れるにつれ，プログラミング言語に求められる仕様上の需要というものが徐々に変化しつつあることを感じる。また，このような技術を実現するにあたって，プログラミング言語と数理論理学の結び付きが必須とされている点も面白い。 PCC に関連する研究は国内においても行われており，産学併せて幾つかのプロジェクトを見つけることができる。例えば，東京大学米澤研究室において公開されている資料やリンクなどが参考になる [米澤] 。