pkm.watasuke.net

seL4

11 min read

マイクロカーネルOSのひとつ

capability, CSpace, CNode

https://docs.sel4.systems/Tutorials/capabilities.html

  • 何にアクセスできるのかを示すもの（？）
  • seL4におけるcapabilityは以下の3つ：
    • カーネルオブジェクトへのアクセスを制御するもの
      • カーネルオブジェクトはCapabilityによって参照・操作されるもの
        • Untyped Memory に対して Retype() を行うことで生成する
      • Thread Control Block (TCB) など
    • 抽象リソースへのアクセスを制御するもの
      • IRQControlなど
      • カーネルオブジェクトと異なり、メモリ領域に対応するのではなく、カーネルが提供する機能やハードウェア制御の権限を表す
    • Untyped capability
      • Untyped Memoryを操作するためのcapability
  • spec/haskell/src/SEL4/Object/Structures.lhs に capability の定義がある
種類用途
ThreadCapTCBを操作
NullCap？
NotificationCapシグナルを操作
IRQHandlerCap割り込みハンドラを制御
EndpointCapIPCを行うためのCapability
DomainCap？
Zombie？
ArchObjectCapCPUアーキテクチャに固有なカーネルオブジェクト（x86のPageTableなど）を操作？
ReplyCap？（どうせIPCの返事に使うんだろ）
UntypedCap空メモリへのCapability
CNodeCapCNodeを操作
IRQControlCap割り込みを制御
  • CNode (Capability Node) という配列に格納される
    • カーネルオブジェクトの一種
    • 前述の Structures.lhs において、CNodeCapの定義とともにカーネルオブジェクトの中身も書いてある： 
      • | CNodeCap {
    capCNodePtr :: PPtr CTE,
    capCNodeBits :: Int,
    capCNodeGuard :: Word,
    capCNodeGuardSize :: Int }
      • CTE は Capability Table Entry
      • Guard は GuardSize のサイズをもつビットパターン
        • 後述のCPtrは先頭がGuardと一致しているらしい
  • CNodeの、Capabilityが格納される領域のことを CSlot と呼ぶ
    • 空であるか、埋まっているかのどちらか（それはそうだろ）
    • CNodes[0] は慣習として空のままにされているらしい
      • そんなGDTの0番目 (null descriptor) みたいなことしてうれしいんだろうか
      • GDTは歴史があるのでまだ理解できるが（といっても経緯を知らないので同じようなものではある）
  • CNodeとCSlotの指定にはCPtrを用いる
  • CSpace は、1つ以上の CNode からなる集合（有向グラフ？）
    • CSpace内の（CNodeに格納されている）Capabilityにアクセスする（direct addressing）際は、操作対象のCNode・CNodeにおけるCSlotのindex・CNodeをトラバースする際のdepthを指定する
      • たとえば seL4_CNode_Copy() の第1～3引数や4～6引数
      • 操作対象の CNode は seL4_CNode となっているが、これは seL4_CPtr と同義
      • depthは基本的に seL4_WordBits
        • 各archの constants.h で、主に (sizeof(seL4_Word) * 8) としてdefineされている
        • RISC-Vとx86_64では sizeof を用いた式ではなく定数になっている（なんで？）
    • CSpaceに対応する構造体があるというより、あるCNodeがrootとなっていて、そこから辿れるCNodeの集合をCSpaceと呼んでいるのか？
      • seL4_CNode_Copy() の第4引数が seL4_CNode src_root となっていることから推測
      • CNodeにCNodeCapが格納されていれば、そこから「次」のCNodeを辿ることができる
    • 例： 
      •   seL4_CNode_Copy(
    // dest
    seL4_CapInitThreadCNode, boot_info->empty.start, seL4_WordBits,
    // src
    seL4_CapInitThreadCNode, seL4_CapInitThreadTCB,  seL4_WordBits,
    seL4_AllRights);
        • （CapabilityのTutorialより一部改変）
        • seL4_CapInitThreadCNode は enum seL4_RootCNodeCapSlots のメンバで、ルートタスクの「CSpaceというアドレス空間」におけるポインタのようなもの？？となっており、これでCNodeを指定したうえでCPtrでスロットの位置を指定している
        • そうするとsrc指定で第4・第5引数の双方に enum seL4_RootCNodeCapSlots を使っていて変だが、ルートタスクにおいてはこれらは同じ意味であるらしい（要出典）
          • つまり、例えば seL4_CapInitThreadCNode は、第1引数などでCNodeを指定する時にも使えるし、CNodeを操作するCapabilityが格納されているスロットを指定するのにも使える
            • seL4_CNode_Copy(a,b,c, seL4_CapInitThreadCNode, seL4_CapInitThreadCNode, seL4_WordBits, d); というわけ

