seL4的編譯和運行

seL4指定了可以運行的平台，按照下面的匹配來編譯它。

ARCHPLATARMVCPU arm imx31 armv6 arm1136jf-s arm omap3 armv7-a cortex-a8 arm am335x armv7-a cortex-a8 ia32 pc99

從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

未能成功。

---

選擇imx6平台：

TOOLPREFIX=arm-linux-gnueabi- ARCH=arm PLAT=imx6 ARMV=armv7-a CPU=cortex-a9 make

對arch/arm/machine/l2c_310.c的284行處做如下修改：

編譯通過，生成kernel.elf鏡像。

---

選擇exynos4平台：

TOOLPREFIX=arm-linux-gnueabi- ARCH=arm PLAT=exynos4 ARMV=armv7-a
CPU=cortex-a9 make

通過修改src/plat/exynos4/../exynos_common/mct.c中的initTimer函數：

編譯通過，生成鏡像。

然後qemu選擇相應的平台nuri或smdkc210，但都不能正常啟動內核鏡像。