虛擬內(nèi)存

seL4不提供虛擬內(nèi)存管理，除了那些用于操作硬件的paging structure。用戶態(tài)必須有服務(wù)去負(fù)責(zé)創(chuàng)建intermediate paging structure，還有mapping和unmapping。

用戶可以自定義自己的地址空間，但要注意內(nèi)核擁有虛擬內(nèi)存的高地址空間。對(duì)于大多數(shù)32位平臺(tái)，這是在0xe000 0000以上。

Paging Structures

啟動(dòng)時(shí)，seL4就初始化了一個(gè)頂層硬件虛擬內(nèi)存對(duì)象叫VSpace，訪問這個(gè)結(jié)構(gòu)的capability是root task的seL4_CapInitThreadVSpace。對(duì)于不同平臺(tái)，這個(gè)capability對(duì)應(yīng)的結(jié)構(gòu)體并不相同。除了top-level paging structure不同以外，intermediate paging structure也因平臺(tái)不同而不同。

當(dāng)所有paging structures的映射關(guān)系已經(jīng)建立完畢以后，還需要建立physical frame和虛擬地址之間的映射關(guān)系。同時(shí)指明虛擬內(nèi)存的讀寫權(quán)限。

幾個(gè)需要建立的映射關(guān)系

top-level paging structure <====> VADDR (例子中不需自己建立)

intermedia paging structure <====> VADDR

physical frame <====> VADDR

一些很讓人困惑的變量類型

==================================================

以下這些其實(shí)都是seL4_CPtr，是對(duì)應(yīng)object的capability。

seL4_X86_Page

seL4_X86_PDPT

seL4_X86_PageDirectory

seL4_X86_PageTable

==================================================

在使用alloc_object分配paging structures或physical frame時(shí)，需要指明想分配的是object，以下都是枚舉型：

seL4_X86_4K: 8

seL4_X86_PDPTObject: 5

seL4_X86_PageDirectoryObject: 11

seL4_X86_PageTableObject: 10

(seL4_X64_PML4Object: 12，這個(gè)是top-level paging structure對(duì)應(yīng)的類型，在本例子中不需要分配)

總結(jié)

以上是生活随笔為你收集整理的鸿蒙系统 微内核 sel4,微内核 seL4 Mapping的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

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