作为微内核操作系统,seL4只提供很少的基础内核服务,复杂的服务将在用户态基于这些基础内核服务实现。
- Threads:是运行CPU的抽象。
- Address spaces:是分配给应用程序的虚拟地址空间,应用程序被限制只能访问其自己的空间。
- Inter-process communication (IPC):通过Endpoint实现的进程间的通信方法。
- Device primitives:允许设备驱动实现在用户态。内核通过IPC来实现中断。
- Capability spaces:存储对内核对象的Capability(也就是一些访问权限),和一些对象信息。
内核对象有以下6个:
- Cnodes:存储权能信息,决定了一个线程的调用特定对象方法的权限。每个Cnode的slot的数量是一定的(2的幂次),并且该数量是在创建该Cnode时确定的。每个slot可以为空。
- Thread Control Block(TCB):代表一个正在运行的进程,是调度,阻塞等操作的最小单元。
- IPC Endpoint:用来辅助进程间IPC,有两种类型的IPC Endpoint,一种是Synchronous Endpoint,另一种是Asynchronous Endpoint,顾名思义,一种是同步的,即在信息没有被接受时会阻塞发送消息的线程,另一种是异步的,只能传递短消息,但不会发生阻塞。
- Virtual Address Space Object:为线程构建VSpace(Virtual Address Space),对应着各种硬件信息。比如,页目录指向页表,而页表项又指向物理的帧(frame)。内核也有ASID Pool 和 ASID Control objects来查看地址空间的状态。
- Interrupt Object:用来接收和确认来自硬件的中断。在Initial Thread中有一个IRQControl的Capability,来创建IRQHandler Capability。IRQHandler Capability通常被授给device dirver来 access中断的来源。一个IRQHandler Capability管理一个特定设备的特定中断来源。例如,一个IRQHandler Capability管理键盘的一个字母的读入。
- Untyped Memory:是内存分配的基础。Untyped Memory只有一个方法(retype),来创建新的内核对象,成功即向调用函数新建对象的Capability。另外,Untyped Memory还可以划分为一组更小的Untyped Memory,实现将系统内存划分为小块来管理。