Domain schedules

Cargo.toml

@@ -12,12 +12,12 @@ members = [
 ]
 
 [workspace.dependencies.sel4-capdl-initializer]
-git = "https://github.com/seL4/rust-sel4"
-rev = "cf43f5d0a97854e9916cc999fdd97ff3b5fbea7b"
+git = "https://github.com/au-ts/rust-sel4"
+branch = "domain_set"
 
 [workspace.dependencies.sel4-capdl-initializer-types]
-git = "https://github.com/seL4/rust-sel4"
-rev = "cf43f5d0a97854e9916cc999fdd97ff3b5fbea7b"
+git = "https://github.com/au-ts/rust-sel4"
+branch = "domain_set"
 
 [profile.release.package.microkit-tool]
 strip = true

build_sdk.py

@@ -489,6 +489,16 @@ def elaborate_all_board_configs(board: BoardInfo) -> list[ConfigInfo]:
             }
             elaborated_configs.append(config)
 
+    for config in SUPPORTED_CONFIGS:
+        config = copy.deepcopy(config)
+        config.name = f"domain-{config.name}"
+        config.kernel_options |= {
+            "KernelTimerFrequency": True,
+            "KernelNumDomains": 32,
+            "KernelNumDomainSchedules": 64,
+        }
+        elaborated_configs.append(config)
+
     return elaborated_configs
 
 

docs/manual.md

