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

[大原雄介，MONOist]

コモンクライテリアをサポートしたフリーなRTOSは貴重な存在

　ということでやっと話がseL4にたどり着いた。こうした経緯で作られたseL4は、まず安全性の確保が第一となっている。基本的にはマイクロカーネルということで、カーネルは本当に最小限の構成になっており、これによりカーネルの肥大化を避けるとともに、必要なコンポーネントだけをロードすることで省フットプリント性も確保できている（図2）(Photo01)。

図2　この数字（SLOC：Source Line of Code）が妥当か？　といわれるとちょっと大げさな気もするのだが、まぁカーネルが小さくなるのはマイクロカーネルとしては当然である［クリックで拡大］

　加えてseL4はOSであると同時にハイパーバイザーの機能も提供しており、例えばLinux ゲストを複数稼働することも可能となっている（図3）(Photo02)。もちろん、ユーザーモードVMM（仮想マシンモニター）をさらに稼働させることも可能だ。

図3　この場合、seL4のハイパーバイザーは、ArmならEL2、x86ならRoot Ring-0、RISC-VならHSモードで動く形になる［クリックで拡大］

　また、セキュリティの肝となるアクセス制御はCapabilityベースのものとなっている。伝統的なセキュアOSの場合、ACL（Access Control List）を利用したものが多いが、これとは対照的な構成である。ただし、そうしたセキュリティを強化したOSの場合、しばしば性能（Performance）が犠牲になるとされる。これに関しては、seL4 FoundationのPerformanceのWebサイトに幾つか数字が載っているが、マイクロカーネルであるが故に、例えば割り込みが入ってからISRが動くまでの時間といったものはなく、代わりにIPCの速度となっている。

　とはいえ、例えば、Cortex-A9などのベースになっているArmv7aアーキテクチャの場合、1GHz駆動のプロセッサ上で以下のような性能を実現できるという。

• IRQ involke（割り込まれたThreadと同一アドレス空間で動作している割り込みハンドラ呼び出しの時間）：平均634cycle（634ns）
• IPC call（同一CPUコア内で動作する、異なるアドレス空間のサーバを呼び出す時間）：平均317cyle（317ns）
• IPC reply（同一CPUコア内で動作する、異なるアドレス空間のクライアントに応答を返す時間）：平均336cycle（336ns）

　これらは、性能的にはかなり高速としてよいかと思う。

　アーキテクチャは今のところ32／64ビットの、それもMMUやHypervisor callをサポートしたモダンなプロセッサ（Armv7a／Armv8a／x64／RISC-V）のみのサポートとなるし、ライセンスは先に書いたようにGPL v2とBSD2条項ライセンスの混合という形なので、商用向けとしてはちょっと使いにくいところもある。しかし、CCをサポートしたフリーなRTOSというのは貴重な存在でもあり、そうした用途向けに現在もさまざまな利用に向けた試みが進められているのがseL4である。