Try   HackMD

F9 microkernel & ARM hypervisor

contributed by <jserv>, <louielu>, <yenWu> , <Shaoyu-Chen>
GitHub: f9-kernel

預期目標

  • 針對低功耗 IoT 應用，打造一個高效、安全的 microkernel, 延續 F9 microkernel 開發成果，修正已知的問題。
  • 藉由 F9 microkernel 過去發展的程式碼，如 MPU + address space 和 L4 API 等等，重新設計一個針對 ARM Cortex-M4 的 hypervisor，符合第三代 microkernel 的設計
    • 參考設計: eChronos: build and formally verifiey a small, versatile, high-assurance real-time operating system for embedded micro-controllers

技術報告

Scrum week 1 (Oct 18 - Oct 21)

Story

  • 重新認識 F9 memory management system (8p)
  • 撰寫 memory management documentation (8p)

Task

  • MPU setting and experience in Cortex-M4
  • address space experience
  • fpage experience
  • MPU documentation
  • address space documentation
  • fpage documentatoin

產出:

影片改進項目:
(1) HackMD 切換到 "Publish" 模式;
(2) 解說程式碼時，儘量用單一視窗全螢幕;

  • MPU documentation
  • Kprobe register via symbol name

需要標注對應的 ticket/issue 連結 jserv

Scrum week2 (Oct 23 - Oct 27)

  • Stand up (10/23):
    • video
    • Basic Grammer in use: 過去式 + 現在完成式 (12~21)
    • F9 microkernel fpage: struct fpage, assign_fpage, assign_fpage_ext
    • Explain BitSec (record)
    • 5 CPE

產出:

  • F9 microkernel memory pool introduction. (video)

F9 microkernel 已知問題

  • Implement Thumb-2 optimized memcpy/memset. #67
  • Measure the latency of (posix) semaphores. #110
  • User thread hang up when one thread is in busy loop. #124
  • Improve Kprobe with symbol table to provide real dynamic tracing. #130
  • Improve memory mamagement documentation. #132
  • Counting CPU Cycle by DWT. #133

F9 microkernel debugging setting

  • platform/debug_uar.c:110, force to use dbg_sync_putchar
  • kernel/kdb.c:149, configs with kdb but don't register to softirq
  • CONFIG_KPROBES: disable kprobes

Then you can print with kdb_dump_* in gdb, and the kernel won't affect by kprobe interrupt.

COMP9242 Advanced OS

  • Page 4: 三個世代的 microkernel 演化
    • Mach (第一代)
      • 180 syscalls
      • 100 kLOC
      • 100 µs IPC
    • L4 (第二代)
      • ~7 syscalls
      • ~10 kLOC
      • ~ 1 µs IPC
    • seL4 (第三代，著重於 capabilities，針對 isolation)
      • ~3 syscalls
      • 9 kLOC
      • 0.1 µs IPC
  • Page 11: seL4 Capabilities
    • Stored in cap space (CSpace)
      • Kernel object made up of CNodes
      • each an array of cap "slots"
  • Page 13: IPC: (Synchronous) Endpoints
  • Page 23: Notifications: Asynchronous Endpoints
  • Page 34: seL4 Address Spaces (VSpaces)
  • Page 47: Interrupt Management

seL4 microkernel

reference to:

Aims

  • Flexible
  • minimal
  • secure, safe, reliable

Monolithic Kernel(Linux) v.s. Microkernel(seL4)

Design Principle

  • Mininality
    • mechanisms, not plocies
    • TCB, effective IPC, small number of services…
  • Generality
    • User-level driver

Feature

  • capability-based access model
  • effective IPC
  • User-level device drivers
  • resource management

Implementation

  • Strict Process orientation
  • Virtual TCB arrary
  • Lazy scheduling
  • Direct process switch
  • Preemption
  • Nonportablility
  • Nonstandard calling convention

Achievement

  • only 8700 C code and few assembly
  • First OS kernel haved undergone the formal verification
  • worst-case execution time

Kernel Object

  • CNode
  • Thread Control block(TCB)
  • IPC Endpoints
  • Notification Object
  • Virtual Address Space Objects
  • Interrupt Objects
  • Untyped Memory

Capability-based Access Model

seL4 引入一套基於 capability 的存取控制模型，每個使用層級的執行緒對應一個 capability space (CSpace)，該空間包含執行緒對應處理的 capabilities，換句話說，後者管理著這個執行緒所存取的資源。

CNode 由 slot 組成，每個 slot 需要 16 byte 的實體記憶體，用以表示一個 capability。如同其他物件，CNode 需要經由 seL4 Untyped Retype，在合適數量的 untyped memory 之上建立。

seL4 用 TCB (thread control block) 描述一個執行緒，而每個執行緒對應一個 CSpace 和 VSpace (可與其他執行緒共享)，一個 TCB 一般有一個 IPC buffer。

seL4 使用訊息傳遞機制，來實作執行緒之間的通訊。

seL4 引入 256 個優先級的搶占式輪轉排程 (preemptive round-robin) 機制，當一個執行緒建立或修改了另一個執行緒，它只能將另一執行緒的優先級設為比它低或跟它一樣。