@@ -109,6 +109,7 @@ This document attempts to clearly describe all of these terms, however as the co
 * [interrupt](#irq)
 * [fault](#fault)
 * [ioport](#ioport)
+* [domain scheduling](#domain)
 
 ## System {#system}
 
@@ -186,6 +187,12 @@ Runnable PDs of the same priority are scheduled in a round-robin manner.
 
 **Passive** determines whether the PD is passive. A passive PD will have its scheduling context revoked after initialisation and then bound instead to the PD's notification object. This means the PD will be scheduled on receiving a notification, whereby it will run on the notification's scheduling context. When the PD receives a *protected procedure* by another PD or a *fault* caused by a child PD, the passive PD will run on the scheduling context of the callee.
 
+#### Domain scheduling
+
+If a Microkit system is built with a domain supported (`release_domain, debug_domain`) config, the PD can be assigned to a scheduling **domain** in the system description. If a PD is assigned to a domain, then the PD will only be allowed to execute when that domain is active. Which domain is active at any given point in time is determined by the [domain schedule](#domain).
+
+The user can describe up to 32 distinct domains by default, and 64 different domain schedule entries. These defaults can be changed in `build_sdk.py` in `elaborate_all_board_configs`. There are two kernel config options: `KernelNumDomains` and `KernelNumDomainSchedules`.
+
 ## Virtual Machines {#vm}
 
 A *virtual machine* (VM) is a runtime abstraction for running guest operating systems in Microkit. It is similar
@@ -346,6 +353,10 @@ delivered to another PD, the fault being handled depends on when the parent PD i
 
 I/O ports are x86 mechanisms to access certain physical devices (e.g. PC serial ports or PCI) using the `in` and `out` CPU instructions. The system description specifies if a protection domain have access to certain port address ranges. These accesses will be executed by seL4 and the result returned to protection domains.
 
+# Domain Scheduling {#domain}
+
+Microkit can be built with experimental support for a method of temporally isolating different groups of PDs called domain scheduling. On a Microkit system, only one domain is active at a time, and the kernel alternates between domains according to a round-robin schedule. A domain schedule consists of an ordered list of domains, each with an associated length of time to run. The kernel will then activate a domain for the specified length of time; after that time has passed, it will deactivate that domain and activate the next domain for its length of time, and so on, proceeding through the list until it wraps back to the first domain. PDs are assigned to domains, such that when a certain domain is active, only PDs belonging to that domain will be scheduled to run.
+
 # SDK {#sdk}
 
 Microkit is distributed as a software development kit (SDK).
@@ -984,6 +995,7 @@ Within the `system` root element the following child elements are supported:
 * `protection_domain`
 * `memory_region`
 * `channel`
+* `domain_schedule` (If using one of the domain configs)
 
 ## `protection_domain`
 
@@ -1000,6 +1012,7 @@ It supports the following attributes:
   Must be be between 4KiB and 16MiB and be 4K page-aligned. Defaults to 8KiB.
 * `cpu`: (optional) set the physical CPU core this PD will run on. Defaults to zero.
 * `smc`: (optional, only on ARM) Allow the PD to give an SMC call for the kernel to perform.. Defaults to false.
+* `domain`: (optional, experimental) Specifies the name of the scheduling domain the PD belongs to.
 
 Additionally, it supports the following child elements:
 
@@ -1135,6 +1148,26 @@ The `end` element has the following attributes:
 The `id` is passed to the PD in the `notified` and `protected` entry points.
 The `id` should be passed to the `microkit_notify` and `microkit_ppcall` functions.
 
+## `domain_schedule`
+
+The `domain_schedule` element, by default, has a list of up to 64 `domain` child elements, and can describe 32 different domains. (bounded by the kernel config). This can be configured by changing the number of schedule entries defined in `elaborate_all_board_configs` in `build_sdk.py`. Each child specifies a particular timeslice in the domain schedule and the order of the child elements specifies the order in which the timeslices will be scheduled. A domain may be named more than once in the schedule, in which case the domain will have multiple timeslices in the schedule.
+
+The `domain` element has the following attributes:
+
+* `name`: Name of the domain.
+* `length`: Length of time the domain will run each time it is active, in microseconds on Aarch64 and Riscv64. On x86 this length is currently defined in ticks as we don't have a static definition of the timer frequency.
+
+The `name` attribute of each `domain` element can be referenced in the `domain` attribute of a `protection_domain` element.
+
+The `domain_idx_shift` element has the following attribute:
+* `shift`: This is the start index of where we will construct our schedule. So if we shift by 5, we will begin constructing the domain schedule from index 5 onwards. If not specified, no shift will be applied, and we will start constructing the schedule from index 0.
+
+
+The `domain_start` element has the following attribute:
+* `index`: This is the start index of the domain schedule. When the kernel reaches the end of the domain schedule, it will wrap around to this index again. This index is an offset into the user defined schedule, and not an absolute index. If no domain start index is set, then the Microkit tool will set this to 0 by default.
+
+The `domain_schedule` element is only valid if the using one of the domain configs (`domain-release`, `domain-debug`, `domain-benchmark`).
+
 # Board Support Packages {#bsps}
 
 This chapter describes the board support packages that are available in the SDK.
@@ -1818,6 +1851,8 @@ which PD caused an exception and details on the PD's state at the time of the fa
 Other than printing fault details, the monitor does not do anything to handle
 the fault, it will simply go back to sleep waiting for any other faults.
 
+When domains are enabled, we will build one monitor for each domain.
+
 ## libmicrokit {#libmicrokit_internals}
 
 Unlike the previous sections, libmicrokit is not its own program but it is worth

example/hello_domains/Makefile

@@ -0,0 +1,70 @@
+#
+# Copyright 2021, Breakaway Consulting Pty. Ltd.
+#
+# 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
+
+ifeq ($(strip $(MICROKIT_CONFIG)),)
+$(error MICROKIT_CONFIG must be specified)
+endif
+
+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 ifeq ($(ARCH),x86_64)
+	TARGET_TRIPLE := x86_64-linux-gnu
+	CFLAGS_ARCH := -march=x86-64 -mtune=generic
+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
+
+HELLO_OBJS := hello.o
+
+IMAGES := hello.elf
+CFLAGS := -nostdlib -ffreestanding -g -O3 -Wall  -Wno-unused-function -Werror -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
+
+all: $(IMAGE_FILE)
+
+$(BUILD_DIR)/%.o: %.c Makefile
+	$(CC) -c $(CFLAGS) $< -o $@
+
+$(BUILD_DIR)/hello.elf: $(addprefix $(BUILD_DIR)/, $(HELLO_OBJS))
+	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
+
+$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) hello.system
+	$(MICROKIT_TOOL) hello.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)

example/hello_domains/README.md

@@ -0,0 +1,22 @@
+<!--
+     Copyright 2024, UNSW
+     SPDX-License-Identifier: CC-BY-SA-4.0
+-->
+# Example - Hello World
+
+This is a basic hello world example with domains. There are three protection
+domains, all with the same source ELF. Each protection domain is assigned to
+its own domain. The domain schedule will infinitely cycle through these domains.
+
+All supported platforms are supported in this example.
+
+## Building
+
+```sh
+mkdir build
+make BUILD_DIR=build MICROKIT_BOARD=<board> MICROKIT_CONFIG=<debug/release/benchmark> MICROKIT_SDK=/path/to/sdk
+```
+
+## Running
+
+See instructions for your board in the manual.

example/hello_domains/hello.c

@@ -0,0 +1,26 @@
+/*
+ * Copyright 2021, Breakaway Consulting Pty. Ltd.
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+#include <stdint.h>
+#include <microkit.h>
+
+void init(void)
+{
+    for (uint64_t i = 0; i < 99999999; i++) {
+        if (i == 99999998) {
+            microkit_dbg_puts("hello, world from ");
+            microkit_dbg_puts(microkit_name);
+            microkit_dbg_puts("\n");
+            i = 0;
+        } else {
+            asm("nop");
+        }
+    }
+
+}
+
+void notified(microkit_channel ch)
+{
+}

example/hello_domains/hello.system

@@ -0,0 +1,25 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2021, Breakaway Consulting Pty. Ltd.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <domain_schedule>
+        <domain name="domain_1" length="1000000" />
+        <domain name="domain_2" length="1000000" />
+        <domain name="domain_3" length="2000000" />
+    </domain_schedule>
+
+    <protection_domain name="hello" domain="domain_1">
+        <program_image path="hello.elf" />
+    </protection_domain>
+
+    <protection_domain name="hello_2" domain="domain_2">
+        <program_image path="hello.elf" />
+    </protection_domain>
+
+    <protection_domain name="hello_3" domain="domain_3">
+        <program_image path="hello.elf" />
+    </protection_domain>
+</system>

monitor/src/main.c

@@ -32,6 +32,7 @@
 extern seL4_IPCBuffer __sel4_ipc_buffer_obj;
 seL4_IPCBuffer *__sel4_ipc_buffer = &__sel4_ipc_buffer_obj;
 
+char monitor_name[MAX_NAME_LEN];
 char pd_names[MAX_PDS][MAX_NAME_LEN];
 seL4_Word pd_names_len;
 char vm_names[MAX_VMS][MAX_NAME_LEN] __attribute__((unused));
@@ -897,7 +898,9 @@ void main(void)
     }
 #endif
 
-    puts("MON|INFO: Microkit Monitor started!\n");
+    puts("MON|INFO: Microkit Monitor started: '");
+    puts(monitor_name);
+    puts("'\n");
 
     monitor();
 }