seL4微内核入门-代码下载运行及资料

不废话，老一套：**编译环境**准备，代码**下载**，代码**编译**，qemu代码**运行**。本文介绍的内容都是好东西，提供全方位的微内核入门指导，就看毅力怎么样了，就像那句话：**笨鸟先飞**。

1. sel4简介

sel4是**微内核**操作系统，号称世界上**最安全**，**最高效**的微内核。提供**非posix**兼容的编程接口，它只提供了少量的服务，创建和管理虚拟地址空间、线程以及进程间通信(IPC)。亮点是**capability机制**，管理每个进程所拥有的资源。这个机制的引入也导致了sel4较**难理解**和应用**开发**。关于微内核的介绍参考上一篇：

seL4微内核入门-微内核介绍

thatway，公众号：OS与AUTOSAR研究seL4微内核入门-微内核介绍

2. Turorial练习

从官网提供的学习教程hello world开始练习，

https://docs.sel4.systems/Tutorials/hello-world.html

2.1 环境准备

这里同样，采用的开发方式为VitrualBox+Ubuntu，下载VitrualBox和Ubuntu镜像（版本>=20.04），安装虚拟机，具体不再描述。sel4开发环境搭建：参考https://docs.sel4.systems/projects/buildsystem/host-dependencies.html，

环境搭建是否正常，以能运行第一个hello world工程为准，详细步骤为:

1）repo工具安装

mkdir ~/bin PATH=~/bin:$PATH curl https://storage.googleapis.com/git-repo-downloads/repo > ~/bin/repo chmod a+x ~/bin/repo

2）lib依赖库和编译工具安装

#The basic build package on Ubuntu is the build-essential package. To install run:sudo apt-getupdatesudo apt-get install build-essential#Additional base dependencies for building seL4 projects on Ubuntu include installing:sudo apt-get install cmake ccache ninja-build cmake-curses-gui sudo apt-get install libxml2-utils ncurses-dev sudo apt-get install curl git doxygen device-tree-compiler sudo apt-get install u-boot-tools sudo apt-get install python3-dev python3-pip python-is-python3 sudo apt-get install protobuf-compiler python3-protobuf sudo apt-get install qemu-system-arm qemu-system-x86 qemu-system-misc sudo apt-get install gcc-arm-linux-gnueabi g++-arm-linux-gnueabi sudo apt-get install gcc-aarch64-linux-gnu g++-aarch64-linux-gnu

3）Python 依赖库

pip3 install--user setuptoolspip3 install--user sel4-deps# Currently we duplicate dependencies for python2 and python3 as a python3 upgrade is in processpip install--user setuptoolspip install--user sel4-deps

4） 编译库依赖

sudo apt-get install clang gdb sudo apt-get install libssl-dev libclang-dev libcunit1-dev libsqlite3-dev sudo apt-get install qemu-kvm

5）证明依赖

sudo apt-get install\ python3 python3-pip python3-dev \ gcc-arm-none-eabi build-essential libxml2-utils ccache \ ncurses-dev librsvg2-bin device-tree-compiler cmake \ ninja-build curl zlib1g-dev texlive-fonts-recommended \ texlive-latex-extra texlive-metapost texlive-bibtex-extra \ mlton-compiler haskell-stack

2.2下载代码

下载代码前安装python依赖用于编译教程

pip install--user aenumpip install--user pyelftools

下载代码前配置repo邮箱信息

git config --global user.email "you@example.com" git config --global user.name "Your Name"

下载代码（这里使用sel4官方的代码进行练习，从github上下载）‍

mkdir sel4-tutorials-manifest cd sel4-tutorials-manifest repo init -u https://github.com/seL4/sel4-tutorials-manifest repo sync

2.3 Hello World****应用生成

初始化hello-world文件夹‍

./init --tut hello-world --solution

hello-world是示例名字，练习其他示例更换这个名字就可以，命令加–solution后缀，可以补全代码。可以看到生成了下面的hello-world文件夹，里面有c代码。

2.4 代码编译

cdhello-world_build ninja

编译成功后显示：

2.5 代码运行

# In build directory, hello-world_build ./simulate

成功后显示：

运行后Ctrl-A, X退出qemu模拟工具。

3. Hello World代码分析

编译的时候，我们使用了**ninja**这个命令，Ninja 是**Google**的一名程序员推出的注重速度的构建工具，一般在Unix/Linux上的程序通过make/makefile来构建编译，而Ninja通过将编译任务并行组织，大大提高了构建速度。

