Re: [seL4] Streamline seL4/libsel4 and make it not depend on libc

I've addressed the comments from both Matthew and Adrian. https://github.com/winksaville/seL4/tree/libsel4-no-libc-dependency I've made the change for seL4_CompileTimeAssert to incorporate the extern of compile_time_assert style. I used just the "no _Static_assert" path for now and didn't define _Static_assert to keep things simple. We should consider only having one version. Also, for now I've left in the declaration of __assert_fail, since that seems "better" to me. But I'm certainly not strong on that decision and will do whatever people want. -- Wink On Wed, Jul 8, 2015 at 7:34 PM Wink Saville wrote:

Working on Mattew's suggestion too.

On Wed, Jul 8, 2015 at 6:17 PM Matthew Fernandez < matthew.fernandez@nicta.com.au> wrote:

...

I feel like I'm fighting a losing battle, so I'll stop objecting to this change wholesale ;) but just some nitpicks of my own... By the way, is there an open PR for this so we can comment inline?

* The changes you've made to syscall_stub_gen.py seem to indicate that you expect this to be run in two environments, "sel4" and "libsel4." By their names, I would guess these are the kernel and userspace, respectively. However, as far as I'm aware, this script is only used for generating userspace stubs. Have I misunderstood the purpose of this? These changes are also a bit messy, leaving existing code in place but commented out.

* You remove the following comment from types.h: "/* seL4_ARM_PageCacheable | seL4_ARM_ParityEnabled */" Looking at this comment, I think it's on the wrong line (should pertain to seL4_ARM_Default_VMAttributes), but it shouldn't be removed. I think it must have been bumped accidentally during a previous merge.

* You change the header guards on benchmark.h. Why?

* Does __assert_fail even need to be prototyped? It looks like the only things that refer to it are conditionally defined macros. The alternatives of (a) prototyping it and expecting it to be provided externally or (b) not prototyping it at all both seem a bit fraught. I'm unsure which is preferable.

* Your definition of a compile-time assertion uses a typedef. I realise this matches the kernel's definition, but in the systems I build I found this did not reliably trigger a compiler error on failure. This was my motivation for modifying libutils' compile-time assertion [0] to be an extern declaration. I found this to be more reliable in practice. What are other people's thoughts/experiences about this?

* You define the STR_JOIN macro which never seems to be used. Oversight?

* The usage information you've added to syscall_stub_gen.py indicates -e is an alias for --environment, which it isn't.

[0]: https://github.com/seL4/libutils/blob/master/include/utils/compile_time.h#L3...

...

Hi Wink,

Change is looking good. Now I just have a couple of minor nitpicks that I might as well mention now before you try and do a pull request * In Kconfig you change 'default y' to 'default n', why? * There are changes to the Makefile to add arch .c files as well as .S files, I believe these are now all gone from the change again? * There is no reason to have a distinction between a CompileTimeAssert and a DebugCompileTimeAssert. Compile time asserts add no run time over head or memory overhead, so

...

regardless of debug mode or not

Everything else looks good to me.

Regarding __assert_fail, I'm fine with it being an 'int' for now. We can change it in the future, but given line counts should stay <2^31 this shouldn't cause any

On 09/07/15 10:48, Adrian Danis wrote: they should always be tested, problems.

...

Adrian

On 08/07/15 10:42, Wink Saville wrote:

...

Adrian,

I've attempted to address all of your comments but I have one small

...

...

__assert_fail in libs/libsel4/include/sel4/assert.h as with line as an unsigned int:

void __assert_fail(const char* str, const char* file, unsigned int line, const char* function);

But in libs/libmuslc/include/assert.h its a "regular" int:

void __assert_fail (const char *, const char *, int, const char *);

So I had to change it so as not to get a compile error. I'd chosen unsigned int because that's how it was in the kernel and looking on the internet I seehere < http://refspecs.linuxbase.org/LSB_3.1.1/LSB-Core-generic/LSB-Core-generic/ba... ,in the linux documentation, its also unsigned int. Hence, this could be

concern. I originall defined problematic in the future, so

...

...

we may want to make it __sel4_assert_fail or some such, your call.

-- Wink

