sel4 線程和執行

線程

seL4提供了表示執行上下文和管理處理器時間的線程。在seL4中，線程由其線程控制塊對象(TCB)表示。每個TCB都有一個相關的CSpace(見第3章)和VSpace(見第7章)，它們可以被其他線程共享。TCB還可以有一個IPC緩沖區(見第4章)，用于在IPC或核心對象調用期間傳遞不适合體系結構定義的消息寄存器的額外參數。雖然一個線程不需要有IPC緩沖區，但是它不能執行大多數核心調用，因為它們需要cap傳輸。每個線程隻屬于一個安全域(見6.3節)。

線程建立

與其他對象一樣，tcb是使用seL4無類型Retype()方法建立的(請參閱

2.4節)。新建立的線程最初是不活動的。通過使用seL4 TCB SetSpace()或seL4 TCB Configure() methods設定它的CSpace和VSpace，然後使用初始堆棧指針和指令指針調用seL4 TCB WriteRegisters()來配置它。然後，可以通過将seL4 TCB WriteRegisters()調用中的Resume -target參數設定為true或單獨調用seL4 TCB Resume()方法來激活線程。在多核機器中，線程将運作在最初建立TCB的同一CPU上。但是，可以通過調用seL4 TCB SetAffinity()将其遷移到其他cpu上。

線程失活

seL4 TCB Suspend()方法取消激活一個線程。挂起的線程稍後可以被恢複。它們的挂起狀态可以通過seL4 TCB ReadRegisters()和seL4 TCB CopyRegisters()方法檢索。如果不需要，它們也可以重新配置和重用，或者無限期地挂起。線程将在其TCB的最後一個功能被删除時自動挂起。

排程

seL4使用具有256個優先級級别的搶占式輪詢排程器。所有線程都有一個最大控制優先級(MCP)和一個優先級，後者是線程的有效優先級。當一個線程建立或修改一個線程(包括它自己)時，它隻能設定另一個線程的優先級和MCP小于或等于它自己的MCP。線程優先級和MCP可以用seL4 TCB Configure()和seL4 TCB SetPriority()， seL4 TCB SetMCPriority()方法設定。

異常

每個線程都有一個相關聯的異常處理程式端點。如果線程導緻

異常時，核心會建立一個帶有相關細節的IPC消息并将其發送給端點。然後，該線程可以采取适當的操作。故障IPC消息參見6.2。

為了啟用異常處理程式，異常處理程式端點的功能必須存在于生成異常的線程的CSpace中。可以使用seL4 TCB SetSpace()或seL4 TCB Configure()方法設定異常處理程式端點。通過這些方法，可以将異常處理程式的功能位址與線程相關聯。當生成異常時使用此位址查找處理程式端點。但是請注意，這些方法不會檢查線程的CSpace中的指定位址上是否存在端點功能。隻有在實際發生異常時才會查找該功能，如果查找失敗，則不會發送異常消息，線程将無限期地挂起。

異常端點必須具有發送和授予權限。回複異常消息重新開機線程。對于某些異常類型，應答的内容消息可以用來設定正在重新啟動的線程的寄存器中的值。詳見6.2節。

讀/寫寄存器方法的消息布局

可以使用seL4 TCB ReadRegisters()和seL4 TCB writereregisters()方法讀寫線程的寄存器。對于一些寄存器,核心将默默地掩蓋某些位或範圍的位,并強迫他們包含特定的值,以確定他們不能惡意設定為值會妥協運作系統,或尊重的價值觀體系結構規範規定為一定值。在X86上，這些位目前是:

寄存器内容通過IPC緩沖區傳送。下面給出了寄存器被複制到/複制到的IPC緩沖區位置。

缺點

線程的操作可能會導緻錯誤。錯誤被傳遞給線程的exception處理程式，以便它可以采取适當的操作。故障類型在消息标簽中指定，包括:seL4 fault CapFault、seL4 fault VMFault、seL4 fault UnknownSyscall、seL4 fault UserException、seL4 fault DebugException、seL4 fault NullFault(表示沒有發生故障，正常IPC message)。

錯誤以模仿來自錯誤線程的調用的方式傳遞。這意味着要發送錯誤消息，錯誤端點必須同時具有寫權限和授予權限。

capability 缺陷

能力故障可能發生在兩個地方。首先，當seL4 Call()或seL4 Send()系統調用引用的功能查找失敗(seL4 NBSend()對無效功能的調用靜默失敗)。在這種情況下，發生故障的能力可能是正在調用的能力，或者IPC緩沖區中caps字段中傳遞的額外能力。

其次，當seL4 Recv()或seL4 NBRecv()對不存在、不是端點或通知功能或沒有接收權限的功能調用時，可能會發生功能故障。

響應錯誤IPC将重新啟動出錯的線程。IPC消息的内容見表6.1。

未知的系統調用

當線程以seL4未知的系統調用号執行系統調用時，就會發生此錯誤。發生故障的線程的注冊集被傳遞給線程的異常處理程式，這樣，如果一個線程正在被虛拟化，它就可以模拟系統調用。

