seL4内核参考手册中文翻译，主要依据的是版本11.0.0（2019年11月20日），并根据内核源码树适时进行了更新（见changelog）。

seL4是操作系统家族中独树一帜的代表，其安全性和形式化验证特点在世界范围内享有口碑。而作为微内核，万把行的代码量无疑对OS学习和研究者都是一个比较轻松的选择。译者这里所做也正是在学习研究基础上的一个小结式的尝试，即通过翻译参考手册，进一步加深认识和理解。

这里发布出来，既是有获取认可共鸣的意思，也是对学人之长回馈少许的实践，正所谓开源贡献吧。为了使阅读者能有所收获，特别是为防止误人子弟，译文在对照源码的基础上认真进行了校正修订，并尽可能对一些费解或过于简略甚至错误的描述作一解释，希望带来有益效果。文字语言谈不上优美精炼，但尽力确保了清楚准确。文档中所有尾注均为译者所加，查了一下有80多条，算是搬运力气活之外的脑力创造吧:)

受视野所限，ARM架构未做认真推敲。欢迎感兴趣者将这里Gitee的Issue页面作为探讨平台，当然更欢迎对译文直接贡献知识。

术语说明

seL4的一个显著特点是使用了一套能力系统来控制各种资源的访问。这个能力是一种内核数据结构，表示特定的资源和操控权限。用户空间的访问，首先要提供或者说引用对应该资源的能力，比如，映射一页物理内存，调用者至少要提供指代该物理页的能力，还要提供要映射到的地址空间能力，等等。

这里列出一些易混淆或对大多数人比较陌生的术语，以及在翻译时所作的选择。

• Capability 能力，如前所述。

• CSlot 存储能力的位置，直译能力插槽，实际就是能力的数据存储表现，因此本质上CSlot和能力是一回事，只不过一个是左值，一个是右值(这里忽略CSlot中表示能力间链接关系部分)。在译文里，多数使用英文slot字眼，偶尔为了顺口使用汉字槽，相反CSlot字眼几乎未使用。

• CNode 能力节点，内核数据结构是CSlot数组，表示逻辑上一组的能力，比如，一个线程的所有能力。因为CNode本身也是一种资源，所以内核中有专门指代CNode的能力，也同样要占用一个CSlot。正因如此，有时候也将CNode译成xx能力，特别是根CNode(见下条)。这与常规数组属性是一致的，如：int a[2]; a[1]是个int，a是int指针，*a同a[0]一个含义。

• CSpace 能力空间，是CNode的逻辑集合，指一个线程所能控制的各级各类能力的集合。内核中并没有CSpace数据结构，其是由逻辑上关联的若干CNode体现。比如，一个线程可以生成子线程，这样它本身的CNode与子线程的CNode就构成了一个CSpace。表示CSpace开始的第一个CNode，称为根CNode（root CNode)，它是查找、引用、定位具体能力的基本出发点。

• CPTR与index、depth 这不是术语，而是seL4查找定位能力时的索引指示或“指针”。因其经常出现且不同寻常含义，所以这里也作一解释。译者将CPTR称为句柄，因为它不是我们通常理解的表示一个具体地址的指针，也不是一个简单的CNode数组索引，而是由CPTR值的各个位值、参照一个根CNode、按一定规则计算出来的能力指示，也即用所谓的index“索引”和depth“深度”来辅助计算。基本所有的能力都是要靠句柄来引用。

• VSpace 地址空间，与我们通常理解的虚拟地址空间含义是一致的，但需注意的是它也是一个能力，内核中是用一级(顶级)页表能力来表示。

请注意：以上所有单词都有可能被称为能力！！

• sporadic thread 狭义上是“零星线程”、“偶发线程”的意思，但本文这个线程模型既可以实现偶发的零星线程，也可以实现周期性线程，开发团队的有关论文阐述了理论设计。为避免歧义，查阅了一些国内资料，包括知网和学府教材，暂未得到理想译文，因此这里保留英文不动。

电子书

你可以自己生成，也可以参阅这里比较粗糙的pdf。

《seL4内核参考手册》

翻译工具

有道翻译。有时其翻译的相当准确顺畅，特此致谢！

原文重要信息