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)​