seL4 / microkit

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

Remove hardcoding of RISCV toolchain prefix #201

Closed wucke13 closed 1 week ago

wucke13 commented 2 months ago

https://github.com/seL4/microkit/blob/d1ea5bceaa5ac1c41516ff9e02f23c13525331ff/build_sdk.py#L36

Is not very compatible, i.e. the cross compiler toolchain from the nixpkgs has the riscv64-none-elf- target prefix instead.

Relevant upstream seL4 Issue: https://github.com/seL4/seL4/issues/1309 and PR: https://github.com/seL4/seL4/pull/1310

Please note that the upstream seL4 PR's do not solve the issue entirely for microkit, due to the hardcoding in build_sdk.py

Ivan-Velickovic commented 2 months ago

The RISC-V toolchain (https://github.com/riscv-collab/riscv-gnu-toolchain) uses unknown-elf- for the no-OS toolchain so it seems like Nix has decided to change the triple.

Rather than continue dealing with GCC messiness, I will probably just go with implementing https://github.com/seL4/microkit/issues/180.

wucke13 commented 2 months ago

@Ivan-Velickovic I feel the pain! Probably somebody from the nixpkgs felt the unknown to be an irregularity compared to the usual none and hence decided to stick with the pattern, instead of sticking with whatever upstream does.

While I'm in principle quite sympathetic with just using LLVM, I think that might narrow down use-case scenarios for microkit in an uncomfortable way.

If I could make a wish, it would be the following:
I'd like to specify the target prefix per architecture, for example using environment variables. For the clang case, this target prefix could just be an empty string. Then I'd like to specify the name of each tool, i.e c-compiler and linker. These two would then default to clang.

Ivan-Velickovic commented 2 months ago

What compiler Microkit uses for its components should not have any affect on users of Microkit. I am not sure how Microkit switching to LLVM would affect users, could you provide details?

For example at Trustworthy Systems we use both GCC and Clang with Microkit despite Microkit using GCC for all the SDK components.

wucke13 commented 2 months ago

What compiler Microkit uses for its components should not have any affect on users of Microkit. I am not sure how Microkit switching to LLVM would affect users, could you provide details?

I guess for the average user, it does not affect them. They download the SDK, and be good with it. But, once we talk about certification of safety critical things, this becomes much harder. Likely certification requires tight control over all code that goes into the system, and likely to that goal compiling the SDK yourself is preferable. Different organizations might have additional internal constraints on which compiler is used. In theory, you can use any compiler as long as you can reasonably demonstrate that it is ok. But, what if you already have a specific GCC with a lot of evidence readily available for the assurance? That is precisely the kind of scenario where using a very specific toolchain can decrease the cost of a safety critical system severely, making the difference between being economical viable or not. TL;DR for normal users, downloading the binary release of the sdk is fine and comfortable, but in safety critical systems compiling yourself with a toolchain you pick might be much easier to certify.

Other than that, the ABI Cafe already uncovered some niche yet interesting bugs. While I would assume most object code between gcc/clang can be linked together, in a safety context I'd prefer not to take any chances. If there is a large legacy application developed for gcc (that one would not feel comfortable to move to clang), not mixing the gcc and the llvm code generation unit's object code can be a tiny step towards more robustness.

Both reasons provided are only relevant for a niche of the entire group of (embedded-) developers, hence I'm by no means against defaulting to clang. But, for some safety critical contexts (such as aviation, where I try to push microkit), reserving the user the freedom to compile the sdk with the toolchain of their choice may be valueable. I know this is not a sexy argument, and it isn't modern. But to these industries, conservative and legacy compatible design is very appealing.