Declare stable API & ABI to ease implementation of Rust API

Question

Declare stable API & ABI to ease implementation of Rust API

wucke13 opened this issue 6 months ago · 15 comments

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:

#if defined(CONFIG_RISCV_HYPERVISOR_SUPPORT)

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.

Keep everything like it is on microkit side. On Rust side
- Detect the $MICROKIT_SDK path
- Ignore benchmark config, but
- translate debug/release from Rust to debug/release header files in microkit
- Run rust-bindgen in build.rs to dynamically generate the bindings
- Have a Cargo feature per each officially supported target board, use that feature to pick the target board
Change microkit to one set of header-files per processor architecture. On Rust side
- Detect the $MICROKIT_SDK path
- Ignore benchmark config, but
- translate debug/release from Rust to debug/release header files in microkit
- Run rust-bindgen in build.rs to dynamically generate the bindings
Change microkit to one set of header-files per processor architecture. On Rust side
- Detect the $MICROKIT_SDK path
- Ignore benchmark config, but
- translate debug/release from Rust to debug/release header files in microkit
- Run rust-bindgen in build.rs to dynamically generate the bindings
Change microkit to one set of header-files per processor architecture and commit to a stable ABI. On Rust side
- Ignore benchmark config, but
- translate debug/release from Rust to debug/release header files in microkit
- Run rust-bindgen in once when publishing the crate generate the bindings
Change microkit to one set of header-files per processor architecture and commit to a stable ABI. On Rust side
- Ignore benchmark config, but
- translate debug/release from Rust to debug/release header files in microkit
- Manually write bindings down to the syscalls. No microkit header files required.

From 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 of microkit, 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!

Answer 1 · 2024-05-29T18:45:29.000Z

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

Output of the script on my distribution of microkit

