当前位置: 首页 > 工具软件 > seL4 > 使用案例 >

seL4微内核学习之二:seL4中的一些基础概念

戚修雅
2023-12-01

作为微内核操作系统,seL4只提供很少的基础内核服务,复杂的服务将在用户态基于这些基础内核服务实现。

  1. Threads:是运行CPU的抽象。
  2. Address spaces:是分配给应用程序的虚拟地址空间,应用程序被限制只能访问其自己的空间。
  3. Inter-process communication (IPC):通过Endpoint实现的进程间的通信方法。
  4. Device primitives:允许设备驱动实现在用户态。内核通过IPC来实现中断。
  5. Capability spaces:存储对内核对象的Capability(也就是一些访问权限),和一些对象信息。

内核对象有以下6个:

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