Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
60 changes: 30 additions & 30 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

8 changes: 4 additions & 4 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -12,12 +12,12 @@ members = [
]

[workspace.dependencies.sel4-capdl-initializer]
git = "https://github.com/seL4/rust-sel4"
rev = "413940c8058da32098c464f6cd09e550b230505c"
git = "https://github.com/au-ts/rust-sel4"
rev = "535c47d3044f1de7dd54b80d485b51f9e105c8be"

[workspace.dependencies.sel4-capdl-initializer-types]
git = "https://github.com/seL4/rust-sel4"
rev = "413940c8058da32098c464f6cd09e550b230505c"
git = "https://github.com/au-ts/rust-sel4"
rev = "535c47d3044f1de7dd54b80d485b51f9e105c8be"

[profile.release.package.microkit-tool]
strip = true
11 changes: 11 additions & 0 deletions docs/manual.md
Original file line number Diff line number Diff line change
Expand Up @@ -255,6 +255,16 @@ a size isn't specified, the memory region will be sized by the length
of the prefill file, rounded up to the smallest page size or the user
specified page size.

A *memory region* can also be prefilled with bootinfo by the capDL Initialiser
Comment thread
terryzbai marked this conversation as resolved.
via the paramter `prefill_bootinfo` in the [System Description File](#sysdesc).
If a size isn't specified, the memory region defaults to a single smallest page.
The supported bootinfo types include:
* `x86_vbe`
* `x86_mbmap`
* `x86_acpi_rsdp`
* `x86_framebuffer`
* `x86_tsc_freq`

## Channels {#channels}

A *channel* enables two protection domains to interact using protected procedures or notifications.
Expand Down Expand Up @@ -1037,6 +1047,7 @@ It supports the following attributes:
* `page_size`: (optional) Size of the pages used in the memory region; must be a supported page size if provided. Defaults to the largest page size for the target architecture that the memory region is aligned to.
* `phys_addr`: (optional) The physical address for the start of the memory region (must be a multiple of the page size).
* `prefill_path`: (optional) Path to a file containing data that the memory region will be filled with at initialisation.
* `prefill_bootinfo`: (optional) Bootinfo type that the memmory region will be filled with by the capDL initialiser.

The `memory_region` element does not support any child elements.

Expand Down
80 changes: 80 additions & 0 deletions example/bootinfo/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
#
# Copyright 2026, 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

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),x86_64)
TARGET_TRIPLE := x86_64-linux-gnu
CFLAGS_ARCH := -march=x86-64 -mtune=generic
KERNEL := $(BOARD_DIR)//elf/sel4.elf
KERNEL_32B := $(BOARD_DIR)//elf/sel4_32.elf
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 := bootinfo.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):
mkdir -p $@

$(BUILD_DIR)/%.o: %.c Makefile | $(BUILD_DIR)
$(CC) -c $(CFLAGS) $< -o $@

$(BUILD_DIR)/%.elf: $(BUILD_DIR)/%.o
$(LD) $(LDFLAGS) $^ $(LIBS) -o $@

$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) bootinfo.system
$(MICROKIT_TOOL) bootinfo.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)

qemu: $(IMAGE_FILE) $(KERNEL_32B)
ifeq ($(ARCH),x86_64)
qemu-system-x86_64 \
-cpu qemu64,+fsgsbase,+pdpe1gb,+xsaveopt,+xsave \
-m "1G" \
-display none \
-serial mon:stdio \
-kernel $(KERNEL_32B) \
-initrd $(IMAGE_FILE)
else
$(error Unsupported ARCH)
endif
30 changes: 30 additions & 0 deletions example/bootinfo/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
<!--
Copyright 2026, UNSW
SPDX-License-Identifier: CC-BY-SA-4.0
-->
# Example - Hello World

This is a basic example that demonstrates how one can define
a MemoryRegion prefilled with BootInfo and map it to a PD, so
the PD can read the BootInfo in userland.

Supported BootInfo includes:
- x86_vbe
- x86_mbmap
- x86_acpi_rsdp
- x86_framebuffer
- x86_tsc_freq

As Microkit loader does not pass the DTB through on ARM and RISC-V,
so only x86 is supported in this example for now.

## Building

```sh
mkdir build
make BUILD_DIR=build MICROKIT_BOARD=<board> MICROKIT_CONFIG=<debug/release/benchmark> MICROKIT_SDK=/path/to/sdk qemu
```

## Running

See instructions for your board in the manual.
Loading