Multikernel

build_sdk.py

@@ -17,6 +17,7 @@
 from shutil import copy
 from pathlib import Path
 from dataclasses import dataclass
+import shutil
 from sys import executable
 from tarfile import open as tar_open, TarInfo
 import platform as host_platform
@@ -91,6 +92,7 @@ class BoardInfo:
     gcc_cpu: Optional[str]
     loader_link_address: int
     kernel_options: KERNEL_OPTIONS
+    multikernels: Optional[int] = None
 
 
 @dataclass
@@ -130,6 +132,19 @@ class ConfigInfo:
             "KernelPlatform": "maaxboard",
         } | DEFAULT_KERNEL_OPTIONS_AARCH64,
     ),
+    BoardInfo(
+        name="maaxboard_multikernel",
+        arch=KernelArch.AARCH64,
+        gcc_cpu="cortex-a53",
+        loader_link_address=0x50000000,
+        kernel_options={
+            "KernelPlatform": "maaxboard",
+            "KernelEnableMultikernelSupport": True,
+            # TODO: Derive from device tree?
+            # "KernelMultikernelNumCPUs": 4,
+            "KernelMultikernelNumCPUs": 2,
+        } | DEFAULT_KERNEL_OPTIONS_AARCH64,
+    ),
     BoardInfo(
         name="imx8mm_evk",
         arch=KernelArch.AARCH64,
@@ -185,6 +200,20 @@ class ConfigInfo:
             "KernelARMPlatform": "ultra96v2",
         } | DEFAULT_KERNEL_OPTIONS_AARCH64,
     ),
+    BoardInfo(
+        name="odroidc4_multikernel",
+        arch=KernelArch.AARCH64,
+        gcc_cpu="cortex-a55",
+        loader_link_address=0x20000000,
+        kernel_options={
+            "KernelPlatform": "odroidc4",
+            "KernelArmVtimerUpdateVOffset": False,
+            "KernelEnableMultikernelSupport": True,
+            # TODO: Derive from device tree?
+            # "KernelMultikernelNumCPUs": 4,
+            "KernelMultikernelNumCPUs": 2,
+        } | DEFAULT_KERNEL_OPTIONS_AARCH64,
+    ),
     BoardInfo(
         name="qemu_virt_aarch64",
         arch=KernelArch.AARCH64,
@@ -198,6 +227,20 @@ class ConfigInfo:
             "KernelArmExportPTMRUser": True,
         } | DEFAULT_KERNEL_OPTIONS_AARCH64,
     ),
+    BoardInfo(
+        name="qemu_virt_aarch64_multikernel",
+        arch=KernelArch.AARCH64,
+        gcc_cpu="cortex-a53",
+        loader_link_address=0x70000000,
+        kernel_options={
+            "KernelPlatform": "qemu-arm-virt",
+            "QEMU_MEMORY": "2048",
+            "KernelArmExportPTMRUser": True,
+            "KernelEnableMultikernelSupport": True,
+            # TODO: Derive from device tree?
+            "KernelMultikernelNumCPUs": 2,
+        } | DEFAULT_KERNEL_OPTIONS_AARCH64,
+    ),
     BoardInfo(
         name="qemu_virt_riscv64",
         arch=KernelArch.RISCV64,
@@ -424,7 +467,9 @@ def build_sel4(
 ) -> Dict[str, Any]:
     """Build seL4"""
     build_dir = build_dir / board.name / config.name / "sel4"
-    build_dir.mkdir(exist_ok=True, parents=True)
+    # clear to remove the cmake cache
+    shutil.rmtree(build_dir, ignore_errors=True)
+    build_dir.mkdir(parents=True)
 
     sel4_install_dir = build_dir / "install"
     sel4_build_dir = build_dir / "build"
@@ -719,7 +764,7 @@ def main() -> None:
 
     if not args.skip_tool:
         tool_target = root_dir / "bin" / "microkit"
-        test_tool()
+        # test_tool()
         build_tool(tool_target, args.tool_target_triple)
 
     if not args.skip_docs:
@@ -748,6 +793,9 @@ def main() -> None:
                     raise Exception("Unexpected ARM physical address bits defines")
                 loader_defines.append(("PHYSICAL_ADDRESS_BITS", arm_pa_size_bits))
 
+            if (num_multikernels := sel4_gen_config.get("MULTIKERNEL_NUM_CPUS")) is not None:
+                loader_defines.append(("NUM_MULTIKERNELS", num_multikernels))
+
             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)

