マイクロカーネルとモノリシックカーネルの設計比較

何を「カーネル空間」に置くか

カーネル設計の本質的な問いは1つです——スケジューラ、メモリ管理、ファイルシステム、デバイスドライバ、ネットワークスタックのうち、どこまでを特権的なカーネル空間に置き、どこからをユーザー空間に追い出すか。

カーネル空間のコードはCPUの特権モードで動き、全メモリと全ハードウェアに直接触れます。だから速い。しかし同時に、その中の1つのバグがシステム全体を巻き込む。ドライバのヌルポインタ参照1つで OS ごと停止しうるのは、ドライバがカーネル空間にいるからです。この緊張関係が、以下のアーキテクチャの分岐を生みます。前提として、特権とユーザーの境界そのものは カーネルモードとユーザーモード を参照してください。

4つのアーキテクチャ

重要なのは、これらが性能と堅牢性のトレードオフ曲線上の異なる点だということです。モノリシックは境界越えのコストをゼロに近づける代わりに障害隔離を犠牲にし、マイクロは逆を取ります。ユニカーネルは「そもそも信頼できる単一アプリしか動かさない」と割り切って隔離を捨て、最速・最小を狙います。

なぜIPCコストが決定打になるのか

マイクロカーネルでは、アプリがファイルを1回読むだけでも、こうなります。

モノリシック:  app --syscall--> [カーネル内のFS] --> 結果
                 （境界越えは1往復だけ）

マイクロ:      app --IPC--> FSサーバー --IPC--> ドライバサーバー
                 --IPC--> FSサーバー --IPC--> app
                 （ユーザー空間サーバー間で何往復もIPC）

各IPCは、アドレス空間をまたぐメッセージパッシングです。送信側のメッセージをカーネルが受け取り、受信側へ渡し、CPUの実行コンテキストを切り替える。これは プロセス間通信（IPC） の中でも特にコストが集中する処理で、初期のマイクロカーネルではここが致命傷になりました。

Mach の教訓

1980年代後半のカーネギーメロン大学の Mach は、マイクロカーネルの概念を広めた先駆けです。しかし Mach の IPC は重く、メッセージのコピーやポート管理のオーバーヘッドが大きく、「マイクロカーネルは遅い」という評価を定着させてしまいました。macOS/iOS の XNU は Mach をベースにしますが、性能のため BSD 部分やドライバをカーネル内に同居させたハイブリッドであり、純粋なマイクロカーネルではありません。

L4 のブレークスルー

1993年、Jochen Liedtke は 「IPC が遅いのはマイクロカーネルの宿命ではなく、実装が悪いだけだ」 と主張し、L4 を作りました。鍵は徹底した最小化です。

L4 は Mach 比で IPC を1桁から2桁高速化し、マイクロカーネルが実用速度に到達できることを示しました。ここでの境界越えコストは、本質的には コンテキストスイッチ と同種の「実行の切り替え」であり、それをいかに削るかが勝負でした。

seL4：正しさを証明する

L4 の系譜の到達点が seL4 です（2009年、オーストラリアの NICTA/Data61）。これは世界初の、カーネルの実装が仕様通りに動くことを形式手法で機械的に証明した汎用OSカーネルです。

証明されたのは、おおよそ次のことです。

• C実装が抽象仕様に正確に対応する（機能正当性）。バッファオーバーフローやヌルポインタ参照、未定義動作がカーネル内に存在しないことが数学的に保証される。
• 後の研究で、情報の不正な流出が起きない（機密性・完全性）といった性質も証明された。

これが可能だったのは、カーネルが極小（約1万行のCコード）で、機構だけを持ちポリシーを持たないからです。小さく保つ設計判断そのものが、検証可能性という価値を生んだわけです。seL4 は航空・自動車・防衛など、バグが許されない領域で使われます。

設計トレードオフの整理

純粋なマイクロカーネルが商用デスクトップを席巻しなかった一方、その思想は広く浸透しています。Windows と macOS はハイブリッド、Linux ですらドライバをモジュール化し、近年は eBPF で一部処理を安全にカーネルへ載せるなど、「機構とポリシーの分離」というマイクロの発想を取り込んでいます。

まとめ

• カーネル設計とは どこまでを特権空間に置くか の選択であり、性能と障害隔離のトレードオフ曲線上の点を選ぶこと。
• モノリシックは境界越えゼロで高速だが障害が波及、マイクロは隔離に優れるがIPCコストが宿命的な課題。
• L4 が IPC を最小化してその課題を打破し、seL4 は極小設計を活かして正しさの形式証明にまで到達した。

入口の境界は カーネルモードとユーザーモード、通信の仕組みは プロセス間通信（IPC）、切り替えコストは コンテキストスイッチ も合わせてどうぞ。