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 < [email protected]> 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 <[email protected] <mailto: > [email protected]>> 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 <[email protected] > <mailto:[email protected]>> wrote: > > > > Will do. > > > > > > On Mon, Jun 29, 2015, 7:05 PM Anna Lyons < > [email protected] > > <mailto:[email protected]>> 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 > > [email protected] > > https://sel4.systems/lists/listinfo/devel > > > > > > > > _______________________________________________ > > Devel mailing list > > [email protected] > > 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 [email protected] https://sel4.systems/lists/listinfo/devel
