論文紹介： Theseus: an Experiment in Operating System Structure and State Management

先日、Kernel/VM探検隊 onlineというイベントにて、RustでOSを設計するという論文をまとめて紹介するというLTを行いました。

RustはOS界の銀の弾丸になりうるか
RustはOS界の 銀の弾丸になりうるか 論文で見るRustで変わるOS設計 1

しかし、10分間のプレゼンで3本の論文を紹介するとかいう、かなり無茶苦茶な発表だったので説明している箇所もかなり限定的で、解説全体として非常に雑なものになってしまいました。
そこでこの記事で、このLTで触れた論文の1つであるTheseusというOSについて説明したものをもう少し詳しくみていきたいと思います。

論文概要

  • タイトル： Theseus: an Experiment in Operating System Structure and State Management
  • 著者： Kevin Boos, Namitha Liyanage, Ramla Ijaz, Lin Zhong
  • 会議： 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI ‘20)
Theseus: an Experiment in Operating System Structure and State Management | USENIX

USENIX系会議でOS関連のトップカンファレンスの一つであるOSDIの論文です。
先日のLTで紹介したうちのReadLeafに関する論文もこの年のこの会議で発表されたものです。

この論文では、OSのステートスピルというものを減らすことを目的としたOS設計を模索しています。
ステートスピルとは、あるコンポーネントの変更可能なステートが他のコンポーネントとのインタラクションでステートの一部が他のコンポーネント内に残ってしまい、その漏れたステートを持ったコンポーネントがクラッシュしてしまうことで、もともとのコンポーネントもその影響を受けてクラッシュするというものです。
このステートスピルを減らすOS設計のために、Rustのコンパイラレベルで保証される性質をOSの設計でもなるべく保つことで、ランタイムでおこなうべきことを減らせる、というのがこの論文のポイントです。

ちなみに「Theseus」の読み方なのですが、ギリシア神話が元ネタなのですが、日本では「テセウス」で知られていますが、著者らは英語読みで「シーシアス」、というように喋っていたので、自分もLTでは「シーシアス」と紹介しました。

Theseusのデザインの原則

Theseusはcellと呼ばれるソフトウェアコンポーネントの組み合わせにより成り立ちます（Rustのstd::cellとは関係ありません）。
デザインの原則として以下の3つを挙げています。

  1. すべてのcellはランタイムで永続的な（runtime-persistent）境界を持つ
  2. 言語とコンパイラの力を最大限活かす
  3. cell間のステートスピルをなくす

順にどういうことかをみていきます

cellはRustのクレートとして実装され、実行時にはcell間の依存関係についてのメタデータとともにロードされます。
ロードされたcellはCellNamespace上で管理されます。
各cellをクレートとして実装することで、そのクレートのオブジェクトファイルとcellが直接対応することになります。
cellの依存関係はクレートの依存関係と等しくなるので、循環した依存関係は発生しません。
このクレートして実装された境界により、後述するcellスワッピングやエラーからの復帰が簡略化されます。

2つ目の原則である言語とコンパイラのもたらす安全性の保証を活かすために、Theseusのランタイムモデルは言語のランタイムモデルと同じように、シングルアドレススペースで（同じメモリ領域に対して複数のアドレスをマッピングしたりしない）、単一の特権レベルで（途中で実行モードが変わったりしない）、単一のヒープ（グローバルアロケータしか使わない）で実行されるようになっています。
これらにより、コンパイル時に行われる型やライフタイムなどの不変条件のチェックをそのまま活用することができ、OS的に他の仕組みを導入する必要がありません。
Rustが保証してくれていない性質としてリソースのリーク（resource leakage）の問題があります。実はRustはメモリリークが起きないことは保証してくれません（例えばstd::rc::RCで循環参照をつくるとメモリリークになります）。
ただし、ここでのリソースリークは広義のメモリリークというより、タスクがなんらかのオブジェクトを抱えたままエラーで異常終了する、といったケースを考えているようです。
これを防ぐために、TheseusではクリーンアップのロジックはすべてDropハンドラで実装することにし、独自のスタックアンワインディングを実装することで異常終了した場合でもリソースが解放されるようにしています。
このスタックアンワインディングで使う情報はすべてコンパイル時に生成されるので、実行時にコストがかかることはありません。

