seL4微内核入门-代码下载运行及资料
原创 thatway 那路谈OS与SoC嵌入式软件 2022-09-27 07:30
不废话，老一套：
编译环境
准备，代码下载
，代码编译
，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-get update
sudo 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 setuptools
pip3 install--user sel4-deps
# Currently we duplicate dependencies for python2 and python3 as a python3 upgrade is in process
pip install--user setuptools
pip 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 aenum
pip 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 代码编译
cd hello-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 -
为教程生成的自述文件。
int main(int argc, char *argv[]) {
printf("Hello, World!\n");
printf("Second hello\n");
return 0;
}
如果修改了应用的源码，重新运行重建项目
:
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
后记：
本文中搭环境的部分比较多，
可以加我微信thatway1989
，备注进群
。然后拉你进本公众号的交流群
：OS与AUTOSAR研究-交流群，可以讨论搭环境、汽车软件、操作系统软件等知识，一起学习。
最近回想下我学技术的过程，
如下：
“啥都懂一点
，啥都不精通
，
干啥都能干
，干啥啥不是
，
专业入门劝退
，堪称程序员杂家
”。
后续会继续更新，
纯干货
分析，无广告，不打赏，欢迎
转载
，欢迎
评论交流
！