Enable benchmarking tools on SEL4
Hi, I am going to measure the resource consumption of process on SEL4 and I found the tutorial here: https://docs.sel4.systems/BenchmarkingGuide.html One thing I am confused about is how to enable the benchmark feature shown below: "This feature can be enabled from the menuconfig list (seL4 Kernel > Enable benchmarks > Track threads and kernel CPU utilisation time)." It seems like there should be a file "menuconfig" or some other similar object I can modify. But I cannot find such an object. I would appreciate if you could give me any suggestions. Thank you! Best, Zhonghao
Hi Zhonghao,
Some of the information on that page is somewhat out of date, as we've since moved from a Kconfig/Kbuild build system to a CMake-based build system. So to enable the benchmarks, you would first have to 'cd' into your build directory where you once called the 'init-build.sh' or 'griddle' script. Then using 'ccmake' or similar, change the 'KernelBenchmarks' config option to either: 'generic', 'track_kernel_entries', 'tracepoints', or 'track_utilisation', depending on whatever you wish to benchmark. Sorry for any inconveniences, we'll update the page within a day or two. Sincerely, Damon
participants (2)
-
Lee, Damon (Data61, Kensington NSW) -
Zhonghao Liao