虚拟内存

seL4不提供虚拟内存管理，除了那些用于操作硬件的paging structure。用户态必须有服务去负责创建intermediate paging structure，还有mapping和unmapping。

用户可以自定义自己的地址空间，但要注意内核拥有虚拟内存的高地址空间。对于大多数32位平台，这是在0xe000 0000以上。

Paging Structures

启动时，seL4就初始化了一个顶层硬件虚拟内存对象叫VSpace，访问这个结构的capability是root task的seL4_CapInitThreadVSpace。对于不同平台，这个capability对应的结构体并不相同。除了top-level paging structure不同以外，intermediate paging structure也因平台不同而不同。

当所有paging structures的映射关系已经建立完毕以后，还需要建立physical frame和虚拟地址之间的映射关系。同时指明虚拟内存的读写权限。

几个需要建立的映射关系

• top-level paging structure <====> VADDR （例子中不需自己建立）
• intermedia paging structure <====> VADDR
• physical frame <====> VADDR

一些很让人困惑的变量类型

==================================================
以下这些其实都是seL4_CPtr，是对应object的capability。
seL4_X86_Page
seL4_X86_PDPT
seL4_X86_PageDirectory
seL4_X86_PageTable
==================================================
在使用alloc_object分配paging structures或physical frame时，需要指明想分配的是object，以下都是枚举型：
seL4_X86_4K: 8
seL4_X86_PDPTObject: 5
seL4_X86_PageDirectoryObject: 11
seL4_X86_PageTableObject: 10
（seL4_X64_PML4Object: 12，这个是top-level paging structure对应的类型，在本例子中不需要分配）