diff --git a/aws-proofs/README.md b/aws-proofs/README.md index 2daced4c..486555b5 100644 --- a/aws-proofs/README.md +++ b/aws-proofs/README.md @@ -18,6 +18,7 @@ automatically spins up and terminates the corresponding AWS instance. - `L4V_FEATURES`: Optional kernel features to test. Either `MCS` or empty. - `L4V_PLAT`: Platform variant to test (optional). Either a platform name or unset. +- `NUM_DOMAINS`: Optional override for the `KenrelNumDomains` config setting. - `session`: which session to run (e.g. `CRefine` or `ASpec`, or `ASpec CRefine`, i.e. a space-separated string). Runs all sessions if unset. diff --git a/aws-proofs/action.yml b/aws-proofs/action.yml index 5fce2212..a5864cca 100644 --- a/aws-proofs/action.yml +++ b/aws-proofs/action.yml @@ -17,6 +17,9 @@ inputs: L4V_PLAT: description: 'Platform variant to test (optional). Either a platform name or unset.' required: false + NUM_DOMAINS: + description: 'Optional override for KernelNumDomains config setting.' + required: false session: description: 'Which proof session to run (space-separated string)' required: false diff --git a/aws-proofs/steps.sh b/aws-proofs/steps.sh index 3e4e0f7a..e6b42ef1 100755 --- a/aws-proofs/steps.sh +++ b/aws-proofs/steps.sh @@ -67,6 +67,7 @@ ssh -o SendEnv=INPUT_CI_BRANCH \ -o SendEnv=INPUT_L4V_ARCH \ -o SendEnv=INPUT_L4V_FEATURES \ -o SendEnv=INPUT_L4V_PLAT \ + -o SendEnv=INPUT_NUM_DOMAINS \ -o SendEnv=INPUT_MANIFEST \ -o SendEnv=INPUT_ISA_BRANCH \ -o SendEnv=INPUT_SESSION \ diff --git a/aws-proofs/vm-steps.sh b/aws-proofs/vm-steps.sh index 1a17ff97..efe3f0a1 100755 --- a/aws-proofs/vm-steps.sh +++ b/aws-proofs/vm-steps.sh @@ -58,7 +58,11 @@ isabelle/bin/isabelle components -a export L4V_ARCH=${INPUT_L4V_ARCH} export L4V_FEATURES=${INPUT_L4V_FEATURES} export L4V_PLAT=${INPUT_L4V_PLAT} -L4V_ARCH_FEATURES="${L4V_ARCH}${L4V_FEATURES:+-${L4V_FEATURES}}${L4V_PLAT:+-${L4V_PLAT}}" + +FEATURES_STR=${L4V_FEATURES:+-${L4V_FEATURES}} +PLAT_STR=${L4V_PLAT:+-${L4V_PLAT}} +NUM_DOMAINS_STR=${INPUT_NUM_DOMAINS:+-${INPUT_NUM_DOMAINS}} +L4V_ARCH_FEATURES="${L4V_ARCH}${FEATURES_STR}${PLAT_STR}${NUM_DOMAINS_STR}" CACHE_NAME=${INPUT_CACHE_NAME} if [ -z "${CACHE_NAME}" ] diff --git a/seL4-platforms/platforms.yml b/seL4-platforms/platforms.yml index 50fb362b..7c12e1c0 100644 --- a/seL4-platforms/platforms.yml +++ b/seL4-platforms/platforms.yml @@ -132,8 +132,8 @@ platforms: modes: [64] smp: [64] platform: tqma8xqp1gb + req: [tqma] march: armv8a - disabled: true OMAP3: arch: arm diff --git a/sel4test-hw/build.py b/sel4test-hw/build.py index f54be849..46432562 100644 --- a/sel4test-hw/build.py +++ b/sel4test-hw/build.py @@ -31,7 +31,8 @@ def hw_build(manifest_dir: str, build: Build): script = [ ["../init-build.sh"] + build.settings_args(), ["ninja"], - ["tar", "czf", f"../{build.name}-images.tar.gz", "images/"] + ["tar", "czf", f"../{build.name}-images.tar.gz", "images/"], + ["cp", "kernel/kernel.elf", f"../{build.name}-kernel.elf"] ] return run_build_script(manifest_dir, build, script)