search

seL4 / microkit

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

Switch to LLVM based tools (?) #180

Open Ivan-Velickovic opened 1 month ago

Ivan-Velickovic commented 1 month ago

Recently I've made a PR for RISC-V support to Microkit (https://github.com/seL4/microkit/pull/179) which means that Microkit now supports multiple architectures.

This means that we need a new toolchain dependency since GCC only compiles to a certain architecture. This is a bit annoying as I cannot find a toolchain for RISC-V that works on both macOS/Linux and has prebuilt binaries.

It seems like you are expected to build a toolchain from source from https://github.com/riscv-collab/riscv-gnu-toolchain which is kind of ridiculous. I tried https://github.com/riscv-software-src/homebrew-riscv but could not get it working.

Now, even if this problem was solved, we still have the issue where every time we add a new architecture, we have to depend on a whole new toolchain.

This issue has come up before and my reasoning for sticking with GCC was that it is known to work with binary verification while Clang/LLVM is not. If we were to use GCC it would mean that we would be able to ship binaries in the SDK that have been known to pass binary verification, although currently we are not doing that.

Since binary verification isn't being currently maintained, I don't know whether it's worth sticking to GCC. Clang/LLVM is widely available and supports all of the architectures we need with a single set of tools which would make it easier to build Microkit from source.

@lsf37 do you have any opinions?

Ivan-Velickovic commented 1 month ago

I should be explicit that this only affects the components that Microkit builds, so:

Users of Microkit of course will continue to be able to use whatever toolchain they want to compile their code.

lsf37 commented 1 month ago

One thing to think about is that seL4 SMP is currently broken on clang/LLVM.

Ivan-Velickovic commented 1 month ago

One thing to think about is that seL4 SMP is currently broken on clang/LLVM.

Good point. I want to add SMP support fairly soon so we'll have to stick with GCC for the time being.

But assuming we have that fixed, do you see any other issues with switching?

lsf37 commented 1 month ago

Another thing to take into account is translation validation (binary verification) only works for gcc currently. Not sure if there are plans at UNSW to change that, and if that is relevant for the parts that you want to use clang for.

Otherwise, no problems with clang in general.