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
35 changes: 33 additions & 2 deletions example/cap_sharing/Makefile
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)
endif
4 changes: 4 additions & 0 deletions example/cap_sharing/cap_sharing.system
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@
SPDX-License-Identifier: BSD-2-Clause
-->
<system>
<cnode name="sharing_cnode" size_bits="8" />

<protection_domain name="primary" priority="1">
<program_image path="cap_sharing.elf" />

Expand All @@ -16,6 +18,8 @@
<!-- You can also have it of yourself -->
<cap_sc slot="3" pd="primary" />
<cap_tcb slot="4" pd="primary" />

<cap_cspace slot="5" cnode_name="sharing_cnode" />
</cspace>
</protection_domain>

Expand Down
8 changes: 6 additions & 2 deletions libmicrokit/include/microkit.h
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