abs-config: lift ASpec+ExecSpec config values from C config

[lsf37]

This is the result of an investigation into lifting the configuration values the user can set in the kernel build system directly into the abstract and executable specifications without manual intervention. The investigation was successful, and this PR implements the feature.

Specifically, we add:

• a CMake build target in cspec for just generating config (without needing compiler or preprocessor tool chain)
• a python script for parsing the generated config header and generating Isabelle Kernel_Config theories for each L4V_ARCH configuration. Changing these kernel configs will now change values such as numDomains, retypeFanOutLimit, timeSlice etc

The PR also make long names mandatory for definition unfolding of these constants, so it becomes clear which proofs depend on their value and might fail because of a change.

This does not necessarily make the proofs generic in these constants, but you can now set different values in the kernel build system and rerun the proofs to see if they still work. There is a good chance that this works for some of them (e.g. CONFIG_TIME_SLICE, CONFIG_RESET_CHUNK_BITS, CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION). More work like PR #410 is needed for other values, but with together PR #410 CONFIG_NUM_DOMAINS is now the only value that needs to be changed for adjusting the number of domains.

This PR is on top of #410 and should be merged afterwards.

Test with seL4/seL4#713

[lsf37]

A sample generated config file for ARM looks like this:

(*
 * Copyright 2021, Proofcraft Pty Ltd
 *
 * SPDX-License-Identifier: GPL-2.0-only
 *)

chapter "Kernel Configuration"

theory Kernel_Config
imports Platform
begin

(*
  GENERATED -- DO NOT EDIT! Changes will be overwritten.

  This file was generated from ~/ver/l4v/spec/cspec/c/config-build/ARM/gen_config/kernel/gen_config.h
  by the script ~/ver/l4v/spec/cspec/c/gen-config-thy.py.
*)

definition CONFIG_WORD_SIZE :: nat where
  "CONFIG_WORD_SIZE \<equiv> 32"

definition CONFIG_USER_TOP :: machine_word where
  "CONFIG_USER_TOP \<equiv> 0xa0000000"

definition CONFIG_L1_CACHE_LINE_SIZE_BITS :: nat where
  "CONFIG_L1_CACHE_LINE_SIZE_BITS \<equiv> 5"

definition CONFIG_PADDR_USER_DEVICE_TOP :: machine_word where
  "CONFIG_PADDR_USER_DEVICE_TOP \<equiv> 4294967295"

definition CONFIG_ROOT_CNODE_SIZE_BITS :: nat where
  "CONFIG_ROOT_CNODE_SIZE_BITS \<equiv> 12"

definition CONFIG_TIMER_TICK_MS :: machine_word where
  "CONFIG_TIMER_TICK_MS \<equiv> 2"

definition timeSlice :: nat where
  "timeSlice \<equiv> 5"  (* CONFIG_TIME_SLICE *)

definition retypeFanOutLimit :: machine_word where
  "retypeFanOutLimit \<equiv> 256"  (* CONFIG_RETYPE_FAN_OUT_LIMIT *)

definition workUnitsLimit :: nat where
  "workUnitsLimit \<equiv> 100"  (* CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION *)

definition resetChunkBits :: nat where
  "resetChunkBits \<equiv> 8"  (* CONFIG_RESET_CHUNK_BITS *)

definition CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS :: nat where
  "CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS \<equiv> 230"

definition numDomains :: nat where
  "numDomains \<equiv> 16"  (* CONFIG_NUM_DOMAINS *)

definition numPriorities :: nat where
  "numPriorities \<equiv> 256"  (* CONFIG_NUM_PRIORITIES *)

definition CONFIG_MAX_NUM_NODES :: nat where
  "CONFIG_MAX_NUM_NODES \<equiv> 1"

definition CONFIG_KERNEL_STACK_BITS :: nat where
  "CONFIG_KERNEL_STACK_BITS \<equiv> 12"

definition CONFIG_MAX_NUM_TRACE_POINTS :: nat where
  "CONFIG_MAX_NUM_TRACE_POINTS \<equiv> 0"

definition CONFIG_USER_STACK_TRACE_LENGTH :: nat where
  "CONFIG_USER_STACK_TRACE_LENGTH \<equiv> 0"


