seL4のIncremental Consistencyについて
はじめに
最近趣味でseL4の実装や論文を調べているのですが、seL4のIncremental Consistencyという考え方がとても面白かったので記事にしました。
背景
検証を目的としたOSでは、並行性に起因する複雑性を回避するためにBig Kernel Lockを使って割り込みを無効化することが多いです。seL4も基本的にこの方針ですが、カーネルオブジェクトの作成や削除といった重い処理では保留されている割り込みを(もしあれば)処理する実装になっています。これはInterrupt latencyを改善するためです。
実装
seL4のコードの内、preemptionPoint関数が使用されている箇所の例を以下に示します。この関数はseL4_CNode_Revokeで使用されます。カーネルオブジェクトの削除を繰り返す重い処理です。
preemptionPoint関数の定義を以下に示します。保留された割り込みがある場合、EXCEPTION_PREEMPTEDを返すことが分かります。
EXCEPTION_PREEMPTEDが返った場合、handleSyscall関数の中で以下の処理が実行されます。handleInterrupt関数は保留中の割り込みがあることを記録するだけです。
最終的に以下の部分でschedule関数が実行され、ユーザーランドのデバイスドライバが割り込みを処理します。
重要なのはactiveThread関数の以下の処理です。ここではFaultIPをNextIPにセットしています。FaultIPはシステムコール呼び出しに使う命令(risvならecall命令)のアドレスであるため、ユーザーランドの処理はecall命令から再開され、システムコールが再実行されます。
この実装により、複数のカーネルオブジェクトの削除が1つのカーネルオブジェクトの削除の繰り返しになり、かつ削除間の間に保留されている割り込みが(もしあれば)処理されるため、Interrupt latencyが改善されます。非常に賢い実装ですね。
Incremental Consistency
上で紹介した実装は「Incremental Consistency」と呼ばれています。割り込みをポーリングで処理することで、カーネルが常に一貫性のある状態を保つことができ、検証が楽になります。もし一時的に割り込みを有効化する実装になっていた場合、カーネルオブジェクトの作成/削除の途中で割り込まれる可能性があり、カーネルが一時的に一貫性のない状態になるため、検証が難しくなります。
おわりに
本記事ではseL4のIncremental Consistencyという考え方について紹介しました。割り込みの扱いを簡単にしつつ、実用性を考えてInterrupt latencyを改善するという、seL4ならではのアプローチで面白かったです。今後もseL4の実装を調べつつ、できれば証明を読みたいと思っています。(まずはIsabelle/HOLの勉強からですが...)お楽しみに!!
参考資料
[1] Bernard Blackham, Yao Shi, and Gernot Heiser. 2012. Improving interrupt response time in a verifiable protected microkernel. In Proceedings of the 7th ACM european conference on Computer Systems, April 10, 2012. ACM, Bern Switzerland, 323–336. https://doi.org/10.1145/2168836.2168869
[2] Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. 2014. Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32, 1 (February 2014), 1–70. https://doi.org/10.1145/2560537
[3] Matthew Warton. 2005. Single kernel stack L4. (2005). Retrieved November 9, 2024 from https://trustworthy.systems/publications/theses_public/05/Warton:be.abstract
[4] Richard P. Draves, Brian N. Bershad, Richard F. Rashid, and Randall W. Dean. 1991. Using continuations to implement thread management and communication in operating systems. SIGOPS Oper. Syst. Rev. 25, 5 (September 1991), 122–136. https://doi.org/10.1145/121133.121155
Discussion