seL4的编译和运行

seL4指定了可以运行的平台，按照下面的匹配来编译它。

从github上clone到工程后，执行如下：

如果遇到cc1: all warnings being treated as errors，在Makefile中找到CFLAGS，加上-Wno-unused-but-set-variable：

如果编译成功，应该是下面的结果：

看看都生成了哪些文件：

Fig 1 make之前目录结构

Fig 2 make之后目录结构

Fig 1是没有make的目录，Fig 2是make之后的目录。多出了：

• 目录api
• 目录arch
• 目录plat
• kernel_all.c
• kernel_all.c_pp
• kernel.elf
• kernel.elf.strip
• kernel_final.c
• kernel_final.s

• kernel.o

  其中kernel.elf包含所有seL4内核的调试信息，我们要用QEMU来执行这个elf格式的镜像。下面是qemu支持的平台：
  

我们需要为镜像选择正确的qemu运行的平台，运行命令：

这里没有适合seL4运行的平台，似乎seL4没有在QEMU中启动和运行。

另外在seL4官方文档中，指出下列平台也可以运行seL4：

• Intel platforms

  1. a PC99-style Intel Architecture 32-bit x86 (ia32)
  2. There is also experimental support for the 64-bit Intel x86_64 architecture.

• ARM platforms

  1. The Arndale dual core A15 ARM development board
  2. The Beagleboard, Omap 3530
  3. The Inforce IFC6410 development board, running a Qualcomm Krait processor that is like an A15.
  4. The KZM-ARM11-01. The kernel for this board is the one that is formally verified.
  5. The Odroid-X Exynos4412 board
  6. The Odroid-XU Exynos 5 board
  7. The Sabre Lite i.mx6 board.
  8. The Beaglebone Black is a community-supported port.

但对Odroid-XU Exynos 5进行编译：

TOOLPREFIX=arm-none-eabi- ARCH=arm PLAT=exynos5 ARMV=armv7-a CPU=cortex-a15 make

未能成功。