Skip to content

Commit

Permalink
checkpoint: linux getting to user-space, but crashing in user-space
Browse files Browse the repository at this point in the history
Problem is that FPU access in Linux or Linux user-space causes
exceptions *in Linux*, which is weird for two reasons:

1. We have the FPU enabled for QEMU in seL4 so I would think that the
   guest would have FPU access as well.
2. Why is an illegal instruction exception that happened *within Linux*
   being handled by Linux instead of the VMM?
  • Loading branch information
Ivan-Velickovic committed Sep 12, 2024
1 parent 5b2b951 commit db45bfd
Show file tree
Hide file tree
Showing 13 changed files with 623 additions and 53 deletions.
2 changes: 1 addition & 1 deletion build.zig
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ pub fn build(b: *std.Build) void {
"-Werror",
"-Wno-unused-function",
"-mstrict-align",
"-fno-sanitize=undefined", // @ivanv: ideally we wouldn't have to turn off UBSAN
// "-fno-sanitize=undefined", // @ivanv: ideally we wouldn't have to turn off UBSAN
}
});

Expand Down
Binary file modified examples/simple/board/qemu_virt_riscv64/linux
Binary file not shown.
7 changes: 1 addition & 6 deletions examples/simple/board/qemu_virt_riscv64/linux_config
Original file line number Diff line number Diff line change
Expand Up @@ -344,14 +344,11 @@ CONFIG_RISCV_ISA_C=y
CONFIG_RISCV_ISA_SVNAPOT=y
CONFIG_RISCV_ISA_SVPBMT=y
CONFIG_TOOLCHAIN_HAS_V=y
CONFIG_RISCV_ISA_V=y
CONFIG_RISCV_ISA_V_DEFAULT_ENABLE=y
CONFIG_RISCV_ISA_V_UCOPY_THRESHOLD=768
# CONFIG_RISCV_ISA_ZICBOM is not set
# CONFIG_RISCV_ISA_ZICBOZ is not set
CONFIG_TOOLCHAIN_HAS_ZIHINTPAUSE=y
CONFIG_TOOLCHAIN_NEEDS_EXPLICIT_ZICSR_ZIFENCEI=y
CONFIG_FPU=y
# CONFIG_FPU is not set
CONFIG_IRQ_STACKS=y
CONFIG_THREAD_SIZE_ORDER=2
CONFIG_RISCV_MISALIGNED=y
Expand Down Expand Up @@ -604,8 +601,6 @@ CONFIG_HAVE_PREEMPT_DYNAMIC_KEY=y
CONFIG_ARCH_WANT_LD_ORPHAN_WARN=y
CONFIG_ARCH_SUPPORTS_DEBUG_PAGEALLOC=y
CONFIG_ARCH_SUPPORTS_PAGE_TABLE_CHECK=y
CONFIG_DYNAMIC_SIGFRAME=y
CONFIG_ARCH_HAS_KERNEL_FPU_SUPPORT=y

#
# GCOV-based kernel profiling
Expand Down
46 changes: 44 additions & 2 deletions examples/simple/board/qemu_virt_riscv64/overlay.dts
Original file line number Diff line number Diff line change
Expand Up @@ -14,10 +14,52 @@
status = "disabled";
};

soc {
rtc@101000 {
status = "disabled";
};

pci@30000000 {
status = "disabled";
};

virtio_mmio@10008000 {
status = "disabled";
};

virtio_mmio@10007000 {
status = "disabled";
};

virtio_mmio@10006000 {
status = "disabled";
};

virtio_mmio@10005000 {
status = "disabled";
};

virtio_mmio@10004000 {
status = "disabled";
};

virtio_mmio@10003000 {
status = "disabled";
};

virtio_mmio@10002000 {
status = "disabled";
};

virtio_mmio@10001000 {
status = "disabled";
};
};

