In the QEMU toolchain setup, I built and booted a single protection domain. Then I looked at system descriptions and capability-based authority. The next useful experiment is to connect two isolated programs without treating communication as an implicit privilege.
Microkit channels give us a small, explicit place to start. A channel connects exactly two protection domains (PDs). For this experiment, one PD sends a notification and the other handles it. A notification is a signal, not a payload-bearing message. We will use shared memory or protected procedures in a later experiment if we need to move data.
Describe the Connection
Create a new working directory and save the following as channels.system:
<?xml version="1.0" encoding="UTF-8"?>
<system>
<protection_domain name="sender">
<program_image path="sender.elf" />
</protection_domain>
<protection_domain name="receiver">
<program_image path="receiver.elf" />
</protection_domain>
<channel>
<end pd="sender" id="1" />
<end pd="receiver" id="2" />
</channel>
</system>
The two channel IDs are local to their respective PDs. The sender calls channel 1; the receiver observes channel 2. Neither identifier is a global address for the other process. Microkit provisions the channel and the authority associated with it from this description.
Write the Sender
Save as sender.c:
#include <microkit.h>
#define RECEIVER_CHANNEL 1
void init(void)
{
microkit_dbg_puts("sender: notifying receiver\n");
microkit_notify(RECEIVER_CHANNEL);
}
void notified(microkit_channel ch)
{
(void)ch;
}
The sender signals once during initialization. This is intentionally a one-shot example: there is no timer or event loop generating repeated traffic.
Write the Receiver
Save as receiver.c:
#include <microkit.h>
#define SENDER_CHANNEL 2
void init(void)
{
microkit_dbg_puts("receiver: initialized\n");
}
void notified(microkit_channel ch)
{
if (ch == SENDER_CHANNEL) {
microkit_dbg_puts("receiver: notification received\n");
}
}
The notified entry point runs when Microkit delivers a notification to this PD. Checking the channel identifier is important once a domain has more than one communication path.
Build the Two Programs
This experiment uses Microkit SDK 2.4.0, the qemu_virt_aarch64 board, and its debug configuration, matching Part 1. First export MICROKIT_SDK to the directory containing the SDK's VERSION, board, and bin entries.
The following commands assume the AArch64 cross compiler and linker from Part 1 are installed. Set the tools for your host:
export CC=aarch64-elf-gcc
export LD=aarch64-elf-ld
export CC=aarch64-linux-gnu-gcc
export LD=aarch64-linux-gnu-ld
Then run the common build steps in the directory containing the three files:
set -eu
: "${MICROKIT_SDK:?Set MICROKIT_SDK first}"
BOARD_DIR="$MICROKIT_SDK/board/qemu_virt_aarch64/debug"
mkdir -p build
for name in sender receiver; do
"$CC" -c -nostdlib -ffreestanding -g -O2 -Wall -Werror \
-mstrict-align -I"$BOARD_DIR/include" \
"$name.c" -o "build/$name.o"
"$LD" -L"$BOARD_DIR/lib" "build/$name.o" \
-lmicrokit -Tmicrokit.ld -o "build/$name.elf"
done
"$MICROKIT_SDK/bin/microkit" channels.system \
--search-path build \
--board qemu_virt_aarch64 \
--config debug \
-o build/loader.img \
-r build/report.txt
The build should produce sender.elf, receiver.elf, loader.img, and report.txt under build/. These commands are a reproducible example based on the SDK's hello build pattern, not a claim that I have independently executed this exact two-PD build.
Boot with QEMU
Use the same QEMU configuration as the first article:
qemu-system-aarch64 \
-machine virt,virtualization=on \
-cpu cortex-a53 -smp 1 -m 2G \
-nographic -serial mon:stdio -nic none \
-device loader,file=build/loader.img,addr=0x70000000,cpu-num=0
qemu-system-aarch64 \
-object memory-backend-ram,id=guestmem,size=2G,reserve=off \
-machine virt,virtualization=on,memory-backend=guestmem \
-cpu cortex-a53 -smp 1 -m 2G \
-nographic -serial mon:stdio -nic none \
-device loader,file=build/loader.img,addr=0x70000000,cpu-num=0
Look for output containing the following lines (startup messages and the ordering of initialization output may differ):
sender: notifying receiver
receiver: initialized
receiver: notification received
The key observation is that the receiver's notified handler runs. Exit QEMU with Ctrl+A, then X.
What Did We Actually Establish?
We configured two separate protection domains, built two executable images, and declared one communication channel. The sender did not discover or invoke the receiver by name at runtime; it used the local channel identifier provisioned by the system description.
There are important limits to this result. Notifications do not carry application data, and multiple notifications can coalesce before the receiver runs. This demonstration does not measure latency, prove application-level isolation, or constitute formal verification of the two programs. It does illustrate how a communication path can be made explicit and reviewable.
A useful follow-up exercise is to remove the channel element and try building again. The example no longer has the declared communication authority, which is the design property I want to keep in view when systems grow.