pkm.watasuke.net

seL4

7 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
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を辿ることができる

TCB

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

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

ブート

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

Graph View

Backlinks