2. seL4-Capabilities

2023-09-11  本文已影响0人  Savior2016

这是seL4运行机制的第1篇。
截图中的代码和log不额外说明,都是指截图的最后一行

首先,我们从代码开始,这是最直观的东西。从程序中语言化的概念性的东西有点过于玄虚,汉化之后就更加铺所迷离的。

首先初始化capabilities并编译:

./init --tut capabilities
ninja

然后运行:

./simulate

最开始我们会看到下面的log:

原始输出.png
对照程序来看,首先我们看到了CNode里面slots的数量。
slot数量.png
对应到程序的下面一行:
slot数量对应的程序.png
然后是输出CNode的大小为0:
后续log.png
对应到程序的:
输出大小0对应的程序.png
这里需要计算CNode的大小。
CNode的结构.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); 

再次编译运行,就计算出大小了:


计算出CNode大小.png

我们再往下看log,它最后报了一个错误:


failed

对应的代码是这里:


code.png

为啥呢?
这明显他把一个capability复制到了first_free_slot:


first

然后又搞了一个last_slot,这里面根本没有任何capability:


last_slot

所以按照提示,我们把first_free_slot复制给他就行了:


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!");

再次编译运行,输出是:


log

对应下面的程序:


image.png

根据提示我们知道这里应该删除slot。
我们使用下面的函数删除:


image.png
seL4_CNode_Revoke(seL4_CapInitThreadCNode, seL4_CapInitThreadTCB, seL4_WordBits);

也可以用seL4_CNode_Delete,这个函数需要删除两次,seL4_CNode_Revoke可以把所有复制出capability都删除。

另外,seL4_CNode_Move函数在移动的源位置为空时就会出现seL4_FailedLookup错误。

编译运行,结果如下:


image.png

这次又报错没有挂起线程了。
对应下面的代码:


image.png

使用seL4_TCB_Suspend函数挂起:

image.png
seL4_TCB_Suspend(seL4_CapInitThreadTCB);

再次编译运行:


done
上一篇下一篇

猜你喜欢

热点阅读