sel4 線程和執(zhí)行

線程

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

線程創(chuàng)建

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

線程失活

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

調(diào)度

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

異常

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

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

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

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

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

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

缺點(diǎn)

線程的操作可能會(huì)導(dǎo)致錯(cuò)誤。錯(cuò)誤被傳遞給線程的exception處理程序，以便它可以采取適當(dāng)?shù)牟僮鳌９收项愋驮谙?biāo)簽中指定，包括:seL4 fault CapFault、seL4 fault VMFault、seL4 fault UnknownSyscall、seL4 fault UserException、seL4 fault DebugException、seL4 fault NullFault(表示沒有發(fā)生故障，正常IPC message)。

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

capability 缺陷

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

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

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

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

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

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

用戶異常

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

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

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

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

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

此外，為每個(gè)目標(biāo)平臺(tái)定義了seL4 NumExclusiveBreakpoints、seL4 NumExclusiveWatchpoints和seL4 NumDualFunctionMonitors，以反映某種類型的可用硬件斷點(diǎn)/觀察點(diǎn)的數(shù)量。

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

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

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

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

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

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

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

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

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

VM異常

該線程導(dǎo)致頁面錯(cuò)誤。響應(yīng)錯(cuò)誤IPC將重新啟動(dòng)線程。IPC消息的內(nèi)容如下。

域

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

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

總結(jié)

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

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