sel4 線程和執(zhí)行

線程

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

線程創(chuàng)建

與其他對象一樣，tcb是使用seL4無類型Retype()方法創(chuàng)建的(請參閱
2.4節(jié))。新創(chuàng)建的線程最初是不活動的。通過使用seL4 TCB SetSpace()或seL4 TCB Configure() methods設置它的CSpace和VSpace，然后使用初始堆棧指針和指令指針調(diào)用seL4 TCB WriteRegisters()來配置它。然后，可以通過將seL4 TCB WriteRegisters()調(diào)用中的Resume -target參數(shù)設置為true或單獨調(diào)用seL4 TCB Resume()方法來激活線程。在多核機器中，線程將運行在最初創(chuàng)建TCB的同一CPU上。但是，可以通過調(diào)用seL4 TCB SetAffinity()將其遷移到其他cpu上。

線程失活

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

調(diào)度

seL4使用具有256個優(yōu)先級級別的搶占式輪詢調(diào)度器。所有線程都有一個最大控制優(yōu)先級(MCP)和一個優(yōu)先級，后者是線程的有效優(yōu)先級。當一個線程創(chuàng)建或修改一個線程(包括它自己)時，它只能設置另一個線程的優(yōu)先級和MCP小于或等于它自己的MCP。線程優(yōu)先級和MCP可以用seL4 TCB Configure()和seL4 TCB SetPriority()， seL4 TCB SetMCPriority()方法設置。

異常

每個線程都有一個相關聯(lián)的異常處理程序端點。如果線程導致
異常時，內(nèi)核會創(chuàng)建一個帶有相關細節(jié)的IPC消息并將其發(fā)送給端點。然后，該線程可以采取適當?shù)牟僮鳌９收螴PC消息參見6.2。

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

異常端點必須具有發(fā)送和授予權(quán)限。回復異常消息重啟線程。對于某些異常類型，應答的內(nèi)容消息可以用來設置正在重新啟動的線程的寄存器中的值。詳見6.2節(jié)。

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

可以使用seL4 TCB ReadRegisters()和seL4 TCB writereregisters()方法讀寫線程的寄存器。對于一些寄存器,內(nèi)核將默默地掩蓋某些位或范圍的位,并強迫他們包含特定的值,以確保他們不能惡意設置為值會妥協(xié)運行系統(tǒng),或尊重的價值觀體系結(jié)構(gòu)規(guī)范規(guī)定為一定值。在X86上，這些位目前是:

寄存器內(nèi)容通過IPC緩沖區(qū)傳送。下面給出了寄存器被復制到/復制到的IPC緩沖區(qū)位置。

缺點

線程的操作可能會導致錯誤。錯誤被傳遞給線程的exception處理程序，以便它可以采取適當?shù)牟僮鳌９收项愋驮谙撕炛兄付?#xff0c;包括:seL4 fault CapFault、seL4 fault VMFault、seL4 fault UnknownSyscall、seL4 fault UserException、seL4 fault DebugException、seL4 fault NullFault(表示沒有發(fā)生故障，正常IPC message)。

錯誤以模仿來自錯誤線程的調(diào)用的方式傳遞。這意味著要發(fā)送錯誤消息，錯誤端點必須同時具有寫權(quán)限和授予權(quán)限。

capability 缺陷

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

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

響應錯誤IPC將重新啟動出錯的線程。IPC消息的內(nèi)容見表6.1。

未知的系統(tǒng)調(diào)用

當線程以seL4未知的系統(tǒng)調(diào)用號執(zhí)行系統(tǒng)調(diào)用時，就會發(fā)生此錯誤。發(fā)生故障的線程的注冊集被傳遞給線程的異常處理程序，這樣，如果一個線程正在被虛擬化，它就可以模擬系統(tǒng)調(diào)用。

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

用戶異常

用戶異常用于交付體系結(jié)構(gòu)定義的異常。例如，如果用戶線程試圖將一個數(shù)字除以0，就會發(fā)生這樣的異常。

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

調(diào)試異常:斷點和觀察點

調(diào)試異常用于將跟蹤和調(diào)試相關事件傳遞給線程。斷點點、觀察點、跟蹤事件和指令性能采樣事件都是例子。當內(nèi)核被配置為包含這些事件時(當配置硬件調(diào)試API被設置時)，用戶空間線程就支持這些事件。關于可用的硬件調(diào)試資源的信息以下列常量的形式呈現(xiàn):