dev_build.py

@@ -81,7 +81,7 @@ def main():
     if not BUILD_DIR.exists():
         BUILD_DIR.mkdir()
 
-    tool_rebuild = f"cd {CWD / 'tool/microkit'} && cargo build --release"
+    tool_rebuild = f"cd {CWD / 'tool/microkit'} && cargo build"
     r = system(tool_rebuild)
     assert r == 0
 
@@ -90,7 +90,7 @@ def main():
     make_env["MICROKIT_BOARD"] = args.board
     make_env["MICROKIT_CONFIG"] = args.config
     make_env["MICROKIT_SDK"] = str(release)
-    make_env["MICROKIT_TOOL"] = (CWD / "tool/microkit/target/release/microkit").absolute()
+    make_env["MICROKIT_TOOL"] = (CWD / "tool/microkit/target/debug/microkit").absolute()
     make_env["LLVM"] = str(args.llvm)
 
     # Choose the makefile based on the `--example-from-sdk` command line flag

example/benchmarks/Makefile

@@ -0,0 +1,78 @@
+#
+# Copyright 2025, UNSW.
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+ifeq ($(strip $(BUILD_DIR)),)
+$(error BUILD_DIR must be specified)
+endif
+
+ifeq ($(strip $(MICROKIT_SDK)),)
+$(error MICROKIT_SDK must be specified)
+endif
+
+ifeq ($(strip $(MICROKIT_BOARD)),)
+$(error MICROKIT_BOARD must be specified)
+endif
+
+MICROKIT_CONFIG ?= benchmark
+
+BOARD_DIR := $(MICROKIT_SDK)/board/$(MICROKIT_BOARD)/$(MICROKIT_CONFIG)
+
+ARCH := ${shell grep 'CONFIG_SEL4_ARCH  ' $(BOARD_DIR)/include/kernel/gen_config.h | cut -d' ' -f4}
+
+ifeq ($(ARCH),aarch64)
+  TARGET_TRIPLE := aarch64-none-elf
+  CFLAGS_ARCH := -mstrict-align
+else ifeq ($(ARCH),riscv64)
+  TARGET_TRIPLE := riscv64-unknown-elf
+  CFLAGS_ARCH := -march=rv64imafdc_zicsr_zifencei -mabi=lp64d
+else
+$(error Unsupported ARCH)
+endif
+
+ifeq ($(strip $(LLVM)),True)
+  CC := clang -target $(TARGET_TRIPLE)
+  AS := clang -target $(TARGET_TRIPLE)
+  LD := ld.lld
+else
+  CC := $(TARGET_TRIPLE)-gcc
+  LD := $(TARGET_TRIPLE)-ld
+  AS := $(TARGET_TRIPLE)-as
+endif
+
+MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit
+
+IMAGES := manager.elf \
+  signal_low_to_hi_same_core__high.elf signal_low_to_hi_same_core__low.elf \
+  signal_hi_to_low__high.elf signal_hi_to_low__low.elf \
+  signal_2way_low_to_hi__low.elf signal_2way_low_to_hi__mid.elf signal_2way_low_to_hi__high.elf
+
+CFLAGS := -MMD -MP -nostdlib -ffreestanding -g -O2 -Wall -Wno-unused-function -I$(BOARD_DIR)/include $(CFLAGS_ARCH)
+LDFLAGS := -L$(BOARD_DIR)/lib
+LIBS := -lmicrokit -Tmicrokit.ld
+
+IMAGE_FILE = $(BUILD_DIR)/loader.img
+REPORT_FILE = $(BUILD_DIR)/report.txt
+SYSTEM_FILE = benchmarks.system
+SYSTEM_FILE_PP = $(BUILD_DIR)/$(SYSTEM_FILE).pp
+
+all: $(IMAGE_FILE)
+
+$(BUILD_DIR)/%.o: %.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/%.elf: $(BUILD_DIR)/%.o $(BUILD_DIR)/print.o
+	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+-include $(addprefix $(BUILD_DIR)/, $(IMAGES:.elf=.d))
+-include $(BUILD_DIR)/print.d
+
+$(SYSTEM_FILE_PP): $(SYSTEM_FILE)
+	cpp -MMD -MP $< -o $@
+	sed -i '/^#/d' $@
+
+-include $(BUILD_DIR)/$(SYSTEM_FILE).d
+
+$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) $(SYSTEM_FILE_PP)
+	$(MICROKIT_TOOL) $(SYSTEM_FILE_PP) --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)