3つ目の原則であるステートスピルをなくすために、Theseusではopaque exportationという仕組みでクライアント・サーバー間で通信します。従来の場合は、サーバー側でステートを持ちその進捗とかを管理しますが、Theseusではクライアント側にそのようなステートは輸出し、所有権がクライアント側に移ります（exportation）。
一方でサーバー側のプライベートなステートは型安全性により守られます（opaque）。
こうすることで、クライアント側が所有権を持つため、クリーンアップのロジックも当然クライアント側で自動で行われるので、あえて実装する必要がなくなります。
複数クライアントでステートを共有する場合、Arcなどのリファレンスカウントを持つオブジェクトを使いますが、このような場合、ステートはヒープ上におかれることになります。
これはヒープへのステートスピルのように見えますが、このようなヒープアロケーションそのものはStringのようなオブジェクトをつくるときにも起こるのでそもそも避け得ないものであり、ヒープアロケーションを表すArcなどのオブジェクトの所有権はクライアントが持つことになり、そのオブジェクトを辿っていけばヒープにアロケートされたオブジェクトによるステートスピルも検出できるので、ヒープそのものの内部状態を考える必要はない、としています。

具体例

原則２、３をLTのスライドには入れたが、発表時間の都合上吹っ飛ばしたメモリ管理の例で見てみましょう。

TheseusではMappedPage型で仮想メモリを管理しています。シングルアドレススペースを実現するために、MappedPage型の所有権を保有することが対応するページとフレームの所有権を保有することを意味します。
よって、複数からマップされることはページとフレームの所有権を複数箇所で保有することを意味してしまうため、コンパイル時に禁止されます。
また、このアロケートされた領域はDropハンドラでしか解放されません。これにより、ライフタイムが尽きたときのみページとフレームが解放されるので、use-after-freeのようなバグを防ぐことができます。
また、writableやexecutableかも、それぞれ専用の型を用意することで、型レベルで制御しています。
このMappedPageオブジェクトをopaque exportationでは所有権ごとクライアントが受け取ることになります。サーバー側は使われている仮想メモリエリア（VMA）のリストを管理するということは必要ありません。

CellスワッピングによるLive Evolution

Theseusはnano_coreと呼ばれる他のcellが動的にロードされていき、cellスワッピングという仕組みで機能を拡張していきます。
6章で詳しく説明されているのですが、文章を書くのが疲れたので、このブログではスキップします。

実験・評価

CellスワッピングによるLive Evolutionにより、複数のスケジューラを切り替えたり、ネットワーク越しのアップデート機能などを実際に実装しています。

フォルトリカバリーの仕組みがちゃんと動くかの評価のためにQEMUのエミュレーターで実行時にランダムにフォルトを挿入するという大胆な方法で実験し、MINIX3と比べクラッシュすることが少ないことを確かめています。

マイクロベンチマークなどを用い、オーバーヘッドが十分に少ないことを確かめていますが、Linux並みの機能を実現しているわけではないことには留意する必要があります。

限界

低レイヤーの世界ではどうしてもunsafeを使うことが必要になります。unsafeコードは独立性を損ねる場合もあるので問題です。
また、Rustのコンパイラとcore/allocライブラリを信用しているのでそれらのsoundness holesの影響を受けてしまいます。
Rust言語そのものの性質に大きく依存しているので、他の言語のコンポーネントは残念ながら使えません。

まとめ

いかがでしたか？ちゃんと理解できましたか？僕も正直理解できているか自信がない箇所が結構あります。
が、Rustを活用することでのOS設計のメリットというのが垣間見えたと思います。

Theseusのコードはオープンソースになっていて、実装についてのドキュメントもあるので、そちらも目を通してみるとより理解できるのではないでしょうか。自分はまだ手が回っていませんが…

自作OSに関する新しい書籍が発売されるなど、自作OSに対する関心が高まりつつある（？）今日この頃ですが、従来のOSとは違ったアプローチのOSを探求するというのもまたおもしろいと思います。