響應錯誤IPC允許重新啟動線程和/或修改線程的寄存器。如果應答的标簽為0，線程将重新啟動。另外，如果消息長度不為零，則故障線程的寄存器集将被更新，如表6.2和表6.3所示。在這種情況下，更新的寄存器數量由消息标記的length字段控制。

使用者異常

使用者異常用于傳遞體系結構定義的異常。例如，如果使用者線程試圖将一個數字除以0，就會發生這樣的異常。

響應錯誤IPC允許重新啟動線程和/或修改線程的寄存器。如果應答的标簽為0，線程将重新啟動。另外，如果消息長度非零，那麼發生故障的線程的寄存器集将被更新，如表6.4和表6.5所示。在這種情況下，更新的寄存器數量由消息标記的length字段控制。

調試異常:斷點和觀察點

調試異常用于将跟蹤和調試相關事件傳遞給線程。斷點點、觀察點、跟蹤事件和指令性能采樣事件都是例子。當核心被配置為包含這些事件時(當配置硬體調試API被設定時)，使用者空間線程就支援這些事件。關于可用的硬體調試資源的資訊以下列常量的形式呈現:

**seL4 NumHWBreakpoints 😗*定義了硬體平台上所有可用類型的可用硬體中斷寄存器的總數。以ARM Cortex A7為例，有6個專用指令斷點寄存器和4個專用資料觀察點寄存器，總共有10個螢幕寄存器。是以，在這個平台上，seL4NumHWBreakpoints被定義為10。指令斷點寄存器将始終被配置設定為較低的api - id，資料觀察點将始終跟随它們被配置設定。

此外，為每個目标平台定義了seL4 NumExclusiveBreakpoints、seL4 NumExclusiveWatchpoints和seL4 NumDualFunctionMonitors，以反映某種類型的可用硬體斷點/觀察點的數量。

seL4 NumExclusiveBreakpoints：定義僅在指令執行時才可能産生錯誤的硬體寄存器的數量。目前這隻會在ARM平台上設定。第一個獨占斷點的API-ID在seL4 FirstBreakpoint中給出。如果沒有指令中斷獨占寄存器，則seL4 NumExclusiveBreakpoints将被設定為0,seL4 FirstBreakpoint将被設定為-1。

**seL4 NumExclusiveWatchpoints：**定義僅在資料通路時才可産生故障的硬體寄存器的數量ca。目前這隻會在ARM平台上設定。第一個獨占觀察點的API-ID在seL4 FirstWatchpoint中給出。如果沒有資料中斷獨占寄存器，則seL4 NumExclusiveWatchpoints将被設定為0,seL4 FirstWatchpoint将被設定為-1。

seL4 NumDualFunctionMonitors：定義硬體寄存器的數量，可以在任何類型的通路上産生錯誤，也就是說，寄存器同時支援指令和資料中斷。目前隻在x86平台上設定。第一個雙功能螢幕的API-ID在seL4 FirstDualFunctionMonitor中給出。如果沒有雙函數中斷寄存器，seL4 NumDualFunctionMonitors将被設定為0,seL4 FirstDualFunctionMonitor将被設定為-1。

調試異常:單步

當配置了使用者空間線程時(當設定了配置硬體調試API時)，核心提供了對使用硬體單步使用者空間線程的支援。為此，它公開調用，seL4 TCB configuresinglestep。

調用者需要選擇一個API-ID，該API-ID對應于指令斷點點，用于設定單步執行功能(例如，API-ID從0到seL4 NumExclusiveBreakpoints - 1)。然而，并不是所有的硬體平台都需要一個實際的硬體斷點寄存器來提供單步功能。如果調用者的硬體平台需要使用硬體斷點寄存器，它将使用bp num中給它的斷點寄存器，并在bp_was_consumed中傳回true。如果底層平台不需要硬體斷點來提供單個步進，那麼seL4将在bp was consume中傳回false，并保持bp num不變。

如果bp_was_consumed是真的,調用者不應試圖重新配置bp num斷點或監視點使用直到調用者禁用單步和注冊釋出,随後通過調用seL4 TCB ConfigureSingleStepping,或與n instr fault-reply 0。将num指令設定為0将禁用單步執行。

在需要為單個步進功能配置實際硬體寄存器的架構上，seL4将限制可以配置為單步進的寄存器的數量，在任何給定時間為一個。目前為單步調試配置的寄存器(如果有的話)将是單步調試故障應答中的隐式bp num參數。

核心的單步操作，也支援在傳遞單步錯誤消息之前跳過一定數量的指令。在單步執行時，應該将Num指令設定為1，或者在恢複單步執行之前将任何非零整數值設定為跳過這麼多指令。還可以在單步調試故障的故障應答中設定這個跳過計數。

VM異常

該線程導緻頁面錯誤。響應錯誤IPC将重新啟動線程。IPC消息的内容如下。

域

用域來隔離獨立的子系統，使它們之間的資訊流限制在之間。核心根據一個固定的、由時間觸發的時間表在域之間切換。固定的排程通過常量CONFIG-NUM_DOMAINS和全局變量ksDomSchedule編譯到核心中。

線程隻屬于一個域，并且隻在該域處于活動狀态時運作。seL4 DomainSet Set()方法更改線程的域。調用者必須擁有域權能和線程的TCB權能。初始線程以域權能開始(見4.1節)。