**seL4 NumHWBreakpoints 😗*定義了硬件平臺上所有可用類型的可用硬件中斷寄存器的總數(shù)。以ARM Cortex A7為例，有6個專用指令斷點寄存器和4個專用數(shù)據(jù)觀察點寄存器，總共有10個監(jiān)視器寄存器。因此，在這個平臺上，seL4NumHWBreakpoints被定義為10。指令斷點寄存器將始終被分配為較低的api - id，數(shù)據(jù)觀察點將始終跟隨它們被分配。

此外，為每個目標平臺定義了seL4 NumExclusiveBreakpoints、seL4 NumExclusiveWatchpoints和seL4 NumDualFunctionMonitors，以反映某種類型的可用硬件斷點/觀察點的數(shù)量。

seL4 NumExclusiveBreakpoints：定義僅在指令執(zhí)行時才可能產(chǎn)生錯誤的硬件寄存器的數(shù)量。目前這只會在ARM平臺上設置。第一個獨占斷點的API-ID在seL4 FirstBreakpoint中給出。如果沒有指令中斷獨占寄存器，則seL4 NumExclusiveBreakpoints將被設置為0,seL4 FirstBreakpoint將被設置為-1。

**seL4 NumExclusiveWatchpoints：**定義僅在數(shù)據(jù)訪問時才可產(chǎn)生故障的硬件寄存器的數(shù)量ca。目前這只會在ARM平臺上設置。第一個獨占觀察點的API-ID在seL4 FirstWatchpoint中給出。如果沒有數(shù)據(jù)中斷獨占寄存器，則seL4 NumExclusiveWatchpoints將被設置為0,seL4 FirstWatchpoint將被設置為-1。

seL4 NumDualFunctionMonitors：定義硬件寄存器的數(shù)量，可以在任何類型的訪問上產(chǎn)生錯誤，也就是說，寄存器同時支持指令和數(shù)據(jù)中斷。目前只在x86平臺上設置。第一個雙功能監(jiān)視器的API-ID在seL4 FirstDualFunctionMonitor中給出。如果沒有雙函數(shù)中斷寄存器，seL4 NumDualFunctionMonitors將被設置為0,seL4 FirstDualFunctionMonitor將被設置為-1。

調(diào)試異常:單步

當配置了用戶空間線程時(當設置了配置硬件調(diào)試API時)，內(nèi)核提供了對使用硬件單步用戶空間線程的支持。為此，它公開調(diào)用，seL4 TCB configuresinglestep。

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

如果bp_was_consumed是真的,調(diào)用者不應試圖重新配置bp num斷點或監(jiān)視點使用直到調(diào)用者禁用單步和注冊發(fā)布,隨后通過調(diào)用seL4 TCB ConfigureSingleStepping,或與n instr fault-reply 0。將num指令設置為0將禁用單步執(zhí)行。

在需要為單個步進功能配置實際硬件寄存器的架構(gòu)上，seL4將限制可以配置為單步進的寄存器的數(shù)量，在任何給定時間為一個。當前為單步調(diào)試配置的寄存器(如果有的話)將是單步調(diào)試故障應答中的隱式bp num參數(shù)。

內(nèi)核的單步操作，也支持在傳遞單步錯誤消息之前跳過一定數(shù)量的指令。在單步執(zhí)行時，應該將Num指令設置為1，或者在恢復單步執(zhí)行之前將任何非零整數(shù)值設置為跳過這么多指令。還可以在單步調(diào)試故障的故障應答中設置這個跳過計數(shù)。

VM異常

該線程導致頁面錯誤。響應錯誤IPC將重新啟動線程。IPC消息的內(nèi)容如下。

域

用域來隔離獨立的子系統(tǒng)，使它們之間的信息流限制在之間。內(nèi)核根據(jù)一個固定的、由時間觸發(fā)的時間表在域之間切換。固定的調(diào)度通過常量CONFIG-NUM_DOMAINS和全局變量ksDomSchedule編譯到內(nèi)核中。

線程只屬于一個域，并且只在該域處于活動狀態(tài)時運行。seL4 DomainSet Set()方法更改線程的域。調(diào)用者必須擁有域權(quán)能和線程的TCB權(quán)能。初始線程以域權(quán)能開始(見4.1節(jié))。

總結(jié)

以上是生活随笔為你收集整理的sel4线程和执行的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯，歡迎將生活随笔推薦給好友。