Hi Norrathep,

What sort of benchmarking would you like to do?

libsel4bench: https://github.com/seL4/seL4_libs/tree/master/libsel4bench provides primitives for reading cycle counters etc.

For benchmarking inside the kernel itself, we have some minimal support for adding trace points in this file: https://github.com/seL4/seL4/blob/master/include/benchmark.h

In the next few weeks we'll be releasing the seL4 benchmarking suite.

Thanks, Anna.

Anna Lyons Kernel engineer / PhD Student DATA61 | CSIRO E anna.lyons@nicta.com.aumailto:kevin.elphinstone@nicta.com.au www.data61.csiro.auhttp://www.data61.csiro.au

CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61

On 24/03/2016 9:49 am, Norrathep Rattanavipanon wrote: Hello,

What's the best way to benchmark my program inside sel4? I saw wiki page about running sel4 bench (https://wiki.sel4.systems/Benchmarking%20guidehttps://wiki.sel4.systems/Benchmarking%20guide) but it wasnt filled yet. So I wonder if there's any public guide or tutorial on that?

I also found this https://github.com/seL4/libplatsupport/blob/master/arch_include/x86/platsupp... and tried both rdtsc_pure and rdtsc_cpuid but neither of them seems to produce reliable results.

Best,

-- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

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