assert.h                                 19c726ba438dedefd0f648c7aac99712eea89b16
autoconf.h                               5b3bf1738844bf31b01aa706f55ae4084a88f519
benchmark_tracepoints_types.h            f21877e4c696306d1c6d905edaa82a9521ae4b58
benchmark_track_types.h                  c977d168a4dc1bdc33db6f4376ced4c15af42e8c
benchmark_utilisation_types.h            6c9fe82d3676103c2de60e77512af300dba22e07
bootinfo.h                               bac1a007f216c1241d2de7d94ff50de88315623f
bootinfo_types.h                         4fa6cd1cf69d195363aec4216d573e3fcf608dd5
config.h                                 c93418752737b902e8831f5bff4b89e6415ea7a4
constants_cortex_a15.h                   f4800b70afd85bdc1df5c5ffe81bfcbc36a01300
constants_cortex_a35.h                   969c68369768667d807931d9cba148eb2bb5d0b3
constants_cortex_a53.h                   f91116ddc8172db31ee6809b091ca2e48e5ca9be
constants_cortex_a55.h                   550315c3568021c3e1a8d24fc5898416f4287aec
constants_cortex_a57.h                   3b0e1b9b203050196f6b51e2a43eb6f27546d0cc
constants_cortex_a72.h                   ee2e1abec7f6eb7c51f99af1362c3f205902896a
constants_cortex_a7.h                    a3d8ac5fdb9a59af0e9fed8c7d276b3cf1165738
constants_cortex_a8.h                    08acfea6a10d5f63e5a942b97b2aebe603bf18d5
constants_cortex_a9.h                    2d75e6387b7bd2037711ae88fc9394ef2df6b5b7
constants.h                              0c4044c4bc6c5b8c4adc3ed7d04f605804d77206
constants.h                              1532b752464b2dcbbb0fcd50a3a8e7b20d7615bc
constants.h                              39ec52b598305594783c80856700e9284a55a9f2
constants.h                              441432220ab22554dc6c9099137c1cf09f771fc8
constants.h                              4681c641056716079b79dde2219003c7fbeaae38
constants.h                              5260c8629fe7c9b86fa3544c46580a41e1d0ed1a
constants.h                              5f74bbd4299ecc29a122e9f680b7c7d5e911ccdc
constants.h                              633f8d98d1fd6996ca5db1a99e06d304c96564cb
constants.h                              64cf93e6cd54e14df5590aa2dcce430f622533bd
constants.h                              69e92e467c763394004e0d4c6193a89215161950
constants.h                              754cde05c937e9a0b9fafd5a38fb1b6349ac3d0c
constants.h                              77919cd4a9ae84400e799bf852b5fb18d676700b
constants.h                              c9998c865973168c68fa0566a1ae419859fe2c4b
constants.h                              ca3cd2d1e6e55ff2af4e3b26ea84dca862a6c79d
constants.h                              e2880b547a8a00022d174282e4211e67dcf7db7d
constants.h                              e8223096b03767822dcee9704d0d8a97587b6d17
debug_assert.h                           47984f11bdd21698c64959cd0b2f980093087d12
deprecated.h                             21317f0eda6bccecedb30b5449853297a38b150e
deprecated.h                             4d8e08b7e3209e2c4f245a3859032ccb63c53743
deprecated.h                             62bfb45a086fcdb66beea4c00a8ce0d5c1af260b
deprecated.h                             b9943d1374c9149f1aa7767855e65e69aab76e59
errors.h                                 4f90ac508b89f994116cea688231a38dfbe45452
exIPC.h                                  bfbe9209ffc6b8e040073724fc674a36a6c5af4c
faults.h                                 614a2bfcea4bde2c0d8403e7da08b449efaaa7dc
faults.h                                 d5bf450a6911f001ba4a19292ec39a7605c9fe93
faults.h                                 ec263c62f89ab107023aee7ff697f1774efbe354
functions.h                              e3a97dd4bffabe194cb8d945634c1f9186fd9c56
gen_config.h                             026f7722b1bf9684e940d39b39af3b38c3b2d1d2
gen_config.h                             069e35fca0aeb50b155382446de60e2292b01c3d
gen_config.h                             0e259e994a65af955ed8ba17098598b31cc6ffba
gen_config.h                             0fcaaee41f92816f8611cc4e6c7496e941e52b8b
gen_config.h                             124207c826d84b75bafb303a1df6df97061d2811
gen_config.h                             14f5dc967c3e7be1f645da506d18bc8f179e48dd
gen_config.h                             162b9f414bb0d8a607245b1767393433f13893e4
gen_config.h                             1fda547af0f11080ec5683dff89fcbae4a386ef7
gen_config.h                             200d08b827e4060dc02e2c8cb1a1bd11f473dfc5
gen_config.h                             280d6e6a04478d939ac48f9bafd9326f7f082799
gen_config.h                             2bd28178bfac426728f467a5cb325919db243fff
gen_config.h                             30101890d0874f4a0105956e132bdbd30e6285c6
gen_config.h                             30b6b2a6af3a184ab0948de12fe5ab223928a456
gen_config.h                             37bab7679fc8205c4063f49b1d27c364e4215a52
gen_config.h                             38137444b97c2b3632bf1c88a296f4845612df14
gen_config.h                             3dcbc3ef206dbbb08d1c5125bd9947484aad54f7
gen_config.h                             46dc5294a19cce584c3bc02bc5a18b092aeced0d
gen_config.h                             49b9024a353a2906196a339875cadd8c127f7450
gen_config.h                             5176833bc68a1c384ad978e208e184a58844f2e8
gen_config.h                             539db7e93ea751dd6533105c64247b05e85e7f02
gen_config.h                             574b80ce97534db1e4f0b70b2fcfe61464069d43
gen_config.h                             579fbdd5c7b38041a68d87ff06428cd57c5a6968
gen_config.h                             57f0a46e656526e472ff9c0fa60793f194fb1db5
gen_config.h                             5acf822d8f3e0e0df5809551c1486032392af1b0
gen_config.h                             5e7640a3eb83f8bb7c8108b967f17c3b95b281f8
gen_config.h                             611aa3e78e4e1c9bb6a159f4eef08c44cf6a3d3b
gen_config.h                             6a50f2b18c23c175cf21cbc40cf2600a292a576a
gen_config.h                             6e0e2afdaa72b16d7fbf49a4dac56110cb164474
gen_config.h                             6fbaf18464bef013402cc597225848fc422a255c
gen_config.h                             7b51d4de635a69fb702501de8e508d1972c21e5c
gen_config.h                             80828fcbee88631816fb8c21160ac6f245c30357
gen_config.h                             87e68fdd67f37ad76086125c074f40b5d95afd62
gen_config.h                             91761fd31046fbb6548a33cb5fcf510b3a60a181
gen_config.h                             94d25219dbfc3ef4ac9a45a354926c9eba1c81a7
gen_config.h                             9be91f727f301e8410182051a98796480c11f7d6
gen_config.h                             a1372c73144b76f1fdaa926bf232f6d0bf817a06
gen_config.h                             a1f1d85fbf4659a61553f338b6b117fe026525fe
gen_config.h                             a48d0f67efcf1d85822f6fc7c7cfc402cbd11357
gen_config.h                             a60440fcc595fb9c4d38632d2acc940ad36dda6b
gen_config.h                             aee0bcee31514bf00fb2c963a1c22c3f52a4c55e
gen_config.h                             af771841397d5b96802b5655bac44d45d59580c3
gen_config.h                             b1929f33877945e7ffa5beb596dc935b69cba265
gen_config.h                             b319f64c96d37ae7877d3d03468b1951ac7ae59a
gen_config.h                             b5680be98eca3738099b7ce1fee0a817d73e1471
gen_config.h                             b59c8a50df02f487e2b30af47fe51b5020fe6e36
gen_config.h                             b6300f696f79da7f99b2dd8e1a6349bf54da0492
gen_config.h                             b6e6233ac715043ac9118af8899d54c93744ed28
gen_config.h                             bb2812ffd2178dc189fed5d27926f4643fed5529
gen_config.h                             bc2970dac1b45ef53483881b8f76c59266a844d5
gen_config.h                             bcafcad88cef5d1c4fdfcc400e72824c4f1f1903
gen_config.h                             bdf7d4a1675a959fc5e13733e1cc1b8ec946a5ea
gen_config.h                             c5feae2ed3a54bdfa21006e72a47984e2b4b7323
gen_config.h                             c6ee6ac912a64b8a686db8739661edf3172cd0bc
gen_config.h                             ca8a62f467cd85904c37c958e75124882932664b
gen_config.h                             cbe387b0d95b25b6c7553ffbd35b57a9b99f92e4
gen_config.h                             cd8d084b0d12695d456a1eef6b2469e15ba0ab99
gen_config.h                             de65c4b795a007fa20a8d0023992f69da0e178f7
gen_config.h                             df4a49c6b8e5ead3fca895eac0e0a996835d73d3
gen_config.h                             e0666a3f64d13745bfb4c5c652d59cdb57d84bfa
gen_config.h                             e0d04e150195477897a676738eedf3a4b93f6878
gen_config.h                             e9e4f3c1cbbd6a03d0987ad47cf43ba9f5cf6c23
gen_config.h                             ec78cde37ed0068e15e558d4a2ea334275f62187
gen_config.h                             ed2f79d28d3c6e16566b304322d02213a789f215
gen_config.h                             efcc2a4d23931a2e1522824664a65ca4b5e695c4
gen_config.h                             f2b923710d3f1ad3ed1cfc1f7e6aef956280969c
gen_config.h                             f82ddcb7c2ac5018bec0e395402dd166cf022a30
gen_config.h                             fb8cb01fb7ef11c616dd2a23628f3deb019d0fa7
gen_config.h                             fc002cdbc8981bd182ada20e5fd66425c559b5e8
gen_config.h                             fd265c2ddd3a8125fab93343bfad27bb2e47e18c
gen_config.h                             fee7d2be41c624c422477d482c948c06b6982c2a
invocation.h                             00ae53a97a5de7c9b2b9c0e6d6129a24ad3e8798
invocation.h                             01ae918a3fe783f8c7260c73c9065bb43884228d
invocation.h                             868118debecb8d5f4edbd2ac77ca401b97bbc59a
invocation.h                             bc75b45f69945f357db6320b59e0ff9100372db5
invocation.h                             cd7957747d5ea8f24ba918356adce50691929e15
macros.h                                 c56662810a5bc050263e8d8645e1a0974b3c57f9
mapping.h                                34c5eb1fe0a3661c44581ba5b43c2a3d5af23794
mapping.h                                6cc8c40cb885d65d04f24cae2674d707bfcfd23e
mapping.h                                acd5e56c6b7da96193a94370ae715735020605ec
mapping.h                                bfbe9209ffc6b8e040073724fc674a36a6c5af4c
microkit.h                               7f81f60ebda3d07c8bcfbf83d61afd7d51e6c673
objecttype.h                             1938f6b77bfd813511f3243bd0b83c30ef9999c4
objecttype.h                             77f4fc66c7aeb4b8260110e29e31c5c555b7ad91
objecttype.h                             b39a887261ab426b049942f3e0548eef2d65b7fe
objecttype.h                             ba77e3da18fadb2406c3aaf2abc8afd35eb0b164
objecttype.h                             c351e03d484dbaf325e1dd94fdb28df20a8b809e
sel4_client.h                            4e873bfe0250b0e92a1fd4db6b94e406fc76427a
sel4_client.h                            dfbb5fbdeb85f794adf4d5a41174210c8ec4abd3
sel4.h                                   2bb10765d3be36ab10b2e2af40ee255aa5f5fa3b
shared_types_gen.h                       3b1f3f60d7fe71742141a7013c01c32507bf6b7e
shared_types.h                           9235eeeef2ca731c23fc7328ac77b2fad4ea087d
shared_types.h                           a4837e9359476da2003a1abbff99c91b09ed11df
simple_types.h                           0279a42cb0044027c7c9d27aa394d2739e9bf412
simple_types.h                           a3593ef984ad7efcf13d52853bf035861304e516
simple_types.h                           b6c742758ffdeb48fa2a60287cffe5f27b1264a7
syscall.h                                a01378fe41eb3a789d5a5550cb2cde43904ef04a
syscalls.h                               2a10213055f2e413fac228998c1becf39c93e190
syscalls.h                               52e434e4898727360b503a4b585d85bcab49a147
syscalls.h                               776d2d41a42d032e0d1607ca2a671b70a48162cc
syscalls.h                               ccd2691a304cc1fecf59692d15639fbd2eb8dff2
syscalls.h                               e487bfd2f1d4dc8b5ace6695b46cc2ad46f3f84c
syscalls_master.h                        8f7469c948cdd33867b28b43a2b7865a68735193
syscalls_mcs.h                           498096db663311db682f22e8b19a4207438846f6
types_gen.h                              2435c37a5133690036dbb7548744dc9f9bfe19bd
types_gen.h                              26e25b151fce1a4b2b3f450c402b44cfdba77d56
types_gen.h                              62c2f6ff21331e7f4f1f4fcba6877f177b2e700b
types_gen.h                              72713ee778b218eb8289a562806e9d28ea80973c
types.h                                  116716552dbd499e80c2bf565afe5861a5902fa5
types.h                                  64ba618afaa5e96d6d394b2e825355b8008e0fc2
types.h                                  8ab5527676d1cffdb9f64c2426c9c123824b40ef
types.h                                  c40e2cc5447a8ed65e62e8c9417573c76c3e7825
types.h                                  d3450f9f155381850270caa1d7d1953fd8b406e9
types.h                                  d9b5b7a47547bcc35f35bd274d1ea92cabeef8f8
virtual_client.h                         114925187c5e752421611db17bcef6e9fcb4be2c

