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

Thanks for your time reviewing! Quick question: Which Kconfig and Makefile for the first two bullet points? Your absolutely right on CompileTimeAssert, I'll remove DebugCompileTimeAssert. On Wed, Jul 8, 2015 at 5:48 PM Adrian Danis wrote:

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 they should always be tested, 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 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 concern. I originall defined __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 see here 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 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 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-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

_______________________________________________ Devel mailing listDevel@sel4.systemshttps://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.