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

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... On 09/07/15 10:48, 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 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 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-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 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.