There are a number of project out there that involve developing on seL4 using Rust. This RFC is an exploration of what can/needs to be done within the seL4 project itself to allow full advantage of rust tooling and language for building on seL4, with minimal extra friction.
I like the spirit of the RFC, and personally Iām on board with providing a proper typed libsel4 layer for Rust. Iād consider that the fun and easy part and would be happy to contribute time to that. As pointed out in the draft RFC and discussion here there are multiple developments out there that would already be good candidates for that layer, at least as inspiration/for adaption. In addition to the ones mentioned so far, I also like the Icecap libraries.
What Iām less clear on is how to achieve the goal of an easy/effortless dev + build experience. This may mostly be because I donāt know too much about cargo and the Rust build tools. Some concrete questions:
are we expecting cargo to invoke the seL4 build system and produce a seL4 binary to package with user space?
how does that mesh with the crate structure Rust expects? Can seL4 releases + bottom-level (untyped) Rust libraries be generated and packaged as a crate other work can depend on? If yes, what would working on a seL4 dev version look like where maybe no crate is published yet? (This would be mostly for CI during seL4 development, not so much for people wanting to use seL4).
how does support for the different config options of seL4 work in Rust builds? Can everything be mapped to corresponding concepts in Rust builds?
I presume target architecture, platform, etc would be selected in the cargo.toml file? What would an example look like?
While supporting and maintaining a Rust library layer seems doable in terms of effort, extending cargo like the fel4 project does not look like a sustainable option to me.
Related work for a looser coupling to the cmake build system for seL4 would be the Core Platform work. Not sure how directly applicable that is, but ideas from there might translate over.
In addition to a typed library layer, it would make sense to build up a few further libraries, in particular for resource management and common primitives, in terms of functionality along the lines of what currently exists in GitHub - seL4/seL4_libs: No-assurance libraries for rapid-prototyping of seL4 apps. for C. Iād keep that separate from this RFC discussion though build that up over time.
One approach that could be considered is trying to focus requirements by first picking a seL4 framework like CAmkES or the seL4 Core Platform and focus on what it would take to write rust as first class apps in one of those environments. By starting from something that already defines a process abstraction and a runtime environment, itās easier to build a rust foundation on top.
From this approach, itās easier to motivate whatās missing from the core seL4 libraries and tooling to support rust in these settings. Otherwise, itās harder to argue the requirements for the libraries when theyāre trying to be the foundational rust support for all rust app runtime environments.
Yes, all of seL4_libs might be a bit much. Letās focus on the the base libsel4 layer (typed) and general build first.
I suspect integrating with CAmkES and CP will be one step harder, because you also have to configure components and connections etc and it draws in more dependencies. Itād be great to have that, but Iād be fine with a more bare-bones environment first as well.
My personal interest in this would actually be experimenting with something more dynamic than either of CAmkES/CP (without verification, but at least with type safety), thatās why Iām keen on at least the bottom layer library + build capability without a component framework. E.g. longer term, itād be nice to have something like Thread::spawn just work on seL4 or even an async framework that can use seL4 threads. These would all be within the same address space, and could be running inside a component framework or not (if it supports multi-threading).
One of my biggest issues with using seL4 effortlessly is the build system. Repo isā¦ interesting, but can largely be ignored once sync is run. CMake is a fairly standard build tool for C/C++ but the way itās used in seL4 is more complicated than the average and it also doesnāt follow some of the best practices (CMake makes this hard). The biggest issue I see is that the build system assumes that the kernel and libsel4 are compiled at the same time, with the same settings.
I understand why the ABI isnāt stable and I donāt think it needs to be. That would seemingly suggest stability across versions which I think is unnecessary. I am curious which things currently impact the ABI and why. I know that architecture/platform do (reasonable), MCS or not also does (reasonable).
For example, if Iām building for riscv64, how do I know whether KernelCtzNoBuiltin changes the ABI? I donāt know why it would but Iāve read a lot about seL4 lately and none of it suggests otherwise.
How does this relate to Rust (or other languages). All of the Rust attempts at seL4 that Iāve seen have a separate tool that takes a set of configuration options like KernelCtzNoBuiltin and turns them into a kernel and custom libsel4 to be used. This makes using seL4 with Rust unlike most libraries.
Ideally, Iād want to get to the point where the options that impact the ABI is documented, at least in a comment in the script that generates libsel4.
Edit:
Rust/Cargo currently supports conditional compilation using an extensible key-value system, though there are builtin configuration pairs that are always available/standard.
debug_assertions - enabled by default for debug builds.
Adding custom options is possible but has implications when those options have to be exposed through the dependency management of cargo. If seL4ās ABI only relied on these (and MCS ātakes overā), then building a Rust crate and publishing it for a specific version of seL4 would allow anyone to program against the kernel without any additional effort.
Obviously, this ignores the question of bundling the kernel along with rootserver/elfloader/etc. but I think we can consider that out of scope for the current discussion.
My draft PR is in line with that, I feel, but is strictly a documentation effort. I would be happy to put some time into implementing something more concrete.
As a PoC, Iām re-implementing some of the inline assembly in Rust. Idea being, is to be able to put it in a stand-alone repo, perhaps published to crates.io, and adapt the current seL4 build system to link that in. These are some of the things that Iām aiming for
Identical to the C functions at the binary level
Compilation handled by the rust ecosystem
integrates seamlessly into current cmake system
Possibility of reducing the complexity of cmake.
Should this PoC go well, I see the following being a feasible reality:
There exists a libsel4 library as a rust crate
This crate is fetched, built, and linked-in by the cmake system
You could write a rust server with code as follows:
fn called_straight_away_by_c_root_server(/* snip */) {
sel4::$KERNEL_OBJ_INTERFACE::$METHOD(/* snip */);
// compile failure if not built with kernel debug printing: macro doesn't exist
sel4::debug_println!("Hello, World");
}
Rust handles that in a very nice way. Below is an example. To the library user, the path to an arch-specific interface would be sel4::arch;, and
// src/arch/mod.rs
#[cfg(target = "aarch64")]
mod aarch64;
#[cfg(target = "aarch64")]
pub use aarch64::*;
#[cfg(target = "x86_64")]
mod x86_64;
#[cfg(target = "x86_64")]
pub use x86_64::*;
This is a common pattern. Hereās one example of how Rusts core library uses it to make simd portable between architectures (Though that area goes into some pretty advanced usage)
For target selection, itās done as so:
# Add the target to the rust toolchain. Only needs doing once
rustup target add aarch64-unknown-none
cargo build --target aarch64-unknown-none
You can set up custom target triples. Goes into some detail here, but in brief:
cargo build --target target_tripple_file.json
There exists a CMakeLists library that aims to make the invocation and linkage of rust into a cmake built C/CPP project seemless. Working out what to do there is part of my work on the PoC
This is problematic, because the seL4 build is already too complex and should definitely not depend on crates.io. For developing the inline asm functions, it might make sense to start in a separate repo, but for maintenance they should eventually end up where the C inlines asm functions are and the rest of the low-level (untyped) Rust libsel4 is generated, because that is extremely tightly coupled with the kernel implementation.
The typed Rust libsel4 on top of that would make sense as a separate repo and should probably also stay that way.
Iām not saying it (low-level lib) shouldnāt end up as a crate on crates.io, I think that might make sense, itās just that the seL4 build should not depend on a Rust build, but only the other way around (Rust build can depend on or invoke a seL4 build).
One possible way of going about things, is to have the (for example) inline asm functions sitting in a dedicated crate, and use cargos vendoring infrastructure.
At my work, we have some crates vendored into our mono-repo for modification. We are also going to be experimenting with open-sourcing some internal libraries. These libraries have a degree of coupling with our core code. One idea being is that we āinlineā the crate into our mono-repo with vendoring, keeping our local code in-sync with our core code, and periodically up-streaming the the changes.
What it should mean (in theory), for seL4 rust-dependancies , is that as far as the mono-repo code-base is concerned, everything is organised as if it is integrated into the mono-repo as you describe.
Keeping the XY problem in mind: The key-stone issue here is maintainability/stability in the context of this code being very tightly coupled to the kernel. Anything upstreamed into mainline is conditional on these two qualities not being compromised in any way.
Others might be ahead of me with this, and have experience using this method. I can share our experience as we acquire it.
seL4 CMake system isā¦ interesting: āThe biggest issue I see is that the build system assumes that the kernel and libsel4 are compiled at the same time, with the same settings.ā - Ahmed Charles
āthe seL4 build should not depend on a Rust build, but only the other way aroundā GK
I have a project (currently in a private repository) that successfully integrated selfe-sys and a rootserver (mostly in Rust, compiled in staticlib mode) into a regular seL4 CMake build, using the Corrosion extension to CMake for doing cargo builds.
If you only check out GitHub - seL4/seL4: The seL4 microkernel, you can use just itās CMakeLists.txt to build a kernel + libsel4 for a particular configuration:
git clone https://github.com/sel4/sel4.git
cmake -G Ninja -C sel4/configs/ARM_verified.cmake -DCMAKE_INSTALL_PREFIX=$PWD/stage sel4/
ninja install
ls stage/
# bin libsel4
$ ls stage/libsel4/
# include src
$ ls stage/libsel4/include/
# api autoconf.h interfaces kernel sel4
The kernel can be built independently of libsel4, but it does use some of the headers that are in the libsel4 tree. libsel4 does require the kernel build has been processed by CMake before libsel4 can be built due to a large number of configuration dependencies they share, but you can build it independently, provided you use the same configuration options that were used for the kernel.
I knew this before, it was the intent of my post, so sorry if I communicated that poorly. The core question is, which configuration options impact the ABI and therefore have to be the same?
The previously mentioned KernelCtzNoBuiltinhopefully doesnāt impact the ABI, but thatās not documented anywhere that Iāve seen.
I think this would be easier to answer for specific definitions of impact and ABI. But I agree it makes sense to make it easier for people to know which options are safe to change without breaking their user level programs. Iāve written up a few different scenarios from different interpretations of impact and ABI:
Thereās probably only a few options that affect the syscall ABI - the actual ABI for performing the actual syscall machine instructions and argument register allocation layout: MCS/non-MCS and the KernelSel4Arch options.
Thereās more options that affect whether certain debug system call numbers exist such as KernelPrinting or KernelBenchmarks, but this list could probably be enumerated.
If you consider the kernel object sizes are part of the ABI, then there are various options that change the size of different kernel objects. Some CMake options change the size of the TCB object which affects the seL4_Untyped_Retype interface. For the same sized untyped object you can create a different number of TCB objects depending on certain kernel configuration options. This may be not considered ABI breaking for some dynamic systems that implement their object creation code dynamically, but it may be considered ABI breaking for static systems that rely on performing all object allocation offline and compiling an allocation spec into their root loader.
The seL4_Bootinfo_t object is part of the ABI between the kernel and roottasks, but all other user programs arenāt affected. Essentially any kernel config option can change the contents of this object. Dynamic systems can likely handle a wider range of config changes without requiring recompilation, but extremely static systems may require recompilation for any config change. Any kernel config option that changes the size of itās binary image will result in a different layout of initial untyped objects being described in the seL4_Bootinfo_t. There are experiments with the capDL language to verify full system properties from a system spec that depends on knowing an exact initial Untyped layout and would also treat that as part of the ABI.
This is what I wouldāve expected and I would consider this the baseline. I hope we can get to a point where these options are documented for a given release.
I think this is fine, as long as executing those system calls when they do not exist results in a well defined error. Iām not sure whether this currently results in a fault to the TCBās exception endpoint or in an error result, but either one should be fine from the perspective of independently compiling a Rust libsel4.
Can one currently ask the kernel what those sizes are dynamically? Is that something that could be added? That would allow the current libsel4 to ignore that API and continue to hardcode the values based on configuration but allow a Rust libsel4 to dynamically determine the values.
Iām fine with some users deciding to take on the burden of managing more configuration options if they get some benefit, like verification, in return. I think the current interface here is sufficient for everything to be determined dynamically, if one decides that is sufficient, right?
As a concrete example:
tagged_union seL4_Fault seL4_FaultType {
-- generic faults
tag NullFault 0
tag CapFault 1
tag UnknownSyscall 2
tag UserException 3
#ifdef CONFIG_HARDWARE_DEBUG_API
tag DebugException 4
#endif
#ifdef CONFIG_KERNEL_MCS
tag Timeout 5
-- arch specific faults
tag VMFault 6
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
tag VGICMaintenance 7
tag VCPUFault 8
tag VPPIEvent 9
#endif
#else
-- arch specific faults
tag VMFault 5
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
tag VGICMaintenance 6
tag VCPUFault 7
tag VPPIEvent 8
#endif
#endif
}
The CONFIG_HARDWARE_DEBUG_API configuration doesnāt change the number which comes after it, but CONFIG_KERNEL_MCS does. This seems like an unnecessary ABI break, though in this case, MCS obviously breaks the ABI in many other ways.
In general, I think a reasonable goal would be to have a Rust libsel4 which can be published to crates.io and used without having to determine all of the configuration options that were used to build your kernel.