オープンソースRTOS「seL4」の紆余曲折からマイクロカーネルの進化を俯瞰する：リアルタイムOS列伝（19）（1/3 ページ）

IoT（モノのインターネット）市場が拡大する中で、エッジ側の機器制御で重要な役割を果たすことが期待されているリアルタイムOS（RTOS）について解説する本連載。第19回は、コモンクライテリアなどにも対応する第3世代マイクロカーネルのオープンソースRTOS「seL4」を紹介する。

[大原雄介，MONOist]

　前回に続き、今回も大学発のリアルタイムOS（RTOS）である。「seL4」とは“Secure Embedded L4 Microkernel”の略である。原型になっているのは、“Secure Embedded”の付かない、ただの「L4 Microkernel」（L4 Kernelと称されることが多い）。

⇒連載記事「リアルタイムOS列伝」バックナンバー

第1世代マイクロカーネルのMach OSから、第2世代の「L3」へ

　L4 Kernelはマイクロカーネルの研究における第2世代に属する。マイクロカーネルといえば、かの「Mach OS」を連想される方が多いと思うし実際有名であるが、これとは別の流れとしてドイツのJochen Liedtke（ヨッヘン・リートケ）博士が開発した「L3」から始まる一連のOS（というかマイクロカーネル）が存在する。もともとはMach OSなどに代表される第1世代のマイクロカーネルでは、特にIPCが非常にオーバーヘッドが多いという問題があり、これに不満を覚えたLiedtke博士が1988年に開発したのがL3である。このL3は、マイクロカーネルの原則にはやや反するがi386のアセンブラで記述され（つまり機種依存性がある）、結果として非常に高速なIPCが実装されたマイクロカーネルの構築に成功した。

　L3の成功は、Mach OSなどのその他の不満点にも目を向けるきっかけとなった。結局、L3と似たような発想で、「高性能なマイクロカーネル」を構築するべく1993年から作業が始められたのがL4 Kernel（以下、L4）である。Liedtke博士はまたもや、このL4の初期バージョンをi386のアセンブラで記述している。ACM（国際計算機学会）の「SOSP（Symposium on Operating Systems Principles） 1993」で発表された“Improving IPC by kernel design”という論文によれば、この初期バージョンのL4のIPCはMach OSの20倍高速になったとしている。

　この成功は他の研究機関の目を引くのに十分であり、1996年あたりからドレスデン工科大やUNSW（ニューサウスウェールズ大学）、IBMを含む複数の研究機関でL4の他のアーキテクチャへのインプリメントが始まる（何しろi386のアセンブラで記述されているから、他のアーキテクチャへの移行にはそれなりに手間が掛かる）。Liedtke博士自身もIBMのワトソン研究センターに移籍し、ここでL4をベースとしたOS（例えば、Sawmill OS）などの開発に携わった。

　1999年にLiedtke博士はカールスルーエ大学のシステムアーキテクチャグループを引き継ぎ、ここでマイクロカーネルの研究を継続した。このグループで、高性能なマイクロカーネルが高級言語で構築できるというコンセプトの実証のため、L4をC++言語で記述した「L4Ka::Hazelnut」を開発する。L4Ka::Hazelnutは、IA32に加えてARMアーキテクチャもサポートし、またアセンブラ版に比べて性能低下も許容範囲に収まっていたため、この時点でL4のアセンブラ版カーネルは事実上廃止されることになった。この後継が2001年に登場した「L4Ka::Pistachio」で、主に機種依存性を廃するとともに、新しいKernel API（L4v2 API）を実装したバージョンとなっている。

　これとは別にドレスデン工科大では、独自実装となる「L4/Fiasco」が1998年から開発されていた。こちらは一部のAtom演算を除き、完全にカーネルをプリエンプティブ（L4Ka::Hazelnutや、その後継のL4Ka::Pistachioはカーネル内での同時実行が極端に限られている）にしようという試みであるが、残念ながらこれは一度挫折し、プリエンプティブ性は限られたものになってしまった。ただ、x86からAMD64、Armプラットフォームなどを幅広くサポートするとともに、L4Ka::Hazelnutで実装されたL4v2 APIに、さらに拡張を加えて実装している。このL4/Fiascoの上にLinuxを載せたものが「L4 Linux」で現在も提供されている。