JSON kernel config output

seL4 kernel
1

After the hangout, I decided to do a little prototyping: Add json file with config values by ahmedcharles · Pull Request #893 · seL4/seL4 · GitHub

Edit: I went with having all defined values as strings because trying to make numbers work would have potential fidelity issues with floating point.

Discuss.

Example output, kernel/gen_config.json:

{
  "AARCH64_SERROR_IGNORE" : null,
  "ARCH" : "x86",
  "ARCH_AARCH32" : null,
  "ARCH_AARCH64" : null,
  "ARCH_ARM_HYP" : null,
  "ARCH_ARM_V7A" : null,
  "ARCH_ARM_V7VE" : null,
  "ARCH_ARM_V8A" : null,
  "ARCH_IA32" : null,
  "ARCH_RISCV32" : null,
  "ARCH_RISCV64" : null,
  "ARCH_X86" : "1",
  "ARCH_X86_64" : "1",
  "ARCH_X86_BROADWELL" : null,
  "ARCH_X86_GENERIC" : null,
  "ARCH_X86_HASWELL" : null,
  "ARCH_X86_IVY" : null,
  "ARCH_X86_NEHALEM" : "1",
  "ARCH_X86_SANDY" : null,
  "ARCH_X86_SKYLAKE" : null,
  "ARCH_X86_WESTMERE" : null,
  "ARM_CORTEX_A15" : null,
  "ARM_CORTEX_A35" : null,
  "ARM_CORTEX_A53" : null,
  "ARM_CORTEX_A55" : null,
  "ARM_CORTEX_A57" : null,
  "ARM_CORTEX_A7" : null,
  "ARM_CORTEX_A72" : null,
  "ARM_CORTEX_A8" : null,
  "ARM_CORTEX_A9" : null,
  "ARM_HIKEY_OUTSTANDING_PREFETCHERS" : "0",
  "ARM_HIKEY_PREFETCHER_NPFSTRM" : "0",
  "ARM_HIKEY_PREFETCHER_STBPFDIS" : null,
  "ARM_HIKEY_PREFETCHER_STBPFRS" : null,
  "ARM_HIKEY_PREFETCHER_STRIDE" : "0",
  "ARM_SMMU" : null,
  "BENCHMARK_GENERIC" : null,
  "BENCHMARK_TRACEPOINTS" : null,
  "BENCHMARK_TRACK_KERNEL_ENTRIES" : null,
  "BENCHMARK_TRACK_UTILISATION" : null,
  "BINARY_VERIFICATION_BUILD" : null,
  "BOOT_THREAD_TIME_SLICE" : "5",
  "CACHE_LN_SZ" : "64",
  "CLZ_32" : null,
  "CLZ_64" : null,
  "CLZ_NO_BUILTIN" : null,
  "COLOUR_PRINTING" : null,
  "CTZ_32" : null,
  "CTZ_64" : null,
  "CTZ_NO_BUILTIN" : null,
  "DANGEROUS_CODE_INJECTION" : null,
  "DEBUG_BUILD" : null,
  "DEBUG_DISABLE_PREFETCHERS" : null,
  "ENABLE_BENCHMARKS" : null,
  "ENABLE_SMP_SUPPORT" : null,
  "EXPORT_PMC_USER" : null,
  "FASTPATH" : "1",
  "FPU_MAX_RESTORES_SINCE_SWITCH" : "64",
  "FSGSBASE_INST" : null,
  "FSGSBASE_MSR" : "1",
  "FXSAVE" : "1",
  "HARDWARE_DEBUG_API" : null,
  "HAVE_FPU" : "1",
  "HUGE_PAGE" : "1",
  "IOMMU" : null,
  "IRQ_IOAPIC" : "1",
  "IRQ_PIC" : null,
  "IRQ_REPORTING" : null,
  "KERNEL_BENCHMARK" : "none",
  "KERNEL_FSGS_BASE" : "msr",
  "KERNEL_FWHOLE_PROGRAM" : null,
  "KERNEL_INVOCATION_REPORT_ERROR_IPC" : null,
  "KERNEL_IRQ_CONTROLLER" : "IOAPIC",
  "KERNEL_LAPIC_MODE" : "XAPIC",
  "KERNEL_LOG_BUFFER" : null,
  "KERNEL_MCS" : "1",
  "KERNEL_MUTLTIBOOT_GFX_MODE" : "none",
  "KERNEL_OPTIMISATION_CLONE_FUNCTIONS" : "1",
  "KERNEL_OPT_LEVEL" : "-O2",
  "KERNEL_OPT_LEVEL_O0" : null,
  "KERNEL_OPT_LEVEL_O1" : null,
  "KERNEL_OPT_LEVEL_O2" : "1",
  "KERNEL_OPT_LEVEL_O3" : null,
  "KERNEL_OPT_LEVEL_OS" : null,
  "KERNEL_SKIM_WINDOW" : "1",
  "KERNEL_STACK_BITS" : "12",
  "KERNEL_STATIC_MAX_PERIOD_US" : "0",
  "KERNEL_WCET_SCALE" : "1",
  "KERNEL_X86_DANGEROUS_MSR" : null,
  "KERNEL_X86_FPU" : "FXSAVE",
  "KERNEL_X86_IBPB_ON_CONTEXT_SWITCH" : null,
  "KERNEL_X86_IBRS" : "ibrs_none",
  "KERNEL_X86_IBRS_ALL" : null,
  "KERNEL_X86_IBRS_BASIC" : null,
  "KERNEL_X86_IBRS_NONE" : "1",
  "KERNEL_X86_MICRO_ARCH" : "nehalem",
  "KERNEL_X86_RSB_ON_CONTEXT_SWITCH" : null,
  "KERNEL_X86_SYSCALL" : "syscall",
  "MAX_NUM_BOOTINFO_UNTYPED_CAPS" : "230",
  "MAX_NUM_IOAPIC" : "1",
  "MAX_NUM_NODES" : "1",
  "MAX_NUM_TRACE_POINTS" : "0",
  "MAX_NUM_WORK_UNITS_PER_PREEMPTION" : "100",
  "MAX_RMRR_ENTRIES" : "1",
  "MAX_VPIDS" : "0",
  "MULTIBOOT1_HEADER" : "1",
  "MULTIBOOT2_HEADER" : "1",
  "MULTIBOOT_GRAPHICS_MODE_LINEAR" : null,
  "MULTIBOOT_GRAPHICS_MODE_NONE" : "1",
  "MULTIBOOT_GRAPHICS_MODE_TEXT" : null,
  "NO_BENCHMARKS" : "1",
  "NUM_DOMAINS" : "1",
  "NUM_PRIORITIES" : "256",
  "PADDR_USER_DEVICE_TOP" : "140737488355328",
  "PC99_TSC_FREQUENCY" : "0",
  "PLAT" : "pc99",
  "PLAT_IMX7" : null,
  "PLAT_PC99" : "1",
  "PRINTING" : null,
  "RESET_CHUNK_BITS" : "8",
  "RETYPE_FAN_OUT_LIMIT" : "256",
  "ROOT_CNODE_SIZE_BITS" : "13",
  "SEL4_ARCH" : "x86_64",
  "SET_TLS_BASE_SELF" : "1",
  "SUPPORT_PCID" : null,
  "SYSCALL" : "1",
  "SYSENTER" : null,
  "USER_STACK_TRACE_LENGTH" : "0",
  "USER_TOP" : "0xa0000000",
  "USE_LOGCAL_IDS" : null,
  "VERIFICATION_BUILD" : null,
  "VTX" : null,
  "WORD_SIZE" : "64",
  "X2APIC" : null,
  "XAPIC" : "1",
  "XSAVE" : null,
  "XSAVE_FEATURE_SET" : "0",
  "XSAVE_SIZE" : "512"
}
1 Like
2

