- Devel - lists.sel4.systems

Pull request of S91lighttpd
by Hugo V.C. 08 Jun '21

08 Jun '21

Hi, I'm trying to make a pull request as I want to make a very simple (yet useful) change to S91lighttpd file. I wonder where I can find this file in Git as I can find it locally in my build directory: build/overlay/etc/init.d/S91lighttpd but can not find it anywhere else in Git. I assume it is part of some prebuilt file system (overlay?) but still I can't find where this file system is in Git. Any help will be appreciated. Hugo

2 2

Status of the seL4 RISC-V platform Rocketchip
by Axel Heider 07 Jun '21

07 Jun '21

Hi, I'm wondering about the state of the seL4 RISC-V platform "Rocketchip", is anybody actively using this? At the seL4 hardware status page https://docs.sel4.systems/Hardware/rocketchip.html there is not much, and the repo https://github.com/ucb-bar/fpga-zynq has been abandoned. It points to https://github.com/sifive/freedom which has also been abandoned recently. So I wonder, is this platform effectively dead and should be removed? Axel

1 0

watch dog timer and stability mechanisms in sel4 and camkes
by MOHAMAD REZA SHAFIEI 05 Jun '21

05 Jun '21

Hi there. i'm working on my master project and try to implement a system which act as a storage system (a simple sample). so i write my components and its work correctly but some times (rarely) my threads crashes and I couldn't find problem. So i decide to use a service like watch dog timer for garanti all of threads work and when one thread failed and crashed, this mechanism detect it and start another thread or reset the system. My project is on sle4 and camkes framework, a simple solution can implement by some thread controlling (implement WDT in user mode). But I want to know is there in camkes or sel4 any mechanism for this need? a mechanism for garanti stability and system availability? can any body help me? Is there anybody which confront with this need? -- This email was Anti Virus checked by Security Gateway.

1 0

libsel4utils: load_segment memory leak bug
by wzt wzt 05 Jun '21

05 Jun '21

