Make `static inline` optional

[wucke13]

Currently, most of the microkit API is defined static inline. This is nice for lean binaries and good performance, but not so nice for bindings to other programming languages. The reason is as follows:

When all functions were already pre-compiled into libmicrokit.a, then one just needs to match their ABI and link libmicrokit.a to call them.

However as things stand right now, one needs to grab a (cross-compiler) c toolchain, manually write header file that contains all static inline functions but with static inline removed, compile that into a static archive and link it. The big denominator is having to have (and run!) a C-cross-compilation toolchain.

Now here I'm not 100% sure, but I would expect that a nice path in between could be found:

• Put the static inline through a macro
• Make that macro opt-out, e.g. its on per default, but can be disabled
• Compile libmicrokit.a without static inline

From this I would hope for the following behavior:

• When a normal C developer uses the header file, nothing changes. static inline makes all the symbols static to the current compilation unit.
• However, when someone (for example to build Rust bindings) parses the header file to generate a FFI, they can static inline using a macro define and thus get all the unspoiled function declarations. When linking with libmicrokit.a, implementation for the functions is found.

If this does not work (i.e. this creates collisions during linking), one could of course always just compile a libmicrokit.a and libmicrokit_fat.a, where the latter is with all the functions (static inline removed).

[Ivan-Velickovic]

I'll have to think about it some more but my initial thoughts are that we probably do not want to do this.

Given how small the libmicrokit header is, and that is mainly wrappers over seL4 system calls, I think it is okay to reproduce it for languages if necessary (as mentioned here before https://github.com/seL4/microkit/issues/8#issuecomment-1274175449).

The friction with static inline depends on the language. For example, we have used Zig just fine without any installed C toolchain and the existing libmicrokit, so it does depend on the language.

Since the Rust bindings do already exist, I think we would need this problem to come up with a number of languages being used with Microkit to implement a non static inline libmicrokit, which right now isn't the case.

[wucke13]

@Ivan-Velickovic thank you for your response!

For example, we have used Zig just fine without any installed C toolchain and the existing libmicrokit, so it does depend on the language.

I don't want to sound harsh, but this is quite likely the most useless example you could have brought on. Zig has an incredible good cross-compilation story, and zig contains a fully working C frontend (which at least in the past was implemented by having most of a clang among other things under the hood). So of course the best-in-class cross-compiler-on-steroids made for C interop works with a C header.

My personal interest in this of course was Rust motivated, and reading about your recent work on this solves the issue for me. Still I think the C-ABI is the defacto quasi standard of FFIs, and static inline significantly complicates things when using it. I'm indifferent on whether to close this issue or not, my need is (and was unknowingly to me previously) covered, but the issue itself remains as is (modulo the example use-case I picked).

[Ivan-Velickovic]

I understand that Zig is perhaps an outlier, but I was just trying to show that there are systems languages that make it possible. Zig has put in the work to do it, Rust has not.

I can’t make a general statement since I don’t know enough about other systems languages, I was just trying to say that I would not want to prematurely generalise without knowing what other languages (if any) people want to use with Microkit and how they integrate with C.

[Ivan-Velickovic]

but the issue itself remains as is (modulo the example use-case I picked).

Sure, happy to keep it open until something is decided.