CSP 大作业选题 – 微内核

当前开源的主流微内核包括seL4，Fiasco.OC，Zircon。微内核的设计哲学在这些经典系统里有体现、有改变、有发展。本作业要求大家学习在微内核上进行编程，或者阅读理解不同微内核的部分代码（不要担心~微内核代码量本身就小~），从而能够真正地体会微内核的设计原理。具体来说，完成该作业包括如下步骤：

1. （选做题）完成seL4 tutorial 中的：
   • Hello, World!
   • Dynamic Libraries 1,2,3,4
   • Capabilities
   • Untyped
   • Mapping
   • Threads
   • IPC
   • Notifications
   • Interrupts
   • Faults
   该步骤需要大家进行编程，每个小练习都会覆盖到微内核设计中一个具体技术点，每个练习的代码量通常小于20LoC。请大家按照如下链接（建议选择x86架构）完成该练习。https://docs.sel4.systems/Tutorials/
2. 根据上述编程小练习或者根据参考资料-1/3，请具体分析seL4中的内存管理设计（结合Capability、Untyped、Mapping、Threads、IPC、Faults，在分析中需要解释这些抽象在内存管理中作用）。
3. 请结合代码和相关文档列出seL4、Fiasco.OC，Zircon三种微内核的提供的用户态系统服务，支持哪些Linux上的系统调用，进而分析其对于Linux上常见应用的支持能力。
4. 在seL4、Zircon两种微内核上分别测量IPC的性能（都使用x86架构模拟器）。要求线程/进程A利用IPC调用线程/进程B的一个空函数，在A中测量IPC从发出到返回的时间。请分别列出IPC时延并且结合IPC实现逻辑解释其中差异。

参考资料：

1. https://docs.sel4.systems/
2. 环境编译：https://docs.sel4.systems/Docker.html
3. https://www.cse.unsw.edu.au/~cs9242/19/lectures.shtml
4. https://os.inf.tu-dresden.de/fiasco/
5. 环境编译：https://l4re.org/fiasco/build.html
6. https://fuchsia.dev/fuchsia-src/concepts/kernel

参考文献：

1. M3: A Hardware/Operating-System Co-Design to Tame Heterogeneous Manycores (ASPLOS 16)
2. M³x: Autonomous Accelerators via Context-Enabled Fast-Path Communication (ATC 19)
3. SemperOS: A Distributed Capability System (ATC 19)
4. seL4: formal verification of an OS kernel (sosp 09)