這是seL4運(yùn)行機(jī)制的第1篇。
截圖中的代碼和log不額外說明，都是指截圖的最后一行
首先，我們從代碼開始，這是最直觀的東西。從程序中語言化的概念性的東西有點(diǎn)過于玄虛，漢化之后就更加鋪所迷離的。
首先初始化capabilities并編譯：
./init --tut capabilities
ninja
然后運(yùn)行：
./simulate
最開始我們會看到下面的log：
原始輸出.png
對照程序來看，首先我們看到了CNode里面slots的數(shù)量。
slot數(shù)量.png
對應(yīng)到程序的下面一行：
slot數(shù)量對應(yīng)的程序.png
然后是輸出CNode的大小為0：
后續(xù)log.png
對應(yīng)到程序的：
輸出大小0對應(yīng)的程序.png
這里需要計算CNode的大小。
CNode的結(jié)構(gòu).png
CNode里面包含的是capability，每個capability所在的位置叫一個slot。
所以我們計算CNode的大小也就是計算這些slot占了多少空間，slot的大小是用
seL4_SlotBits定義的（為了平臺的兼容性），所以計算方法如下：
CNode大小的計算.png
size_t initial_cnode_object_size_bytes = initial_cnode_object_size * (1u << seL4_SlotBits);
再次編譯運(yùn)行，就計算出大小了：
計算出CNode大小.png
我們再往下看log，它最后報了一個錯誤：
failed
對應(yīng)的代碼是這里：
code.png
為啥呢？
這明顯他把一個capability復(fù)制到了first_free_slot：
first
然后又搞了一個last_slot,這里面根本沒有任何capability：
last_slot
所以按照提示，我們把first_free_slot復(fù)制給他就行了：
copy
error = seL4_CNode_Copy(seL4_CapInitThreadCNode, last_slot, seL4_WordBits,
seL4_CapInitThreadCNode, first_free_slot, seL4_WordBits,
seL4_AllRights);
ZF_LOGF_IF(error, "Failed to copy cap!");
再次編譯運(yùn)行，輸出是：
log
對應(yīng)下面的程序:
image.png
根據(jù)提示我們知道這里應(yīng)該刪除slot。
我們使用下面的函數(shù)刪除：
image.png
seL4_CNode_Revoke(seL4_CapInitThreadCNode, seL4_CapInitThreadTCB, seL4_WordBits);
也可以用seL4_CNode_Delete,這個函數(shù)需要刪除兩次，seL4_CNode_Revoke可以把所有復(fù)制出capability都刪除。
另外，seL4_CNode_Move函數(shù)在移動的源位置為空時就會出現(xiàn)seL4_FailedLookup錯誤。
編譯運(yùn)行，結(jié)果如下：
image.png
這次又報錯沒有掛起線程了。
對應(yīng)下面的代碼：
image.png
使用seL4_TCB_Suspend函數(shù)掛起：
image.png
seL4_TCB_Suspend(seL4_CapInitThreadTCB);
再次編譯運(yùn)行:
done
