Building SeL4 directly on MacOS

seL4 kernel
1

Hi everyone!

I’m pretty new to building on top of SeL4. I have a m1 mac laptop. Personally I hate docker, so I figured I’d get sel4 building directly on macos instead.

Well, a few hours of nonsense and I have it building just fine. The SeL4 test library builds and all the tests pass.

Here’s my setup:

First, you need the regular sel4 dependencies:

brew install cpio ninja make aarch64-elf-gcc qemu repo

python3 -m venv venv
source venv/bin/activate
pip install setuptools pkg_resources protobuf sel4-deps

You need gnu cpio from homebrew because the macos-included cpio tool comes from freebsd, and it doesn’t support the same command-line arguments.

I tried building on top of llvm & clang, but ran into some linker errors when linking the kernel. Something about symbol offsets out of range. I suspect there’s a way to fix that problem, but gcc worked fine so I’m using that.

Next, you need a working platform.cmake file. I saved this to ~/gnu-aarch64.cmake:

set(CMAKE_SYSTEM_NAME      Generic)
set(CMAKE_SYSTEM_PROCESSOR aarch64)

set(CMAKE_OSX_SYSROOT          "" CACHE PATH "" FORCE)
set(CMAKE_OSX_DEPLOYMENT_TARGET "" CACHE STRING "" FORCE)

set(CROSS_COMPILE aarch64-elf-)
set(CROSS_COMPILER_PREFIX aarch64-elf-)
set(PLATFORM qemu-arm-virt)
set(SIMULATION TRUE)

set(GCC_TOOLCHAIN /opt/homebrew/opt/aarch64-elf-gcc) 

set(EXTRA_FLAGS "-Wno-error=attributes")
set(CMAKE_C_FLAGS_INIT "${EXTRA_FLAGS}")
set(CMAKE_CXX_FLAGS_INIT "${EXTRA_FLAGS}")

set(CMAKE_EXE_LINKER_FLAGS_INIT   "-nostdlib")
set(CMAKE_SHARED_LINKER_FLAGS_INIT "${CMAKE_EXE_LINKER_FLAGS_INIT}")

set(CMAKE_LINKER aarch64-elf-ld.bfd)
set(CMAKE_C_COMPILER   aarch64-elf-gcc)
set(CMAKE_CXX_COMPILER aarch64-elf-g++)
set(TRIPLE aarch64-elf)

set(CMAKE_AR /opt/homebrew/bin/aarch64-elf-ar)
set(CMAKE_RANLIB /opt/homebrew/bin/aarch64-elf-ranlib)

set(CMAKE_C_COMPILER_TARGET   ${TRIPLE})
set(CMAKE_CXX_COMPILER_TARGET ${TRIPLE})
set(CMAKE_ASM_COMPILER_TARGET ${TRIPLE})

I’m sure some of the options above aren’t actually needed, but I haven’t tried too hard to simplify it.

  • I’m using -Wno-error=attributes because gcc from homebrew is built without support for the retain attribute, and this leaves those warnings as warnings. There’s probably a nicer way to disable those warnings (is there a flag to not use retain at all?)
  • Most of the other options are there to force the build to use aarch64-elf-gcc instead of defaulting to macos platform defaults.

There’s 2 more errors to fix:

  1. One of the build scripts just tries to run cpio from the system path. You need to force the build to use cpio from homebrew. So, export PATH="/opt/homebrew/opt/cpio/bin/:$PATH"
  2. Homebrew has qemu v10, and there’s currently a bug in the aarch64 & riscv cmake script where it misidentifies qemu version 10 as version 0. The fix is a tiny change to a regex - which hopefully will be merged soon. For now, you may need to apply the change directly. In sel4test, the file is at sel4test/kernel/src/plat/qemu-arm-virt/config.cmake. Change the regex on line 110 from "[0-9](\\.[0-9])+" to "[0-9]+(\\.[0-9]+)+"

Finally, you should be able to build and run sel4. I’m using sel4test. Clone and sync the normal way:

mkdir seL4test
cd seL4test
repo init -u https://github.com/seL4/sel4test-manifest.git
repo sync

Then build:

mkdir build-aarch64
cd build-aarch64
../init-build.sh -DPLATFORM=qemu-arm-virt -DSIMULATION=TRUE  -DCMAKE_TOOLCHAIN_FILE=~/gnu-aarch64.cmake -DCROSS_COMPILER_PREFIX=aarch64-elf-
ninja
./simulate

I’m not sure why -DCROSS_COMPILER_PREFIX needs to be set again on the command line, but it doesn’t build without it.

Anyway, happy hacking. I hope this is helpful to someone!

2

Thanks for posting the issues you ran into.

You seem to be the first person trying out a toolchain with the aarch64-elf- prefix, we can fix that easily by adding it to the list here. Once this is added the -DCROSS_COMPILER_PREFIX won’t be needed anymore. I’ve made a PR here.

The errors about the retain attribute seems to be due to more recent toolchains which unfortunately still hasn’t been resolved, more info here.

The GNU CPIO compatibility is a bit annoying as well, not sure whether there’s a BSD option substitute or if GNU CPIO is genuinely needed.

3

There are plans to get rid of CPIO altogether. But in the meantime, that script needs to be fixed to use the correct path for CPIO, could you send a PR?

4

I don’t think there is a correct path for it since GNU cpio is not installed on macOS by default so it depends on what package manager you use right? Homebrew doesn’t automatically add it to the user’s path so it doesn’t mess up BSD cpio.

5

Good point. Perhaps we should could add a cpio path config option?

6

Yeah I think making the cpio path configurable would be great. In some sense, cpio is part of the cross-compilation toolchain on macOS. So its path should be configurable just like gcc, ar, etc.

7

Thankyou! Honestly it’s a bit weird that homebrew uses aarch64-elf instead of aarch64-elf-none or something like that. But so long as they’re doing that, it’d be nice to have proper support for it.

Re: the retain macro warnings, would it make sense to add a macro definition to force disable the use of the retain attribute? If I’m understanding you correctly, we’d get linker errors if the flag is misused anyway. It would also help with aarch64 on Linux when using the official arm cross compiler toolchain - because that’s also built without support for the retain attribute.

8

Considering retain was added to support Clang’s ldd linker, I’d say only add it if the compiler is Clang and not for gcc by default. But just disabling link time optimisations would fix the Clang problem too.

If I’m understanding you correctly, we’d get linker errors if the flag is misused anyway.

Only one way: If you don’t use the flag while it’s needed, all tests will be removed by the linker and nothing will be done at runtime. sel4test (and sel4bench too probably) is doing symbol tricks to find all test functions.