hello: i found a bug memory leak bug in libsel4utils/src/elf.c static int load_segment(vspace_t *loadee_vspace, vspace_t *loader_vspace, vka_t *loadee_vka, vka_t *loader_vka, const char *src, size_t file_size, int num_regions, sel4utils_elf_region_t regions[num_regions], int region_index) { seL4_CPtr loader_slot; cspacepath_t loader_frame_cap; error = vka_cspace_alloc(loader_vka, &loader_slot); [1] while (pos < segment_size && error == seL4_NoError) { reservation_t reservation; if (loadee_vaddr < region.reservation_vstart) { if ((region_index - 1) < 0) { ZF_LOGE("Invalid regions: bad elf file."); return 1; [2] } } if [2] happned, it not free the prev alloc memory, and then it's memory will be leaked. i think the correct way is invoke vka_cspace_free() before return.

3 2

Mapping VM Kernel Memory
by Michael Neises 05 Jun '21

05 Jun '21

Hello everyone, I have a question about some code I'm using from the seL4 repositories. I have a follow-up question about whether a certain memory mapping strategy is feasible. I'm looking at this kernel module: https://github.com/seL4/camkes-vm-linux/blob/master/camkes-linux-artifacts/… and at this user-space app: https://github.com/seL4/camkes-vm-linux/blob/master/camkes-linux-artifacts/… In short, there is shared memory between a camkes component and the vm-linux. I can tell that the shared memory region is given by accessing /dev/uio0. However, it's not clear to me what exactly this memory region is. As I simulate the kernel, I find this: [ 0.000000] Virtual kernel memory layout: [ 0.000000] modules : 0xffff000000000000 - 0xffff000008000000 ( 128 MB) [ 0.000000] vmalloc : 0xffff000008000000 - 0xffff7dffbfff0000 (129022 GB) [ 0.000000] .text : 0xffff000008080000 - 0xffff0000087d0000 ( 7488 KB) [ 0.000000] .rodata : 0xffff0000087d0000 - 0xffff000008a50000 ( 2560 KB) [ 0.000000] .init : 0xffff000008a50000 - 0xffff000008e00000 ( 3776 KB) [ 0.000000] .data : 0xffff000008e00000 - 0xffff000008f31200 ( 1221 KB) [ 0.000000] .bss : 0xffff000008f31200 - 0xffff000008fb9034 ( 544 KB) [ 0.000000] fixed : 0xffff7dfffe7fb000 - 0xffff7dfffec00000 ( 4116 KB) [ 0.000000] PCI I/O : 0xffff7dfffee00000 - 0xffff7dffffe00000 ( 16 MB) [ 0.000000] vmemmap : 0xffff7e0000000000 - 0xffff800000000000 ( 2048 GB maximum) [ 0.000000] 0xffff7e0000000000 - 0xffff7e0000200040 ( 2 MB actual) [ 0.000000] memory : 0xffff800000000000 - 0xffff800008001000 ( 128 MB) My belief is that /dev/uio0 points to the section here labeled "memory." Is that right? My goal is to perform memory introspection on vm-linux kernel modules. To that end, I think I want to look at the section labeled "modules." Is that possible? Best, Michael Neises

1 0

QEMU simulation: Passing drive to CAmkES ARM VM
by Olof Holmberg 04 Jun '21

04 Jun '21

Hi, I am currently booting a initramfs as the VM so that I later would be able to switch root to a filesystem disk that allows for larger storage and has other software installed that I want inside the VM. I have started the simulate script with a few variants of the following line (Passing the virtio device was a guess since the virtio-net device is supported for networking for the VM. I have also tried to pass only the drive part but it has the same result.): sudo ./simulate --extra-qemu-args="-device virtio-blk-pci,drive=drive0 -drive file=filesystem/testimage,format=raw,if=none,id=drive0" However there are no devices appearing in /dev/ that seem to be the drive passed to qemu such as sdaX or vdaX. There is no output from running "fdisk -l" either. So therefore I wonder if this kind of passthrough is supported by seL4? I have tried to find documentation that relates passing a disk to the VM in seL4 but have not found anything yet. This was done for the qemu-arm-virt platform if that has some significance regarding platform support. Best regards, Olof

2 2

Running ninja twice fails in https://github.com/seL4/sel4webserver
by skydivebcn＠gmail.com 04 Jun '21

04 Jun '21

Hi, I have noticed I'm never unable to run "ninja" for a second time and I'm required to rm -rf all the contents of "build" directory, and run "../init-build.sh" again before running ninja again. If I try to simpley run "ninja" twice the error I get is: (...) /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated (many times...) /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated /home/hugo/seL4/sel4webserver/build/docsite-prefix/src/docsite/_plugins/include_absolute.rb:71: warning: Using the last argument as keyword parameters is deprecated done in 10.04 seconds. Auto-regeneration: disabled. Use --watch to enable. ninja: build stopped: subcommand failed. Any hint on what could be happening? Anyone else having same issue? I'm doing something wrong?

3 5

VGA pass-through using CAmkES VM on x86
by Nicholas Pahl 03 Jun '21

03 Jun '21

Hello all, I am working out of a CAmkES VM manifest and have a function build running on an x86 platform. I have successfully pass-through various PCIe devices (Ethernet, Sata, USB) to a RHEL8 VM. I am attempting to pass-through the VGA controller in the same way as the other PCIe devices, but I am running into errors. I am assuming VGA pass-through requires more effort than just passing the PCIe device through. If anyone has any tips for VGA pass-through or an example CAmkES project that would be greatly appreciated. Also, if anyone has VESA framebuffer pass-through working I would also be interested. I have tried using LibSel4VMMPlatsupportVESAFrameBuffer but have not had any success getting a VM to use it. The card I am trying to pass-through is a Radeon HD 3450. The kernel log's call stack indicates that it is getting into radeon initialization functions, so it does see the VGA controller on the bus. The log seems to be failing to retrieve info from the BIOS. Below is a log of the kernel panic. [ 2.472635] BUG: unable to handle kernel paging request at ffffc90000548480 [ 2.472635] PGD 1013a067 P4D 1013a067 PUD 1013b067 PMD 6fdb8067 PTE 0 [ 2.472635] Oops: 0000 [#1] SMP PTI [ 2.472635] CPU: 0 PID: 349 Comm: systemd-udevd Not tainted 4.18.0-305.el8.x86_64 #1 [ 2.472635] RIP: 0010:radeon_card_posted+0x147/0x200 [radeon] [ 2.472635] Code: 48 8b 83 e8 01 00 00 48 89 c1 83 fa 38 74 53 83 fa 26 0f 87 09 ff ff ff 83 fa 11 76 4d 8b 90 80 60 00 00 48 8b 83 e8 01 00 00 <8b> 80 80 68 00 00 09 d0 a8 01 74 9f 5b b8 01 00 00 00 5d 41 5c c3 [ 2.472635] RSP: 0018:ffffc900005f7960 EFLAGS: 00010202 [ 2.472635] RAX: ffffc90000541c00 RBX: ffff888014950000 RCX: ffffc90000541c00 [ 2.472635] RDX: 0000000016dd1440 RSI: 0000000000000296 RDI: ffff888014950000 [ 2.472635] RBP: ffffc900005f79d8 R08: 0000000000000002 R09: 0000000000000000 [ 2.472635] R10: ffffc900005f79c8 R11: ffffc90000541000 R12: 0000000000000000 [ 2.472635] R13: ffff888014951d90 R14: 0000000000000000 R15: ffff888014950000 [ 2.472635] FS: 00007fe597ad8180(0000) GS:ffff88806fc00000(0000) knlGS:0000000000000000 [ 2.472635] CS: 0010 DS: 0000 ES: 0000 CR0: 0000000080050033 [ 2.472635] CR2: ffffc90000548480 CR3: 0000000016444000 CR4: 00000000000006b0 [ 2.472635] Call Trace: [ 2.472635] igp_read_bios_from_vram+0x18/0xa0 [radeon] [ 2.472635] radeon_get_bios+0x2be/0xf10 [radeon] [ 2.472635] ? __debugfs_create_file+0xc1/0x120 [ 2.472635] ? __debugfs_create_file+0xd5/0x120 [ 2.472635] ? mutex_lock+0xe/0x30 [ 2.472635] ? drm_debugfs_create_files+0x104/0x120 [drm] [ 2.472635] r600_init+0x2b/0x5c0 [radeon] [ 2.472635] radeon_device_init+0x5e7/0xb70 [radeon] [ 2.472635] radeon_driver_load_kms+0x8d/0x240 [radeon] [ 2.472635] drm_dev_register+0xc6/0x1b0 [drm] [ 2.472635] radeon_pci_probe+0x12a/0x1d0 [radeon] [ 2.472635] ? __pm_runtime_resume+0x54/0x70 [ 2.472635] local_pci_probe+0x41/0x90 [ 2.472635] pci_device_probe+0x105/0x1c0 [ 2.472635] really_probe+0x255/0x4a0 [ 2.472635] driver_probe_device+0x49/0xc0 [ 2.472635] device_driver_attach+0x50/0x60 [ 2.472635] __driver_attach+0x61/0x130 [ 2.472635] ? device_driver_attach+0x60/0x60 [ 2.472635] bus_for_each_dev+0x77/0xc0 [ 2.472635] ? klist_add_tail+0x3b/0x70 [ 2.472635] bus_add_driver+0x14d/0x1e0 [ 2.472635] ? 0xffffffffc03fd000 [ 2.472635] driver_register+0x6b/0xb0 [ 2.472635] ? 0xffffffffc03fd000 [ 2.472635] do_one_initcall+0x46/0x1c3 [ 2.472635] ? do_init_module+0x22/0x220 [ 2.472635] ? kmem_cache_alloc_trace+0x131/0x270 [ 2.472635] do_init_module+0x5a/0x220 [ 2.472635] load_module+0x14c5/0x17f0 [ 2.472635] ? __switch_to_asm+0x35/0x70 [ 2.472635] ? __switch_to_asm+0x41/0x70 [ 2.472635] ? __switch_to_asm+0x35/0x70 [ 2.472635] ? __switch_to_asm+0x41/0x70 [ 2.472635] ? __switch_to_asm+0x35/0x70 [ 2.472635] ? __switch_to_asm+0x41/0x70 [ 2.472635] ? __switch_to_asm+0x35/0x70 [ 2.472635] ? __switch_to_asm+0x41/0x70 [ 2.472635] ? __do_sys_init_module+0x13b/0x180 [ 2.472635] __do_sys_init_module+0x13b/0x180 [ 2.472635] do_syscall_64+0x5b/0x1a0 [ 2.472635] entry_SYSCALL_64_after_hwframe+0x65/0xca [ 2.472635] RIP: 0033:0x7fe5966b680e [ 2.472635] Code: 48 8b 0d 7d 16 2c 00 f7 d8 64 89 01 48 83 c8 ff c3 66 2e 0f 1f 84 00 00 00 00 00 90 f3 0f 1e fa 49 89 ca b8 af 00 00 00 0f 05 <48> 3d 01 f0 ff ff 73 01 c3 48 8b 0d 4a 16 2c 00 f7 d8 64 89 01 48 [ 2.472635] RSP: 002b:00007ffc53efb408 EFLAGS: 00000246 ORIG_RAX: 00000000000000af [ 2.472635] RAX: ffffffffffffffda RBX: 00005626ca9314d0 RCX: 00007fe5966b680e [ 2.472635] RDX: 00007fe59722486d RSI: 00000000002c4878 RDI: 00005626cb200450 [ 2.472635] RBP: 00007fe59722486d R08: 00005626ca91501a R09: 0000000000000005 [ 2.472635] R10: 00005626ca915010 R11: 0000000000000246 R12: 00005626cb200450 [ 2.472635] R13: 00005626ca92d120 R14: 0000000000020000 R15: 0000000000000000 [ 2.472635] Modules linked in: radeon(+) i2c_algo_bit drm_kms_helper syscopyarea sysfillrect sysimgblt fb_sys_fops ttm drm ahci libahci e1000e(+) libata crc32c_intel dm_mirror dm_region_hash dm_log dm_mod fuse [ 2.472635] CR2: ffffc90000548480 [ 2.472635] ---[ end trace a2f824fed053010d ]--- [ 2.472635] RIP: 0010:radeon_card_posted+0x147/0x200 [radeon] [ 2.472635] Code: 48 8b 83 e8 01 00 00 48 89 c1 83 fa 38 74 53 83 fa 26 0f 87 09 ff ff ff 83 fa 11 76 4d 8b 90 80 60 00 00 48 8b 83 e8 01 00 00 <8b> 80 80 68 00 00 09 d0 a8 01 74 9f 5b b8 01 00 00 00 5d 41 5c c3 [ 2.472635] RSP: 0018:ffffc900005f7960 EFLAGS: 00010202 [ 2.472635] RAX: ffffc90000541c00 RBX: ffff888014950000 RCX: ffffc90000541c00 [ 2.472635] RDX: 0000000016dd1440 RSI: 0000000000000296 RDI: ffff888014950000 [ 2.472635] RBP: ffffc900005f79d8 R08: 0000000000000002 R09: 0000000000000000 [ 2.472635] R10: ffffc900005f79c8 R11: ffffc90000541000 R12: 0000000000000000 [ 2.472635] R13: ffff888014951d90 R14: 0000000000000000 R15: ffff888014950000 [ 2.472635] FS: 00007fe597ad8180(0000) GS:ffff88806fc00000(0000) knlGS:0000000000000000 [ 2.472635] CS: 0010 DS: 0000 ES: 0000 CR0: 0000000080050033 [ 2.472635] CR2: ffffc90000548480 CR3: 0000000016444000 CR4: 00000000000006b0 [ 2.472635] Kernel panic - not syncing: Fatal exception [ 2.472635] Kernel Offset: disabled [ 2.472635] ---[ end Kernel panic - not syncing: Fatal exception ]---

1 0

Pass Ethernet device to CAmkES ARM VM when using QEMU
by Olof Holmberg 03 Jun '21

03 Jun '21

Hi, I am currently trying to pass a device for ethernet access through qemu to the vm. However there seems to be some issue since the device is not passed through correctly. I have looked at some resources for guidance on how to solve it: https://github.com/seL4/sel4webserver (webserver example) https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/message/X34TX… (old devel thread) And the important parts for this to work seems to be untyped_mmios for the vm (in devices.camkes for qemu-arm-virt): vm0.untyped_mmios = [ "0x8040000:12", // Interrupt Controller Virtual CPU interface (Virtual Machine view) /* TODO: QEMU PCI addresses could change - ideally need to decode from pcie node */ "0x10040000:17", // QEMU PCI MMIO "0x3eff0000:16", // QEMU PCI IO ports "0x40000000:29", // Linux kernel memory regions ]; And passing the device to QEMU in the simulation script: $ sudo ./simulate --extra-qemu-args="-netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01" However when listing the devices with "ip a" on the VM it does not show an eth0 device: # ip a 1: lo: <LOOPBACK,UP,LOWER_UP> mtu 65536 qdisc noqueue qlen 1 link/loopback 00:00:00:00:00:00 brd 00:00:00:00:00:00 inet 127.0.0.1/8 scope host lo valid_lft forever preferred_lft forever inet6 ::1/128 scope host valid_lft forever preferred_lft forever 2: tunl0@NONE: <NOARP> mtu 1480 qdisc noop qlen 1 link/ipip 0.0.0.0 brd 0.0.0.0 3: ip6tnl0@NONE: <NOARP> mtu 1452 qdisc noop qlen 1 link/tunnel6 00:00:00:00:00:00:00:00:00:00:00:00:00:00:00:00 brd 00:00:00:00:00:00:00:00:00:00:00:00:00:00:00:00 But on the host the device that is passed to qemu can be seen: $ ip link show tap0 6: tap0: <BROADCAST,MULTICAST> mtu 1500 qdisc noop state DOWN mode DEFAULT group default qlen 1000 link/ether 62:43:43:54:2d:e6 brd ff:ff:ff:ff:ff:ff I am not sure if I missed something or if it is the QEMU addresses for the pci region that are not correct. Is there any output during boot or build that could give insight in what went wrong when it tries to passthrough the device? Also are there are any resources or guidelines on how to decode the pcie node? (Since I assume this has to be done inside the vm with the limited selection of commands available). Best regards, Olof

1 1

Blocking and unblocking under the MCS kernel
by Robert Kaiser 02 Jun '21

02 Jun '21

Hi all, I'm working on the SOS example of the AOS course, trying to adapt code that used to work under the non-MCS kernel to the now used MCS kernel. So far, this mostly works. However, I'm having problems in resuming a thread that is blocked in an IPC Call operation. In simple cases where the server can reply immediately, the thread is successfully unblocked, simply by replying to the reply object as with the reply capability in the non-MCS kernel. However, if the server does not respond immediately, (i.e. it leaves the calling thread in blocked state, serves some other requests and/or notifications in the meantime, then comes back to reply), replying to the reply object silently fails to unblock the thread for some reason. In the non-MCS kernel, it was necessary in these cases to save the reply capability in a cspace. Therefore I tried to similarly copy/move the reply object to a thread-specific cspace slot, but that doesn't help. I'm sure I'm missing something very basic here. Can anybody point me to the right direction? Best, Robert -- Robert Kaiser Technische Informatik Hochschule RheinMain Wiesbaden Rüsselsheim Computer Engineering RheinMain University of Applied Sciences robert.kaiser(a)hs-rm.de http://www.cs.hs-rm.de/~kaiser tel:(+49)611-9495-1292 fax:(+49)611-9495-1210 Postal Address: Robert Kaiser, Hochschule RheinMain, FB DCSM/Informatik Unter den Eichen 5, 65195 Wiesbaden, Germany

2 2