I like some things about this split, and dislike others. Mostly I think you're splitting on the wrong boundaries. I would prefer something more like the following

libsel4 - This should contain all of the information for system binding. This means most of what you have in libsel4_gen, and the bootinfo header you put in libsel4_bootinfo. What I would not include is any std[int|def|bool|arg] and instead use different type names, perhaps something like sel4_uint8_t, to prevent type collisions. This should result in the minimal library that is just the seL4 syscall ABI, with no dependencies on a libc but also with no definitions that will collide with an actual libc.

libsel4_support - A collection of helpful routines on top of libsel4. This would be what is in libsel4_benchmark and the rest of libsel4_bootinfo

libsel4_rootserver - Minimal libc-like implementations and start routines

I would see libsel4 and libsel4_support being included with the kernel, much like the current libsel4, and then libsel4_rootserver being a separate, and potentially one of many, libraries for defining a minimal operating environment.

Hopefully this actually makes sense and I haven't overlooked something obvious.

Adrian

On 29/06/15 15:48, Wink Saville wrote:

Here is a different approach for removing the libc dependency, it seemed like people thought libsel4 was to big and that as part of the effort of breaking the dependency it should be made smaller. Basically libsel4 does nothing expect satisfy dependency needed for the kernel for some xml files. And I've broken libsel4 into basically 8 other libraries. see here.

This maybe taking things to far, but it does mean people can use only what they need, which I like. The smallest example is app/min-hw which only uses libsel4_gen, libsel4_startup. libsel4_bootinfo and libsel4_putchar. At the other extreme apps/test-newlibs uses everything. Anyway other organizations are certainly possible.

Currently there is at least one known problem, I modified bitfield_gen.py so types_gen.h has no asserts since at the moment the kernel uses assert and userspace is libsel4_assert. We could either do something like I've done and remove them or change the kernel to use libsel4_assert or something else.

Anyway, before creating a pull request I'd like to know what people think.

-- Wink

_______________________________________________
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.