search

seL4 / microkit

Microkit - A simple operating system framework for the seL4 microkernel
Other
70 stars 37 forks source link

Enforce toolchain used for building kernel? #23

Closed Ivan-Velickovic closed 9 months ago

Ivan-Velickovic commented 1 year ago

Since building the SDK requires a specific GCC toolchain, I was wondering whether it should be used for building the kernel as well? I notice that by default the kernel will be built with aarch64-linux-gnu- if it is installed, which is not the same toolchain that's being used for all the other components of seL4CP.

podhrmic commented 1 year ago

Is there a specific reason for using gcc instead of clang? We had good experience cross compiling with clang for RISCV, and presumably the ARM support is only better.

Ivan-Velickovic commented 1 year ago

A benefit I like of using Clang over GCC would be that we can avoid the mess that is GCC cross-compiler toolchains since clang is just a single binary for compiling all architectures (as far as I know). I think that it does not matter too much as the toolchain is only required for building the SDK, user code can use whatever toolchain it wants to.

Ivan-Velickovic commented 9 months ago

I have played around with Clang a bit and unfortunately it seems like it is not much better. In order to build everything needed for Microkit you would need the LLVM linker as well as other tools such as llvm-ar. These are not always easy to install depending on your host system.

I don't find this to be much better than GCC given you now have to acquire various binaries on your system to fully compile everything. With GCC there's just one path you need, but you need to have a separate one for each architecture.

Neither solution is ideal.

To my knowledge, the Zig C compiler is the only truly portable C compiler however the project is too immature and buggy to be used for production software such as Microkit (in my opinion).

Ivan-Velickovic commented 9 months ago

I'm going to close the issue as https://github.com/seL4/microkit/pull/50 has been merged.

Regarding whether to use Clang over GCC, I don't feel strongly towards either. All other seL4 Foundation projects use GCC which may cause Microkit to end up sticking with GCC. I will definitely keep this in mind as the decision is not finalised yet and will decide what to do as we converge Microkit dependencies with current seL4 dependencies. Thanks for bringing it up @podhrmic.