seL4 Mapping（三）

官网链接: Mapping

Mapping

这节课程主要是介绍seL4的虚存管理。

虚存 Virtual memory

除了用于操作硬件分页结构的内核原语之外，seL4不提供虚拟内存管理。用户必须为创建中间级分页结构，映射页面以及取消映射页面提供服务。
用户可以随意的定义他们自己的地址空间布局，但是有一个限制：seL4会占用虚地址空间的高地址部分。在大多数的32位的平台中，内核占用0xe0 00 00 00以上的空间。每个平台的这个变量是不太一样的，可以通过在seL4的源码中通过寻找kernelBase找到这个变量。
上面来个更直观的例子：

+--------------------------+  <- 高地址
|    seL4 Kernel Space     |  <- 内核空间，受保护
+--------------------------+
|                          |  
|        User Space        |  <- 用户空间，可以自由定义
|                          |
+--------------------------+  <- 低地址

分页结构 Paging structures

作为启动进程的一部分，seL4初始化根任务时还会为其创建一个顶级的硬件虚存对象，这个对象被称之为VSpace。根任务中的seL4_CapInitThreadVSpace能力槽是针对该结构可用的能力。对于每种架构（architecture），该能力将会对应不同的与硬件和顶级页结构相符的对象类型。下面的表列出了对于每种支持的架构的对象类型。

Architecture	VSpace Object
aarch32	seL4_PageDirectory
aarch64	seL4_PageGlobalDirectory
ia32	seL4_PageDirectory
x86_64	seL4_PML4
RISC-V	seL4_PageTable

除了顶级的页结构。需要中间硬件虚拟内存对象来映射页面。下面的表按照顺序列出了每个体系结构的这些对象。

Architecture	Objects
aarch32	seL4_PageTable
aarch64	seL4_PageUpperDirectory, seL4_PageDirectory, seL4_PageTable
ia32	seL4_PageTable
x86_64	seL4_PDPT, seL4_PageDirectory, seL4_PageTable
RISC-V	seL4_PageTable

这篇课程使用的是x86_64架构，但是包含了足够多的由seL4提供的虚存API信息以概括了其他的架构。
为了映射或者取消映射每种也结构都能够被调用。下面是一个映射x86_64seL4_PDRT对象的案例。

/* map a PDPT at TEST_VADDR */
error = seL4_X86_PDPT_Map(pdpt, seL4_CapInitThreadVSpace, TEST_VADDR, seL4_X86_Default_VMAttributes);

所有的映射函数都带有三个参数：

该对象映射到的VSpace
映射对象的虚拟地址
虚存属性

