capDL and x86_64 support in Microkit

.github/workflows/sdk.yaml

@@ -34,11 +34,14 @@ jobs:
       - name: Install SDK dependencies
         run: |
           rustup target add x86_64-unknown-linux-musl
+          rustup component add rust-src --toolchain stable-x86_64-unknown-linux-gnu
           rustup target add aarch64-unknown-linux-musl
+          rustup component add rust-src --toolchain stable-aarch64-unknown-linux-musl
           sudo apt update
           sudo apt install software-properties-common
           sudo add-apt-repository ppa:deadsnakes/ppa
           sudo apt install \
+            gcc-x86-64-linux-gnu \
             gcc-riscv64-unknown-elf \
             cmake pandoc device-tree-compiler ninja-build \
             texlive-latex-base texlive-latex-recommended \
@@ -90,14 +93,14 @@ jobs:
       - name: Set version
         run: echo "SDK_VERSION=$(./ci/dev_version.sh)" >> $GITHUB_ENV
       - name: Build SDK (x86-64)
-        run: nix develop --ignore-environment -c bash -c "python3 build_sdk.py --sel4=seL4 --version ${{ env.SDK_VERSION }}-macos-x86-64 --gcc-toolchain-prefix-riscv64 riscv64-none-elf --tool-target-triple=x86_64-apple-darwin"
+        run: nix develop --ignore-environment -c bash -c "python3 build_sdk.py --sel4=seL4 --version ${{ env.SDK_VERSION }}-macos-x86-64 --gcc-toolchain-prefix-x86_64 x86_64-elf --gcc-toolchain-prefix-riscv64 riscv64-none-elf --tool-target-triple=x86_64-apple-darwin"
       - name: Upload SDK (x86-64)
         uses: actions/upload-artifact@v4
         with:
           name: microkit-sdk-${{ env.SDK_VERSION }}-macos-x86-64
           path: release/microkit-sdk-${{ env.SDK_VERSION }}-macos-x86-64.tar.gz
       - name: Build SDK (ARM64)
-        run: nix develop --ignore-environment -c bash -c "python3 build_sdk.py --sel4=seL4 --version ${{ env.SDK_VERSION }}-macos-aarch64 --gcc-toolchain-prefix-riscv64 riscv64-none-elf --tool-target-triple=aarch64-apple-darwin"
+        run: nix develop --ignore-environment -c bash -c "python3 build_sdk.py --sel4=seL4 --version ${{ env.SDK_VERSION }}-macos-aarch64 --gcc-toolchain-prefix-x86_64 x86_64-elf --gcc-toolchain-prefix-riscv64 riscv64-none-elf --tool-target-triple=aarch64-apple-darwin"
       - name: Upload SDK (ARM64)
         uses: actions/upload-artifact@v4
         with:

.reuse/dep5