https://github.com/winksaville/seL4/tree/libsel4-no-libc-dependency

https://github.com/winksaville/libsel4test/tree/libsel4-no-libc-dependency

...

https://github.com/winksaville/libsel4allocman/tree/libsel4-no-libc-dependen...

...

https://github.com/winksaville/libsel4utils/tree/libsel4-no-libc-dependency

...

https://github.com/winksaville/sel4test/tree/libsel4-no-libc-dependency

...

https://github.com/winksaville/libsel4assert https://github.com/winksaville/libsel4benchmark https://github.com/winksaville/libsel4printf https://github.com/winksaville/libsel4putchar https://github.com/winksaville/libsel4startstop

On Tue, Jul 7, 2015 at 1:39 AM Adrian Danis mailto:Adrian.Danis@nicta.com.au> wrote:

Hi Wink,

I started reading the commit to the kernel ( https://github.com/winksaville/seL4/commit/c25d8e1af9126e242e220164e30a5ef6c...) and I liked a lot of it, but I still have a few comments.

* You appear to have added several files to the top level of the include directory and prefixed them with 'sel4_' to try and prevent header name

collisions. Why not put them in the >> 'sel4' subdirectory like we already do (here and in all our other libraries)? In doing this >> you have left headers, for backwards compatibility I assume, in the sel4 directory that then >> include new ones in the top level directory. This all makes no sense to me. >> * I still do not like the way you are implementing assert. In my last e-mail I said to define >> libsel4_assert to __assert_fail and then let the application be responsible for providing >> __assert_fail. The main motivation for doing this is that in the case that you *are* using a C >> library you need to do nothing to handle this change, as it will have a link time >> implementation of __assert_fail. >> * Why is there a prototype for halt in libsel4? It seems to exist because it is referenced by >> your libsel4_start routines. Neither of these should be in libsel4 >> * I do not mind a definition of NULL in libsel4, but you seem to have renamed all the uses of >> NULL->seL4_NULL and then left the definition of NULL in sel4_simple_types.h anyway. Either use >> define NULL or seL4_NULL, not both >> * sel4_vargs.h seems to be left over from some previous attempt at this change, but I don't >> see it referenced anywhere in libsel4 itself >> >> The rest of the changes all good, including the syscall_stub_gen and bitfield_gen changes. >> >> What I would keep in mind with this change is that I would hope that applications that do use >> a C library to require zero modifications with this change. >> >> Adrian >> >> >> On 07/07/15 18:13, Wink Saville wrote: >>> I've got sel4test running with libsel4 not having a dependency on libc. I've pulled out >>> libsel4assert, libsel4benchmark, libsel4printf and libsel4putchar from libsel4 and they are >>> separate libraries >>> >>> The biggest change is to seL4/libsel4 and sel4/tools/bitfield_gen.py. The changes to >>> bitfield_gen.py allow it to generate the same code as before for the kernel but uses the new >>> names for entities in user space. >>> >>> Please let me know what you think. >>> >>> -- Wink >>> >>> >>> https://github.com/winksaville/seL4/tree/libsel4-no-libc-dependency >>> https://github.com/winksaville/libsel4test/tree/libsel4-no-libc-dependency >>> https://github.com/winksaville/libsel4allocman/tree/libsel4-no-libc-dependency >>> https://github.com/winksaville/libsel4utils/tree/libsel4-no-libc-dependency >>> https://github.com/winksaville/sel4test/tree/libsel4-no-libc-dependency >>> https://github.com/winksaville/libsel4assert >>> https://github.com/winksaville/libsel4benchmark >>> https://github.com/winksaville/libsel4printf >>> https://github.com/winksaville/libsel4putchar >>> >>> >>> >>> _______________________________________________ >>> Devel mailing list >>> Devel@sel4.systems <mailto:Devel@sel4.systems> >>> https://sel4.systems/lists/listinfo/devel >> >> >> ---------------------------------------------------------------------------------------------------- >> >> The information in this e-mail may be confidential and subject to legal professional privilege >> and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by >> this email or its attachments. >> > > > > _______________________________________________ > Devel mailing list > Devel@sel4.systems > https://sel4.systems/lists/listinfo/devel >

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.