- Devel - lists.sel4.systems

camkes-VM with QEMU and virutal PCI device
by Samuel Weiser 28 Jun '16

28 Jun '16

Hi again, I'm playing around with camkes-vm in QEMU+KVM. I want to add a virtual PCI device to Linux, which is running as vm0 on top of seL4. However, I got stuck with some errors during system boot. My setup is as follows: QEMU is configured to share a 1MB memory region between the host and the QEMU guest (seL4). Here's what QEMU sets up: (qemu): info mtree ... 00000000fe000000-00000000fe0fffff (prio 1, RW): ivshmem-bar2-container 00000000fe000000-00000000fe0fffff (prio 0, RW)… [View More]: ivshmem.bar2 00000000febf1000-00000000febf10ff (prio 1, RW): ivshmem-mmio ... (qemu): info pci ... Bus 0, device 4, function 0: RAM controller: PCI device 1af4:1110 IRQ 11. BAR0: 32 bit memory at 0xfebf1000 [0xfebf10ff]. BAR2: 64 bit prefetchable memory at 0xfe000000 [0xfe0fffff]. id "" ... I adapted a previously working configuration (optiplex9020.camkes) accordingly with what I thought should be correct. Especially, I added vm0_config.pci_devices_iospace and vm0_config.pci_devices as well as the PCI irq. Here's the configuration: configuration { VM_CONFIGURATION_DEF() VM_PER_VM_CONFIG_DEF(0, 2) vm0.simple_untyped24_pool = 12; vm0.heap_size = 0; vm0.guest_ram_mb = 1536; vm0.kernel_cmdline = VM_GUEST_CMDLINE; vm0.kernel_image = C162_KERNEL_IMAGE; vm0.kernel_relocs = C162_KERNEL_IMAGE; vm0.initrd_image = C162_ROOTFS; vm0.iospace_domain = 0x00; vm0_config.ram = [ [ 0x20800000, 23 ], [ 0x21000000, 24 ], [ 0x22000000, 25 ], [ 0x24000000, 26], [ 0x28000000, 27], [0x30000000, 28], [0x40000000, 29] , [0x60000000, 30], [0xa0000000, 28]]; vm0_config.ioports = [ {"start":0x2f8, "end":0x2ff, "pci_device":0, "name":"COM2 Serial Port"}, {"start":0x2e8, "end":0x2ef, "pci_device":0, "name":"COM4 Serial Port"} ]; vm0_config.irqs = [ {"name":"Serial", "source":3, "level_trig":0, "active_low":0, "dest":3}, {"name":"PCI", "source":11, "level_trig":1, "active_low":1, "dest":11} ]; vm0_config.pci_devices_iospace = 1; vm0_config.pci_devices = [ {"name":"PCI", "bus":0, "dev":0x04, "fun":0, "irq":"PCI", "memory":[ {"paddr":0xfe000000, "size":0x100000, "page_bits":12}, ], }, ]; } However, after creating the MMIO frames and doing some other stuff, the boot process fails, as shown below. The error also occurs if I change or completely remove just the "memory" definition of my PCI device. I also tried different values for "iospace_domain" (QEMU should use 0 as default PCI domain). Thanks in advance for any hints and ideas! Best, Sammey Starting Loader... Parsing bootinfo... 1041793 free cap slots, from 6783 to 1048576 Untyped memory (24) 0x0000000000100000 - 0x0000000000108000 0x0000000000108000 - 0x0000000000109000 0x0000000003000000 - 0x0000000004000000 0x0000000004000000 - 0x0000000008000000 0x0000000008000000 - 0x0000000010000000 0x0000000010000000 - 0x0000000018000000 0x0000000018000000 - 0x000000001c000000 0x000000001c000000 - 0x000000001e000000 0x000000001e000000 - 0x000000001f000000 0x000000001f000000 - 0x000000001f800000 0x000000001f800000 - 0x000000001fc00000 0x0000000001b6b000 - 0x0000000001b6c000 0x0000000001b6c000 - 0x0000000001b70000 0x0000000001b70000 - 0x0000000001b80000 0x0000000001b80000 - 0x0000000001c00000 0x0000000001c00000 - 0x0000000001e00000 0x0000000001e00000 - 0x0000000001f00000 0x0000000001f00000 - 0x0000000001f80000 0x0000000001f80000 - 0x0000000001fc0000 0x0000000001fc0000 - 0x0000000001fe0000 0x0000000001fe0000 - 0x0000000001ff0000 0x0000000001ff0000 - 0x0000000001ff2000 0x0000000001ff2000 - 0x0000000001ff3000 0x0000000001ff3000 - 0x0000000001ff3800 Loader is running in domain 0 Device untyped memory (30) 0x0000000000001000 - 0x0000000000002000 0x0000000000002000 - 0x0000000000004000 0x0000000000004000 - 0x0000000000008000 0x0000000000008000 - 0x0000000000010000 0x0000000000010000 - 0x0000000000020000 0x0000000000020000 - 0x0000000000040000 0x0000000000040000 - 0x0000000000080000 0x0000000000080000 - 0x0000000000100000 0x000000001fc00000 - 0x0000000020000000 0x0000000020001000 - 0x0000000020002000 0x0000000020002000 - 0x0000000020004000 0x0000000020004000 - 0x0000000020008000 0x0000000020008000 - 0x0000000020010000 0x0000000020010000 - 0x0000000020020000 0x0000000020020000 - 0x0000000020040000 0x0000000020040000 - 0x0000000020080000 0x0000000020080000 - 0x0000000020100000 0x0000000020100000 - 0x0000000020200000 0x0000000020200000 - 0x0000000020400000 0x0000000020400000 - 0x0000000020800000 0x0000000020800000 - 0x0000000021000000 0x0000000021000000 - 0x0000000022000000 0x0000000022000000 - 0x0000000024000000 0x0000000024000000 - 0x0000000028000000 0x0000000028000000 - 0x0000000030000000 0x0000000030000000 - 0x0000000040000000 0x0000000040000000 - 0x0000000060000000 0x0000000060000000 - 0x00000000a0000000 0x00000000a0000000 - 0x00000000e0000000 0x00000000e0000000 - 0x0000000000000000 Sorting untypeds... Untyped 0 (cptr=1a39) is of size 15. Placing in slot 17... Untyped 1 (cptr=1a3a) is of size 12. Placing in slot 20... Untyped 2 (cptr=1a3b) is of size 24. Placing in slot 5... Untyped 3 (cptr=1a3c) is of size 26. Placing in slot 2... Untyped 4 (cptr=1a3d) is of size 27. Placing in slot 0... Untyped 5 (cptr=1a3e) is of size 27. Placing in slot 1... Untyped 6 (cptr=1a3f) is of size 26. Placing in slot 3... Untyped 7 (cptr=1a40) is of size 25. Placing in slot 4... Untyped 8 (cptr=1a41) is of size 24. Placing in slot 6... Untyped 9 (cptr=1a42) is of size 23. Placing in slot 7... Untyped 10 (cptr=1a43) is of size 22. Placing in slot 8... Untyped 11 (cptr=1a44) is of size 12. Placing in slot 21... Untyped 12 (cptr=1a45) is of size 14. Placing in slot 18... Untyped 13 (cptr=1a46) is of size 16. Placing in slot 15... Untyped 14 (cptr=1a47) is of size 19. Placing in slot 11... Untyped 15 (cptr=1a48) is of size 21. Placing in slot 9... Untyped 16 (cptr=1a49) is of size 20. Placing in slot 10... Untyped 17 (cptr=1a4a) is of size 19. Placing in slot 12... Untyped 18 (cptr=1a4b) is of size 18. Placing in slot 13... Untyped 19 (cptr=1a4c) is of size 17. Placing in slot 14... Untyped 20 (cptr=1a4d) is of size 16. Placing in slot 16... Untyped 21 (cptr=1a4e) is of size 13. Placing in slot 19... Untyped 22 (cptr=1a4f) is of size 12. Placing in slot 22... Untyped 23 (cptr=1a50) is of size 11. Placing in slot 23... Creating objects... ... Creating object conn1_mmio_frame_4261412864 in slot 6808, from untyped 1a3c... device frame, paddr = 0xfe000000, size = 12 bits Creating object conn1_mmio_frame_4261416960 in slot 6809, from untyped 1a3c... device frame, paddr = 0xfe001000, size = 12 bits Creating object conn1_mmio_frame_4261421056 in slot 6810, from untyped 1a3c... device frame, paddr = 0xfe002000, size = 12 bits ... Creating object vm_vm0_pre_init_ep in slot 10275, from untyped 1a3c... Creating object conn1_iospace_32 in slot 10276, from untyped 1a3c... <=== This is ignored! Creating object conn4_iport_760_767 in slot 10276, from untyped 1a3c... ... Populating slot 21 with cap to conn1_iospace_32... minting (with badge/guard 0x20)... <<seL4 [decodeCNodeInvocation/107 T0xe1ff3900 "rootserver" @804a911]: CNode Copy/Mint/Move/Mutate: Source slot invalid or empty.>> capDL-loader :: << Error: init_cnode_slot:1689: seL4_FailedLookup >> [View Less]

