虛擬內(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)的類型虱疏，在本例子中不需要分配）