如果提供的虚存地址与分页对象的大小不对齐，seL4将屏蔽任何未使用位。例如映射在0xDEADBEEF的4KiB页最终将映射在0xDEADB000上面。对齐含义不清楚的可参考下面的解释：
在 32 位机器上，虚拟地址是 32 位长，通常按照字节来编址，即总共有2³²B的虚存。如果每个页面大小为 4 KiB (即2¹²字节），那么虚拟内存可以容纳的页面数为2³²/2¹²=2²⁰个页。
在地址结构中，前 20 位用于标识虚拟页号（VPN），后 12 位用于页内偏移。因此，每个 4 KiB 的页面在映射到虚存时，必须对齐到虚存的 4 KiB 边界上。这就是为啥映射在0xDEADBEEF的4KiB页最终将被映射在0xDEADB000上面。
虚存属性决定了映射的缓存属性，这是架构依赖的。除了本教程使用的属性seL4_X86_Default_VMAttributes，你可以在libsel4中找到其他的可以替换的值。

Pages 页

一旦所有的中间页结构被映射到了特定的虚拟地址范围，可以通过调用帧（frame）能力将物理帧（frame）映射到这个范围。下面的代码片段展示了一个在地址TEST_VADDR映射一个帧的示例（将物理帧映射到虚拟地址）。

 /* map a read-only page at TEST_VADDR */
 error = seL4_X86_Page_Map(frame, seL4_CapInitThreadVSpace, TEST_VADDR, seL4_CanRead, seL4_X86_Default_VMAttributes);

为了使页面映射成功，必须映射所有的中级分页结构。libsel4中的函数seL4_MappingFailedLookupLevel() 可以被用于确定哪个等级的页结构是缺失的。注意，为了能将一个帧映射多次，必须复制帧能力：每个帧能力只能追踪一个映射。
除了中间分页结构的映射方法所采用的参数之外，页面映射还携带一个right参数，该参数决定了映射的类型。在上面的例子中，我们映射的这个页面是只读的。

Types and sizes

页的类型和大小是体系结构决定的。对于x86和ARM架构，每个尺寸的页面都是具有特定尺寸的不同对象类型（不像人话）。在RISC-V中，页面具有相同的对象类型和不同的大小。配置和硬件设置可改变可用的页面大小。

上面讲了一通看的人乱七八糟的，一方面可能是我翻译的不到位，还有就是解释篇幅是真的小啊。下面具体的总结一下上面说的啥：

解释

在 seL4 操作系统中，虚拟内存管理通过一个叫做 VSpace（虚拟地址空间）来完成，VSpace 是一个虚拟内存的层次结构，负责将虚拟地址映射到物理地址。为了做到这一点，seL4 借助了一些特定的硬件支持（比如 x86 和 ARM 架构的分页机制）和相应的页表对象。可以将 seL4 的虚拟内存结构理解为多级页表管理体系，每一级页表都有不同的角色和功能。下面将详细解释 VSpace 以及各级页表对象：

1、VSpace（虚拟地址空间）

VSpace 是一个抽象的概念，代表了进程可以使用的所有虚拟地址。每个进程在 seL4 中都有自己的虚拟地址空间（VSpace），这个空间通过分层的页表结构将虚拟地址映射到物理内存。VSpace 的核心在于将虚拟地址翻译成实际的物理内存地址。
VSpace 在 seL4 中通常会涉及到下面的几个核心组件：

页表对象（Page Table Objects）：这些对象存储页表条目，它们定义了虚拟地址如何映射到物理地址。
顶级页表（Top-level page structure object）：在某些体系结构中，虚拟地址空间的映射由多级页表组成，顶级页表是多级页表结构中的最高层，负责指向下一级页表。

不同的架构对页表对象有不同的层次结构，下面我们以常见的架构来说明。

2、顶级页结构对象（Top-level Page Table Object）

这个对象处于页表的最高层，用来管理整个虚拟地址空间的最上层映射。它是虚拟内存层次结构的入口，指向中间的页表层次，多级页表的感觉。
不同的硬件架构对顶级页表的命名有所不同（通过上面的表也可以看出来）：
x86_64 架构：

在 x86_64 架构上，顶级页表对象叫做 PML4（Page Map Level 4）。
PML4 是四级页表体系的最高级，用来指向PDPT（Page Directory Pointer Table）。
一个 PML4 条目可以指向 512 个 PDPT 条目，涵盖整个 48 位虚拟地址空间。

3、中间硬件虚拟内存对象（Intermediate Page Table Objects）

这些对象位于顶级页表与实际的页之间，负责分割虚拟地址空间并指向具体的页表条目。
在 x86_64 架构中的中间层次对象：

PDPT（Page Directory Pointer Table）：位于 PML4 下一级，每个 PDPT 对应 512 个 PDE（Page Directory Entry）。
PDE（Page Directory Entry）：指向具体的页表条目（Page Table Entry，PTE），PDE 层次可以覆盖到 1 GiB 的虚拟地址范围。
Page Table Entry (PTE)：这是实际的页表条目，PTE 包含了物理帧（page frame）的地址信息。

4、页表条目（Page Table Entry, PTE）

页表条目是分页机制中的最底层条目，直接映射虚拟页到物理页。每个页表条目通常记录着物理内存页的地址以及该页的访问权限、缓存设置等属性。
PTE 中的地址是指向物理内存页的开始地址，通常是按页对齐的。比如，在使用 4KiB 页大小时，PTE 中记录的地址最低的 12 位是 0（因为页大小是 2^12 B）。

5、举例而言

以x86_64为例：

顶级页表对象是 PML4，负责管理整个虚拟地址空间的最高层。
PML4 中的条目指向 PDPT，每个条目管理 512 GiB 的虚拟地址空间。
PDPT 中的条目指向 PDE，每个条目管理 1 GiB 的虚拟地址空间。
PDE 中的条目指向 PTE，每个条目管理 2 MiB 的虚拟地址空间，或者通过 PTE 对应到具体的 4 KiB 页。

对于 ARMv8-A 架构，过程类似，只是使用了 PGD、PUD、PMD 等层次。

实操

本篇教程使用几个辅助函数去分配对象和能力。使用这几个函数可以帮助把所有的对象和能力槽分配都做了。

Map a page directory

教程运行时，可以看到以下的输出：
在这里插入图片描述
这是因为虽然提供的代码映射在seL4_PDPT对象中，但是缺少两个级别的分页结构。该值对应于libsel4常量SEL4_MAPPING_LOOKUP_NO_PD，它是由于缺少分页结构而无法解析的虚拟地址中的位数。
先看一下代码。

alloc_object这个方法在手册里面搜不到（说起来感觉好多在手册里都没搜到，应该是我找的不对，有知道的哥们可以说一声）其作用相当于将我们在 Untyped 章节中的查找操作和 seL4_Untyped_Retype 操作结合在一起，从 untyped 对象中申请一个特定类型的新对象。同时还会返回存储对应 cap 的 CSlot。
可以看到，代码中已经做了PDPT映射，根据上文，x86虚地址管理，从虚地址到物理地址是四层结构，因此需要我们自己实现PD和PT映射。
映射到PD结构中，需要使用seL4_X86_PageDirectory_Map这个方法。
在这里插入图片描述
代码如下：

error = seL4_X86_PageDirectory_Map(pd, seL4_CapInitThreadVSpace, TEST_VADDR, seL4_X86_Default_VMAttributes);

再次运行的结果如下：
在这里插入图片描述
缺少第四级表结构，所以我们需要映射PDE表。需要注意的是，上面的输出中失败位数已经从30变成了21：这是因为我们进行了PDPT表映射，因此少了的9位在此时能够从新的映射页文件夹中进行解析了。
下面映射PT结构，需要使用的方法是seL4_X86_PageTable_Map。
在这里插入图片描述
代码如下

//这几个映射方法的参数基本是一样的
error = seL4_X86_PageTable_Map(pt,seL4_CapInitThreadVSpace, TEST_VADDR, seL4_X86_Default_VMAttributes);

可以看到输出发生了变化。
在这里插入图片描述
这个页被成功映射且读到了0值，这是因为当从untyped中retype的时候，seL4会将所有的非设备页置零。然而之后想要尝试写这个页，从代码之中可以看到我们映射页的时候是只读的，所以这个操作未能成功且内核产生了一个VM错误。
因为初始任务没有错误处理器（在线程的教程中会有更多的这方面的信息），这会触发插槽0(nil)上的后续功能故障(cap故障)。因为教程下的内核跑在debug模式，所以内核会输出详细的错误信息。
vm错误是最有趣的，他展示了错误的地址，错误的状态寄存器，以及指令地址。就是下面那句话：

vm fault on data at address 0xa000000000 with status 0x7
in thread 0xffffff801fe08400 "rootserver" at address 0x401b39

Remap a page

通过赋予其seL4_ReadWrite权限重新映射这个页以修复该错误，使用seL4_X86_Page_Map这个函数：
在这里插入图片描述
代码如下：

//先接触映射，再重新映射
error = seL4_X86_Page_Unmap(frame);
assert(error == seL4_NoError);
error = seL4_X86_Page_Map(frame, seL4_CapInitThreadVSpace, TEST_VADDR, seL4_ReadWrite, seL4_X86_Default_VMAtt>
assert(error == seL4_NoError);