Hi yf, libsel4 code packaged as part of the seL4 repo is for production, yes. It is used by all downstream projects that I know of.
You can configure inline-ness of the libsel4 functions using the `LibSel4FunctionAttributes` cmake configure option: https://github.com/seL4/seL4/blob/15.0.0/libsel4/CMakeLists.txt In our use, we haven't seen excessive code bloat from inline functions, however, and generally I'd expect for these sorts of small functions it would not make much of a difference. When inclined on Aarch64, my experience is that an seL4_Signal will only take a few instructions. Are you running into code bloat issues from the inline functions (i.e. is there some case where this isn't true?), or is this hypothetical/preference? Julia ________________________________ From: Yanfeng Liu via Devel <[email protected]> Sent: Saturday, May 30, 2026 1:56:57 PM To: [email protected] <[email protected]> Subject: [seL4] libsel4 status Dear experts, It seems that currently libsel4 has many inlined functions thus user space code size is large. I am wondering if this is really necessary? If current libsel4 is not for production use, then it doesnt matter. Otherwise I am wondering if we need support size optimized config as well? I am hoping that libsel4 changes wont affect kernel verification? Regards, yf _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected] This email and any files transmitted with it may contain confidential information. If you believe you have received this email or any of its contents in error, please notify me immediately by return email and destroy this email. Do not use, disseminate, forward, print or copy any contents of an email received in error. _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