2 1

Autocorres Error.
by Dan DaCosta 24 Jun '16

24 Jun '16

seL4 Developers: I apologize in advance if this is not the correct place for this email. I am experimenting with Autocorres as an intern at Rockwell Collin's Advanced Technology Center in Minnesota. My latest experiment is in building a small verified library for manipulation and analysis of adjacency lists. My initial work towards this end generated the following error: exception CTERM raised (line 948 of "~/development/rockwellcollins/verification/l4v/tools/autocorres/utils.ML"): … [View More]

3 3

Resolving issue using camkes-vm with qemu
by Samuel Weiser 20 Jun '16

20 Jun '16

Hi, I just want to share some information which I needed to run camkes-vm with qemu, especially addressing one issue which prevented the guest vm to boot. I basically follow the recommendations of Adrian in [1] and only focus on the simple case without vt-d. 1. use the 'optiplex9020_onevm' configuration as it basically just specifies physical RAM. 2. enable nested KVM [2,3] 3. run QEMU with enough RAM: qemu-system-i386 -nographic \ -m 3GB \ -enable-kvm \ -cpu host \ -… [View More]

2 1

Rust application support
by Kent.Mcleod＠data61.csiro.au 20 Jun '16

20 Jun '16

Using rust (https://www.rust-lang.org) in user applications on top of seL4 with existing C libaries and apps now has limited support. See here for more information: https://wiki.sel4.systems/Rust What you can do: + Build system support for using a rust cargo project as a library or app on seL4 + Use most core libraries (core, alloc, collections, rustc_unicode, and a limited std) + Use rust dependencies from crates.io on seL4 + Use rust to implement camkes components + Using rust's … [View More]

1 0

WIll seL4 support any Unikernel
by XilongPei 16 Jun '16

16 Jun '16

Hi, According to wikipedia.org, Unikernels are specialised, single address space machine images constructed by using library operating systems. A developer selects, from a modular stack, the minimal set of libraries which correspond to the OS constructs required for their application to run. These libraries are then compiled with the application and configuration code to build sealed, fixed-purpose images (unikernels) which run directly on a hypervisor or hardware without an intervening OS … [View More]

3 2

Beaglebone black/CAmkES issue
by Julien Delange 16 Jun '16

16 Jun '16

I am using the second serial interface of the beaglebone black. According to the source code (in libsel4platsupport/plat_include/am335x/sel4platsupport/plat/hw/soc_AM335x.h), the address is 0x48022000). The following line is found in the source #define SOC_UART_1_REGS (0x48022000) So, in CAmkES, I configure the hardware component that represents the serial hardware component with the following attributes: drv.mem_attributes = "0x48022000:0x1000"; The application … [View More]