example/benchmarks/README.md

@@ -0,0 +1,38 @@
+<!--
+     Copyright 2025, UNSW
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+# Example - Benchmarks
+
+This does basic seL4 signalling performance benchmarks.
+
+Note that in these PDs we deliberately subvert the microkit implementation
+so that we have direct control over the mechanisms at play.
+
+## signal_low_to_hi_same_core
+
+This is a one way benchmark, which relies on the fact that the cycle counter
+is a core-local value. This means we can read the cycle count in the low
+priority PD and then read it again in the high priority PD and the values will
+make sense.
+
+This measures the time from a seL4_Signal in a low priority process to the
+seL4_Recv in the higher priority process, i.e. both send and receive. The
+cycle counters are measured in different threads and the end time communicated
+back via shared memory. This is because the next run after the signaller is the
+*destination*, not the *sender*.
+
+## signal_hi_to_low_same_core
+
+This measures the time from a seL4_Signal in a high priority process to when
+that signal returns. This is because higher priority processes will always run
+above low priority, so the next running will be the *sender*. This is **different**
+to the case for low to high.
+
+## signal_2way_low_to_hi_{same,cross}_core
+
+This is a two way benchmark, performing a low to a high invocation, then another
+low to high invocation; so like low -> mid -> high. This design is aimed at
+cross-core scenarios, where we don't have coherent cycle counters across cores,
+so measuring the cycle count on core *A* then core *B* won't produce sensible
+results, as is done in `signal_low_to_hi_same_core`.

example/benchmarks/benchmark.csv

@@ -0,0 +1,6 @@
+name,mean,stddev,min,max,runs,sum,sum_squared
+signal low to high same core,971.2179,23.78885578564039,944,1689,100000,97121790,94383011894
+signal high to low same core,516.18716,19.28573076485147,514,1211,100000,51618716,26682112356
+signal high to low cross core,483.24771,20.14544389572733,478,1179,100000,48324771,23393418813
+signal 2way low to high same core,1939.69662,29.848659946060586,1896,2678,100000,193969662,376331392014
+signal 2way low to high cross core,2100.82227,35.781031316155904,2034,2911,100000,210082227,441473449233

example/benchmarks/benchmark.h

@@ -0,0 +1,55 @@
+#pragma once
+
+#include <microkit.h>
+#include <stdint.h>
+
+#include "config.h"
+#include "pmu.h"
+#include "print.h"
+
+#define UNUSED __attribute__((unused))
+
+/* Because we deliberately subvert libmicrokit in these examples */
+#define INPUT_CAP 1
+#define REPLY_CAP 4
+#define DECLARE_SUBVERTED_MICROKIT()                                           \
+  void notified(microkit_channel ch) {}
+
+/* Inside a benchmark, the start-stop ch */
+#define BENCHMARK_START_STOP_CH 0
+
+#define RECORDING_BEGIN()                                                      \
+  pmu_enable();                                                                \
+  print("BEGIN\n");                                                            \
+  cycles_t sample;                                                             \
+  uint64_t sum = 0;                                                            \
+  uint64_t sum_squared = 0;                                                    \
+  cycles_t min = CYCLES_MAX;                                                   \
+  cycles_t max = CYCLES_MIN;
+
+#define RECORDING_ADD_SAMPLE(start, end)                                       \
+  /* don't let the compiler reorder these before into the benchmark */         \
+  asm volatile("" ::: "memory");                                               \
+  sample = (end - start);                                                      \
+  sum += sample;                                                               \
+  sum_squared += sample * sample;                                              \
+  min = (sample < min) ? sample : min;                                         \
+  max = (sample > max) ? sample : max;
+
+typedef struct {
+  uint64_t sum;
+  uint64_t sum_squared;
+  cycles_t min;
+  cycles_t max;
+} result_t;
+
+#define RECORDING_END(results_ptr)                              \
+  do {                                                                         \
+    /* TODO: cache flushes for multicore? */                                   \
+    print("END\n");                                                            \
+    result_t *_results = (void *)results_ptr;                \
+    _results->sum = sum;                                         \
+    _results->sum_squared = sum_squared;                         \
+    _results->min = min;                                         \
+    _results->max = max;                                         \
+  } while (0)