不废话老一套**编译环境**准备代码**下载**代码**编译**qemu代码**运行**。本文介绍的内容都是好东西提供全方位的微内核入门指导就看毅力怎么样了就像那句话**笨鸟先飞**。1. sel4简介sel4是**微内核**操作系统号称世界上**最安全****最高效**的微内核。提供**非posix**兼容的编程接口它只提供了少量的服务创建和管理虚拟地址空间、线程以及进程间通信(IPC)。亮点是**capability机制**管理每个进程所拥有的资源。这个机制的引入也导致了sel4较**难理解**和应用**开发**。关于微内核的介绍参考上一篇seL4微内核入门-微内核介绍thatway公众号OS与AUTOSAR研究seL4微内核入门-微内核介绍2. Turorial练习从官网提供的学习教程hello world开始练习https://docs.sel4.systems/Tutorials/hello-world.html2.1 环境准备这里同样采用的开发方式为VitrualBoxUbuntu下载VitrualBox和Ubuntu镜像版本20.04安装虚拟机具体不再描述。sel4开发环境搭建参考https://docs.sel4.systems/projects/buildsystem/host-dependencies.html环境搭建是否正常以能运行第一个hello world工程为准详细步骤为:1repo工具安装mkdir ~/bin PATH~/bin:$PATH curl https://storage.googleapis.com/git-repo-downloads/repo ~/bin/repo chmod ax ~/bin/repo2lib依赖库和编译工具安装#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-gnu3Python 依赖库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-deps4 编译库依赖sudo apt-get install clang gdb sudo apt-get install libssl-dev libclang-dev libcunit1-dev libsqlite3-dev sudo apt-get install qemu-kvm5证明依赖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-stack2.2下载代码下载代码前安装python依赖用于编译教程pip install--user aenumpip install--user pyelftools下载代码前配置repo邮箱信息git config --global user.email youexample.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 sync2.3 Hello World****应用生成初始化hello-world文件夹‍./init --tut hello-world --solutionhello-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./simulate4. 学习资料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有哪些。libsel4sel4内核提供的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_libssel4_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/f741d26de6c4CSDN中sel4教程https://blog.csdn.net/Mr0cheng/article/details/104352613sel4源码注释https://gitee.com/laokz/sel4-comment/tree/abc/src“啥都懂一点啥都不精通干啥都能干干啥啥不是专业入门劝退堪称程序员杂家”。后续会继续更新纯干货分析无广告不打赏欢迎转载欢迎评论交流“那路谈OS与SoC嵌入式软件”欢迎关注个人文章汇总https://thatway1989.github.io