4 8

Tidying and real-time
by Jeff Waugh 16 Jun '16

16 Jun '16

This commit… https://github.com/seL4/seL4/commit/c5b6a6a58aae75129cdf5a83f861bdacddbf51d6 … is pleasing. As is the RT API. Passive servers! A seemingly viable and sensible approach to user-space scheduling! Just a quick thumbs up for recent progress. :-)

1 0

CAmkES parsing issue
by Julien Delange 11 Jun '16

11 Jun '16

Hi, I am trying to build a camked application with a UART driver. When trying to build the application, I got the following error: While rendering uart_mem.from.source: 'drv' However, the component is well define. How can I try to get more information/debug of the camkes assembly and find out what is wrong? Thanks! Note: the project can be found there: https://drive.google.com/file/d/0Bxl72qH3r6BjRGxYSXd2LUllcDQ/view?usp=shari…

3 6

camkes arm vm I/0 devices
by Josh Tuttle 08 Jun '16

08 Jun '16

Hey, We have been playing around with the busybox for tk1 that was included in the build. While trying to verify all the I/0 devices, we noticed that the Ethernet device would not come up. Looking though dmesg, it seems to load a driver but never initializes a device. Ifconfig just errors when trying to bring up eth0. Has anyone verified the I/0 devices on tk1 using this build? Not being familiar with busybox, can we follow this: http://elinux.org/Jetson/Busybox_RootFS guide to building a … [View More]

2 1

seL4 benchmarks available
by Anna Lyons 07 Jun '16

07 Jun '16

Hi all, I've just finished pushing the seL4 benchmarking suite out to github. Get it: * manifest: https://github.com/seL4/sel4bench-manifest * explore the applications: https://github.com/seL4/sel4bench. Cheers, -- Anna Lyons Kernel engineer / PhD Student DATA61 | CSIRO E anna.lyons(a)nicta.com.au<mailto:anna.lyons@nicta.com.au> www.data61.csiro.au<http://www.data61.csiro.au> CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse … [View More]

1 0