?Hey Andrew,
Sorry I took so long to get back to you: we have a benchmarking suite, seL4Bench (https://github.com/seL4/sel4bench/blob/master/apps/ipc/src/main.c), which should have userspace timers and precise timestamps available for most platforms. As I understand, you will just have to write a new microbenchmark of your own, and import your library, and then insert calls to the relevant timestamp counter functions (https://wiki.sel4.systems/Benchmarking%20guide)?
Kofi Doku Atuah
Kernel engineer
DATA61 | CSIRO
E kofidoku.atuah@data61.csiro.au
www.data61.csiro.au
CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61
________________________________
From: Devel