seL4的内存管理

在seL4中，除了少量静态内存属于内核，所有的物理内存都由用户态管理。在root task开始运行的时候就已经获取了所有seL4启动时候创建的object相应的capability，还有那些未被使用的物理资源。

untyped memory的概念

除了用于创建root task的object，所有未被使用的物理内存都叫untyped memory，相应的capability都统称为untyped memory capability。untyped memory是一块制定大小的连续物理内存。

untyped object（untyped memory）有一个boolean属性叫device，说明内存对于内核是否可写。如果内存有device属性，那么它就不被RAM支持，只能被一些其他设备支持。device untyped object只能被retype成frame object（physical memory frames，可被映射到虚拟内存）。

在seL4_BootInfo的结构体中有从untyped.start到untyped.end的所有untyped memory对应的capability，而且有一个untyped list保存着这些内存的物理地址，大小和device属性。

retype

只要untyped capability对应的memory大小允许，memory可以被拆分成许多新的object。使用seL4_Untyped_Retype函数对untyped capability进行创建新的capability（同时也是会对应的untyped object进行retype）。新的capability是原来untyped capability的children，children按顺序获得有效内存，且内存是对齐的。例如，创建4k object以后创建16k object，这样有12k就被浪费了。

seL4_Untyped_Retype(parent_untyped, seL4_UntypedObject, untyped_size_bits, seL4_CapInitThreadCNode, 0, 0, child_untyped, 1);

这个函数中的参数：

• parent_untyped是可用内存的capability。

• seL4_UntypedObject是重新定义后的object类型。

• untyped_size_bits是object的大小，如果不是seL4_UntypedObject，那么大小是固定的，可以直接输入0。

• 紧接着三个参数是root，node_index和node_depth用于指明新的capability所在的CNode，这里是root是seL4_CapInitThreadCNode且node_depth是0，指在CSpace root中遍历深度为seL4_WordBits，node_index会被忽略；如果node_depth不为0，那么node_index不会被忽略，而此时是一个多层CSpace。child_untyped是新的capability，注意这个函数不是用来分配新的capability，而是从untyped中分配出新的object并和新的capability关联起来。

• 最后一个参数是数量，填写数量时必须考虑两个点：原来的untyped memory必须足够大，CNode中必须有足够的CSlot去放capability。

用seL4_CNode_Revoke可用回退掉retype操作。