sel4是微核心，它只提供了少數供使用者程式使用的機制。不像linux核心提供了大量的服務。本文主要介紹sel4提供的七個核心物件，著重講述了untyped這一核心物件。
sel4提供了七個核心物件，這七個核心物件構成了乙個程序基本執行環境。它們分別是：
sel4 untyped表示為一塊連續未分配的物理記憶體，使用者程式可以通過untyped cap來使用這塊物理記憶體。下面介紹了untyped cap結構體以及在untyped記憶體上建立tcb核心物件。
untyped cap結構體
untyped cap結構體：
capblocksize：表示當前這段連續的物理記憶體空間大小；
block untyped_capsel4_untyped_retype函式是使用untyped的物理記憶體的唯一api，其有八個引數，分別是：
具體的建立流程如下：
使用者程式呼叫函式sel4_untyped_retype；
sel4_untyped_retype
(child_untyped, sel4_tcbobject,
0, sel4_capinitthreadcnode,0,
0, child_tcb,1)
;
a. 從ipc buffer裡面取出建立核心物件的相關資訊；
b. 根據root、node_index和node_depth找到對應的cnode cap；
c. 檢查該cnode的尺寸是否容得下node_offset以及對應node_offset的slot是否為空；
d. 根據untyped cap資訊得到untyped記憶體的空間記憶體的起始位址，並判斷是否能夠存放核心物件；
e. 呼叫invokeuntyped_retype函式。
invokeuntyped_retype函式更新該untyped cap存放的空閒記憶體資訊，並呼叫createnewobjects函式；
createnewobjects函式的功能如下：
a. 在untyped cap指向的空閒空間初始化tcb；
b. 生成tcb cap；
c. 將該tcb cap插入到第2步找到得的cnode對應的slot裡。
完成。sel4原始碼解析（一） - sel4核心物件
sel4原始碼解析（二） - cspace
sel4原始碼解析（三） - sel4系統呼叫處理流程
sel4原始碼解析（四） - ipc
sel4原始碼解析（五） - notification
sel4原始碼解析（六） - 程序
sel4原始碼解析（七） - vspace
sel4原始碼解析（七） vspace
sel4 vspace指的是程序的虛擬位址空間。armv8 64位版本的sel4 對應的頁表劃分分為四級，分別是 pgd page global directory pud page upper directory pd page directory 和pt page table pgdpgd結構體...
SLF4J原始碼解析（一）
閱讀原始碼之前，首先提幾個問題 帶著上面的兩個問題看下原始碼 bind 方法中通過呼叫findpossiblestaticloggerbinderpathset 方法來查詢日誌框架的繫結 findpossiblestaticloggerbinderpathset 方法中通過classloader或者...
SLF4J原始碼解析（一）
閱讀原始碼之前，首先提幾個問題 帶著上面的兩個問題看下原始碼 bind 方法中通過呼叫findpossiblestaticloggerbinderpathset 方法來查詢日誌框架的繫結 org slf4j slf4j api 1.7.25 slf4j api 1.7.25.jar org slf4...