Specifically, many user space builds default to using -O3 which includes optimisations that increase size and inlines aggressively. -O2 tends to be much more conservative with inlining and in fact seems to not inline most libsel4 functions, even when they are declared inline.
If you are size constrained, then -O2 is usually the better choice (and can even be faster, depending on the code). Cheers, Gerwin > On 2 Jun 2026, at 11:25, Julia Vassiliki via Devel <[email protected]> wrote: > > To some extent, yes: it leaves it up to the decisions of the compiler > as to when it wants to inline functions, so depending on your optimisation > settings the compile might still choose to inline functions. And, since they > are now all publicly visible, without linker garbage collection function > definitions for the libsel4 functions which you don't use will also be > emitted. > > So, maybe. `static inline` and the default/public options are hints to the > compiler that it might choose not to obey, depending on your optimisation > settings. > > Julia > > ________________________________________ > From: Yanfeng Liu via Devel <[email protected]> > Sent: Tuesday, 2 June 2026 10:58 > To: [email protected] > Subject: [seL4] Re: libsel4 status > > Julia, > > Thanks a lot for teaching the LibSel4FunctionAttributes choice. > > Can I confirm that setting it to "public" or "default" will reduce > usage of inline and the size of programs? > > I will try them later if above understanding is correct. > > Regards, > yf > > On Sun, 2026-05-31 at 23:45 +0000, Julia Vassiliki via Devel wrote: >> 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] > > _______________________________________________ > 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] _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
