seL4的內(nèi)存管理
在seL4中，除了少量靜態(tài)內(nèi)存屬于內(nèi)核，所有的物理內(nèi)存都由用戶態(tài)管理旁赊。在root task開始運(yùn)行的時候就已經(jīng)獲取了所有seL4啟動時候創(chuàng)建的object相應(yīng)的capability，還有那些未被使用的物理資源。
untyped memory的概念
除了用于創(chuàng)建root task的object宾毒，所有未被使用的物理內(nèi)存都叫untyped memory，相應(yīng)的capability都統(tǒng)稱為untyped memory capability殿遂。untyped memory是一塊制定大小的連續(xù)物理內(nèi)存诈铛。
untyped object（untyped memory）有一個boolean屬性叫device，說明內(nèi)存對于內(nèi)核是否可寫墨礁。如果內(nèi)存有device屬性幢竹，那么它就不被RAM支持，只能被一些其他設(shè)備支持恩静。device untyped object只能被retype成frame object（physical memory frames焕毫，可被映射到虛擬內(nèi)存）。
在seL4_BootInfo的結(jié)構(gòu)體中有從untyped.start到untyped.end的所有untyped memory對應(yīng)的capability驶乾，而且有一個untyped list保存著這些內(nèi)存的物理地址邑飒，大小和device屬性。
retype
只要untyped capability對應(yīng)的memory大小允許轻掩，memory可以被拆分成許多新的object幸乒。使用seL4_Untyped_Retype函數(shù)對untyped capability進(jìn)行創(chuàng)建新的capability（同時也是會對應(yīng)的untyped object進(jìn)行retype）。新的capability是原來untyped capability的children唇牧，children按順序獲得有效內(nèi)存罕扎，且內(nèi)存是對齊的。例如丐重，創(chuàng)建4k object以后創(chuàng)建16k object腔召，這樣有12k就被浪費(fèi)了。
seL4_Untyped_Retype(parent_untyped, seL4_UntypedObject, untyped_size_bits, seL4_CapInitThreadCNode, 0, 0, child_untyped, 1);
這個函數(shù)中的參數(shù)：
parent_untyped是可用內(nèi)存的capability扮惦。
seL4_UntypedObject是重新定義后的object類型臀蛛。
untyped_size_bits是object的大小，如果不是seL4_UntypedObject崖蜜，那么大小是固定的浊仆，可以直接輸入0。
緊接著三個參數(shù)是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郊尝，注意這個函數(shù)不是用來分配新的capability，而是從untyped中分配出新的object并和新的capability關(guān)聯(lián)起來战惊。
最后一個參數(shù)是數(shù)量流昏，填寫數(shù)量時必須考慮兩個點(diǎn)：原來的untyped memory必須足夠大，CNode中必須有足夠的CSlot去放capability样傍。
用seL4_CNode_Revoke可用回退掉retype操作横缔。