This is looking pretty good, I think. It’d be nice to include version information, e.g. the seL4 version for which it was generated.

3

Good point about the version. Given that a practical problem might be having to deal with a developement/forked/customized version, adding a kernel repo commit ID (if available, otherwise a Hash over the source?) might also have a use case, as there is no need to hack a customized “version-ext”, “build-id” or whatever field then? So the base version is always well defined and customization for whatever reason has a separate, but well defined place.
Maybe this sounds a bit overkill and contradicts a “one and only verified kernel release”, but that can provide a way out of a too fine grained version number semantics discussion.

4

This is something that could be added in the future if there’s a suitable motivation?
We don’t currently provide the version number in any other artifact such as a version string in the kernel.elf or other generated config files.

5

Happy to do this in a second step, but motivation is already there: I have long wanted this info in the verification build to sync/check versions there (currently a giant hack), and if we want user-land to be able to query ABI version and config it’ll need to know at least on the library level (in keeping with the rest of the libsel4 philosophy it wouldn’t need to be in kernel binary). If we wait to provide it, people will start to build workarounds in various build systems (like I did in the verification build).

Maybe the format and exact info needs a bit more discussion, so perfectly fine to decouple it from generating the output in the first place. But we should decide on something before we make the file format official and supported.

Customised or forked seL4 versions are definitely neither encouraged nor supported by the foundation and calling them “seL4” would be a trademark violation. So I would absolutely vote against making that easy. If at all, we should make it intentionally hard, but I’d be happy with just not making it a consideration.

Having a mechanism for dev versions and temporary branches etc is a different story of course. The current use is semVer for released version and semVer with -dev and potentially -branch-dev for dev versions. I don’t think a source hash makes sense, but the git commit ID from the official seL4 repo could be useful (maybe optional).

Then the convention would be SEL4_VERSION with a semVer value and potential -branch-dev for non-release versions and an (optional?) SEL4_ID with git commit ID.

If we wanted we could make the semVer available as 4 separate fields so people don’t have to parse it (major, minor, patch, dev/branch). That’d be easy to generate from the python side at least and wouldn’t need any cmake changes, it could just use the existing VERSION file and git.