[seL4] seL4 System Utilization / Benchmark

Hi,

I'm interested in seeing how much of the CPU is being used by the various threads in my (camkes) application. I'd like a simple "Task Manager" style report of the form:

70% idle 25% can_obj_7_0_control_9_tcb 5% can_obj_7_Int_3_0000_tcb 0% can_obj_7_0_fault_handler_15_0000_tcb etc

I've tried poking around libsel4bench, but I don't see any obvious way of benchmarking the whole system. From what I can tell, it's mostly designed to get cycle counts from specific code segments. Is that right? What's the best way to go about benchmarking the whole system? It's only for debugging, so I'm willing to make some quick-and-dirty changes to the kernel just to see the results.

Thanks, Andrew