Closed wucke13 closed 4 months ago
A further note: I checked, and currently indeed there are differences between the different header files per microkit target. The following shell snippet provides some rough overview:
find $MICROKIT_SDK -type f -name '*.h' -exec sh -c 'cd $(dirname {}); sha1sum $(basename {})' \; | awk '{printf("%-40s %s\n", $2, $1)}' | sort --unique
Outstanding things with differences:
constants.h
deprecated.h
faults.h
gen_config.h
invocation.h
mapping.h
objecttype.h
sel4_client.h
simple_types.h
syscalls.h
types_gen.h
types.h
Have you taken a look at the official Rust support for seL4 userspace, which includes crates for Microkit PDs in Rust?
https://github.com/seL4/rust-sel4
There, we've taken the approach of implementing libmicrokit in pure Rust as a crate called sel4-microkit
(source, docs), built on top of the sel4
crate (source, docs). The sel4
crate is built on top of the sel4-sys
crate, which is generated from the libsel4 headers and .xml/.bf files (note, however, that it is pure Rust too, and does not link against libsel4).
The sel4
crate uses and exposes the seL4 kernel configuration (docs, note that the sel4-config
crate is re-exported by the sel4
crate as sel4::config
). The sel4-microkit
crate uses this configuration information as well.
Would the sel4-microkit
crate meet you needs? What do you think of the approach we've taken? It is different from the approaches you've listed, and is based on having a solid sel4
crate, with a clear configuration story, and then building the much simpler libmicrokit implementation (the sel4-microkit
crate) in pure Rust on top of it.
Have you taken a look at the official Rust support for seL4 userspace, which includes crates for Microkit PDs in Rust?
No, whilst remembering reading about your work in the forum a couple of months ago, it completely went under my radar!
Would the sel4-microkit crate meet you needs?
No, it does not compile with only the things included in microkit-sdk
. Also it pulls in nightly stuff, which isn't great.
What do you think of the approach we've taken?
It seems that it depends on being pointed to seL4 configuration, and then creates a tailored API to suit to that. I really like that it works with pure rust. I really dislike, that this just forwards the configuration problem to the end-user. I just tried compiling a minimal example using sel4-microkit
. First it failed due to depending on nightly. Not great, but whatever. Then it failed due to wanting an seL4 include dir. I pointed it to $MICROKIT_SDK/board/qemu_arm_virt/debug/include/sel4/
but it failed, because its missing interfaces/object-api.xml
which is not a part of the microkit-sdk that I downloaded. In short, sel4-microkit
does not work when provided a microkit-sdk
, which is a dealbreaker (but an easily fixable one, I hope).
I think, your approach is the best one can do, when accepting the premise that there is not stable API/ABI, therefore forcing regeneration of the API based of the XML generated when compiling an seL4.
However, I believe the growth of use and ecosystem on top of this will be plagued similarly like the adaption of seL4. There is a variance on how the API presents (depending on processor architecture, target board, kernel configuration, ...) that is complicated to track. People that build stuff up-on this foundation either again have to embrace the configuration mess, or commit to one configuration introducing incompatibility. Incentives to invest in such an ecosystem is low, because there is always the lingering damocles sword of incompatibility due to an API/ABI change introduced by a software update, or configuration change. Portability is either broken, or hard to achieve and harder to verify/maintain.
Coming back to microkit, one of its promises was to break this complexity, by declaring 1 3 APIs per board. No more many configuration parameters. No more tackling cmake, camkes, etc. just to get seL4 to compile. This is the most significant improvement in the seL4 ecosytem I have seen so far. Your current sel4-microkit
breaks it, by requiring seL4 artifacts that are not delivered in the microkit-sdk
.
TL;DR I believe you did almost as good as possible, given the current flexibility inherent to sel4. I think the sel4-microkit
crate is useless in its current state (as it breaks the one major advantage of microkit), but it should be easy enough to arrange a fix for that together with the upstream microkit project.
Overall my text might sound overly pessimistic, which is not correct. I think you did a great amount of work, and it seems to be well thought through and mostly well put together. I do think, that the current non-stable API/ABI makes it impossible to do better in principal. However, I fear that this approach bears the same clunky user-experience that plagued seL4 adoption for far too long.
Thank for sharing these thoughts!
We really ought to make the seL4/rust-sel4 repo more easily discoverable by pointing to it from the seL4/microkit repo.
First it failed due to depending on nightly. Not great, but whatever.
Some Rust language features required for implementing a reasonable sel4
crate and a fully-featured pure-Rust language runtime are not yet stable. For example, the #[thread_local]
attribute, used for declaring thread-local variables (such __sel4_ipc_buffer
), requires #![feature(thread_local)]
. For now, if we want pure Rust code, the best we can do is be disciplined about minimizing the use of unstable features, and using a mechanism like the rustversion
crate to maximize breadth of toolchain compatibility in the cases where we must use them.
By the way, one can use nightly features on a stable toolchain by setting the environment variable RUSTC_BOOTSTRAP=1
.
Then it failed due to wanting an seL4 include dir. I pointed it to
$MICROKIT_SDK/board/qemu_arm_virt/debug/include/sel4/
but it failed, because its missinginterfaces/object-api.xml
which is not a part of the microkit-sdk that I downloaded. In short,sel4-microkit
does not work when provided a microkit-sdk, which is a dealbreaker (but an easily fixable one, I hope).
This is indeed easily fixable. In this case, SEL4_INCLUDE_DIRS
is required to be set to $MICROKIT_SDK/board/qemu_arm_virt/debug/include
rather than $MICROKIT_SDK/board/qemu_arm_virt/debug/include/sel4
.
I hope that my response so far has addressed your issues with the suitability and usability of the sel4-microkit
crate, which is designed within the constraints imposed by seL4's design. However, I recognize that your larger point is about the challenges imposed on developers by the way that seL4's API and ABI depend on its configuration. This thread contains an interesting discussion on that topic.
Thank for sharing these thoughts!
You are welcome! Thanks for pushing seL4 Rust support forwards!
By the way, one can use nightly features on a stable toolchain by setting the environment variable RUSTC_BOOTSTRAP=1.
Today I learned! That sounds like quite the hack, but for obvious reasons it wont be deprecated anytime soon.
This is indeed easily fixable. In this case, SEL4_INCLUDE_DIRS is required to be set to $MICROKIT_SDK/board/qemu_arm_virt/debug/include rather than $MICROKIT_SDK/board/qemu_arm_virt/debug/include/sel4.
Nope, I tried both. Said object-api.xml
does not exist at all in the microkit-sdk copy that I have. And as long as https://github.com/seL4/microkit/issues/116 remains open, there is no easy way to spot whether we are on the same or a different sdk. Most likely a different one.
Thank you for linking the other thread, and for keeping up on the issue!
A release will happen in the next couple weeks, sorry about that.
If you happen to be using the SDK provided by the tutorial, it will not work with Rust. But if you build from source it should all work.
@Ivan-Velickovic Thank you for the heads up. Building from source is unfortunately not really an option for me. We try to build everything in Nix. Now it happens that pyoxidizer seems to provide no robust option to avoid downloading random stuff from the internet but to use vendored dependencies https://github.com/indygreg/PyOxidizer/issues/744 . Hence its not easily possible for me to package a source built version of the microkit-sdk over on https://github.com/DLR-FT/seL4-nix-utils/ . For context, providing a solid microkit-sdk-bin
package is the reason why I opened #116 .
I'm quite heavy on the complaining side all over the part, but I want to stress that I value your prompt responses and awesome work very much so as well, @Ivan-Velickovic !
PyOxidizer is gone: https://github.com/seL4/microkit/pull/126.
It sounds to me like most of the problems described here should be gone with the upcoming release of microkit (unfortunately not much we can do about still needing a nightly version of Rust). We should make sure to release the corresponding Rust setup simultaneously. Not sure if we'll manage a kernel release in time, but I'd be up for trying to have one consistent release of everything.
Enabled through #126, I know have microkit-sdk built from source available over at https://github.com/dlr-FT/seL4-nix-utils/ . I will check next week, if it that homegrown microkit-sdk works with Nick's Rust related work.
By the way, one can use nightly features on a stable toolchain by setting the environment variable RUSTC_BOOTSTRAP=1.
Today I learned! That sounds like quite the hack, but for obvious reasons it wont be deprecated anytime soon.
Yes, it definitely is a hack! The way I've rationalized this one for myself is that we are borrowing the mechanism that Cargo uses for -Zbuild-std
[1], because we are more or less doing something similar.
I'm going to close this because I think that the original issue is resolved because the rust-seL4 project can be used.
Feel free to re-open if I'm wrong.
@Ivan-Velickovic Is there at least a chance to get away from the 69 different set of header files?
@Ivan-Velickovic Is there at least a chance to get away from the 69 different set of header files?
I don't think so because there is (and there will be more) parts of the header that depend on the board and particular configuration of the kernel. This is why I don't see it being that feasible to have a more general per-architecture microkit.h
.
seL4 is quite tied to a specific platform (at least for ARM and RISC-V) which is why I think at this time it is not really feasible to have the SDK artefacts be general to the architecture.
Currently, I see 23 targets supported by microkit. Each of them has 3 different modes (
benchmark
,debug
&release
). So overall, there are quite some variants of the API offered. To add upon that, the header files itself are polymorphic, as in they themselves contain macros to adapt for different target platforms, i. e. like this:I'm currently trying to make Rust bindings for microkit, as to support implementation of protection domains in Rust. While it is possible to just embrace this high adaptability of the API, I see a real danger that this will (and has in the past!) seriously hindered solid Rust support of microkit (and seL4 in the grander picture). In order to make my life easier (and the programming in Rust for microkit story nicer), I have a wishlist. I present various options, starting with the easy-to-implement-but-not-so-nice to the more-complex-to-implement-but-way-nicer-to-use.
$MICROKIT_SDK
pathbuild.rs
to dynamically generate the bindings$MICROKIT_SDK
pathbuild.rs
to dynamically generate the bindings$MICROKIT_SDK
pathbuild.rs
to dynamically generate the bindingsFrom a user point of view, 4. and 5. are by far the most preferable ones. Its the only option where a pure Rust toolchain, without any libclang/binding generator stuff gets executed on the end-developers machine. They just use the
microkit
/microkit-sys
crate offered on https://crates.io/ . Its also the only option if we want a robust ecoystem to be built on top ofmicrokit
, because only with a stable API & ABI we can avoid spurious type change problems.With Option 4. however, considering that a significant portion of the microkit API is header only, we still would have to involve a C compiler to get a final ELF for the protection domain. Option 5. on the other hand takes C tooling completely out of the equation, we could then compile pure Rust code down to an ELF that is usable in microkit. Of course Option 5. is more work when the ABI changes, these change would have to be ported over to the Rust code by hand.
If offering a stable API & ABI is not possible (or not yet possible), option 3. is preferable. While we do force binding generation on to the end-developer, we can automate quite some stuff. This way we can get away with all the fuzz about different target boards and associated header files. Instead, the combination of the Rust profile (debug vs release) and the Rust target (i.e.
aarch64-unknown-none
) completely determine which header files to pick.I totally understand, that likely asking for Option 5. is quite the ask at this early stage of microkit. However, getting at least to Option 3. would already considerable ease my pain in providing initial Rust support (and more significantly, ease the pain on making Rust libraries on top of microkit).
I'm looking forward for your feedback!