(* These definitions should only be unfolded consciously and carefully: *)
hide_fact (open) CONFIG_WORD_SIZE_def
hide_fact (open) CONFIG_USER_TOP_def
hide_fact (open) CONFIG_L1_CACHE_LINE_SIZE_BITS_def
hide_fact (open) CONFIG_PADDR_USER_DEVICE_TOP_def
hide_fact (open) CONFIG_ROOT_CNODE_SIZE_BITS_def
hide_fact (open) CONFIG_TIMER_TICK_MS_def
hide_fact (open) timeSlice_def
hide_fact (open) retypeFanOutLimit_def
hide_fact (open) workUnitsLimit_def
hide_fact (open) resetChunkBits_def
hide_fact (open) CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS_def
hide_fact (open) numDomains_def
hide_fact (open) numPriorities_def
hide_fact (open) CONFIG_MAX_NUM_NODES_def
hide_fact (open) CONFIG_KERNEL_STACK_BITS_def
hide_fact (open) CONFIG_MAX_NUM_TRACE_POINTS_def
hide_fact (open) CONFIG_USER_STACK_TRACE_LENGTH_def

end

[lsf37]

The theory linter fails because the file Kernel_Config is mentioned in the diff, but is removed. Will put up an issue to fix the linter.

[lsf37]

@mbrcknl adding you to the reviewers in case you wanted to have a look (IIRC, you were involved with some of the C build setup). No pressure, though.

[lsf37]

(going to let the test runs finish before I rebase on the new numdomains state)

[Xaphiosis]

I really like this change, it creates a lot of future improvement potential, and also syncs up the variables. It was super annoying to finish abstract/design proofs, and then build CKernel+CSpec, and in CRefine realise oh, the constant is different in the C, meaning a full rebuild.

Meta thought/concern: original plan for Kernel_Config and its hidden definitions was to indicate that unfolding of Kernel_Config.*_def is strongly discouraged. With these changes, we get a lot of such unfolds, decreasing the deterrent effect. I don't think this is something to address right now, but I'm interested in how you see this play out.

[lsf37]

Meta thought/concern: original plan for Kernel_Config and its hidden definitions was to indicate that unfolding of Kernel_Config.*_def is strongly discouraged. With these changes, we get a lot of such unfolds, decreasing the deterrent effect. I don't think this is something to address right now, but I'm interested in how you see this play out.

Ideally we'd do a pass similar to the one for numDomains to make it actually generic in the constants that get unfolded a lot. They probably don't need to be, and like for numDomains it's likely to improve the proofs. Main question is when we will have time for it.

[Xaphiosis]

Ideally we'd do a pass similar to the one for numDomains to make it actually generic in the constants that get unfolded a lot. They probably don't need to be, and like for numDomains it's likely to improve the proofs. Main question is when we will have time for it.

Indeed. numDomains genericity proved more time-consuming than I anticipated, due to the large amount of unfolds and magic numbers and the many test runs needed. However, my points are incoherent:

• how do we stop people unfolding numDomains_def again given they see the other constants unfolded all over?
• your path forwards sounds good, and we're planning the weekly test to check multiple domains with the help of the above, but if we generalise other variables that's going to be a lot of tests as well; not something solvable at the moment

[lsf37]

• your path forwards sounds good, and we're planning the weekly test to check multiple domains with the help of the above, but if we generalise other variables that's going to be a lot of tests as well; not something solvable at the momen

Yes, ideally we'd somehow extract all necessary conditions into a small theory that can be checked mostly independently. Unclear how well that can work without having access to at least the content in CKernel, but even checking a small theory on top of CKernel would already be much faster than checking all proofs. For that we'd need to get to a point where those constants are guaranteed to not be unfolded anywhere. The work is never done :-)

[corlewis]

This looks really good to me as well (with the caveat that I didn't look too closely at gen-config-thy.py).

I agree with what @Xaphiosis said, it's really exciting to see progress in this direction, with all of the potential improvements and clean-up that it opens up.

[lsf37]

(rebased on master)

Will add the example now and then squash/merge.