From 0a40f153ca6cb32fcc00e4fb740d22f7aac31b5b Mon Sep 17 00:00:00 2001 From: Ivan-Velickovic Date: Thu, 8 Jun 2023 16:40:39 +1000 Subject: [PATCH 1/4] add AArch64 container Add an AArch64 version of the seL4, CAmkES, and L4v containers. seL4 and CAmkES should have full functionality, L4v will be missing the mlton compiler. The Intel containers remain available as before. Co-authored-by: Gerwin Klein Signed-off-by: Gerwin Klein --- Makefile | 18 +++++++-- build.sh | 28 +++++++++++-- dockerfiles/apply-binary_decomp.Dockerfile | 1 + dockerfiles/apply-cakeml.Dockerfile | 1 + dockerfiles/apply-camkes_vis.Dockerfile | 1 + dockerfiles/apply-rust.Dockerfile | 1 + dockerfiles/apply-sysinit.Dockerfile | 1 + dockerfiles/apply-tex.Dockerfile | 1 + dockerfiles/base_tools.Dockerfile | 1 + dockerfiles/cakeml.Dockerfile | 1 + dockerfiles/camkes.Dockerfile | 1 + dockerfiles/extras.Dockerfile | 1 + dockerfiles/l4v.Dockerfile | 3 +- dockerfiles/sel4.Dockerfile | 1 + dockerfiles/sysinit.Dockerfile | 1 + dockerfiles/user.Dockerfile | 1 + scripts/camkes.sh | 16 ++++++-- scripts/l4v.sh | 4 ++ scripts/sel4.sh | 46 ++++++++++++++++++---- scripts/utils/user.sh | 8 +++- 20 files changed, 116 insertions(+), 20 deletions(-) diff --git a/Makefile b/Makefile index 09603c5..0ddf340 100644 --- a/Makefile +++ b/Makefile @@ -48,6 +48,19 @@ endif ETC_LOCALTIME := $(realpath /etc/localtime) +HOST_ARCH ?= $(shell arch) +ifeq ($(HOST_ARCH),x86_64) + DOCKER_PLATFORM := "linux/amd64" +# Intel Macs report i386 instead of x86_64 +else ifeq ($(HOST_ARCH),i386) + DOCKER_PLATFORM := "linux/amd64" +else ifeq ($(HOST_ARCH),arm64) + DOCKER_PLATFORM := "linux/arm64" +else + @echo "Unsupported host architecture: $HOST_ARCH" + @exit 1 +endif + # Extra arguments to pass to `docker run` if it is or is not `podman` - these # are constructed in a very verbose way to be obvious about why we want to do # certain things under regular `docker` vs` podman` @@ -136,7 +149,6 @@ user_run: --group-add sudo \ -v $(HOST_DIR):/host:z \ -v $(DOCKER_VOLUME_HOME):/home/$(shell whoami) \ - -v $(ETC_LOCALTIME):/etc/localtime:ro \ $(USER_IMG) $(EXEC) .PHONY: user_run_l4v @@ -171,12 +183,12 @@ endif .PHONY: build_user build_user: run_checks - $(DOCKER_BUILD) $(DOCKER_FLAGS) \ + $(DOCKER_BUILD) --platform $(DOCKER_PLATFORM) $(DOCKER_FLAGS) \ --build-arg=USER_BASE_IMG=$(DOCKERHUB)$(USER_BASE_IMG) \ -f dockerfiles/extras.Dockerfile \ -t $(EXTRAS_IMG) \ . - $(DOCKER_BUILD) $(DOCKER_FLAGS) \ + $(DOCKER_BUILD) --platform $(DOCKER_PLATFORM) $(DOCKER_FLAGS) \ --build-arg=EXTRAS_IMG=$(EXTRAS_IMG) \ --build-arg=UNAME=$(shell whoami) \ --build-arg=UID=$(shell id -u) \ diff --git a/build.sh b/build.sh index d029466..708b4ab 100755 --- a/build.sh +++ b/build.sh @@ -36,6 +36,9 @@ DOCKER_BUILD="docker build" DOCKER_INSPECT="docker inspect" DOCKER_FLAGS="--force-rm=true" +# By default use host architecture +: "${HOST_ARCH:=$(arch)}" + # Special variables to be passed through Docker to the build scripts : "${SCM}" @@ -62,7 +65,7 @@ build_internal_image() build_args_to_pass_to_docker=$(echo "$build_args" | grep "=" | awk '{print "--build-arg", $1}') # shellcheck disable=SC2086 - $DOCKER_BUILD $DOCKER_FLAGS \ + $DOCKER_BUILD --platform $DOCKER_PLATFORM $DOCKER_FLAGS \ --build-arg BASE_IMG="$base_img" \ --build-arg SCM="$SCM" \ $build_args_to_pass_to_docker \ @@ -95,7 +98,7 @@ apply_software_to_image() # NOTE: it's OK to supply docker build-args that aren't requested in the Dockerfile # shellcheck disable=SC2086 - $DOCKER_BUILD $DOCKER_FLAGS \ + $DOCKER_BUILD --platform $DOCKER_PLATFORM $DOCKER_FLAGS \ --build-arg BASE_BUILDER_IMG="$DOCKERHUB$prebuilt_img" \ --build-arg BASE_IMG="$DOCKERHUB$orig_img" \ --build-arg SCM="$SCM" \ @@ -172,7 +175,7 @@ show_help() | sort \ | tr "\n" "|") cat <&2 exit 1 ;; esac done +if [ "$HOST_ARCH" = "x86_64" ] || \ + [ "$HOST_ARCH" = "amd64" ] || \ + [ "$HOST_ARCH" = "i386" ]; then + DOCKER_PLATFORM="linux/amd64" +elif [ "$HOST_ARCH" = "arm64" ]; then + DOCKER_PLATFORM="linux/arm64" +else + echo "Unsupported host architecture: $HOST_ARCH" + exit 1 +fi + +echo "Building for $DOCKER_PLATFORM" + if [ -z "$img_to_build" ] then echo "You need to supply a \`-b\`" >&2 diff --git a/dockerfiles/apply-binary_decomp.Dockerfile b/dockerfiles/apply-binary_decomp.Dockerfile index e9be92e..72a7692 100644 --- a/dockerfiles/apply-binary_decomp.Dockerfile +++ b/dockerfiles/apply-binary_decomp.Dockerfile @@ -7,6 +7,7 @@ ARG BASE_IMG=trustworthysystems/sel4 # hadolint ignore=DL3006 FROM $BASE_IMG +ARG TARGETPLATFORM LABEL ORGANISATION="Trustworthy Systems" LABEL MAINTAINER="Luke Mondy (luke.mondy@data61.csiro.au)" diff --git a/dockerfiles/apply-cakeml.Dockerfile b/dockerfiles/apply-cakeml.Dockerfile index da40524..272b00a 100644 --- a/dockerfiles/apply-cakeml.Dockerfile +++ b/dockerfiles/apply-cakeml.Dockerfile @@ -13,6 +13,7 @@ FROM $BASE_BUILDER_IMG as builder # hadolint ignore=DL3006 FROM $BASE_IMG +ARG TARGETPLATFORM LABEL ORGANISATION="Trustworthy Systems" LABEL MAINTAINER="Luke Mondy (luke.mondy@data61.csiro.au)" diff --git a/dockerfiles/apply-camkes_vis.Dockerfile b/dockerfiles/apply-camkes_vis.Dockerfile index ecd1c4c..7dcf113 100644 --- a/dockerfiles/apply-camkes_vis.Dockerfile +++ b/dockerfiles/apply-camkes_vis.Dockerfile @@ -7,6 +7,7 @@ ARG BASE_IMG=trustworthysystems/camkes # hadolint ignore=DL3006 FROM $BASE_IMG +ARG TARGETPLATFORM LABEL ORGANISATION="Trustworthy Systems" LABEL MAINTAINER="Luke Mondy (luke.mondy@data61.csiro.au)" diff --git a/dockerfiles/apply-rust.Dockerfile b/dockerfiles/apply-rust.Dockerfile index 4e01cec..d364a2f 100644 --- a/dockerfiles/apply-rust.Dockerfile +++ b/dockerfiles/apply-rust.Dockerfile @@ -7,6 +7,7 @@ ARG BASE_IMG=trustworthysystems/camkes # hadolint ignore=DL3006 FROM $BASE_IMG +ARG TARGETPLATFORM LABEL ORGANISATION="Trustworthy Systems" LABEL MAINTAINER="Luke Mondy (luke.mondy@data61.csiro.au)" diff --git a/dockerfiles/apply-sysinit.Dockerfile b/dockerfiles/apply-sysinit.Dockerfile index a5c6085..c72efa5 100644 --- a/dockerfiles/apply-sysinit.Dockerfile +++ b/dockerfiles/apply-sysinit.Dockerfile @@ -12,6 +12,7 @@ FROM $BASE_BUILDER_IMG as builder # hadolint ignore=DL3006 FROM $BASE_IMG +ARG TARGETPLATFORM LABEL ORGANISATION="Trustworthy Systems" LABEL MAINTAINER="Luke Mondy (luke.mondy@data61.csiro.au)" diff --git a/dockerfiles/apply-tex.Dockerfile b/dockerfiles/apply-tex.Dockerfile index f5b5e89..1a9a366 100644 --- a/dockerfiles/apply-tex.Dockerfile +++ b/dockerfiles/apply-tex.Dockerfile @@ -7,6 +7,7 @@ ARG BASE_IMG=trustworthysystems/sel4 # hadolint ignore=DL3006 FROM $BASE_IMG +ARG TARGETPLATFORM LABEL ORGANISATION="Trustworthy Systems" LABEL MAINTAINER="Gerwin Klein " diff --git a/dockerfiles/base_tools.Dockerfile b/dockerfiles/base_tools.Dockerfile index daed717..2a6df9e 100644 --- a/dockerfiles/base_tools.Dockerfile +++ b/dockerfiles/base_tools.Dockerfile @@ -7,6 +7,7 @@ ARG BASE_IMG=debian:bullseye-slim # hadolint ignore=DL3006 FROM $BASE_IMG +ARG TARGETPLATFORM LABEL ORGANISATION="Trustworthy Systems" LABEL MAINTAINER="Luke Mondy (luke.mondy@data61.csiro.au)" diff --git a/dockerfiles/cakeml.Dockerfile b/dockerfiles/cakeml.Dockerfile index 84e0d9b..cd2618e 100644 --- a/dockerfiles/cakeml.Dockerfile +++ b/dockerfiles/cakeml.Dockerfile @@ -7,6 +7,7 @@ ARG BASE_IMG=trustworthysystems/camkes # hadolint ignore=DL3006 FROM $BASE_IMG +ARG TARGETPLATFORM LABEL ORGANISATION="Trustworthy Systems" LABEL MAINTAINER="Luke Mondy (luke.mondy@data61.csiro.au)" diff --git a/dockerfiles/camkes.Dockerfile b/dockerfiles/camkes.Dockerfile index 4f169fc..230e476 100644 --- a/dockerfiles/camkes.Dockerfile +++ b/dockerfiles/camkes.Dockerfile @@ -7,6 +7,7 @@ ARG BASE_IMG=trustworthysystems/sel4 # hadolint ignore=DL3006 FROM $BASE_IMG +ARG TARGETPLATFORM LABEL ORGANISATION="Trustworthy Systems" LABEL MAINTAINER="Luke Mondy (luke.mondy@data61.csiro.au)" diff --git a/dockerfiles/extras.Dockerfile b/dockerfiles/extras.Dockerfile index 4c0a052..8125c72 100644 --- a/dockerfiles/extras.Dockerfile +++ b/dockerfiles/extras.Dockerfile @@ -7,6 +7,7 @@ ARG USER_BASE_IMG=trustworthysystems/sel4 # hadolint ignore=DL3006 FROM $USER_BASE_IMG +ARG TARGETPLATFORM # This dockerfile is a shim between the images from Dockerhub and the # user.dockerfile. diff --git a/dockerfiles/l4v.Dockerfile b/dockerfiles/l4v.Dockerfile index 508fbff..899e75c 100644 --- a/dockerfiles/l4v.Dockerfile +++ b/dockerfiles/l4v.Dockerfile @@ -7,6 +7,7 @@ ARG BASE_IMG=trustworthysystems/camkes # hadolint ignore=DL3006 FROM $BASE_IMG +ARG TARGETPLATFORM LABEL ORGANISATION="Trustworthy Systems" LABEL MAINTAINER="Luke Mondy (luke.mondy@data61.csiro.au)" @@ -29,5 +30,3 @@ RUN /bin/bash /tmp/l4v.sh \ && apt-get clean autoclean \ && apt-get autoremove --purge --yes \ && rm -rf /var/lib/apt/lists/* - -ENV PATH "${PATH}:/opt/mlton/bin" diff --git a/dockerfiles/sel4.Dockerfile b/dockerfiles/sel4.Dockerfile index 6cb131b..b047fd4 100644 --- a/dockerfiles/sel4.Dockerfile +++ b/dockerfiles/sel4.Dockerfile @@ -7,6 +7,7 @@ ARG BASE_IMG=base_tools # hadolint ignore=DL3006 FROM $BASE_IMG +ARG TARGETPLATFORM LABEL ORGANISATION="Trustworthy Systems" LABEL MAINTAINER="Luke Mondy (luke.mondy@data61.csiro.au)" diff --git a/dockerfiles/sysinit.Dockerfile b/dockerfiles/sysinit.Dockerfile index ef237f7..39be5db 100644 --- a/dockerfiles/sysinit.Dockerfile +++ b/dockerfiles/sysinit.Dockerfile @@ -7,6 +7,7 @@ ARG BASE_IMG=trustworthysystems/camkes # hadolint ignore=DL3006 FROM $BASE_IMG +ARG TARGETPLATFORM LABEL ORGANISATION="Trustworthy Systems" LABEL MAINTAINER="Luke Mondy (luke.mondy@data61.csiro.au)" diff --git a/dockerfiles/user.Dockerfile b/dockerfiles/user.Dockerfile index 57fd4e1..b47fe7c 100644 --- a/dockerfiles/user.Dockerfile +++ b/dockerfiles/user.Dockerfile @@ -7,6 +7,7 @@ ARG EXTRAS_IMG=extras # hadolint ignore=DL3006 FROM $EXTRAS_IMG +ARG TARGETPLATFORM # Get user UID and username ARG UID diff --git a/scripts/camkes.sh b/scripts/camkes.sh index fd41a24..c8878d2 100644 --- a/scripts/camkes.sh +++ b/scripts/camkes.sh @@ -35,6 +35,7 @@ possibly_toggle_apt_snapshot # Get dependencies as_root dpkg --add-architecture i386 +as_root dpkg --add-architecture arm64 as_root apt-get update -q as_root apt-get install -y --no-install-recommends \ acl \ @@ -43,7 +44,6 @@ as_root apt-get install -y --no-install-recommends \ linux-libc-dev:i386 \ pkg-config \ spin \ - lib32stdc++-10-dev \ # end of list # Required for testing @@ -84,8 +84,18 @@ as_root pip3 install --no-cache-dir \ # end of list # Get stack -wget -O - https://get.haskellstack.org/ | sh -echo "export PATH=\"\$PATH:\$HOME/.local/bin\"" >> "$HOME/.bashrc" +export GHCUP_INSTALL_BASE_PREFIX=/opt/ghcup +curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | BOOTSTRAP_HASKELL_NONINTERACTIVE=1 \ + BOOTSTRAP_HASKELL_GHC_VERSION=9.2.8 \ + BOOTSTRAP_HASKELL_CABAL_VERSION=3.10 \ + BOOTSTRAP_HASKELL_INSTALL_STACK=1 sh + +# shellcheck disable=SC1091 +source "$GHCUP_INSTALL_BASE_PREFIX/.ghcup/env" +echo "export GHCUP_INSTALL_BASE_PREFIX=/opt/ghcup" >> "$HOME/.bashrc" +echo "source $GHCUP_INSTALL_BASE_PREFIX/.ghcup/env" >> "$HOME/.bashrc" + +as_root rm -f "$GHCUP_INSTALL_BASE_PREFIX"/.ghcup/cache/* # Pick a random group ID, one that won't clash with common user GIDs as_root groupadd -g "$STACK_GID" stack diff --git a/scripts/l4v.sh b/scripts/l4v.sh index a5e680d..29ee5b4 100644 --- a/scripts/l4v.sh +++ b/scripts/l4v.sh @@ -7,6 +7,10 @@ set -exuo pipefail +# make sure PATH etc is set up +# shellcheck disable=SC1091 +source "$HOME/.bashrc" + # Source common functions DIR="${BASH_SOURCE%/*}" test -d "$DIR" || DIR=$PWD diff --git a/scripts/sel4.sh b/scripts/sel4.sh index 737e5c9..1611e1d 100644 --- a/scripts/sel4.sh +++ b/scripts/sel4.sh @@ -25,11 +25,29 @@ test -d "$DIR" || DIR=$PWD # tmp space for building : "${TEMP_DIR:=/tmp}" +X64_CROSS="g++-10-aarch64-linux-gnu gcc-10-aarch64-linux-gnu gcc-10-multilib" +ARM64_CROSS="gcc-10-x86-64-linux-gnu:arm64 g++-10-x86-64-linux-gnu:arm64 \ + gcc-10-i686-linux-gnu:arm64 g++-10-i686-linux-gnu:arm64" + +# TARGETPLATFORM is set by docker during the build process +if [ "$TARGETPLATFORM" = "linux/amd64" ]; then + CROSS="$X64_CROSS" +elif [ "$TARGETPLATFORM" = "linux/arm64" ]; then + CROSS="$ARM64_CROSS" +else + echo "Unknown target platform $TARGETPLATFORM" + exit 1 +fi + # Add additional architectures for cross-compiled libraries. # Install the tools required to compile seL4. as_root apt-get update -q +as_root dpkg --add-architecture amd64 +as_root dpkg --add-architecture i386 as_root dpkg --add-architecture armhf as_root dpkg --add-architecture armel +as_root dpkg --add-architecture arm64 +# shellcheck disable=SC2086 as_root apt-get install -y --no-install-recommends \ astyle=3.1-2+b1 \ build-essential \ @@ -55,19 +73,17 @@ as_root apt-get install -y --no-install-recommends \ u-boot-tools \ clang-11 \ g++-10 \ - g++-10-aarch64-linux-gnu \ g++-10-arm-linux-gnueabi \ g++-10-arm-linux-gnueabihf \ gcc-10 \ - gcc-10-aarch64-linux-gnu \ gcc-10-arm-linux-gnueabi \ gcc-10-arm-linux-gnueabihf \ gcc-10-base \ - gcc-10-multilib \ gcc-riscv64-unknown-elf \ libclang-11-dev \ qemu-system-arm \ - qemu-system-misc + qemu-system-misc \ + $CROSS # end of list if [ "$DESKTOP_MACHINE" = "no" ] ; then @@ -87,7 +103,22 @@ if [ "$DESKTOP_MACHINE" = "no" ] ; then as_root update-alternatives --auto "$name" || : done done - + if [ "$TARGETPLATFORM" = "linux/amd64" ]; then + MORE_COMP="" + elif [ "$TARGETPLATFORM" = "linux/arm64" ]; then + MORE_COMP="gcc-${compiler_version}-x86-64-linux-gnu \ + cpp-${compiler_version}-x86-64-linux-gnu \ + g++-${compiler_version}-x86-64-linux-gnu \ + gcc-${compiler_version}-i686-linux-gnu \ + cpp-${compiler_version}-i686-linux-gnu \ + g++-${compiler_version}-i686-linux-gnu \ + " + else + echo "Unknown target platform $TARGETPLATFORM" + exit 1 + fi + + # shellcheck disable=SC2086 for compiler in gcc-${compiler_version}-arm-linux-gnueabi \ cpp-${compiler_version}-arm-linux-gnueabi \ g++-${compiler_version}-arm-linux-gnueabi \ @@ -97,10 +128,11 @@ if [ "$DESKTOP_MACHINE" = "no" ] ; then gcc-${compiler_version}-arm-linux-gnueabihf \ cpp-${compiler_version}-arm-linux-gnueabihf \ g++-${compiler_version}-arm-linux-gnueabihf \ + $MORE_COMP # end of list do - echo ${compiler} - for file in $(dpkg-query -L ${compiler} | grep /usr/bin/); do + echo "${compiler}" + for file in $(dpkg-query -L "${compiler}" | grep /usr/bin/); do name=$(basename "$file" | sed "s/-${compiler_version}\$//g") # shellcheck disable=SC2001 link=$(echo "$file" | sed "s/-${compiler_version}\$//g") diff --git a/scripts/utils/user.sh b/scripts/utils/user.sh index 7d500ac..be3d381 100644 --- a/scripts/utils/user.sh +++ b/scripts/utils/user.sh @@ -29,7 +29,7 @@ fgroup="${group_info[0]}" fgid="${group_info[2]}" GROUP_OK=false -if [ "$fgroup" == "$GROUP" ] && [ "$fgid" == "$GID" ] ; then +if [ "$fgroup" = "$GROUP" ] && [ "$fgid" = "$GID" ] ; then # This means the group creation has gone OK, so make a user # with the corresponding group GROUP_OK=true @@ -108,10 +108,13 @@ grep "export" /root/.bashrc >> "/home/${UNAME}/.bashrc" # Note that this block does not do parameter expansion, so will be # copied verbatim into the user's .bashrc. # We use this to ensure they have the repo program in their path, +# that they pick up any potentially present Haskell installation, # and to ensure they start in the /host dir (aka, their own file # path) cat << 'EOF' >> "/home/${UNAME}/.bashrc" export PATH=/scripts/repo:$PATH +export GHCUP_INSTALL_BASE_PREFIX=/opt/ghcup +[ -r /opt/ghcup/.ghcup/env ] && source /opt/ghcup/.ghcup/env cd /host EOF @@ -128,6 +131,9 @@ chown -R "$chown_setting" /isabelle # Isabelle expects a home dir folder. ln -s /isabelle "/home/${UNAME}/.isabelle" +# Make Haskell installation writable if it exists +[ -d /opt/ghcup ] && chown -R "${UNAME}" /opt/ghcup + # Make sure the user owns their home dir chown -R "$chown_setting" "/home/${UNAME}" chmod -R ug+rw "/home/${UNAME}" From c067d05f827df8dfb3dff35d8b8ae64cc3cf6ceb Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 12 May 2024 20:31:27 +1000 Subject: [PATCH 2/4] github: add a MacOS M1 build job Signed-off-by: Gerwin Klein --- .github/workflows/docker-build.yml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/.github/workflows/docker-build.yml b/.github/workflows/docker-build.yml index acfc8da..a9b114e 100644 --- a/.github/workflows/docker-build.yml +++ b/.github/workflows/docker-build.yml @@ -9,8 +9,8 @@ name: Build on: [pull_request] jobs: - build: - name: Docker images + build-amd64: + name: Docker images (AMD64) runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 @@ -18,6 +18,15 @@ jobs: # the following will also build the plain camkes image: - run: ./build.sh -v -b camkes -s cakeml -s rust + build-arm64: + name: Docker images (ARM64) + runs-on: [self-hosted, macos, ARM64] + steps: + - uses: actions/checkout@v4 + - run: ./build.sh -v -b sel4 + # the following will also build the plain camkes image: + - run: ./build.sh -v -b camkes -s cakeml -s rust + # This needs to rebuild the seL4 and camkes images (apart from cakeml/rust), # but putting l4v in the same job as the large camkes-cakeml-rust image # overflows the disk space of the GitHub runner. From c66283a1c8d865b09fde8387ea7cbf11b313e011 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 13 May 2024 16:43:21 +1000 Subject: [PATCH 3/4] update README - remove obsolete options and settings - spell check - update github org URLs - update descriptions to current seL4 CI - update CLI instructions - markdown lint Signed-off-by: Gerwin Klein --- README.md | 65 ++++++++++++++++++++++++++++--------------------------- 1 file changed, 33 insertions(+), 32 deletions(-) diff --git a/README.md b/README.md index b6eec6a..1772aa1 100644 --- a/README.md +++ b/README.md @@ -1,10 +1,11 @@ -# Dockerfiles for seL4, CAmkES, and L4v dependencies +# Docker containers for seL4, CAmkES, and L4v dependencies ## Requirements @@ -13,11 +14,11 @@ It is recommended you add yourself to the docker group, so you can run docker commands without using sudo. - ## Quick start -To get a running build environment for sel4 and camkes, run: - git clone https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git +To get a running build environment for seL4 and CAmkES, run: + + git clone https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles.git cd seL4-CAmkES-L4v-dockerfiles make user @@ -27,15 +28,17 @@ Or to map a particular directory to the /host dir in the container: ## What is this? -This repository contains dockerfiles which map out the dependencies for seL4, CAmkES, and L4v. It also contains some infrastructure to allow people to use the containers in a useful way. -These dockerfiles are used as the basis for regression testing in the Trustworthy Systems group, and hence should represent a well tested and up to date environment +This repository contains docker files which map out the dependencies for seL4, CAmkES, and L4v. It also contains some infrastructure to allow people to use the containers in a useful way. + +These docker files are used as the basis for regression testing in the seL4 Foundation, and hence should represent a well tested and up to date environment ## To run -Get the repository of Dockerfiles by cloning them from GitHub: - git clone https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git +Get the repository of docker files by cloning them from GitHub: + + git clone https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles.git cd seL4-CAmkES-L4v-dockerfiles To get an environment within the container, run: @@ -81,6 +84,7 @@ to start the container interactively in your current directory, or: to execute commands in the container in your current directory. ### Example of compiling seL4 test + Start by creating a new workspace on your machine: mkdir ~/sel4test @@ -119,19 +123,18 @@ Compile and simulate seL4 test for x86-64: All is well in the universe - ## Adding dependencies -The images and dockerfiles for seL4/CAmkES/L4v only specify enough dependencies to pass the tests in the \*tests.dockerfile. The `extras.dockerfile` acts as a shim between the DockerHub images and the `user.dockerfile`. -Adding dependencies into the `extras.dockerfile` will build them the next time you run `make user`, and then be cached from then on. +The images and docker files for seL4/CAmkES/L4v only specify enough dependencies to pass the tests in the \*tests.docker file. The `extras.dockerfile` acts as a shim between the DockerHub images and the `user.dockerfile`. +Adding dependencies into the `extras.dockerfile` will build them the next time you run `make user`, and then be cached from then on. -## To build the local dockerfiles +## To build the local Docker files -To build the Dockerfiles locally, you will need to use the included `build.sh` script. It has a help menu: +To build the Docker files locally, you will need to use the included `build.sh` script. It has a help menu: ./build.sh -h - build.sh [-r] -b [sel4|camkes|l4v] -s [binary_decomp|cakeml|camkes_vis|riscv|rust|sysinit|] -s ... -e MAKE_CACHES=no -e ... + build.sh [-r] -b [sel4|camkes|l4v] -s [binary_decomp|cakeml|camkes_vis|riscv|rust|sysinit] -s ... -e MAKE_CACHES=no -e ... -r Rebuild docker images (don't use the docker cache) -v Verbose mode @@ -139,50 +142,48 @@ To build the Dockerfiles locally, you will need to use the included `build.sh` s -e Build arguments (NAME=VALUE) to docker build. Use a -e for each build arg. -p Pull base image first. Rather than build the base image, get it from the web first - - Sneaky hints: - - To build 'prebuilt' images, you can run: - build.sh -b [riscv|cakeml] - but it will take a while! - - You can actually run this with '-b sel4-rust', or any other existing image, - but it will ruin the sorting of the name. + -a Supply x86_64 for building Intel images, and arm64 for Arm images. + Defaults to x86_64 on x86-based hosts and arm64 on ARM64 hosts. ### Example builds To build the seL4 image, run: -`./build.sh -b sel4` + ./build.sh -b sel4 Note that the `-b` flag stands for the `base image`. There are 3 base images: `sel4`, `camkes`, and `l4v`. Each base image includes the previous one, i.e.: the `camkes` image has everything the `sel4` image has, plus the camkes dependencies. To add additional software to the image, you can use the `-s` flag, to add `software`. For example: -`./build.sh -b sel4 -s riscv # This adds the RISCV compilers` + ./build.sh -b camkes -s cakeml # This adds the CakeML compiler -`./build.sh -b sel4 -s riscv -s rust # This adds the RISCV compilers and a rust compiler` + ./build.sh -b sel4 -s cakeml -s rust # This adds the CakeML compiler and Rust compiler You can also pass configuration variables through to docker (in docker terms, these are `BUILD_ARGS`) by using the `-e` flag. For example, you can turn off priming the build caches: -`./build.sh -b sel4 -e MAKE_CACHES=no` + ./build.sh -b sel4 -e MAKE_CACHES=no To speed things up, you can ask to pull the base image from DockerHub first with the `-p` flag: -`./build.sh -p -b sel4 -s riscv # This adds the RISCV compilers` - - + # This adds the CakeML compiler and pulls camkes from DockerHub + ./build.sh -p -b camkes -s cakeml ## Security + Running Docker on your machine has its own security risks which you should be aware of. Be sure to read the Docker documentation. Of particular note in this case, your UID and GID are being baked into an image. Any other user on the host who is part of the docker group could spawn a separate container of this image, and hence have read and write access to your files. Of course, if they are part of the docker group, they could do this anyway, but it just makes it a bit easier. Use at your own risk. - ## Released images on DockerHub -The Trustworthy Systems group pushes "known working" images to DockerHub under the `trustworthysystems/` DockerHub organisation. Images with the `:latest` tag are the ones currently in use in the Trustworthy Systems regression system, and so are considered to be "known working". Furthermore, each time an image is pushed out, it is tagged with a YYYY_MM_DD formatted date. +The seL4 CI pushes "known working" images to DockerHub under the [`trustworthysystems/` DockerHub organisation][1]. Images with the `:latest` tag are the ones currently in use in the seL4 CI system, and so are considered to be "known working". Furthermore, each time an image is pushed out, it is tagged with a `YYYY_MM_DD` formatted date. + +To ensure (fairly) reproducible builds of docker images, the images are built using Debian Snapshot (an apt repository that can be pinned to a date in time). When changes are made to the scripts or Docker files in this repo, they are built against a "known working" date of Debian Snapshot - in other words, a date in which we were able to build all the Docker images, and they passed all of our tests. This avoids issues where something in Debian Testing or Unstable has changed and causes apt conflicts, or a newer version breaks the seL4 build process. -To ensure (fairly) reproducible builds of docker images, the images are built using Debian Snapshot (an apt repository that can be pinned to a date in time). When changes are made to the scripts or Dockerfiles in this repo, they are built against a "known working" date of Debian Snapshot - in other words, a date in which we were able to build all the Docker images, and they passed all of our tests. This avoids issues where something in Debian Testing or Unstable has changed and causes apt conflicts, or a newer version breaks the seL4 build process. + -Internally, the Trustworthy Systems regression system will, once a week, attempt to build the docker images using regular apt (not using Snapshot), and if successful, will update the "known working" date. This means on the next build of the docker images that gets pushed out will be using this bumped Snapshot date. Typically, the further in time we get from a Debian release, the more packages we need to fetch from Testing or Unstable, and as such, the less likely this automatic bumping is to work, due to above mentioned issues. With some human intervention, it can usually be fixed up fairly easily. However, even without intervention, the "known working" images will continue to function and build. +[1]: https://hub.docker.com/u/trustworthysystems From e0f4c247cd1d1525817f3f550f52f7ff09df7ea3 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 14 May 2024 10:46:04 +1000 Subject: [PATCH 4/4] github: no cached images on self-hosted runner Prevent the job from using cached images on the self-hosted runner to make sure we are picking up the current state of the remote Debian repo. GitHub runners start from scratch each time, so they won't have any cached images available. Signed-off-by: Gerwin Klein --- .github/workflows/docker-build.yml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/.github/workflows/docker-build.yml b/.github/workflows/docker-build.yml index a9b114e..bc7149c 100644 --- a/.github/workflows/docker-build.yml +++ b/.github/workflows/docker-build.yml @@ -23,9 +23,12 @@ jobs: runs-on: [self-hosted, macos, ARM64] steps: - uses: actions/checkout@v4 - - run: ./build.sh -v -b sel4 + # don't use cached images on the self-hosted runner to make sure we are + # picking up current Debian repo state. The GitHub runners start from + # scratch, so don't need it. + - run: ./build.sh -rv -b sel4 # the following will also build the plain camkes image: - - run: ./build.sh -v -b camkes -s cakeml -s rust + - run: ./build.sh -rv -b camkes -s cakeml -s rust # This needs to rebuild the seL4 and camkes images (apart from cakeml/rust), # but putting l4v in the same job as the large camkes-cakeml-rust image