seL4微核心學習之二：seL4中的一些基礎概念

作為微核心作業系統，seL4隻提供很少的基礎核心服務，複雜的服務将在使用者态基于這些基礎核心服務實作。

1. Threads：是運作CPU的抽象。
2. Address spaces：是配置設定給應用程式的虛拟位址空間，應用程式被限制隻能通路其自己的空間。
3. Inter-process communication (IPC)：通過Endpoint實作的程序間的通信方法。
4. Device primitives：允許裝置驅動實作在使用者态。核心通過IPC來實作中斷。
5. Capability spaces：存儲對核心對象的Capability（也就是一些通路權限），和一些對象資訊。

核心對象有以下6個：

1. Cnodes：存儲權能資訊，決定了一個線程的調用特定對象方法的權限。每個Cnode的slot的數量是一定的（2的幂次），并且該數量是在建立該Cnode時确定的。每個slot可以為空。
2. Thread Control Block（TCB）：代表一個正在運作的程序，是排程，阻塞等操作的最小單元。
3. IPC Endpoint：用來輔助程序間IPC，有兩種類型的IPC Endpoint，一種是Synchronous Endpoint，另一種是Asynchronous Endpoint，顧名思義，一種是同步的，即在資訊沒有被接受時會阻塞發送消息的線程，另一種是異步的，隻能傳遞短消息，但不會發生阻塞。
4. Virtual Address Space Object：為線程建構VSpace（Virtual Address Space），對應着各種硬體資訊。比如，頁目錄指向頁表，而頁表項又指向實體的幀（frame）。核心也有ASID Pool 和 ASID Control objects來檢視位址空間的狀态。
5. Interrupt Object：用來接收和确認來自硬體的中斷。在Initial Thread中有一個IRQControl的Capability，來建立IRQHandler Capability。IRQHandler Capability通常被授給device dirver來 access中斷的來源。一個IRQHandler Capability管理一個特定裝置的特定中斷來源。例如，一個IRQHandler Capability管理鍵盤的一個字母的讀入。
6. Untyped Memory：是記憶體配置設定的基礎。Untyped Memory隻有一個方法（retype），來建立新的核心對象，成功即向調用函數建立對象的Capability。另外，Untyped Memory還可以劃分為一組更小的Untyped Memory，實作将系統記憶體劃分為小塊來管理。