Here https://github.com/winksaville/sel4-min-sel4/tree/new-libs 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 https://github.com/winksaville/sel4-min-sel4/tree/new-libs/libs.
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
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: Herehttps://github.com/winksaville/sel4-min-sel4/tree/new-libs 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 herehttps://github.com/winksaville/sel4-min-sel4/tree/new-libs/libs.
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.systemsmailto: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.
I'll give it go.
On Mon, Jun 29, 2015, 6:21 PM Adrian Danis Adrian.Danis@nicta.com.au wrote:
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 https://github.com/winksaville/sel4-min-sel4/tree/new-libs 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 https://github.com/winksaville/sel4-min-sel4/tree/new-libs/libs.
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 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.
Hi,
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.
The asserts are really important to avoid horrible bugs when using functions created by the bitfield generator, so if we go ahead with this let's make sure they survive in some form.
Cheers, Anna.
________________________________
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.
Will do.
On Mon, Jun 29, 2015, 7:05 PM Anna Lyons Anna.Lyons@nicta.com.au wrote:
Hi,
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.
The asserts are really important to avoid horrible bugs when using functions created by the bitfield generator, so if we go ahead with this let's make sure they survive in some form.
Cheers, Anna.
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
Here https://github.com/winksaville/sel4-min-sel4/tree/no-libc3 is try #3, I've pasted the commit message below as it tells the story, let me know what you think:
libsel4 with no libc dependency.
The primary changes are introducing sel4_types.h and removing std* types plus porting assert and printf code from the kernel to libsel4. All of this means the code within libsel4 does not overload any typical libc entities. So now libsel4 uses types like seL4_Uint32 ... instead of uint32_t. And printf is now seL4_Printf and assert is seL4_Assert ....
I'm also using sel4_ prefixes for various files as I felt it was more consistent with the names of the entities within the files.
The only new library is libsel4_benchmark and since it consists of just sel4_benchmark.h we might want to move that back into libsel4. I would have liked to move out libsel4_assert, libsel4_printf and libsel4_putchar but since asserts are used by low level generated code I couldn't come up with a good way of doing that.
Finally, the only file modified that effects kernel code is kernel/tools/bitfield_gen.py. It needed to be modified as it generates files for both kernel and user space. And for user space the generated code (types_gen.h) needed to use the new types and asserts. The changes should not change what is generated for the kernel and I did a comparison of kernel_final.{c|s} before and after my change and the only differences were time stamps
-- Wink
On Mon, Jun 29, 2015 at 7:07 PM Wink Saville wink@saville.com wrote:
Will do.
On Mon, Jun 29, 2015, 7:05 PM Anna Lyons Anna.Lyons@nicta.com.au wrote:
Hi,
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.
The asserts are really important to avoid horrible bugs when using functions created by the bitfield generator, so if we go ahead with this let's make sure they survive in some form.
Cheers, Anna.
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
One other note, this isn't done. It still needs to be integrated with muslc (libc) and at a minimum seL4_Halt needs to be properly implemented. And I'm sure there will be plenty of other changes needed but I hope we're closer.
On Thu, Jul 2, 2015 at 5:11 PM Wink Saville wink@saville.com wrote:
Here https://github.com/winksaville/sel4-min-sel4/tree/no-libc3 is try #3, I've pasted the commit message below as it tells the story, let me know what you think:
libsel4 with no libc dependency. The primary changes are introducing sel4_types.h and removing std*types plus porting assert and printf code from the kernel to libsel4. All of this means the code within libsel4 does not overload any typical libc entities. So now libsel4 uses types like seL4_Uint32 ... instead of uint32_t. And printf is now seL4_Printf and assert is seL4_Assert ....
I'm also using sel4_ prefixes for various files as I felt it was more consistent with the names of the entities within the files. The only new library is libsel4_benchmark and since it consists of just sel4_benchmark.h we might want to move that back into libsel4. I would have liked to move out libsel4_assert, libsel4_printf andlibsel4_putchar but since asserts are used by low level generated code I couldn't come up with a good way of doing that.
Finally, the only file modified that effects kernel code is kernel/tools/bitfield_gen.py. It needed to be modified as it generates files for both kernel and user space. And for user space the generatedcode (types_gen.h) needed to use the new types and asserts. The changes should not change what is generated for the kernel and I did a comparison of kernel_final.{c|s} before and after my change and the only differences were time stamps
-- Wink
On Mon, Jun 29, 2015 at 7:07 PM Wink Saville wink@saville.com wrote:
Will do.
On Mon, Jun 29, 2015, 7:05 PM Anna Lyons Anna.Lyons@nicta.com.au wrote:
Hi,
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.
The asserts are really important to avoid horrible bugs when using functions created by the bitfield generator, so if we go ahead with this let's make sure they survive in some form.
Cheers, Anna.
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
Though I'm still opposed to this change overall, my two cents on the current state:
- Should we just put the benchmarking code in libsel4bench [0]? I realise the former is for benchmarking the kernel and the latter is (arguably) for benchmarking userspace, but it seems to me a better home for it.
- You've used `#pragma message` in one instance. I would prefer `#error` for consistency, though I'm aware `#pragma message` is more portable. Moreover, why are we emitting messages here in the first place? It's a perfectly valid (in fact the default) configuration to have the benchmarking syscalls disabled.
[0]: https://github.com/seL4/libsel4bench
On 03/07/15 10:19, Wink Saville wrote:
One other note, this isn't done. It still needs to be integrated with muslc (libc) and at a minimum seL4_Halt needs to be properly implemented. And I'm sure there will be plenty of other changes needed but I hope we're closer.
On Thu, Jul 2, 2015 at 5:11 PM Wink Saville <wink@saville.com mailto:wink@saville.com> wrote:
Here <https://github.com/winksaville/sel4-min-sel4/tree/no-libc3> is try #3, I've pasted the commit message below as it tells the story, let me know what you think: libsel4 with no libc dependency. The primary changes are introducing sel4_types.h and removing std* types plus porting assert and printf code from the kernel to libsel4. All of this means the code within libsel4 does not overload any typical libc entities. So now libsel4 uses types like seL4_Uint32 ... instead of uint32_t. And printf is now seL4_Printf and assert is seL4_Assert .... I'm also using sel4_ prefixes for various files as I felt it was more consistent with the names of the entities within the files. The only new library is libsel4_benchmark and since it consists of just sel4_benchmark.h we might want to move that back into libsel4. I would have liked to move out libsel4_assert, libsel4_printf and libsel4_putchar but since asserts are used by low level generated code I couldn't come up with a good way of doing that. Finally, the only file modified that effects kernel code is kernel/tools/bitfield_gen.py. It needed to be modified as it generates files for both kernel and user space. And for user space the generated code (types_gen.h) needed to use the new types and asserts. The changes should not change what is generated for the kernel and I did a comparison of kernel_final.{c|s} before and after my change and the only differences were time stamps -- Wink On Mon, Jun 29, 2015 at 7:07 PM Wink Saville <wink@saville.com <mailto:wink@saville.com>> wrote: Will do. On Mon, Jun 29, 2015, 7:05 PM Anna Lyons <Anna.Lyons@nicta.com.au <mailto:Anna.Lyons@nicta.com.au>> wrote: Hi, > > 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. > The asserts are really important to avoid horrible bugs when using functions created by the bitfield generator, so if we go ahead with this let's make sure they survive in some form. Cheers, Anna. ________________________________ 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
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.
Moving sel4_benchmark.h into libsel4 was something I was thinking we might do. I'm thinking longer maybe it could significantly expand and possibly have supporting c sources so that's why I kept it separate for now.
On using error rather than message, NP, I chose message because I didn't want to always force people to change the configuration, but maybe that would be error is better.
Some what related, I've chosen to always assume putchar would be available in some configurations, so I created sel4_debug_printf.h/sel4_debug_assert.h which uses NDEBUG to conditionally turn off/on asserts and printf. Where as sel4_printf.h/sel4_assert.h assumes putchar would always be available. So this a different behavior then previously and people may not like it.
As I said, still quite a bit to discuss and of course, the main one: is having libsel4 independent of libc something that's desirable? Which, obviously you don't think it is, but others seem to like it, so we'll see what happens. -- Wink
On Thu, Jul 2, 2015, 5:25 PM Matthew Fernandez < matthew.fernandez@nicta.com.au> wrote:
Though I'm still opposed to this change overall, my two cents on the current state:
- Should we just put the benchmarking code in libsel4bench [0]? I
realise the former is for benchmarking the kernel and the latter is (arguably) for benchmarking userspace, but it seems to me a better home for it.
- You've used `#pragma message` in one instance. I would prefer `#error`
for consistency, though I'm aware `#pragma message` is more portable. Moreover, why are we emitting messages here in the first place? It's a perfectly valid (in fact the default) configuration to have the benchmarking syscalls disabled.
On 03/07/15 10:19, Wink Saville wrote:
One other note, this isn't done. It still needs to be integrated with
muslc (libc) and at a minimum
seL4_Halt needs to be properly implemented. And I'm sure there will be
plenty of other changes
needed but I hope we're closer.
On Thu, Jul 2, 2015 at 5:11 PM Wink Saville <wink@saville.com <mailto:
wink@saville.com>> wrote:
Here <https://github.com/winksaville/sel4-min-sel4/tree/no-libc3>is try #3, I've pasted the
commit message below as it tells the story, let me know what youthink:
libsel4 with no libc dependency. The primary changes are introducing sel4_types.h and removingstd* types
plus porting assert and printf code from the kernel to libsel4.All of
this means the code within libsel4 does not overload anytypical libc
entities. So now libsel4 uses types like seL4_Uint32 ...instead of
uint32_t. And printf is now seL4_Printf and assert isseL4_Assert ....
I'm also using sel4_ prefixes for various files as I felt itwas more
consistent with the names of the entities within the files. The only new library is libsel4_benchmark and since it consistsof just
sel4_benchmark.h we might want to move that back into libsel4.I would
have liked to move out libsel4_assert, libsel4_printf andlibsel4_putchar
but since asserts are used by low level generated code Icouldn't come up
with a good way of doing that. Finally, the only file modified that effects kernel code is kernel/tools/bitfield_gen.py. It needed to be modified as itgenerates
files for both kernel and user space. And for user space thegenerated code
(types_gen.h) needed to use the new types and asserts. Thechanges should
not change what is generated for the kernel and I did acomparison of
kernel_final.{c|s} before and after my change and the onlydifferences
were time stamps -- Wink On Mon, Jun 29, 2015 at 7:07 PM Wink Saville <wink@saville.commailto:wink@saville.com> wrote:
Will do. On Mon, Jun 29, 2015, 7:05 PM Anna Lyons <Anna.Lyons@nicta.com.au
<mailto:Anna.Lyons@nicta.com.au>> wrote: Hi, > > Currently there is at least one known problem, I modified > bitfield_gen.py so types_gen.h has no asserts since atthe moment the
> kernel uses assert and userspace is libsel4_assert. Wecould either do
> something like I've done and remove them or change thekernel to use
> libsel4_assert or something else. > The asserts are really important to avoid horrible bugs whenusing
functions created by the bitfield generator, so if we goahead with this
let's make sure they survive in some form. Cheers, Anna. ________________________________ The information in this e-mail may be confidential andsubject to legal professional
privilege and/or copyright. National ICT Australia Limitedaccepts no liability for any
damage caused by this email or its attachments. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
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.
@Harry,
I'll fix the comment.
Using print_string is a good idea, I'll look into how to create a string with __FILE__, __LINE__, __func__ at compile time rather than runtime, maybe just using paste ("#") will work.
I guess my feeling is asserts should work without the user having to do extra steps, so there should be a default one in any case. Also, I believe it can be overridden at link time by the user supplying their own implementation.
On using "assert 0" to eliminate duplicate code, do you mean eliminate "_seL4_Fail" and just have "_seL4_AssertFail"?
On Thu, Jul 2, 2015 at 7:52 PM Wink Saville wink@saville.com wrote:
Moving sel4_benchmark.h into libsel4 was something I was thinking we might do. I'm thinking longer maybe it could significantly expand and possibly have supporting c sources so that's why I kept it separate for now.
On using error rather than message, NP, I chose message because I didn't want to always force people to change the configuration, but maybe that would be error is better.
Some what related, I've chosen to always assume putchar would be available in some configurations, so I created sel4_debug_printf.h/sel4_debug_assert.h which uses NDEBUG to conditionally turn off/on asserts and printf. Where as sel4_printf.h/sel4_assert.h assumes putchar would always be available. So this a different behavior then previously and people may not like it.
As I said, still quite a bit to discuss and of course, the main one: is having libsel4 independent of libc something that's desirable? Which, obviously you don't think it is, but others seem to like it, so we'll see what happens. -- Wink
On Thu, Jul 2, 2015, 5:25 PM Matthew Fernandez < matthew.fernandez@nicta.com.au> wrote:
Though I'm still opposed to this change overall, my two cents on the current state:
- Should we just put the benchmarking code in libsel4bench [0]? I
realise the former is for benchmarking the kernel and the latter is (arguably) for benchmarking userspace, but it seems to me a better home for it.
- You've used `#pragma message` in one instance. I would prefer
`#error` for consistency, though I'm aware `#pragma message` is more portable. Moreover, why are we emitting messages here in the first place? It's a perfectly valid (in fact the default) configuration to have the benchmarking syscalls disabled.
On 03/07/15 10:19, Wink Saville wrote:
One other note, this isn't done. It still needs to be integrated with
muslc (libc) and at a minimum
seL4_Halt needs to be properly implemented. And I'm sure there will be
plenty of other changes
needed but I hope we're closer.
On Thu, Jul 2, 2015 at 5:11 PM Wink Saville <wink@saville.com <mailto:
wink@saville.com>> wrote:
Here <https://github.com/winksaville/sel4-min-sel4/tree/no-libc3>is try #3, I've pasted the
commit message below as it tells the story, let me know what youthink:
libsel4 with no libc dependency. The primary changes are introducing sel4_types.h and removingstd* types
plus porting assert and printf code from the kernel tolibsel4. All of
this means the code within libsel4 does not overload anytypical libc
entities. So now libsel4 uses types like seL4_Uint32 ...instead of
uint32_t. And printf is now seL4_Printf and assert isseL4_Assert ....
I'm also using sel4_ prefixes for various files as I felt itwas more
consistent with the names of the entities within the files. The only new library is libsel4_benchmark and since itconsists of just
sel4_benchmark.h we might want to move that back into libsel4.I would
have liked to move out libsel4_assert, libsel4_printf andlibsel4_putchar
but since asserts are used by low level generated code Icouldn't come up
with a good way of doing that. Finally, the only file modified that effects kernel code is kernel/tools/bitfield_gen.py. It needed to be modified as itgenerates
files for both kernel and user space. And for user space thegenerated code
(types_gen.h) needed to use the new types and asserts. Thechanges should
not change what is generated for the kernel and I did acomparison of
kernel_final.{c|s} before and after my change and the onlydifferences
were time stamps -- Wink On Mon, Jun 29, 2015 at 7:07 PM Wink Saville <wink@saville.commailto:wink@saville.com> wrote:
Will do. On Mon, Jun 29, 2015, 7:05 PM Anna Lyons <Anna.Lyons@nicta.com.au
<mailto:Anna.Lyons@nicta.com.au>> wrote: Hi, > > Currently there is at least one known problem, I modified > bitfield_gen.py so types_gen.h has no asserts since atthe moment the
> kernel uses assert and userspace is libsel4_assert. Wecould either do
> something like I've done and remove them or change thekernel to use
> libsel4_assert or something else. > The asserts are really important to avoid horrible bugswhen using
functions created by the bitfield generator, so if we goahead with this
let's make sure they survive in some form. Cheers, Anna. ________________________________ The information in this e-mail may be confidential andsubject to legal professional
privilege and/or copyright. National ICT Australia Limitedaccepts no liability for any
damage caused by this email or its attachments. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
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.
My main problem with this change remains bringing in all of this IO implementation into the C library. As far as I can tell all of the putchar, printf, varargs, halt etc is introduced just to support assertions. Why not rely on the user system to provide the actual assertion implementation, allowing all of the I/O code to be moved out of this library?
i.e. define assert to something like
#ifdef NDEBUG #define libsel4_assert(x) (void)0 #else #define libsel4_assert(x) ((void)((x) || (__assert_fail(#x, __FILE__, __LINE__, __func__),0))) #endif void __assert_fail (const char *, const char *, int, const char *);
And then rely on the user code to provide an implementation of __assert_fail, which if they are linking against the muslc library is already provided.
Adrian
On 03/07/15 13:11, Wink Saville wrote:
@Harry,
I'll fix the comment.
Using print_string is a good idea, I'll look into how to create a string with __FILE__, __LINE__, __func__ at compile time rather than runtime, maybe just using paste ("#") will work.
I guess my feeling is asserts should work without the user having to do extra steps, so there should be a default one in any case. Also, I believe it can be overridden at link time by the user supplying their own implementation.
On using "assert 0" to eliminate duplicate code, do you mean eliminate "_seL4_Fail" and just have "_seL4_AssertFail"?
On Thu, Jul 2, 2015 at 7:52 PM Wink Saville <wink@saville.com mailto:wink@saville.com> wrote:
Moving sel4_benchmark.h into libsel4 was something I was thinking we might do. I'm thinking longer maybe it could significantly expand and possibly have supporting c sources so that's why I kept it separate for now. On using error rather than message, NP, I chose message because I didn't want to always force people to change the configuration, but maybe that would be error is better. Some what related, I've chosen to always assume putchar would be available in some configurations, so I created sel4_debug_printf.h/sel4_debug_assert.h which uses NDEBUG to conditionally turn off/on asserts and printf. Where as sel4_printf.h/sel4_assert.h assumes putchar would always be available. So this a different behavior then previously and people may not like it. As I said, still quite a bit to discuss and of course, the main one: is having libsel4 independent of libc something that's desirable? Which, obviously you don't think it is, but others seem to like it, so we'll see what happens. -- Wink On Thu, Jul 2, 2015, 5:25 PM Matthew Fernandez <matthew.fernandez@nicta.com.au <mailto:matthew.fernandez@nicta.com.au>> wrote: Though I'm still opposed to this change overall, my two cents on the current state: - Should we just put the benchmarking code in libsel4bench [0]? I realise the former is for benchmarking the kernel and the latter is (arguably) for benchmarking userspace, but it seems to me a better home for it. - You've used `#pragma message` in one instance. I would prefer `#error` for consistency, though I'm aware `#pragma message` is more portable. Moreover, why are we emitting messages here in the first place? It's a perfectly valid (in fact the default) configuration to have the benchmarking syscalls disabled. [0]: https://github.com/seL4/libsel4bench On 03/07/15 10:19, Wink Saville wrote: > One other note, this isn't done. It still needs to be integrated with muslc (libc) and at a minimum > seL4_Halt needs to be properly implemented. And I'm sure there will be plenty of other changes > needed but I hope we're closer. > > On Thu, Jul 2, 2015 at 5:11 PM Wink Saville <wink@saville.com <mailto:wink@saville.com> <mailto:wink@saville.com <mailto:wink@saville.com>>> wrote: > > Here <https://github.com/winksaville/sel4-min-sel4/tree/no-libc3> is try #3, I've pasted the > commit message below as it tells the story, let me know what you think: > > libsel4 with no libc dependency. > The primary changes are introducing sel4_types.h and removing std* types > plus porting assert and printf code from the kernel to libsel4. All of > this means the code within libsel4 does not overload any typical libc > entities. So now libsel4 uses types like seL4_Uint32 ... instead of > uint32_t. And printf is now seL4_Printf and assert is seL4_Assert .... > I'm also using sel4_ prefixes for various files as I felt it was more > consistent with the names of the entities within the files. > The only new library is libsel4_benchmark and since it consists of just > sel4_benchmark.h we might want to move that back into libsel4. I would > have liked to move out libsel4_assert, libsel4_printf and libsel4_putchar > but since asserts are used by low level generated code I couldn't come up > with a good way of doing that. > Finally, the only file modified that effects kernel code is > kernel/tools/bitfield_gen.py. It needed to be modified as it generates > files for both kernel and user space. And for user space the generated code > (types_gen.h) needed to use the new types and asserts. The changes should > not change what is generated for the kernel and I did a comparison of > kernel_final.{c|s} before and after my change and the only differences > were time stamps > > -- Wink > > On Mon, Jun 29, 2015 at 7:07 PM Wink Saville <wink@saville.com <mailto:wink@saville.com> <mailto:wink@saville.com <mailto:wink@saville.com>>> wrote: > > Will do. > > > On Mon, Jun 29, 2015, 7:05 PM Anna Lyons <Anna.Lyons@nicta.com.au <mailto:Anna.Lyons@nicta.com.au> > <mailto:Anna.Lyons@nicta.com.au <mailto:Anna.Lyons@nicta.com.au>>> wrote: > > > Hi, > > > > > 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. > > > > The asserts are really important to avoid horrible bugs when using > functions created by the bitfield generator, so if we go ahead with this > let's make sure they survive in some form. > > Cheers, > Anna. > > ________________________________ > > 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 > > > > _______________________________________________ > 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.
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Here https://github.com/winksaville/sel4-min-sel4/tree/no-libc-using-libsel4_gen is another try, there are now separate libs for printf, putchar and assert plus some new simple apps. The app myassert shows overriding of the assert methods, here is the commit message:
libsel4 without dependencies on libc.
There are now separate libs for benchmark, assert, printf and putchar:
libs/libsel4_benchmark libs/libsel4_assert libs/libsel4_printf libs/libsel4_putchar
And some simple test apps:
apps/test-newlibs -> test simple things apps/min-app -> Does nothing, just retuns 0 apps/hw -> tests putchar apps/helloworld -> tests printf apps/assert -> tests seL4_Asserts .. apps/myassert -> tests that we can override _seL4_AssertFail .. apps/bootinfo -> tests that we can access seL4_BootInfo
The primary changes are introducing sel4_types.h and removing std* types plus porting assert and IO code from the kernel to libsel4_assert and libsel4_printf, libsel4_putchar.
This means the code within libraries do not overload any typical libc entities. Instead the libraries use types like seL4_Uint32 ... instead of uint32_t. And printf is now seL4_Printf and assert is seL4_Assert ....
Finally, the only file modified that effects kernel code is kernel/tools/bitfield_gen.py. It needed to be modified as it generates files for both kernel and user space. And for user space the generated code (types_gen.h) needed to use the new types and asserts. The changes should not change what is generated for the kernel and I did a comparison of kernel_final.{c|s} before and after my change and the only differences were time stamps.
On Thu, Jul 2, 2015 at 9:47 PM Adrian Danis Adrian.Danis@nicta.com.au wrote:
My main problem with this change remains bringing in all of this IO implementation into the C library. As far as I can tell all of the putchar, printf, varargs, halt etc is introduced just to support assertions. Why not rely on the user system to provide the actual assertion implementation, allowing all of the I/O code to be moved out of this library?
i.e. define assert to something like
#ifdef NDEBUG #define libsel4_assert(x) (void)0 #else #define libsel4_assert(x) ((void)((x) || (__assert_fail(#x, __FILE__, __LINE__, __func__),0))) #endif void __assert_fail (const char *, const char *, int, const char *);
And then rely on the user code to provide an implementation of __assert_fail, which if they are linking against the muslc library is already provided.
Adrian
On 03/07/15 13:11, Wink Saville wrote:
@Harry,
I'll fix the comment.
Using print_string is a good idea, I'll look into how to create a string with __FILE__, __LINE__, __func__ at compile time rather than runtime, maybe just using paste ("#") will work.
I guess my feeling is asserts should work without the user having to do extra steps, so there should be a default one in any case. Also, I believe it can be overridden at link time by the user supplying their own implementation.
On using "assert 0" to eliminate duplicate code, do you mean eliminate "_seL4_Fail" and just have "_seL4_AssertFail"?
On Thu, Jul 2, 2015 at 7:52 PM Wink Saville wink@saville.com wrote:
Moving sel4_benchmark.h into libsel4 was something I was thinking we might do. I'm thinking longer maybe it could significantly expand and possibly have supporting c sources so that's why I kept it separate for now.
On using error rather than message, NP, I chose message because I didn't want to always force people to change the configuration, but maybe that would be error is better.
Some what related, I've chosen to always assume putchar would be available in some configurations, so I created sel4_debug_printf.h/sel4_debug_assert.h which uses NDEBUG to conditionally turn off/on asserts and printf. Where as sel4_printf.h/sel4_assert.h assumes putchar would always be available. So this a different behavior then previously and people may not like it.
As I said, still quite a bit to discuss and of course, the main one: is having libsel4 independent of libc something that's desirable? Which, obviously you don't think it is, but others seem to like it, so we'll see what happens. -- Wink
On Thu, Jul 2, 2015, 5:25 PM Matthew Fernandez < matthew.fernandez@nicta.com.au> wrote:
Though I'm still opposed to this change overall, my two cents on the current state:
- Should we just put the benchmarking code in libsel4bench [0]? I
realise the former is for benchmarking the kernel and the latter is (arguably) for benchmarking userspace, but it seems to me a better home for it.
- You've used `#pragma message` in one instance. I would prefer
`#error` for consistency, though I'm aware `#pragma message` is more portable. Moreover, why are we emitting messages here in the first place? It's a perfectly valid (in fact the default) configuration to have the benchmarking syscalls disabled.
On 03/07/15 10:19, Wink Saville wrote:
One other note, this isn't done. It still needs to be integrated with
muslc (libc) and at a minimum
seL4_Halt needs to be properly implemented. And I'm sure there will be
plenty of other changes
needed but I hope we're closer.
On Thu, Jul 2, 2015 at 5:11 PM Wink Saville <wink@saville.com <mailto:
wink@saville.com>> wrote:
Here <https://github.com/winksaville/sel4-min-sel4/tree/no-libc3>is try #3, I've pasted the
commit message below as it tells the story, let me know what youthink:
libsel4 with no libc dependency. The primary changes are introducing sel4_types.h and removingstd* types
plus porting assert and printf code from the kernel tolibsel4. All of
this means the code within libsel4 does not overload anytypical libc
entities. So now libsel4 uses types like seL4_Uint32 ...instead of
uint32_t. And printf is now seL4_Printf and assert isseL4_Assert ....
I'm also using sel4_ prefixes for various files as I felt itwas more
consistent with the names of the entities within the files. The only new library is libsel4_benchmark and since itconsists of just
sel4_benchmark.h we might want to move that back intolibsel4. I would
have liked to move out libsel4_assert, libsel4_printf andlibsel4_putchar
but since asserts are used by low level generated code Icouldn't come up
with a good way of doing that. Finally, the only file modified that effects kernel code is kernel/tools/bitfield_gen.py. It needed to be modified as itgenerates
files for both kernel and user space. And for user space thegenerated code
(types_gen.h) needed to use the new types and asserts. Thechanges should
not change what is generated for the kernel and I did acomparison of
kernel_final.{c|s} before and after my change and the onlydifferences
were time stamps -- Wink On Mon, Jun 29, 2015 at 7:07 PM Wink Saville <wink@saville.commailto:wink@saville.com> wrote:
Will do. On Mon, Jun 29, 2015, 7:05 PM Anna Lyons <Anna.Lyons@nicta.com.au
<mailto:Anna.Lyons@nicta.com.au>> wrote: Hi, > > Currently there is at least one known problem, Imodified
> bitfield_gen.py so types_gen.h has no asserts since atthe moment the
> kernel uses assert and userspace is libsel4_assert. Wecould either do
> something like I've done and remove them or change thekernel to use
> libsel4_assert or something else. > The asserts are really important to avoid horrible bugswhen using
functions created by the bitfield generator, so if we goahead with this
let's make sure they survive in some form. Cheers, Anna. ________________________________ The information in this e-mail may be confidential andsubject to legal professional
privilege and/or copyright. National ICT Australia Limitedaccepts no liability for any
damage caused by this email or its attachments. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
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.
Devel mailing listDevel@sel4.systemshttps://sel4.systems/lists/listinfo/devel
Whoops, here https://github.com/winksaville/sel4-min-sel4/tree/no-libc-dependency is the correct link, the link in the previous message was older.
On Fri, Jul 3, 2015 at 3:39 PM Wink Saville wink@saville.com wrote:
Here https://github.com/winksaville/sel4-min-sel4/tree/no-libc-using-libsel4_gen is another try, there are now separate libs for printf, putchar and assert plus some new simple apps. The app myassert shows overriding of the assert methods, here is the commit message:
libsel4 without dependencies on libc. There are now separate libs for benchmark, assert, printf and putchar: libs/libsel4_benchmark libs/libsel4_assert libs/libsel4_printf libs/libsel4_putchar And some simple test apps: apps/test-newlibs -> test simple things apps/min-app -> Does nothing, just retuns 0 apps/hw -> tests putchar apps/helloworld -> tests printf apps/assert -> tests seL4_Asserts .. apps/myassert -> tests that we can override _seL4_AssertFail .. apps/bootinfo -> tests that we can access seL4_BootInfo The primary changes are introducing sel4_types.h and removing std*types plus porting assert and IO code from the kernel to libsel4_assert and libsel4_printf, libsel4_putchar.
This means the code within libraries do not overload any typical libc entities. Instead the libraries use types like seL4_Uint32 ... insteadof uint32_t. And printf is now seL4_Printf and assert is seL4_Assert ....
Finally, the only file modified that effects kernel code is kernel/tools/bitfield_gen.py. It needed to be modified as it generates files for both kernel and user space. And for user space the generatedcode (types_gen.h) needed to use the new types and asserts. The changes should not change what is generated for the kernel and I did a comparison of kernel_final.{c|s} before and after my change and the only differences were time stamps.
On Thu, Jul 2, 2015 at 9:47 PM Adrian Danis Adrian.Danis@nicta.com.au wrote:
My main problem with this change remains bringing in all of this IO implementation into the C library. As far as I can tell all of the putchar, printf, varargs, halt etc is introduced just to support assertions. Why not rely on the user system to provide the actual assertion implementation, allowing all of the I/O code to be moved out of this library?
i.e. define assert to something like
#ifdef NDEBUG #define libsel4_assert(x) (void)0 #else #define libsel4_assert(x) ((void)((x) || (__assert_fail(#x, __FILE__, __LINE__, __func__),0))) #endif void __assert_fail (const char *, const char *, int, const char *);
And then rely on the user code to provide an implementation of __assert_fail, which if they are linking against the muslc library is already provided.
Adrian
On 03/07/15 13:11, Wink Saville wrote:
@Harry,
I'll fix the comment.
Using print_string is a good idea, I'll look into how to create a string with __FILE__, __LINE__, __func__ at compile time rather than runtime, maybe just using paste ("#") will work.
I guess my feeling is asserts should work without the user having to do extra steps, so there should be a default one in any case. Also, I believe it can be overridden at link time by the user supplying their own implementation.
On using "assert 0" to eliminate duplicate code, do you mean eliminate "_seL4_Fail" and just have "_seL4_AssertFail"?
On Thu, Jul 2, 2015 at 7:52 PM Wink Saville wink@saville.com wrote:
Moving sel4_benchmark.h into libsel4 was something I was thinking we might do. I'm thinking longer maybe it could significantly expand and possibly have supporting c sources so that's why I kept it separate for now.
On using error rather than message, NP, I chose message because I didn't want to always force people to change the configuration, but maybe that would be error is better.
Some what related, I've chosen to always assume putchar would be available in some configurations, so I created sel4_debug_printf.h/sel4_debug_assert.h which uses NDEBUG to conditionally turn off/on asserts and printf. Where as sel4_printf.h/sel4_assert.h assumes putchar would always be available. So this a different behavior then previously and people may not like it.
As I said, still quite a bit to discuss and of course, the main one: is having libsel4 independent of libc something that's desirable? Which, obviously you don't think it is, but others seem to like it, so we'll see what happens. -- Wink
On Thu, Jul 2, 2015, 5:25 PM Matthew Fernandez < matthew.fernandez@nicta.com.au> wrote:
Though I'm still opposed to this change overall, my two cents on the current state:
- Should we just put the benchmarking code in libsel4bench [0]? I
realise the former is for benchmarking the kernel and the latter is (arguably) for benchmarking userspace, but it seems to me a better home for it.
- You've used `#pragma message` in one instance. I would prefer
`#error` for consistency, though I'm aware `#pragma message` is more portable. Moreover, why are we emitting messages here in the first place? It's a perfectly valid (in fact the default) configuration to have the benchmarking syscalls disabled.
On 03/07/15 10:19, Wink Saville wrote:
One other note, this isn't done. It still needs to be integrated with
muslc (libc) and at a minimum
seL4_Halt needs to be properly implemented. And I'm sure there will
be plenty of other changes
needed but I hope we're closer.
On Thu, Jul 2, 2015 at 5:11 PM Wink Saville <wink@saville.com
mailto:wink@saville.com> wrote:
Here <https://github.com/winksaville/sel4-min-sel4/tree/no-libc3>is try #3, I've pasted the
commit message below as it tells the story, let me know what youthink:
libsel4 with no libc dependency. The primary changes are introducing sel4_types.h andremoving std* types
plus porting assert and printf code from the kernel tolibsel4. All of
this means the code within libsel4 does not overload anytypical libc
entities. So now libsel4 uses types like seL4_Uint32 ...instead of
uint32_t. And printf is now seL4_Printf and assert isseL4_Assert ....
I'm also using sel4_ prefixes for various files as I felt itwas more
consistent with the names of the entities within the files. The only new library is libsel4_benchmark and since itconsists of just
sel4_benchmark.h we might want to move that back intolibsel4. I would
have liked to move out libsel4_assert, libsel4_printf andlibsel4_putchar
but since asserts are used by low level generated code Icouldn't come up
with a good way of doing that. Finally, the only file modified that effects kernel code is kernel/tools/bitfield_gen.py. It needed to be modified as itgenerates
files for both kernel and user space. And for user space thegenerated code
(types_gen.h) needed to use the new types and asserts. Thechanges should
not change what is generated for the kernel and I did acomparison of
kernel_final.{c|s} before and after my change and the onlydifferences
were time stamps -- Wink On Mon, Jun 29, 2015 at 7:07 PM Wink Saville <wink@saville.commailto:wink@saville.com> wrote:
Will do. On Mon, Jun 29, 2015, 7:05 PM Anna Lyons <Anna.Lyons@nicta.com.au
<mailto:Anna.Lyons@nicta.com.au>> wrote: Hi, > > Currently there is at least one known problem, Imodified
> bitfield_gen.py so types_gen.h has no asserts since atthe moment the
> kernel uses assert and userspace is libsel4_assert. Wecould either do
> something like I've done and remove them or change thekernel to use
> libsel4_assert or something else. > The asserts are really important to avoid horrible bugswhen using
functions created by the bitfield generator, so if we goahead with this
let's make sure they survive in some form. Cheers, Anna. ________________________________ The information in this e-mail may be confidential andsubject to legal professional
privilege and/or copyright. National ICT AustraliaLimited 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
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.
Devel mailing listDevel@sel4.systemshttps://sel4.systems/lists/listinfo/devel
-
Adrian Danis -
Anna Lyons -
Matthew Fernandez -
Wink Saville