Capability Structure

Capabitlity 我們可以想成是一張通行證，這張通行證有指名你去哪個地方，還有你有什麼權限可以做什麼事情。

所以 Capabitlity 包含 Object reference 和 Access rights，對應到上面我們說的，如下圖：

Capability Derivative Tree(CDT)

透過上面解釋，我們將延伸它的概念，Capability 是可以做演化的，你可以將複製他並且降低他的權限，而這個概念就延伸出 Capability Derivative Tree，他方便我們來管理 child cap，複製這個概念很重要，我們做任何存取都要靠 cap，所以移交 cap 是非常重要的，而 CDT 還有很重要的功能就是要可以追蹤自己給出去的 child cap。

注意，在 boot time 時，只會有一個 Untype Memory，而所有的 object 都是從他 retype() 出來的。Yen-Kuan Wu

CNode Structure

CNode 我們可以想像成放通行證的櫃子，櫃子裡有很多抽屜，裏面可能放著通行證，也有可能沒有，這邊很有趣，我們可能可以用裡面的通行證來開令一個抽屜。如下圖：

在創造一個 CNode 時我們要給我要開多少個抽屜的櫃子Yen-Kuan Wu
附帶一提，slot num 需要是 2 的冪次Yen-Kuan Wu

請用 GraphViz 重新製作下圖 jserv

好的，我試看看Yen-Kuan Wu

 CNode
 _____
| Cap-|-----> Object
|-----|
| Cap-|-----> CNode
|-----|       _____
|     |      |     |
|-----|      |-----|
|     |         .
|-----|         .
   .         256 slot
   .
   .
256 slot

CSpace

最後我們來到最大的集合，CSpace 是一個 directed graph，他裡面的 node 只能是 CNode，所以 CSpace 可能包含多個 CNode 又或沒有，CNode cap 可以互相串聯。

  • CSpace

Capability Address Lookup

這邊直接介紹 CSpace 裡要如何查表，這邊看到了 guard，他的用意是保護各自的記憶體，如果開頭不合即 fail，所以每個 CSpace 有不一致的 Address 存取方式。

這邊還需要 "depth limit"，我們會發現 L2 CNode Cap(0x00F00000) 和 L3 CNode Cap(0x00F00000) 是一樣的，所以我們用它來區分。

Capability Method

  • mint()

用指定的 cap 當模板，鑄造一個新的 cap，但他的權限只能小於原本的，這個 method 也會用在 badge cap(在探討 IPC 時會在討論到)Yen-Kuan Wu

  • copy()

複製一模一樣的 cap include badge and guardYen-Kuan Wu

  • move()

移動指定的 cap 至指定的 slotYen-Kuan Wu

  • mutate()

mint() + move() 但不留下 orignal capYen-Kuan Wu

  • delete()

remove the cap from specified slotYen-Kuan Wu
More over, if the cap is the least one, the object would be destroiedYen-Kuan Wu

  • revoke()

delete() each of the derived of the specified capYen-Kuan Wu

暫時紀錄一些重點

Thread Control Block

虛擬 CPU register

Endpoint

syncronize IPC
sender block until the receiver come
so do receiver
Grant rights allow to transfer cap

Notification

single word = set of binary semaphore
use badge to modify the Notification Status
return single world to communication
bindTCB can allow only one thread to wait()

Virtual Address Space Objects

page

Interrupt Objects

useful for unprivilege Driver

Untyped Memory

All object are created by retype()

Build seL4

build dependencies

my ghc version is 7.6.3, cabal version is 1.20.0.2Yen-Kuan Wu

seL4 projects

The seL4 kernel is usually built as part of project. Each project has a wiki entry associated with it that gives more information. The information on this page is common to all of them.

We modelled the seL4 development process on the Android development process. Each project consist of an XML file that describes which repositories to use, and how to lay them out to make a buildable system.

The available projects so far are:

  • verification, the seL4 proofs.
  • seL4test, a test suite for seL4, including a Library OS layer.
  • CAmkES, a component architecture for embedded systems based on seL4. See the CAmkES pages for more documentation about CAmkES.
  • VMM a componentised virtual machine monitor for ia32 platforms using Intel VT-X and VT-D extensions.
  • RefOS, a reference example of how one might build a multi-server operating system on top of seL4. It was built as a student project.

Object Create

First, we have to confirm what is the mode of resource managerment.

Globle Resource Mangerment

PIC

At the time of boot, all available memory space are already untyped objects.

Retype() to the specified object

There is a flow.

Send Msg via IPC -> kernel decode msg -> decode the cap( might be untyped_cap_t ) carried by the msg -> decode the cap and determinte which operation(might be retype()) would be trigged -> passing the argument and execute the operation(the object you want to create)

seL4test

all is fine but some bug,
Push the patch: Fix the missing symbolic link directory for "libsel4sync"Yen-Kuan Wu

build seL4 on Jetson TK1

refernece to: https://wiki.sel4.systems/Hardware/jetsontk1

flow

  • update the u-boot and enable the hyper mode
  • boot with specify user.elf

Reference

Last changed by 
 
Louie Lu
0
3920
Published on HackMD