Answer 2 · 2024-05-30T00:47:31.000Z

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.

Answer 3 · 2024-05-30T17:06:02.000Z

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.

Answer 4 · 2024-05-30T17:56:36.000Z

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 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).

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.

Answer 5 · 2024-05-30T18:58:50.000Z

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 #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!

Answer 6 · 2024-05-30T19:03:08.000Z

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.

Answer 7 · 2024-05-30T19:09:53.000Z

@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 indygreg/PyOxidizer#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 !

Answer 8 · 2024-05-30T19:22:48.000Z

PyOxidizer is gone: #126.

Answer 9 · 2024-05-30T23:12:49.000Z

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.

Answer 10 · 2024-05-31T15:22:21.000Z

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.

Answer 11 · 2024-05-31T21:55:15.000Z

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.

[1] https://github.com/rust-lang/cargo/blob/9ba3894b16a60981c3155a32f40bd9df6d719d34/src/cargo/core/compiler/mod.rs#L1184

Answer 12 · 2024-06-11T09:17:23.000Z

I'm going to close this because I think that the original issue is resolved because the rust-seL4 project can be used.

Answer 13 · 2024-06-11T09:17:41.000Z

Feel free to re-open if I'm wrong.

Answer 14 · 2024-06-12T10:08:08.000Z

@Ivan-Velickovic Is there at least a chance to get away from the 69 different set of header files?

Answer 15 · 2024-06-13T03:17:30.000Z

@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.