# seL4内核参考手册

**Repository Path**: logzig/sel4_reference_manual

## Basic Information

- **Project Name**: seL4内核参考手册
- **Description**: seL4内核参考手册中文翻译
- **Primary Language**: 其他
- **License**: GPL-2.0
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 28
- **Created**: 2021-09-29
- **Last Updated**: 2024-05-29

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

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

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内核参考手册》](./sel4.0.9.pdf)

### 翻译工具

[有道翻译](http://fanyi.youdao.com/)。有时其翻译的相当准确顺畅，特此致谢！

### [原文重要信息](./README1.md)