Switch to LLVM based tools (?)

[Ivan-Velickovic]

Recently I've made a PR for RISC-V support to Microkit (#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]

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

• kernel
• bootloader
• monitor/initial task
• libmicrokit

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

[lsf37]

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

[Ivan-Velickovic]

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]

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.

[Ivan-Velickovic]

Given that binary verification only works for GCC and it is likely that people in the community would change the SDK to use vendored/trusted versions of GCC anyways, I'm going to stick with GCC for now.

We can always re-open/revisit later.