From 08ff07fe59b7580dd0e30add8b601e43e2b0c32d Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 10 Dec 2023 11:44:14 +0100 Subject: [PATCH 1/3] cspec/c: provide NUM_DOMAINS build override option Setting the environment variable INPUT_NUM_DOMAINS will cause the build to override the KernelNumDomains setting in the config file with the provided setting. Signed-off-by: Gerwin Klein --- spec/cspec/c/kernel.mk | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/spec/cspec/c/kernel.mk b/spec/cspec/c/kernel.mk index 98a9f1dc85..efcc48a92c 100644 --- a/spec/cspec/c/kernel.mk +++ b/spec/cspec/c/kernel.mk @@ -108,6 +108,10 @@ ${OVERLAY}: ${DEFAULT_OVERLAY} @cp $< $@ endif +ifdef INPUT_NUM_DOMAINS +KERNEL_CMAKE_EXTRA_OPTIONS += -DKernelNumDomains=${INPUT_NUM_DOMAINS} +endif + # Initialize the CMake build. We purge the build directory and start again # whenever any of the kernel sources change, so that we can reliably pick up # changes to the build config. From 2114b7928125da824cb887443a75856e799ae667 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 10 Dec 2023 11:49:39 +0100 Subject: [PATCH 2/3] github: add NUM_DOMAINS test matrix This will now test with the following num_domains settings: - PRs: default as in config file, no matrix - push to master: with NUM_DOMAINS = 1 and default (= '') - weekly test: with NUM_DOMAINS = 1, 7, and default The default in the current config files is 16. 1 leads to structural code changes is the setting most likely to break. 7 is for checking that the proofs also work with a value that is not a power of 2. Signed-off-by: Gerwin Klein --- .github/workflows/proof-deploy.yml | 2 ++ .github/workflows/weekly-clean.yml | 2 ++ 2 files changed, 4 insertions(+) diff --git a/.github/workflows/proof-deploy.yml b/.github/workflows/proof-deploy.yml index bf2006f651..d33c78b8f1 100644 --- a/.github/workflows/proof-deploy.yml +++ b/.github/workflows/proof-deploy.yml @@ -37,6 +37,7 @@ jobs: fail-fast: false matrix: arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64] + num_domains: ['1', ''] # test only most recent push: concurrency: l4v-regression-${{ github.ref }}-${{ strategy.job-index }} steps: @@ -45,6 +46,7 @@ jobs: with: L4V_ARCH: ${{ matrix.arch }} xml: ${{ needs.code.outputs.xml }} + NUM_DOMAINS: ${{ matrix.num_domains }} env: AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }} AWS_SECRET_ACCESS_KEY: ${{ secrets.AWS_SECRET_ACCESS_KEY }} diff --git a/.github/workflows/weekly-clean.yml b/.github/workflows/weekly-clean.yml index 4bc06134ce..4363b48531 100644 --- a/.github/workflows/weekly-clean.yml +++ b/.github/workflows/weekly-clean.yml @@ -18,11 +18,13 @@ jobs: fail-fast: false matrix: arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64] + num_domains: ['1', '7', ''] steps: - name: Proofs uses: seL4/ci-actions/aws-proofs@master with: L4V_ARCH: ${{ matrix.arch }} + NUM_DOMAINS: ${{ matrix.num_domains }} cache_read: '' # start with empty cache, but write cache back (default) env: AWS_ACCESS_KEY_ID: ${{ secrets.AWS_ACCESS_KEY_ID }} From 15c46e72c99f7e08c82f6b8a93870afce357c234 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 10 Dec 2023 12:58:22 +0100 Subject: [PATCH 3/3] runtest: echo NUM_DOMAINS override Signed-off-by: Gerwin Klein --- run_tests | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/run_tests b/run_tests index 0921cb0c85..0b7b023291 100755 --- a/run_tests +++ b/run_tests @@ -122,7 +122,9 @@ returncode = 0 for arch in archs: features = os.environ.get("L4V_FEATURES", "") plat = os.environ.get("L4V_PLAT", "") - print(f"Testing for L4V_ARCH='{arch}', L4V_FEATURES='{features}', L4V_PLAT='{plat}':") + num_domains = os.environ.get("INPUT_NUM_DOMAINS", "") + print(f"Testing for L4V_ARCH='{arch}', L4V_FEATURES='{features}', L4V_PLAT='{plat}', " + f"INPUT_NUM_DOMAINS='{num_domains}'") os.environ["L4V_ARCH"] = arch # Provide L4V_ARCH_IS_ARM for Corres_Test in lib/ROOT