chosen {
stdout-path = "/uart@10000000";
bootargs = "console=ttyS0 loglevel=8 earlycon=ns16550a,0x10000000";
bootargs = "console=ttyS0 loglevel=8 earlycon=ns16550a,0x10000000 no4lvl";
linux,initrd-start = <0x8c000000>;
linux,initrd-end = <0x8d000000>;
linux,initrd-end = <0x8e000000>;
};
};
Binary file modified examples/simple/board/qemu_virt_riscv64/rootfs.cpio.gz
Binary file not shown.
2 changes: 1 addition & 1 deletion examples/simple/board/qemu_virt_riscv64/simple.system
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@

<memory_region name="serial" size="0x1_000" phys_addr="0x10000000" />

<protection_domain name="VMM" priority="254">
<protection_domain name="VMM" priority="254" stack_size="0x2000">
<program_image path="vmm.elf" />
<map mr="guest_ram" vaddr="0x80000000" perms="rw" setvar_vaddr="guest_ram_vaddr" />
<virtual_machine name="linux">
Expand Down
11 changes: 10 additions & 1 deletion examples/simple/build.zig
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ const ConfigOptions = enum {
benchmark
};

pub fn build(b: *std.Build) void {
pub fn build(b: *std.Build) !void {
const optimize = b.standardOptimizeOption(.{});

// Getting the path to the Microkit SDK before doing anything else
Expand Down Expand Up @@ -177,15 +177,24 @@ pub fn build(b: *std.Build) void {
const linux_image_path = b.fmt("board/{s}/linux", .{ microkit_board });
const kernel_image_arg = b.fmt("-DGUEST_KERNEL_IMAGE_PATH=\"{s}\"", .{ linux_image_path });

var prng = std.Random.DefaultPrng.init(blk: {
var seed: u64 = undefined;
try std.posix.getrandom(std.mem.asBytes(&seed));
break :blk seed;
});
const rand = prng.random();

const initrd_image_path = b.fmt("board/{s}/rootfs.cpio.gz", .{ microkit_board });
const initrd_image_arg = b.fmt("-DGUEST_INITRD_IMAGE_PATH=\"{s}\"", .{ initrd_image_path });
const dtb_image_arg = b.fmt("-DGUEST_DTB_IMAGE_PATH=\"{s}\"", .{ b.getInstallPath(.prefix, "linux.dtb") });
const random_arg = b.fmt("-DRANDOM=\"{}\"", .{ rand.int(usize) });
guest_images.addCSourceFile(.{
.file = libvmm_dep.path("tools/package_guest_images.S"),
.flags = &.{
kernel_image_arg,
dtb_image_arg,
initrd_image_arg,
random_arg,
"-x",
"assembler-with-cpp",
}
Expand Down
9 changes: 5 additions & 4 deletions examples/simple/vmm.c
Original file line number Diff line number Diff line change
Expand Up @@ -123,6 +123,7 @@ void init(void) {
return;
}
success = virq_register(GUEST_VCPU_ID, SERIAL_IRQ, &serial_ack, NULL);
assert(success);
/* Just in case there is already an interrupt available to handle, we ack it here. */
microkit_irq_ack(SERIAL_IRQ_CH);
/* Finally start the guest */
Expand All @@ -132,10 +133,10 @@ void init(void) {
void notified(microkit_channel ch) {
switch (ch) {
case SERIAL_IRQ_CH: {
bool success = virq_inject(GUEST_VCPU_ID, SERIAL_IRQ);
if (!success) {
LOG_VMM_ERR("IRQ %d dropped on vCPU %d\n", SERIAL_IRQ, GUEST_VCPU_ID);
}
// bool success = virq_inject(GUEST_VCPU_ID, SERIAL_IRQ);
// if (!success) {
// LOG_VMM_ERR("IRQ %d dropped on vCPU %d\n", SERIAL_IRQ, GUEST_VCPU_ID);
// }
break;
}
default:
Expand Down
Loading

0 comments on commit db45bfd

Please sign in to comment.