Skip to content

Switch to two level cnodes #538

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
terryzbai wants to merge 7 commits into
base: main
Choose a base branch
from
Draft

Switch to two level cnodes #538

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
a6e34f9
tool/elf: decouple program headers from segments
dreamliner787-9 Jun 19, 2026
0c8df63
tool/elf: refactored program headers table mgmt
dreamliner787-9 Jun 19, 2026
c7abd5a
tool/elf: + segment with multiple program headers
dreamliner787-9 Jun 19, 2026
d9b1e0a
Switch rust-sel4 to mainline commit
dreamliner787-9 Jun 22, 2026
2ae2c19
Make two-level CNodes for PD's CSpace
terryzbai Jun 26, 2026
b68bb06
example: add rules for QEMU tests in Makefile
terryzbai Jun 26, 2026
04bef0b
tool: check slot of extra caps
terryzbai Jun 26, 2026
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
93 changes: 62 additions & 31 deletions Cargo.lock
View file
Open in desktop

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
View file
Open in desktop
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/au-ts/rust-sel4"
rev = "33cb132571121a8d846ad3be9066617087ee5c32"
git = "https://github.com/seL4/rust-sel4"
rev = "c30d0e44fb32c15239049ce402ef2a8c72499aa3"

[workspace.dependencies.sel4-capdl-initializer-types]
git = "https://github.com/au-ts/rust-sel4"
rev = "33cb132571121a8d846ad3be9066617087ee5c32"
git = "https://github.com/seL4/rust-sel4"
rev = "c30d0e44fb32c15239049ce402ef2a8c72499aa3"

[profile.release.package.microkit-tool]
strip = true
35 changes: 33 additions & 2 deletions example/cap_sharing/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ LIBS := -lmicrokit -Tmicrokit.ld

IMAGE_FILE = $(BUILD_DIR)/loader.img
REPORT_FILE = $(BUILD_DIR)/report.txt
SPEC = $(BUILD_DIR)/capdl_spec.json
KERNEL_32B = $(BUILD_DIR)/sel4_32.elf

all: $(IMAGE_FILE)

Expand All @@ -67,5 +69,34 @@ $(BUILD_DIR)/%.o: %.c Makefile | $(BUILD_DIR)
$(BUILD_DIR)/%.elf: $(BUILD_DIR)/%.o
$(LD) $(LDFLAGS) $^ $(LIBS) -o $@

$(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) cap_sharing.system
$(MICROKIT_TOOL) cap_sharing.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
$(IMAGE_FILE) $(KERNEL_32B) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(IMAGES)) cap_sharing.system
$(MICROKIT_TOOL) cap_sharing.system --search-path $(BUILD_DIR) --board $(MICROKIT_BOARD) --config $(MICROKIT_CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE) --capdl-json $(SPEC)

ifeq ($(ARCH),x86_64)
qemu: $(KERNEL_32B) $(IMAGE_FILE)
qemu-system-x86_64 \
-cpu qemu64,+fsgsbase,+pdpe1gb,+xsaveopt,+xsave \
-m "1G" \
-display none \
-serial mon:stdio \
-kernel $(KERNEL_32B) \
-initrd $(IMAGE_FILE)
else ifeq ($(ARCH),aarch64)
qemu: $(IMAGE_FILE)
qemu-system-aarch64 \
-machine virt,virtualization=on -cpu cortex-a53 \
-nographic \
-m size=2G \
-serial mon:stdio \
-device loader,file=$(IMAGE_FILE),addr=0x70000000,cpu-num=0
else ifeq ($(ARCH),riscv64)
qemu: $(IMAGE_FILE)
qemu-system-riscv64 \
-machine virt \
-kernel $(IMAGE_FILE) \
-nographic \
-m size=2G \
-serial mon:stdio
else
$(error Unsupported ARCH)
Comment thread
terryzbai marked this conversation as resolved.
endif
8 changes: 6 additions & 2 deletions libmicrokit/include/microkit.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,10 @@ typedef seL4_MessageInfo_t microkit_msginfo;
#define BASE_IOPORT_CAP 394
#define BASE_USER_CAPS 458

/* This should be kept in sync with `PD_ROOT_CAP_BITS` in capdl/builder.rs */
#define PD_ROOT_CAP_BITS 6
#define PD_ROOT_CAP_SIZE (1ULL << PD_ROOT_CAP_BITS)

#define MICROKIT_MAX_USER_CAPS 128
#define MICROKIT_MAX_CHANNELS 62
#define MICROKIT_MAX_CHANNEL_ID (MICROKIT_MAX_CHANNELS - 1)
Expand Down Expand Up @@ -594,9 +598,9 @@ static inline void microkit_deferred_irq_ack(microkit_channel ch)
**/
static inline seL4_CPtr microkit_cspace_root_slot_to_cptr(seL4_Word slot)
{
if (slot > MICROKIT_MAX_USER_CAPS) {
if (slot == 0 || slot >= PD_ROOT_CAP_SIZE) {
return seL4_CapNull;
}

return BASE_USER_CAPS + slot;
return slot << (seL4_WordBits - PD_ROOT_CAP_BITS);
}
Loading
Loading