@@ -7,6 +7,7 @@ Files:
   tool/microkit/Cargo.lock
   example/rust/Cargo.lock
   example/rust/support/*.json
+  initialiser/support/*.json
   flake.lock
   CHANGES.md
   VERSION

DEVELOPER.md

@@ -22,6 +22,7 @@ This section attempts to list the packages or external development tools which a
 * xmllint
 * qemu-system-aarch64
 * qemu-system-riscv64
+* qemu-system-x86_64
 
 To build the documentation you also need
 * pandoc
@@ -37,13 +38,15 @@ On a Debian-like system you can do:
 
     $ curl https://sh.rustup.rs -sSf | sh
     $ rustup target add x86_64-unknown-linux-musl
+    $ rustup component add rust-src --toolchain stable-x86_64-unknown-linux-gnu
     $ sudo apt install build-essential git cmake ninja-build \
         device-tree-compiler libxml2-utils \
         pandoc texlive-latex-base texlive-latex-recommended \
         texlive-fonts-recommended texlive-fonts-extra \
         python3.12 python3.12-venv \
-        qemu-system-arm qemu-system-misc \
-        gcc-riscv64-unknown-elf
+        qemu-system-arm qemu-system-misc qemu-system-x86 \
+        gcc-riscv64-unknown-elf \
+        gcc-x86-64-linux-gnu
     $ python3.12 -m venv pyenv
     $ ./pyenv/bin/pip install --upgrade pip setuptools wheel
     $ ./pyenv/bin/pip install -r requirements.txt
@@ -72,7 +75,7 @@ On macOS, with the [Homebrew](https://brew.sh) package manager you can do:
     $ curl https://sh.rustup.rs -sSf | sh
     $ brew tap riscv-software-src/riscv
     $ brew install riscv-tools
-    $ brew install pandoc cmake dtc ninja libxml2 python@3.12 coreutils texlive qemu
+    $ brew install x86_64-elf-gcc pandoc cmake dtc ninja libxml2 python@3.12 coreutils texlive qemu
     $ python3.12 -m venv pyenv
     $ ./pyenv/bin/pip install --upgrade pip setuptools wheel
     $ ./pyenv/bin/pip install -r requirements.txt
@@ -100,15 +103,14 @@ Will give a shell with all the required dependencies to build the SDK.
 An important note is that Nix's RISC-V cross-compiler will have a different
 prefix to the default one the SDK build script expects.
 
-When you build the SDK, provide an extra argument `--toolchain-prefix-riscv64 riscv64-none-elf`.
+When you build the SDK, provide two extra arguments:
+`--gcc-toolchain-prefix-x86_64 x86_64-elf --gcc-toolchain-prefix-riscv64 riscv64-none-elf`.
 
 ## seL4 Version
 
 The SDK includes a binary of the seL4 kernel.
 During the SDK build process the kernel is build from source.
 
-At this point in time there are some minor changes to the seL4 kernel required for Microkit. This is temporary, more details can be found [here](https://github.com/seL4/microkit/issues/52).
-
 Please clone seL4 from:
 
     https://github.com/seL4/seL4.git

README.md

@@ -7,11 +7,12 @@
 
 The purpose of the seL4 Microkit is to enable system designers to create static software systems based on the seL4 microkernel.
 
-The seL4 Microkit consists of four parts:
+The seL4 Microkit consists of five components:
 
    * Microkit bootloader
+   * CapDL initialiser
    * Microkit library
-   * Microkit initial task
+   * Microkit monitor
    * Microkit tool
 
 The Microkit is distributed as a software development kit (SDK).

build_sdk.py

@@ -33,12 +33,15 @@
 
 TRIPLE_AARCH64 = "aarch64-none-elf"
 TRIPLE_RISCV = "riscv64-unknown-elf"
+# TODO: this won't work for LLVM, to fix later
+TRIPLE_X86_64 = "x86_64-linux-gnu"
 
 KERNEL_CONFIG_TYPE = Union[bool, str]
 KERNEL_OPTIONS = Dict[str, Union[bool, str]]
 
 DEFAULT_KERNEL_OPTIONS = {
     "KernelIsMCS": True,
+    "KernelRootCNodeSizeBits": "17",
 }
 
 DEFAULT_KERNEL_OPTIONS_AARCH64 = {
@@ -50,16 +53,34 @@
 
 DEFAULT_KERNEL_OPTIONS_RISCV64 = DEFAULT_KERNEL_OPTIONS
 
+DEFAULT_KERNEL_OPTIONS_X86_64 = {
+    "KernelPlatform": "pc99",
+    "KernelX86MicroArch": "generic",
+} | DEFAULT_KERNEL_OPTIONS
+
 
 class KernelArch(IntEnum):
     AARCH64 = 1
     RISCV64 = 2
+    X86_64 = 3
 
     def target_triple(self) -> str:
         if self == KernelArch.AARCH64:
             return TRIPLE_AARCH64
         elif self == KernelArch.RISCV64:
             return TRIPLE_RISCV
+        elif self == KernelArch.X86_64:
+            return TRIPLE_X86_64
+        else:
+            raise Exception(f"Unsupported toolchain architecture '{self}'")
+
+    def rust_toolchain(self) -> str:
+        if self == KernelArch.AARCH64:
+            return f"{self.to_str()}-sel4-minimal"
+        elif self == KernelArch.RISCV64:
+            return f"{self.to_str()}imac-sel4-minimal"
+        elif self == KernelArch.X86_64:
+            return f"{self.to_str()}-sel4-minimal"
         else:
             raise Exception(f"Unsupported toolchain target triple '{self}'")
 
@@ -69,11 +90,16 @@ def is_riscv(self) -> bool:
     def is_arm(self) -> bool:
         return self == KernelArch.AARCH64
 
+    def is_x86(self) -> bool:
+        return self == KernelArch.X86_64
+
     def to_str(self) -> str:
         if self == KernelArch.AARCH64:
             return "aarch64"
         elif self == KernelArch.RISCV64:
             return "riscv64"
+        elif self == KernelArch.X86_64:
+            return "x86_64"
         else:
             raise Exception(f"Unsupported arch {self}")
 
@@ -89,7 +115,7 @@ class BoardInfo:
     name: str
     arch: KernelArch
     gcc_cpu: Optional[str]
-    loader_link_address: int
+    loader_link_address: int | None
     kernel_options: KERNEL_OPTIONS
 
 
@@ -314,6 +340,60 @@ class ConfigInfo:
             "KernelRiscvExtF": True,
         } | DEFAULT_KERNEL_OPTIONS_RISCV64,
     ),
+    BoardInfo(
+        name="x86_64_generic",
+        arch=KernelArch.X86_64,
+        gcc_cpu="generic",
+        loader_link_address=None,
+        kernel_options={
+            # @billn revisit
+            "KernelSupportPCID": False,
+            "KernelVTX": False,
+        } | DEFAULT_KERNEL_OPTIONS_X86_64,
+    ),
+    # This particular configuration requires support for Intel VT-x
+    # (plus nested virtualisation on your host if targeting QEMU).
+    # AMD SVM is currently unsupported by seL4.
+    BoardInfo(
+        name="x86_64_generic_vtx",
+        arch=KernelArch.X86_64,
+        gcc_cpu="generic",
+        loader_link_address=None,
+        kernel_options={
+            # @billn revisit
+            "KernelSupportPCID": False,
+            "KernelVTX": True,
+            "KernelX86_64VTX64BitGuests": True,
+        } | DEFAULT_KERNEL_OPTIONS_X86_64,
+    ),
+    # BoardInfo(
+    #     name="x86_64_generic_no_pcid",
+    #     arch=KernelArch.X86_64,
+    #     gcc_cpu="generic",
+    #     loader_link_address=None,
+    #     kernel_options={
+    #         "KernelVTX": False,
+    #         # QEMU TCG and some CPUs doesn't support PCID, so we have a
+    #         # special configuration here for convenience.
+    #         # For the generic configs, we want that on, as it improve context switching
+    #         # performance by allowing seL4 to skip flushing the entire TLB when
+    #         # switching page tables.
+    #         "KernelSupportPCID": False,
+    #     } | DEFAULT_KERNEL_OPTIONS_X86_64,
+    # ),
+    # BoardInfo(
+    #     name="x86_64_generic_no_skim",
+    #     arch=KernelArch.X86_64,
+    #     gcc_cpu="generic",
+    #     loader_link_address=None,
+    #     kernel_options={
+    #         "KernelVTX": False,
+    #         # No mitigation against Meltdown attack for non-vulnerable processors to
+    #         # prevent needless performance degredation
+    #         "KernelSkimWindow": False,
+    #     } | DEFAULT_KERNEL_OPTIONS_X86_64,
+    # ),
+    # # @billn Do we need a x86_64_generic_no_pcid_no_skim ??
 )
 
 SUPPORTED_CONFIGS = (
@@ -339,12 +419,17 @@ class ConfigInfo:
         kernel_options={
             "KernelDebugBuild": False,
             "KernelVerificationBuild": False,
-            "KernelBenchmarks": "track_utilisation"
+            "KernelBenchmarks": "track_utilisation",
+            "KernelSignalFastpath": True,
         },
         kernel_options_arch={
             KernelArch.AARCH64: {
                 "KernelArmExportPMUUser": True,
             },
+            KernelArch.X86_64: {
+                "KernelExportPMCUser": True,
+                "KernelX86DangerousMSR": True,
+            }
         },
     ),
 )
@@ -520,11 +605,13 @@ def build_sel4(
             copy(p, dest)
             dest.chmod(0o744)
 
-    platform_gen = sel4_build_dir / "gen_headers" / "plat" / "machine" / "platform_gen.json"
-    dest = root_dir / "board" / board.name / config.name / "platform_gen.json"
-    dest.unlink(missing_ok=True)
-    copy(platform_gen, dest)
-    dest.chmod(0o744)
+    if not board.arch.is_x86():
+        # only non-x86 platforms have this file to describe memory regions
+        platform_gen = sel4_build_dir / "gen_headers" / "plat" / "machine" / "platform_gen.json"
+        dest = root_dir / "board" / board.name / config.name / "platform_gen.json"
+        dest.unlink(missing_ok=True)
+        copy(platform_gen, dest)
+        dest.chmod(0o744)
 
     gen_config_path = sel4_install_dir / "libsel4/include/kernel/gen_config.json"
     with open(gen_config_path, "r") as f:
@@ -637,9 +724,66 @@ def build_lib_component(
         dest.chmod(0o744)
 
 
+def build_initialiser(
+    component_name: str,
+    custom_rust_sel4_dir: Path,
+    root_dir: Path,
+    build_dir: Path,
+    board: BoardInfo,
+    config: ConfigInfo,
+) -> None:
+    sel4_src_dir = build_dir / board.name / config.name / "sel4" / "install"
+
+    cargo_cross_options = "-Z build-std=core,alloc,compiler_builtins -Z build-std-features=compiler-builtins-mem"
+    cargo_target = board.arch.rust_toolchain()
+    rust_target_path = Path("initialiser/support/targets").absolute()
+
+    dest = (
+        root_dir / "board" / board.name / config.name / "elf" / f"{component_name}.elf"
+    )
+
+    # To save on build times, we share a single 'build target' dir for the component,
+    # this means many initialiser dependencies do not have to be rebuilt unless something
+    # with the seL4 headers changes or the target architecture.
+    rust_target_dir = build_dir / component_name
+    component_build_dir = build_dir / board.name / config.name / component_name
+    component_build_dir.mkdir(exist_ok=True, parents=True)
+
+    if custom_rust_sel4_dir is None:
+        capdl_init_elf = component_build_dir / "bin" / "sel4-capdl-initializer.elf"
+        cmd = f"""
+            RUSTC_BOOTSTRAP=1 \
+            RUST_TARGET_PATH={rust_target_path} SEL4_PREFIX={sel4_src_dir.absolute()} \
+            cargo install {cargo_cross_options} \
+            --target {cargo_target} \
+            --git https://github.com/au-ts/rust-seL4 --branch capdl_dev sel4-capdl-initializer \
+            --target-dir {rust_target_dir} \
+            --root {component_build_dir}
+        """
+    else:
+        capdl_init_elf = custom_rust_sel4_dir / "target" / cargo_target / "release" / "sel4-capdl-initializer.elf"
+        cmd = f"""
+            cd {custom_rust_sel4_dir} && SEL4_PREFIX={sel4_src_dir.absolute()} {cargo_env} \
+            cargo build {cargo_cross_options} --target {cargo_target} \
+            --release -p sel4-capdl-initializer
+        """
+
+    r = system(cmd)
+    if r != 0:
+        raise Exception(
+            f"Error building: {component_name} for board: {board.name} config: {config.name}"
+        )
+
+    dest.unlink(missing_ok=True)
+    copy(capdl_init_elf, dest)
+    # Make output read-only
+    dest.chmod(0o744)
+
+
 def main() -> None:
     parser = ArgumentParser()
     parser.add_argument("--sel4", type=Path, required=True)
+    parser.add_argument("--rust-sel4", type=Path, required=False, default=None, help="Compile capDL initialiser from local repository")
     parser.add_argument("--tool-target-triple", default=get_tool_target_triple(), help="Compile the Microkit tool for this target triple")
     parser.add_argument("--llvm", action="store_true", help="Cross-compile seL4 and Microkit's run-time targets with LLVM")
     parser.add_argument("--boards", metavar="BOARDS", help="Comma-separated list of boards to support. When absent, all boards are supported.")
@@ -661,8 +805,10 @@ def main() -> None:
 
     global TRIPLE_AARCH64
     global TRIPLE_RISCV
+    global TRIPLE_X86_64
     TRIPLE_AARCH64 = args.gcc_toolchain_prefix_aarch64
     TRIPLE_RISCV = args.gcc_toolchain_prefix_riscv64
+    TRIPLE_X86_64 = args.gcc_toolchain_prefix_x86_64
 
     version = args.version
 
@@ -745,7 +891,6 @@ def main() -> None:
                 sel4_gen_config = build_sel4(sel4_dir, root_dir, build_dir, board, config, args.llvm)
             loader_printing = 1 if config.name == "debug" else 0
             loader_defines = [
-                ("LINK_ADDRESS", hex(board.loader_link_address)),
                 ("PRINTING", loader_printing)
             ]
             # There are some architecture dependent configuration options that the loader
@@ -761,9 +906,12 @@ def main() -> None:
                     raise Exception("Unexpected ARM physical address bits defines")
                 loader_defines.append(("PHYSICAL_ADDRESS_BITS", arm_pa_size_bits))
 
-            build_elf_component("loader", root_dir, build_dir, board, config, args.llvm, loader_defines)
+            if not board.arch.is_x86():
+                loader_defines.append(("LINK_ADDRESS", hex(board.loader_link_address)))
+                build_elf_component("loader", root_dir, build_dir, board, config, args.llvm, loader_defines)
             build_elf_component("monitor", root_dir, build_dir, board, config, args.llvm, [])
             build_lib_component("libmicrokit", root_dir, build_dir, board, config, args.llvm)
+            build_initialiser("initialiser", args.rust_sel4, root_dir, build_dir, board, config)
 
     # Setup the examples
     for example, example_path in EXAMPLES.items():
@@ -780,6 +928,7 @@ def main() -> None:
             dest.chmod(0o744)
 
     if not args.skip_tar:
+        print(f"Generating {tar_file}")
         # At this point we create a tar.gz file
         with tar_open(tar_file, "w:gz") as tar:
             tar.add(root_dir, arcname=root_dir.name, filter=tar_filter)