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,
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!
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