seL4 实验环境

1 前期准备: Tools

在正式进行项目的 下载/编译/开发/测试 之前，需要准备好系统环境，安装一些依赖软件和基本的配置。比较快速的方式是使用 Docker 部署实验环境，使用官方提供的 docker ，在本地出构建隔离的实验环境，一步到位。或用我接下来使用手动安装配置环境，参考官方文档 System configuration and building

下列安装步骤适用于 Ubuntu 22.04，如果是其他的系统版本可参考官方文档 Host Dependencies

1.1 repo 工具(必选)

首先安装 repo 工具，参考 android 官方文档 安装 repo，另外为尽可能避免网络下载问题，我使用清华大学开源镜像站

hinzer@dev:~/source$ mkdir ~/bin

hinzer@dev:~/source$ curl https://mirrors.tuna.tsinghua.edu.cn/git/git-repo -o ~/bin/repo
hinzer@dev:~/source$ chmod a+x ~/bin/repo

hinzer@dev:~/source$ echo 'export PATH=$PATH:~/bin' >> ~/.bashrc 
hinzer@dev:~/source$ echo 'export REPO_URL="https://mirrors.tuna.tsinghua.edu.cn/git/git-repo/"' >> ~/.bashrc
hinzer@dev:~/source$ source ~/.bashrc

repo 是一个用 python 实现的工具，基于 git 的版本管理，更多介绍 [[git 和 repo]]

1.2 seL4 基础依赖(必选)

hinzer@dev:~/source$ sudo apt-get update
hinzer@dev:~/source$ sudo apt-get install build-essential
hinzer@dev:~/source$ sudo apt-get install cmake ccache ninja-build cmake-curses-gui
hinzer@dev:~/source$ sudo apt-get install libxml2-utils ncurses-dev
hinzer@dev:~/source$ sudo apt-get install curl git doxygen device-tree-compiler
hinzer@dev:~/source$ sudo apt-get install u-boot-tools
hinzer@dev:~/source$ sudo apt-get install python3-dev python3-pip python-is-python3
hinzer@dev:~/source$ sudo apt-get install protobuf-compiler python3-protobuf

# Simulating with QEMU
hinzer@dev:~/source$ sudo apt-get install qemu-system-arm qemu-system-x86 qemu-system-misc

# Cross-compiling for ARM targets
hinzer@dev:~/source$ sudo apt-get install gcc-arm-linux-gnueabi g++-arm-linux-gnueabi
hinzer@dev:~/source$ sudo apt-get install gcc-aarch64-linux-gnu g++-aarch64-linux-gnu

# Cross-compiling for RISC-V targets
N/A

1.3 Python 基础依赖(必选)

hinzer@dev:~/source$ pip3 install--user setuptools
hinzer@dev:~/source$ pip3 install--user sel4-deps
# Currently we duplicate  dependencies for python2 and python3 as a python3 upgrade is in process
hinzer@dev:~/source$ pip install--user setuptools
hinzer@dev:~/source$ pip install--user sel4-deps

1.4 CAmkES 构建依赖(可选)

# Python Dependencies
hinzer@dev:~/source$ pip3 install --user camkes-deps
hinzer@dev:~/source$ pip install --user camkes-deps

# Haskell Dependencies
hinzer@dev:~/source$ curl -sSL https://get.haskellstack.org/ | sh
hinzer@dev:~/source$ sudo apt-get install haskell-stack

# Build Dependencies
hinzer@dev:~/source$ sudo apt-get install clang gdb
hinzer@dev:~/source$ sudo apt-get install libssl-dev libclang-dev libcunit1-dev libsqlite3-dev
hinzer@dev:~/source$ sudo apt-get install qemu-kvm

1.5 Proof 证明依赖(可选)

# Proof Dependencies
hinzer@dev:~/source$ 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

## The build system for the seL4 kernel requires several python packages:
hinzer@dev:~/source$ pip3 install --user --upgrade pip
hinzer@dev:~/source$ pip3 install --user sel4-deps

## Haskell Stack
hinzer@dev:~/source$ stack upgrade --binary-only
hinzer@dev:~/source$ which stack # should be $HOME/.local/bin/stack

# Isabelle Setup
N/A

2 构建项目: seL4test(可选)

2.1 使用 repo 检出 seL4test

hinzer@dev:~/source$ mkdir seL4test
hinzer@dev:~/source$ cd seL4test
hinzer@dev:~/source/seL4test$ repo init -u https://github.com/seL4/sel4test-manifest.git
hinzer@dev:~/source/seL4test$ repo sync

2.2 配置 x86_64 构建目录

hinzer@dev:~/source/seL4test$ mkdir build-x86
hinzer@dev:~/source/seL4test$ cd build-x86
hinzer@dev:~/source/seL4test/build-x86$ ../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE
hinzer@dev:~/source/seL4test/build-x86$ ninja

2.3 运行 QEMU 模拟器

hinzer@dev:~/source/seL4test/build-x86$ ./simulate

Test VSPACE0002 passed
....
All is well in the universe

3 运行程序: “hello, world!”

运行一个简单的用户级程序，在 seL4 系统上喊出一句 “hello, world!”，也同时验证之前配置的环境可用。参考项目下的 README.md 文件，或者参考官方文档 Hello, World!

3.1 安装依赖

hinzer@dev:~/source$ pip install --user aenum
hinzer@dev:~/source$ pip install --user pyelftools

3.2 获取源码

hinzer@dev:~/source$ mkdir sel4-tutorials-manifest
hinzer@dev:~/source$ cd sel4-tutorials-manifest
hinzer@dev:~/source/sel4-tutorials-manifest$ repo init -u https://github.com/seL4/sel4-tutorials-manifest
hinzer@dev:~/source/sel4-tutorials-manifest$ repo sync

3.3 使用方式

hinzer@dev:~/source/sel4-tutorials-manifest$ ./init --tut hello-world --solution

hinzer@dev:~/source/sel4-tutorials-manifest$ cd hello-world_build

hinzer@dev:~/source/sel4-tutorials-manifest/hello-world_build$ ninja

# In build directory, hello-world_build
hinzer@dev:~/source/sel4-tutorials-manifest/hello-world_build$ ./simulate

按键 Ctrl-A, X 退出 qemu 模拟环境

3.4 源码解析

来到 hello-world 模块的源码视角，hello-world.md 是为用户制作的描述文件，查看模块的说明信息。CMakeLists.txt 是用于将当前 hello-world 模块加入构建系统的配置文件，通过 cmake 将源文件导入构建系统。最终将源文件 main.c 构建成平台可执行的用户程序。

hinzer@dev:~/source/sel4-tutorials-manifest/hello-world$ tree
.
├── CMakeLists.txt # cmake 使用的脚本文件
├── hello-world.md # 描述文件
└── src
    └── main.c # 源文件

1 directory, 3 files

hinzer@dev:~/source/sel4-tutorials-manifest/hello-world$ cat ./src/main.c

include <stdio.h>

int main(int argc, char *argv[]) {
    printf("Hello, World!\n"); // 输出 "Hello, World!\n" 

    printf("Second hello\n");
    return 0;
}

4 References

1. The seL4® Microkernel