sel4源码解析（七） - vspace
sel4 vspace指的是进程的虚拟地址空间。armv8 64位版本的sel4 对应的页表划分分为四级，分别是：pgd（page global directory）、pud（page upper directory）、pd（page directory）和pt（page table）。
本文主要介绍了sel4关于页表的基本数据结构体、sel4为初始进程创建页表的过程解析以及简要的描述了AArch64架构虚拟地址到物理地址的转换流程。
基本数据结构
pgd
pgd结构体：
- pud_base_address：指向pud基地址的指针（指向的pud大小为4K）；
block pgde_pud {
padding 16
field_high pud_base_address 36
padding 10
field pgde_type 2 -- must be 0b11
}
pgd cap结构体：
- capPGDMappedASID：进程的ASID（address space Identifiers）；
- capPGDBasePtr：指向pgd结构体的指针。
block page_global_directory_cap {
field capPGDMappedASID 16
field_high capPGDBasePtr 48
field capType 5
field capPGDIsMapped 1
padding 58
}
pud
pud结构体：
- pd_base_address：指向pd基地址的指针（指向的pd大小为4K）；
block pude_pd {
padding 16
field_high pd_base_address 36
padding 10
field pude_type 2
}
pud cap结构体：
- capPUDMappedASID：进程的ASID（address space Identifiers）；
- capPUDBasePtr：指向pud结构体的指针；
- capPUDMappedAddress：指向映射的虚拟地址。
block page_upper_directory_cap {
field capPUDMappedASID 16
field_high capPUDBasePtr 48
field capType 5
field capPUDIsMapped 1
field_high capPUDMappedAddress 10
padding 48
}
pd
pd结构体：
- pt_base_address：指向pt基地址的指针（指向的pt大小为4K）；
block pde_small {
padding 16
field_high pt_base_address 36
padding 10
field pde_type 2
}
pd cap结构体：
- capPDMappedASID：进程的ASID（address space Identifiers）；
- capPDBasePtr：指向pd结构体的指针；
- capPDMappedAddress：指向映射的虚拟地址。
block page_directory_cap {
field capPDMappedASID 16
field_high capPDBasePtr 48
field capType 5
padding 10
field capPDIsMapped 1
field_high capPDMappedAddress 19
padding 29
}
pt
pte结构体：
- 描述页面属性；
block pte {
padding 9
field UXN 1
padding 6
field_high page_base_address 36
field nG 1
field AF 1
field SH 2
field AP 2
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
field AttrIndx 4
#else
padding 1
field AttrIndx 3
#endif
field reserved 2 -- must be 0b11
}
page_table_cap结构体：
- capPTMappedASID：进程的ASID（address space Identifiers）；
- capPTBasePtr：指向pt结构体的指针；
- capPTMappedAddress：指向映射的虚拟地址。
block page_table_cap {
field capPTMappedASID 16
field_high capPTBasePtr 48
field capType 5
padding 10
field capPTIsMapped 1
field_high capPTMappedAddress 28
padding 20
}
sel4进程分配地址空间
这里以初始进程为例，初始进程的页表建立过程大致分为三步：创建内存、建立映射、填充页表项属性。具体如下所示：
create_rootserver_objects函数
-
为vspace分配内存空间，大小为4k。这片内存用于存放pgd的地址映射关系；
-
为rootserver.paging分配内存空间，大小为存放初始进程的镜像尺寸。这片内存用于存放pud、pd、pt的地址映射关系；
BOOT_CODE void create_rootserver_objects(pptr_t start, v_region_t v_reg, word_t extra_bi_size_bits)
{
...
rootserver.vspace = alloc_rootserver_obj(seL4_VSpaceBits, 1);
/* paging structures are 4k on every arch except aarch32 (1k) */
word_t n = arch_get_n_paging(v_reg);
rootserver.paging.start = alloc_rootserver_obj(seL4_PageTableBits, n);
rootserver.paging.end = rootserver.paging.start + n * BIT(seL4_PageTableBits);
...
}
create_it_address_space函数
-
创建vspace_cap即page_global_directory_cap，他的成员capPGDBasePtr指向create_rootserver_objects为vspace分配的4k内存首地址，包含 2 9 2^9 29个pud表项；
-
为pud的映射关系表分配内存，其大小为4K，包含了 2 9 2^9 29个pd表项（从rootserver.paging中取出）。capPUDBasePtr指向pud的基地址，capPUDMappedAddress指向映射的虚拟地址。在pgd里插入该pud表项；
-
为pd的映射关系表分配内存，其大小为4K，包含了 2 9 2^9 29个pt表项（从rootserver.paging中取出）。capPDBasePtr指向pd的基地址，capPDMappedAddress指向映射的虚拟地址。在pud里插入该pd表项；
-
为pt的映射关系表分配内存，其大小为4K，包含了 2 9 2^9 29个表项（从rootserver.paging中取出）。capPTBasePtr指向pt的基地址，capPTMappedAddress指向映射的虚拟地址。在pd里插入该pT表项；
BOOT_CODE cap_t create_it_address_space(cap_t root_cnode_cap, v_region_t it_v_reg)
{
cap_t vspace_cap;
vptr_t vptr;
seL4_SlotPos slot_pos_before;
seL4_SlotPos slot_pos_after;
/* create the PGD */
vspace_cap = cap_vtable_cap_new(
IT_ASID, /* capPGDMappedASID */
rootserver.vspace, /* capPGDBasePtr */
1 /* capPGDIsMapped */
);
slot_pos_before = ndks_boot.slot_pos_cur;
write_slot(SLOT_PTR(pptr_of_cap(root_cnode_cap), seL4_CapInitThreadVSpace), vspace_cap);
/* Create any PUDs needed for the user land image */
for (vptr = ROUND_DOWN(it_v_reg.start, PGD_INDEX_OFFSET);
vptr < it_v_reg.end;
vptr += BIT(PGD_INDEX_OFFSET)) {
if (!provide_cap(root_cnode_cap, create_it_pud_cap(vspace_cap, it_alloc_paging(), vptr, IT_ASID))) {
return cap_null_cap_new();
}
}
/* Create any PDs needed for the user land image */
for (vptr = ROUND_DOWN(it_v_reg.start, PUD_INDEX_OFFSET);
vptr < it_v_reg.end;
vptr += BIT(PUD_INDEX_OFFSET)) {
if (!provide_cap(root_cnode_cap, create_it_pd_cap(vspace_cap, it_alloc_paging(), vptr, IT_ASID))) {
return cap_null_cap_new();
}
}
/* Create any PTs needed for the user land image */
for (vptr = ROUND_DOWN(it_v_reg.start, PD_INDEX_OFFSET);
vptr < it_v_reg.end;
vptr += BIT(PD_INDEX_OFFSET)) {
if (!provide_cap(root_cnode_cap, create_it_pt_cap(vspace_cap, it_alloc_paging(), vptr, IT_ASID))) {
return cap_null_cap_new();
}
}
slot_pos_after = ndks_boot.slot_pos_cur;
ndks_boot.bi_frame->userImagePaging = (seL4_SlotRegion) {
slot_pos_before, slot_pos_after
};
return vspace_cap;
}
- 最后由函数create_frames_of_region填充页表的页表项，具体可以参看pt的结构体；
AArch64架构虚拟地址转换的简要过程
虚拟地址转换成物理地址流程：
- 取虚拟地址高九位结合TTBR_ELx寄存器找到pgd的首地址；
- 再取虚拟地址九位得到pgde，里面包含pud的首地址；
- 再取九位得到pude，里面包含pd的首地址；
- 再取九位得到pde，里面包含pt的首地址；
- 剩余的低十二位为页内地址。
相关链接
sel4源码解析（一） - sel4内核对象
sel4源码解析（二） - CSpace
sel4源码解析（三） - sel4系统调用处理流程
sel4源码解析（四） - ipc
sel4源码解析（五） - Notification
sel4源码解析（六） - 进程
sel4源码解析（七） - vspace