可见ninja跟makefile同级别的都是构建工具，生成编译器使用的规则。

在sel4-tutorials-manifest/hello-world_build/build.ninja文件中可以看到

执行ninja命令就会通过这个build.ninja进行编译，会找到hello-world的代码

cmake是makefile之上的一层封装。

CMakeLists.txt – cmake使用的脚本，将根任务合并到更广泛的 seL4 构建系统中的文件。

src/main.c - 初始任务的单个源文件。

hello-world.md - 为教程生成的自述文件。

intmain(intargc,char*argv[]){printf("Hello, World!\n");printf("Second hello\n");return0;}

如果修改了应用的源码，重新运行重建项目:

Bash # In build directory, hello-world_build ninja

然后再运行simulator:

# In build directory, hello-world_build./simulate

4. 学习资料

sel4原理熟悉，主要从两条路进行学习：

一边是sel4的参考手册：

https://gitee.com/18855162320/sel4_reference_manual/blob/master/sel4.0.9.pdf，

另一边就是基于Tutorials教程开始一步一步的做实验，这样可以做到理论和实践结合。（turorials中camkes相关的例子可以先不学习）

辅助库介绍：

tutorials工程中，其他辅助库的介绍，除了sel4微内核之外，还需要提供一些库，才能让你的应用程序运行起来。

sel4内核：首先是sel4内核。单单的一个内核运行起来，是没法运行一个例如hello world这样的程序的，因为这个程序需要链接其他的库，比如stdio中的printf，而且该程序和内核交互，就需要知道内核提供的标准API有哪些。

libsel4：sel4内核提供的api都用内核源码工程里面的libsel4这个库来描述。里面是sel4内核支持的标准api。

sel4_libs：当一个程序连接了这个libsel4之后，就可以使用sel4内核的标准api了，这个和Linux内核提供的标准api类似，是和操作系统密切关联的。非posix标准的。另外这个libsel4库不是很好用，因此在这之上又堆叠了一个sel4_libs库，这个库是对sel4标准api的进一步功能性的封装，比如分配一个cap对象，调用者无需知道更下层的sel4标准api调用的细节。

musllibc：这个是开源的一个libc库，和sel4是没有直接关系的。用到这个工程里面来，主要是提供标准的符合posix标准的api，其他的操作系统也是可以使用的。因此应用程序可以直接使用libsel4中的函数，也可以使用sel4_libs中的函数，比较标准的功能就可以使用muscllibc中的功能了。为了打通muslibc和sel4_libs，sel4_libs中提供了一个libsel4muslcsys这样的一个库，muslibc中的一些功能通过sys call的方式调用到libsel4muslcsys这个接口库中，这个接口库就会调用sel4_libs中的相应函数。当然muslibc中的有些函数可能会直接调用libsel4的函数接口（目前还没有看到muslibc中或者libsel4中有对这两个库的对接口的实现，可能这个猜测不对）

sel4runtime：一般程序里面都有一个main函数，作为该程序的入口位置，但是，这个程序的运行并不是从main开始的，在运行main之前，其实还做了其他的一些工作，比如堆栈指针的设置，环境变量的获取，其他的一些准备工作等等。一般编译器，比如gcc编译器编译一个比如hello world这样的一个代码的时候，会指定该程序的入口地址是 _start, 就是会找寻源码，把 _start开始的代码放在该程序代码段的最开始位置，hello_world.c源码中并没有 _start这个函数或者标号，所以这个标号是其他地方的，且是会被hello_world.c链接进来的源码，在sel4 tutorial工程里，我们用sel4runtime（里面是源码）和lshello_world.c一起编译，链接。这个sel4runtime工程里面提供了各个架构的 _start入口标号，该标号紧跟着的是该架构的一些汇编语言，处理堆栈等等，之后跳转到一个简单的c函数处，该c函数收集环境变量，传入参数等，并最终调用main函数。

其他资料：

seL4内核启动分析：

https://www.jianshu.com/p/f741d26de6c4

CSDN中sel4教程：

https://blog.csdn.net/Mr0cheng/article/details/104352613

sel4源码注释：

https://gitee.com/laokz/sel4-comment/tree/abc/src

“啥都懂一点，啥都不精通，

干啥都能干，干啥啥不是，

专业入门劝退，堪称程序员杂家”。

后续会继续更新，纯干货分析，无广告，不打赏，欢迎转载，欢迎评论交流！

“那路谈OS与SoC嵌入式软件”，欢迎关注！

个人文章汇总：https://thatway1989.github.io