Untyped Memory

https://docs.sel4.systems/Tutorials/untyped.html

  • 全ての利用可能な物理メモリへのCapabilityは、Untyped memoryへのCapabilityとしてルートタスクに渡される
  • Untyped Memory は、特定のサイズを持つ連続した物理メモリのブロック
  • Untyped Capability は、カーネルオブジェクトとそれらへのCapabilityにRetypeできる
  • Untyped Capability は、そこにカーネルが書き込みできるかどうかを示すboolean device を持つ
    • true である（カーネルが書き込めない）メモリ領域って何？BIOSとかに予約されてる領域なのか？（だとしたらそこを Untyped Memory としてルートタスクに渡す意味がわからない）
  • これに対して行える処理は seL4_Untyped_Retype() のみ
    • Untyped Capability のタイプを変更？
    • カーネルオブジェクトが付随するタイプのCapabilityであれば、カーネルオブジェクトを作成し、それを操作するためのCapabilityと共に返却
    • Untyped Capability を retype して作った Capability は、もとの Capability の子 (children) となる
      • 親が参照するメモリ領域の一部にアクセスできるようになる
    • seL4_Untyped_Retype(
    seL4_Untyped _service, seL4_Word type, seL4_Word size_bits,
    seL4_CNode root, seL4_Word node_index, seL4_Word node_depth, seL4_Word node_offset,
    seL4_Word num_objects)
      • _service : retype したい Untyped Memory
      • type : seL4_TCBObject などの retype 先
      • size_bits : オブジェクトのサイズが可変である場合に使う
        • Untyped Object がそう
    • チュートリアルでは以下のようなことをやっている
      1. ルートタスクに与えられた Untyped Memory から適切なものを選ぶ
        1. サイズが十分（？）で、device がfalseであるようなもの
          1. サイズは seL4_TCBBits + 1 となっているが、TCB以外にも作成してそうなのにそれらを考慮していないのか？
          2. 2^n でサイズを指定するから、最も大きいサイズである seL4_TCBBits に1足すだけで良い、ということらしい
            1. TCBBits は 11 で、 EndpointBits + NotificationBits = 5 + 4 = 9 だから正しそう
      2. それを Untyped に Retype することで Untyped Object を得る
      3. それを親として、（Untyped Object内での？） CNode 内のオフセットをずらしつつカーネルオブジェクト（TCB、Endpoint、Notification）を作っていく
        1. offset は 1 ずつズレていくが、これはどういうことなのだろうか　カーネルオブジェクトのサイズぶんズラすというわけではないのか？
        2. この offset はおそらく CNode における offset で、Retype して得られた Capability を格納する先を指定するためのものだから、カーネルオブジェクトは関係ない

TCB

https://docs.sel4.systems/Tutorials/threads.html
Thread Control Object

  • カーネルオブジェクトの一種
  • CSpace root と呼ばれるCNode capabilityを持つ
    • 空である場合がある

ブート

  • 最初に起動するタスクは root task と呼ばれる
    • 全てのcapabilityを制御できる
    • struct BootInfoをもらえる
      • untypedList という、Untyped Memory オブジェクトの情報をもつ seL4_UntypedDesc の配列がある
  • seL4_Untyped_Retype() によって BootInfo.untypedList の要素を任意のCapability（あるいはobject）に変換していく
  • seL4_x86-64でのブート処理

Graph View

Backlinks