- Devel - lists.sel4.systems

The seL4 Summit 2022 will be in Munich, Germany, on 10-12 Oct 2022
by June Andronick (seL4 Foundation) 29 Apr '22

29 Apr '22

It is our pleasure to confirm that the seL4 Summit 2022 will be in: Munich, Germany in the week of Oct 10th, 2022 It will be hosted by seL4 Foundation member Hensoldt Cyber. It will be a hybrid in-person/online event (if you'd like to propose a talk to be delivered remotely, please notify it in the submission). Remember that you have until Monday 9th of May 2022 to propose a talk. https://sel4.systems/news/2022 https://sel4.systems/Foundation/Summit/ https://sel4.systems/Foundation/Summit/cfp

1 0

Sending extraCaps over IPC | Unable to send 2 caps
by Sid Agrawal 29 Apr '22

29 Apr '22

Hello seL4 devs and users, I am trying to send two capabilities from one process to another via the extraCaps mechanism in the IPC. I can get it working when I send just 1 cap, but when I am sending 2 caps, the 2nd one never makes it. The extraCaps field on the receiver side is somehow always 1. Looking at the seL4 manual, I understood that I could send more than 1 capability via an IPC. But since on the receiver side, I can only specify one receive slot, I assumed that if more than 1 capability is received, it will be put in the consecutive slots. Not sure if this is a valid assumption. Looking at kerne/libsel4/include/sel4/constants.h <https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/constants.h#L…>, I see that seL4_MsgMaxExtraCaps is set to 2, so I think I should be able to send 2 caps. I have spent about 3 days trying to make this work and thought that at this stage, it would be best to ask :) My C code on the sender side looks something like this: seL4_CPtr cap1 = <alloc some capability> seL4_CPtr cap2 = <alloc some capability> seL4_SetMR(0, 0xabcd); seL4_SetCap(0, cap1); seL4_SetCap(1, cap2); seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 2, 1); tag = seL4_Call(receivers_ep_cap, tag); On the receive side, the code looks something like this: /* Allocate one csapce slot */ cspacepath_t received_cap_path_1; error = vka_cspace_alloc_path(simple-vka, &received_cap_path_1); <- slot = 2786 assert(error == 0); /* Allocate another csapce slot */ cspacepath_t received_cap_path_2; error = vka_cspace_alloc_path(simple-vka, &received_cap_path_2); <- slot = 2785(somehow decreasing) assert(error == 0); /* Since the allocated slots are decreasing in count, I pick the lesser one as my first slot * assuming that if more than 1 cap is received it will be put in the next slot */ seL4_CPtr min_cptr = MIN(received_cap_path_1.capPtr, received_cap_path_2.capPtr); seL4_SetCapReceivePath( /* _service */ received_cap_path.root, /* index */ min_cptr, /* depth */ received_cap_path.capDepth); tag = recv(&sender_badge); assert(seL4_MessageInfo_get_extraCaps(tag) == 2); <--- This asser fails. Thanks again!! Sid Graduate Student @ UBC

2 2

RTReply and cap xfer
by Sam Leffler 22 Apr '22

22 Apr '22

The kernel supports attaching a capability to an RTReply xfer. sel4test even checks this WAI. But capdl doesn't seem to support it as I see no way to express the set of rights associated with a capability to an RTReply object. I added capdl support so I can mark the Grant right and verified cap xfer works. TWas this intentional? -Sam

1 0

Running vm_multi app on qemu-arm-virt platform, udhcpc can not return
by ybbekele＠aggies.ncat.edu 22 Apr '22

22 Apr '22

Hi, I tried to build vm_multi for qemu-arm-virt using the procedures in this link https://docs.sel4.systems/projects/camkes-vm/. After building, I used the generated simulation file to do ./simulate in my build directory. After displaying 'welcome to buildroot', the console always prints the log "udhcpc: sending discover",which indicates udhcpc can not return. The related log was shown below: Starting syslogd: OK Starting syslogd: OK Starting syslogd: OK Starting klogd: OK Starting klogd: OK Starting klogd: OK Running sysctl: OK Running sysctl: OK Running sysctl: OK Initializing random number generator... [ 7.195263] random: dd: uninitialized urandom read (512 bytes read) done. Initializing random number generator... [ 7.315113] random: dd: uninitialized urandom read (512 bytes read) done. Initializing random number generator... [ 7.300770] random: dd: uninitialized urandom read (512 bytes read) done. Starting network: OK Starting network: OK Starting network: OK udhcpc: started, v1.31.0 udhcpc: started, v1.31.0 ifconfig: SIOCGIFFLAGS: No such device [ 9.077855] random: mktemp: uninitialized urandom read (6 bytes read) [ 9.177878] random: mktemp: uninitialized urandom read (6 bytes read) Welcome to Buildroot udhcpc: sending discover udhcpc: sending discover udhcpc: sending discover udhcpc: sending discover As the simulation process progresses there was an error: _utspace_split_alloc@split.c:266 Failed to find any untyped capable of creating an object at address 0x10080000 alloc_vm_device_cap@main.c:938 Grabbing the entire cap for device memory alloc_vm_device_cap@main.c:941 Failed to grab the entire cap My question is: 1. Is the two things have dependencies (The error and the hang at booting the system up)? 2. How can this issue be solved? 3. Is this issue related to the TimeServer component being imported to Qemu (as this is indicated as a requirement to run multi_vm on qemu-arm-virt)? Thank you for your time

1 0

Why vppi is sent from kernel to vmm by fault endpoint but not by notification ?
by wtliang785 21 Apr '22

21 Apr '22

hello devel, Why vppi , such as vtimer interrupt to guest, is sent from kernel to vmm by fault endpoint but not by notification? I see that spi to guest is sent from kernel to vmm by notification. thank you.

1 0

Reminder seL4 developer hangout/video call
by Gerwin Klein 19 Apr '22

19 Apr '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Apr 19, 10pm (UTC) * Sydney: Wed, Apr 20, 8am * Central Europe: Wed, Apr 20, 12 midnight * US Pacific Time: Tue, Apr 19, 3pm Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

1 0

Re: Combatting spam on this list
by Isaac Beckett 13 Apr '22

13 Apr '22

Thanks Peter! In my experience posts like that, linking to pornographic websites, are not made by humans anyway, but rather by bots. I don’t think this will effect humans too much except at the very beginning. It may make sense to implement a different captcha, as often the developers of those bots can outsource solving common captcha providers to underpaid humans. Using an uncommon or home-grown captcha solution will make it less likely that bots will be able to get around them using that method. And attacks like these aren’t targeted, usually, so I doubt the bot writers will adapt for one specific mailing list. That will stop bots from signing up in the first place, hopefully. We could also maybe report abuse of free email services like Gmail or Hotmail or similar in a semi-automated fashion. Would not surprise me if there is some sort of API for that. But on the other hand with the way those companies work it could be a waste of time and effort, since they might not do anything. And it may also make sense to keep track of which domains non-malicious users are sending email from. That way we can ban entire domains without worrying about getting rid of legitimate users unintentionally. For example, a small webmail service that we may not realize is a public email service at first, could be used by both a malicious user and a legitimate one. That way we’re only banning domains controlled by spammers exclusively. There’s lots of resources for this stuff thankfully, you can go on a whole tangent reading about email spam prevention on Wikipedia. I wish you luck with figuring out how to stop this annoying nonsense.

3 2

Unrecognized OPCODE fence.i/csrw
by porter.188＠osu.edu 13 Apr '22

13 Apr '22

I'm trying to setup a development machine for seL4 work. I would like to use v12.1.0. I setup seL4test-manifest per instructions here https://docs.sel4.systems/Hardware/spike.html repo init -u https://github.com/seL4/sel4test-manifest.git repo sync mkdir cbuild cd cbuild ../init-build.sh -DPLATFORM=spike -DRISCV64=1 # The default cmake wrapper sets up a default configuration for the target platform. # To change individual settings, run `ccmake` and change the configuration # parameters to suit your needs. ninja # If your target binaries can be executed in an emulator/simulator, and if # our build system happens to support that target emulator, then this script # might work for you: ./simulate I used repo init -u https://github.com/seL4/sel4test-manifest.git -b refs/tags/12.1.0 to be sure I got 12.1.0 but it doesn't matter, both branches/tags give the same error when I configure/compile. $ ../init-build.sh -DPLATFORM=spike -DRISCV64=1 -DSIMULATION=1 loading initial cache file /mnt/data/sel4test/projects/sel4test/settings.cmake -- Set platform details from PLATFORM=spike -- KernelPlatform: spike -- Setting from flags KernelSel4Arch: riscv64 -- Found seL4: /mnt/data/sel4test/kernel -- Found GCC with prefix riscv64-unknown-linux-gnu- -- Found GCC with prefix riscv64-unknown-linux-gnu- -- The C compiler identification is GNU 10.2.0 -- The CXX compiler identification is GNU 10.2.0 -- The ASM compiler identification is GNU -- Found assembler: /mnt/data/opt/riscv/bin/riscv64-unknown-linux-gnu-gcc -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Check for working C compiler: /mnt/data/opt/riscv/bin/riscv64-unknown-linux-gnu-gcc - skipped -- Detecting C compile features -- Detecting C compile features - done -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Check for working CXX compiler: /mnt/data/opt/riscv/bin/riscv64-unknown-linux-gnu-g++ - skipped -- Detecting CXX compile features -- Detecting CXX compile features - done -- Found elfloader-tool: /mnt/data/sel4test/tools/seL4/elfloader-tool -- /mnt/data/sel4test/build/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating... -- CPIO test cpio_reproducible_flag PASSED -- Found musllibc: /mnt/data/sel4test/projects/musllibc -- Found util_libs: /mnt/data/sel4test/projects/util_libs -- Found seL4_libs: /mnt/data/sel4test/projects/seL4_libs -- Found sel4_projects_libs: /mnt/data/sel4test/projects/sel4_projects_libs -- Found sel4runtime: /mnt/data/sel4test/projects/sel4runtime -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- libmuslc architecture: 'riscv' (from KernelSel4Arch 'riscv64') -- Detecting cached version of: musllibc -- Found Git: /usr/bin/git (found version "2.25.1") -- Not found cache entry for musllibc - will build from source -- Found PythonInterp: /usr/bin/python (found version "2.7.18") CMake Warning (dev) at /home/user/.local/lib/python3.8/site-packages/cmake/data/share/cmake-3.22/Modules/FindPackageHandleStandardArgs.cmake:438 (message): The package name passed to `find_package_handle_standard_args` (NANOPB) does not match the name of the calling package (Nanopb). This can lead to problems in calling code that expects `find_package` result variables (e.g., `_FOUND`) to follow a certain pattern. Call Stack (most recent call first): /mnt/data/sel4test/tools/nanopb/extra/FindNanopb.cmake:340 (FIND_PACKAGE_HANDLE_STANDARD_ARGS) /mnt/data/sel4test/tools/seL4/cmake-tool/helpers/nanopb.cmake:29 (find_package) /mnt/data/sel4test/projects/sel4_projects_libs/libsel4nanopb/CMakeLists.txt:11 (include) This warning is for project developers. Use -Wno-dev to suppress it. -- Found NANOPB: /mnt/data/sel4test/tools/nanopb -- Configuring done -- Generating done -- Build files have been written to: /mnt/data/sel4test/build user@user-KVM:/mnt/data/sel4test/build$ ninja [42/267] Building ASM object kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj FAILED: kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj /usr/bin/ccache /mnt/data/opt/riscv/bin/riscv64-unknown-linux-gnu-gcc --sysroot=/mnt/data/sel4test/build -I/mnt/data/sel4test/kernel/include/plat/default -I/mnt/data/sel4test/kernel/include -I/mnt/data/sel4test/kernel/include/64 -I/mnt/data/sel4test/kernel/include/arch/riscv -I/mnt/data/sel4test/kernel/include/arch/riscv/arch/64 -I/mnt/data/sel4test/kernel/include/plat/spike -I/mnt/data/sel4test/kernel/include/plat/spike/plat/64 -I/mnt/data/sel4test/kernel/libsel4/include -I/mnt/data/sel4test/kernel/libsel4/arch_include/riscv -I/mnt/data/sel4test/kernel/libsel4/sel4_arch_include/riscv64 -I/mnt/data/sel4test/kernel/libsel4/sel4_plat_include/spike -I/mnt/data/sel4test/kernel/libsel4/mode_include/64 -I/mnt/data/sel4test/build/kernel/gen_config -I/mnt/data/sel4test/build/kernel/autoconf -I/mnt/data/sel4test/build/kernel/gen_headers -I/mnt/data/sel4test/build/kernel/generated -march=rv64imac -mabi=lp64 -D__KERNEL_64__ -O2 -g -DNDEBUG -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -DDEBUG -g -ggdb -mcmodel=medany -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -MD -MT kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj -MF kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj.d -o kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj -c /mnt/data/sel4test/kernel/src/arch/riscv/head.S /mnt/data/sel4test/kernel/src/arch/riscv/head.S: Assembler messages: /mnt/data/sel4test/kernel/src/arch/riscv/head.S:24: Error: unrecognized opcode `fence.i' /mnt/data/sel4test/kernel/src/arch/riscv/head.S:31: Error: unrecognized opcode `csrw sscratch,x0' [44/267] Invoking muslc build system /mnt/data/sel4test/projects/musllibc/src/unistd/getcwd.c: In function 'getcwd': cc1: warning: function may return address of local variable [-Wreturn-local-addr] /mnt/data/sel4test/projects/musllibc/src/unistd/getcwd.c:9:7: note: declared here 9 | char tmp[PATH_MAX]; | ^~~ ninja: build stopped: subcommand failed. I tried riscv-gcc 10.2.0 and 11.1.0 with the same results. $ riscv64-unknown-linux-gnu-gcc --version riscv64-unknown-linux-gnu-gcc (gca312387ab1) 10.2.0 Copyright (C) 2020 Free Software Foundation, Inc. This is free software; see the source for copying conditions. There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. Is there some extension I need to add to get this working? Where do I do that?

2 2

答复: Report "Failed to touch ram region" error using virtio_console when assigned for Arm-VM more than 3G memory
by Han JingLong 韩景龙 12 Apr '22

12 Apr '22

Hi The root cause of this problem has been found, when Guest OS do the virtio console driver probe, if virtqueue's desc addr allocated by alloc_pages_exact() in the setup_vq() function is >= 0x100000000 (it is common when the memory of VM allocated exceeds 3G), at first It will be shifted right 12 bits by Guest OS(turn into a value >= 0x100000), and then use iowrite32(iobase + VIRTIO_PCI_QUEUE_PFN) to notify Host, after unsigned int type data be shifted left 12 bits by Host, the higest bits 0x1 of virtqueue's desc addr will be lost. I have submitted a PR for the amendment, waiting for the review and merge into the main branch. https://github.com/seL4/seL4_projects_libs/pull/43 BR. Allen 发件人: Han JingLong 韩景龙发送时间: 2022年3月21日 20:27 收件人: 'devel(a)sel4.systems' <devel(a)sel4.systems> 主题: Report "Failed to touch ram region" error using virtio_console when assigned for Arm-VM more than 3G memory Hi I had make virtio_console work well on my environment(armv8, RAM is 8G) based on vm_multi with Linux Guest OS(512M) and Android Guest OS(<= 3G) But I meet an error(vm_ram_touch@guest_ram.c:157<mailto:vm_ram_touch@guest_ram.c:157> Failed to touch ram region: Not registered RAM region) when assign for a VM(Android Guest OS) more than 3G memory. 1. Some logs are added for debugging this issue： +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c @@ -86,6 +86,7 @@ static int emul_io_out(virtio_emul_t *emul, unsigned int offset, unsigned int si assert(size == 4); int queue = emul->virtq.queue; emul->virtq.queue_pfn[queue] = value; + printf("[hjl] queue_size:%d desc:%p\n", emul->virtq.queue_size[queue], (void *)(uintptr_t)(value << 12)); vring_init(&emul->virtq.vring[queue], emul->virtq.queue_size[queue], (void *)(uintptr_t)(value << 12), VIRTIO_PCI_VRING_ALIGN); break; +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul_helpers.c @@ -25,10 +25,43 @@ static int write_guest_mem(vm_t *vm, uintptr_t phys, void *vaddr, size_t size, s int vm_guest_write_mem(vm_t *vm, void *data, uintptr_t address, size_t size) { + bool is_inram = false; + vm_mem_t *guest_memory = &vm->mem; + for (int i = 0; i < guest_memory->num_ram_regions; i++) { + if (guest_memory->ram_regions[i].start <= address && + guest_memory->ram_regions[i].start + guest_memory->ram_regions[i].size >= address + size) { + /* We are within a ram region*/ + is_inram = true; + } + } + + if (!is_inram) { + printf("[hjl] write mem addr:%p size:0x%lx\n", address, size); + for (int index = 0; index < guest_memory->num_ram_regions; index++) { + printf("[hjl] write mem ram_regions start:%p size:0x%lx\n", guest_memory->ram_regions[index].start, guest_memory->ram_regions[index].size); + } + } + return vm_ram_touch(vm, address, size, write_guest_mem, data); } int vm_guest_read_mem(vm_t *vm, void *data, uintptr_t address, size_t size) { + bool is_inram = false; + vm_mem_t *guest_memory = &vm->mem; + for (int i = 0; i < guest_memory->num_ram_regions; i++) { + if (guest_memory->ram_regions[i].start <= address && + guest_memory->ram_regions[i].start + guest_memory->ram_regions[i].size >= address + size) { + /* We are within a ram region*/ + is_inram = true; + } + } + + if (!is_inram) { + printf("[hjl] read mem addr:%p size:0x%lx\n", address, size); + for (int index = 0; index < guest_memory->num_ram_regions; index++) { + printf("[hjl] read mem ram_regions start:%p size:0x%lx\n", guest_memory->ram_regions[index].start, guest_memory->ram_regions[index].size); + } + } return vm_ram_touch(vm, address, size, read_guest_mem, data); } 2. The detailed log is as follows: [hjl] queue_size:128 desc:0x8eb6000 [hjl] queue_size:128 desc:0x8eb8000 [hjl] read mem addr:0x8eb8802 size:0x2 [hjl] read mem ram_regions start:0x80000000 size:0x80000 [hjl] read mem ram_regions start:0x80080000 size:0x17cda00 [hjl] read mem ram_regions start:0x8184da00 size:0xa5b2600 [hjl] read mem ram_regions start:0x8be00000 size:0x83ae98 [hjl] read mem ram_regions start:0x8c63ae98 size:0x29c5168 [hjl] read mem ram_regions start:0x8f000000 size:0x26d35 [hjl] read mem ram_regions start:0x8f026d35 size:0xc0fd92cb vm_ram_touch@guest_ram.c:157<mailto:vm_ram_touch@guest_ram.c:157> Failed to touch ram region: Not registered RAM region 3. devices.camkes configuration reference is as follows: #define VM1_RAM_BASE 0x80000000 #define VM1_RAM_SIZE 0xD0000000 #define VM1_DTB_ADDR 0x8F000000 //VM1_RAM_BASE + 0xF000000 #define VM1_INITRD_ADDR 0x8BE00000 //VM1_DTB_ADDR - VM1_INITRD_MAX_SIZE vm1.untyped_mmios = [ "0x80000000:28", // RAM "0x90000000:28", // RAM "0xa0000000:28", // RAM "0xb0000000:28", // RAM "0xc0000000:28", // RAM "0xd0000000:28", // RAM "0xe0000000:28", // RAM "0xf0000000:28", // RAM "0x100000000:28", // RAM "0x110000000:28", // RAM "0x120000000:28", // RAM "0x130000000:28", // RAM "0x140000000:28", // RAM /* "0x150000000:28", // RAM "0x160000000:28", // RAM "0x170000000:28", // RAM "0x180000000:28", // RAM "0x190000000:28", // RAM "0x1a0000000:28", // RAM "0x1b0000000:28", // RAM */ ]; 4. Present situation: At present, I tracked and found that When the Guest OS's virtio_console driver do the probe, it created the vring and iowrite to notify VMM of the virtqueue desc 's physical address in setup_vq() /* create the vring */ static void *vring_alloc_queue(struct virtio_device *vdev, size_t size, dma_addr_t *dma_handle, gfp_t flag) { ...... void *queue = alloc_pages_exact(PAGE_ALIGN(size), flag); if (queue) { phys_addr_t phys_addr = virt_to_phys(queue); *dma_handle = (dma_addr_t)phys_addr; /* activate the queue */ iowrite32(virtqueue_get_desc_addr(vq) >> VIRTIO_PCI_QUEUE_ADDR_SHIFT, vp_dev->ioaddr + VIRTIO_PCI_QUEUE_PFN); I'm very confused why is the physical memory allocated for virtqueue desc not within the effective memory range of VM when assign the memory to it exceeds 3G? BR. Allen 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

Combatting spam
by David Barrass 12 Apr '22

12 Apr '22

Hi Peter, Thank you for raising this issue - it is an annoying distraction. The general standard of the list is very high as one would expect and it is a shame to see this kind of behaviour polluting the discussions. I am very happy to have to earn a privilege to post and am happy for anything I post to be moderated. I would welcome any proposition to keep spammers off the list whilst keeping it open but I don't think any solution should impose additional burdens on the moderators. I think that this warrants a bit of thought and will give this some consideration. Your proposal sounds good and I support it. In the meantime thank you and many thanks to all the team who make this happen. I find the work on seL4 very valuable and relevant. best regards to all, David

1 0

Combatting spam on this list
by Peter Chubb 12 Apr '22

12 Apr '22

Hi Folks, We're trying hard to avoid spam coming through this list. In particular we moderate all emails coming from non-members, and only let through on-topic postings. Recently, however, we've had some people join the list, and then posting spam. I'm proposing that the first post a person makes will always be moderated; and we'll turn off the moderation after the first on-topic posting. Anyone who posts spam will have that address marked as discard immediately. This means that *all* next posts will be moderated until I or one of the other moderators lets them through, because I'll be changing the default processing. Comments? I'd rather keep things as open as possible, but spammers are making it hard. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.

1 0

RFC 10
by Gerwin Klein 11 Apr '22

11 Apr '22

This is a last call for comments for RFC-10 before the TSC votes on it this week: https://sel4.atlassian.net/browse/RFC-10 The RFC is about consolidating AArch64 page table objects and has been uncontroversial so far, just wanted to make sure people are aware of it. Cheers, Gerwin

2 1

Does the lastest master branch support gic v3 virtulization?
by wtliang785 10 Apr '22

10 Apr '22

hello devel, We want to use Sel4 in our project, but the gic version is v3. I know sel4 kernel 12.1.0 version does not support v3 virtuliazation. My question is that what is the status for supporting the v3 virtulization in lastest sel4 kernel master branch? Does the lastest master branch support gic v3 virtulization? thank you Peter Wang

2 1

capDL-tool fix for empty CNode slots
by Sam Leffler 07 Apr '22

07 Apr '22

If you generate capdl for a CNode with empty slots, capDL-tool incorrectly calculates CDL_CapMap::num because it uses Map.size which doesn't include empty slots. The right way to calculate "num" is by taking the max of the key values +1. diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs index ec0eda9..b4a2cbb 100644 --- a/capDL-tool/CapDL/PrintC.hs +++ b/capDL-tool/CapDL/PrintC.hs @@ -224,7 +224,7 @@ memberSlots objs obj_id slots irqNode cdt ms = showSlots objs obj_id (Map.toList slots) irqNode cdt ms +++ "}," where - slot_count = Map.size slots + slot_count = if Map.null slots then 0 else (fst $ Map.findMax slots) + 1 printInit :: [Word] -> String printInit argv = -Sam

2 3

Interrupt handling - General Purpose Timer
by JENKINSON Mark 07 Apr '22

07 Apr '22

Hi seL4 Devel, We are trying to use the General Purpose Timer1 for our i.MX8MQ-based board within a simple CAmkES app. GPT1 is initialising and starting OK, but the interrupt handler for handling rollover is not being triggered. Through instrumenting the code with printf's, the GPT initialisation looks reasonable, and the expected rollover interrupt is being generated and seen within handleInterrupt(); however, the interrupt handler routine that has been registered is not being called. I'm hoping that someone can give me some ideas where to investigate next please? A few more details: From gpt_init() (in util_libs/libplatsupport/src/mach/imx/gpt.c), instrumentation within allocate_irq_callback() confirms that, for: gpt->irq_id = ps_irq_register(&gpt->io_ops.irq_ops, irq, gpt_handle_irq, gpt); our values are: irq->type = 3; // PS_INTERRUPT irq->irq.number = 87 (0x57); // 55 (0x37) + 32 = 87 (0x57) which agrees with the GPT1 entry from our dts file (when combined with the offset of 32, which I've seen explained elsewhere): gpt@302d0000 {... reg = < 0x302d0000 0x10000 >; interrupts = < 0x00 0x37 0x04 >;... And gpt_handle_irq() is registered as the interrupt handler, which resets the rollover flag and manages the counter's high_bits variable. Resulting from this call to ps_irq_register(), gpt->irq_id = 27 (0x1b), although I'm not sure of the significance of this irq_id value. Our test app starts GPT1. After ~3 mins, the timer rolls over, as expected. Instrumentation in handleInterrupt(irq) is triggered with: irq = 87 (0x57); // as expected, the GPT1 rollover interrupt However, gpt_handle_irq() is never called, despite being associated with irq 87 back in the ps_irq_register() call. Instrumentation in handleInterrupt() shows that the IRQSignal case is executed and sendSignal() is called. Within sendSignal, the NtfnState_Idle case is executed, calling ntfn_set_active(ntfnPtr, badge), with badge = 1. I stop tracking the flow there, but pick up again that ackInterrupt() is visited with irq = 87 (0x57). Everything looks in order (the right interrupt is generated at the right time and is detected) except gpt_handle_irq() is not called. The timer app keeps ticking away, but without the rollover management, time ends up skipping. Thanks for your help, Mark. This message contains information that may be privileged or confidential and is the property of the Capgemini Group. It is intended only for the person to whom it is addressed. If you are not the intended recipient, you are not authorized to read, print, retain, copy, disseminate, distribute, or use this message or any part thereof. If you receive this message in error, please notify the sender immediately and delete all copies of this message.

1 0

OpenPower/PowerPC/ppc64le port: major concerns and obstacles
by Isaac Beckett 06 Apr '22

06 Apr '22

Hello seL4 devel! Recently I was on the developer hangout meeting and brought up a ppc port. Interest seemed low, and some even called ppc a “niche” architecture which seems unfair. There was also the much more concrete concerns of funding and overall maintenance. I believe an PPC port would be very valuable, and I plan to do a whole essay/write up of some sort, but I am also not the most familiar with the technical challenges, and could use more information on those. I do think there is definitely people who would want to run seL4 on PowerPC platforms. PowerPC is one of the few ISAs that has existing, modern hardware without closed-source binary blobs, which I believe pose a real threat to the trustworthiness of the hardware seL4 is currently capable of running on.

2 1

A way to reclaim initial thread resources
by Marcin Witkowski 06 Apr '22

06 Apr '22

Hey, I am currently looking for a way to reclaim resources allocated by kernel for the rootserver thread, i.e. memory for CNode, TCB, BootInfo, etc. My current approach looks like this: * in rootserver instead of calling seL4_TCB_Suspend, call custom syscall seL4_ReclaimRootserverResources. This sycall as parameters takes CNode and slot no. after which kernel should be able to freely write new caps. This CNode is main CNode of some component initialized by the rootserver. * implmenetation of this syscall then suspends initial thread, schedules new thread, revokes most of rootserver's resources, notably TCB, BootInfo, IPCBuffer, VSpace and CNode. Then for those now free memory regions new untyped capabilities are created, with the same sizes as the original objects. Lastly, new capabilities are written to subsequent slots in CNode a'la boot.c, so with null MDBNode; mdbRevocable and mdbFirstBadged set to true. This solution has couple of problems. First and foremost, it requires creating additional syscall to handle this. Secondly, even though the component _technically_ has access to this newly created capabilities, it doesn't know where they are, or how big they are. This could be partially band-aided by hardcoding this information in relevant component, but that is far from elegant. This component also recives rest of the untyped memory from rootserver, including bootinfo entries about this memory specification, so that renders solution with hardcoding spec even worse. Last but not least, before the seL4_ReclaimRootserverResources is called, all the components are resumed using seL4_TCB_Resume as part of rootserver's work, so there could be race-condition between calling reclaiming syscall, and component initialization (although I am not 100% sure about that part) Is there maybe a better way to do it, and I am doing it all round? The perfect solution would be to somehow extend bootinfo and/or remaining untypeds that were given by the kernel to the rootserver.

2 3

Reminder seL4 developer hangout/video call
by Birgit Brecknell 04 Apr '22

04 Apr '22

Hi all A friendly reminder that the seL4 developer hangout is on this week: Wed, Apr 6, 7am (UTC), Topics: (open) * Sydney: Wed, Apr 6, 5pm * Central Europe: Wed, Apr 6, 9am * US Pacific Time: Wed, Apr 6, 12 midnight (There are too many time zones in the world to cite them all :-)) Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

3 2

The Call for Presentations for the seL4 summit 2022 is out!
by June Andronick (seL4 Foundation) 01 Apr '22

01 Apr '22

We are calling for proposals to present at the seL4 Summit 2022! Share your seL4 work. Share your seL4 experience. Share your seL4 thoughts. Share your seL4 questions. Check the full Call For Presentations and topics of interest at: https://sel4.systems/Foundation/Summit/cfp <https://sel4.systems/Foundation/Summit/cfp> To propose a talk, send an abstract of one page or less by Monday 9th of May 2022 to summit(a)sel4.systems <mailto:summit@sel4.systems>. Please do spread the word and also encourage others to submit a talk if you like their work! Thanks, June

1 0

Overlapping pointer returned by memalign
by WILLIAMS Stephen 01 Apr '22

01 Apr '22

Hi, I’m currently working on a project porting drivers from U-Boot to seL4 and have run into an unexpected problem seemingly triggered by use of the memalign within the U-Boot drivers. What I am seeing is that calls to memalign from within my CAmkES component can return pointers to regions which overlap with those previously returned by malloc. Obviously this leads to the two allocated regions trampling over each other and resulting corruption of data. I’m at a complete loss to explain this behaviour and would be very grateful to receive any suggestions or pointers. Thanks for your help, Stephen This message contains information that may be privileged or confidential and is the property of the Capgemini Group. It is intended only for the person to whom it is addressed. If you are not the intended recipient, you are not authorized to read, print, retain, copy, disseminate, distribute, or use this message or any part thereof. If you receive this message in error, please notify the sender immediately and delete all copies of this message.

3 9

Re: How to switch virtual machines linux in vm_multi from camkes-vm-example?
by Peter Chubb 31 Mar '22

31 Mar '22

>>>>> "yjy" == yjy <yjy7894(a)126.com> writes: yjy> `screen /dev/ttyUSB0 115200`. I have a shell terminal that can yjy> see the output from VM0. I input @1 to shell, which is useless. It only works at the start of a line. Peter C yjy> At 2022-03-31 14:12:16, peter(a)chubb.wattle.id.au wrote: >>>>>>> "yjy" == yjy <yjy7894(a)126.com> writes: >> yjy> Hi, I have already run the camkes-vm-example vm_multi on my yjy> board, but i don't know how to switch linux vm shell from another yjy> linux vm, Can anyone help me solve this? >> >> If you're talking about controlling the serial console to talk to >> different VMs, the instructions are >> https://github.com/seL4/camkes-vm in the README.md under 'Serial' >> >> >> In brief, output from different VMs is colour coded. Switch >> between them for input with @0, @1, @2 etc. >> >> Peter C _______________________________________________ Devel >> mailing list -- devel(a)sel4.systems To unsubscribe send an email to >> devel-leave(a)sel4.systems yjy> [2 <text/html; GBK (base64)>] -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.

1 0

How to switch virtual machines linux in vm_multi from camkes-vm-example?
by yjy 31 Mar '22

31 Mar '22

Hi, I have already run the camkes-vm-example vm_multi on my board, but i don't know how to switch linux vm shell from another linux vm, Can anyone help me solve this? Best, Comet

2 1

Question for student research
by Seth Nielson 31 Mar '22

31 Mar '22

Hi. I am mentoring a student group trying to do some work on SEL4. We are trying to setup basic TCP/IP networking and are really struggling to find documentation or up-to-date guides. We found a project that has networking (it even has some filesystem and a small webserver as part of the project). We thought we just about had the networking component working for QEMU but there seems to be issues with QEMU and networking, at least the way we did it. Does anyone have any how-to guides for getting basic networking up and running? If QEMU is not great for networking, please suggest a development board. Thanks much.

2 2

Information for Additional Virtio Driver Support of Sel4
by Tao Heng 陶恒-SW 28 Mar '22

28 Mar '22

Hi list， Is there any specific plan or some related development for supporting the Additional Virtio Driver (* e.g Virtio Blk, Virtio RNG, Virtio Balloon), as you mentioned in READ.md of libsel4vmmplatsupport, especially for the Virtio Blk? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

2 2

propagating initial thread's capabilities
by Sam Leffler 28 Mar '22

28 Mar '22

The rootserver gets various caps setup for it by the kernel (see Table 9.1 in the manual). This includes the gobal ASID, IRQ, Domain, and Sched controllers. I need these caps in a process created by the rootserver. This is within a CAmkES environment. So far I've created CAmkES component attributes that signal the rootserver should hand-off a cap by moving the rootserver's cap to the designated CNode just before it terminates. This involves modifications to CAmkES, capDL, and the rootserver. Is there a better way? Is there an existing example of doing this? Are any of these global objects accessible some other way than hand-off from the rootserver? -Sam

2 4

Questions about Kscurdomain variable.
by 603644559＠qq.com 25 Mar '22

25 Mar '22

In the case of multiple cores, is the scheduling of each core judged according to the kscurdomain, that is, the scheduling table of the domain is maintained by an operating system, rather than an independent kscurdomain in a core and a scheduling table of the domain in each core?

1 0

Hi,
by ezabujpz＠uuf.me 23 Mar '22

23 Mar '22

Hi, https://www.assortlist.com I would like to use network (TCP) on seL4, I know that I should probably be using lwip, however I have no idea how to properly initialize it (this is the first time I'm working in such a hardware close environment), so I need some help or some kind of example, but I don't know where to look. I'm working on ia32.

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 22 Mar '22

22 Mar '22

Hi all A friendly reminder that the seL4 developer hangout is on this week: Tue, Mar 22, 9pm (UTC), Topics: (open) * Sydney: Wed, Mar 23, 8am * Central Europe: Tue, Mar 22, 10pm * US Pacific Time: Tue, Mar 22, 2pm (There are too many time zones in the world to cite them all :-)) Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

3 2

Report "Failed to touch ram region" error using virtio_console when assigned for Arm-VM more than 3G memory
by Han JingLong 韩景龙 21 Mar '22

21 Mar '22

Hi I had make virtio_console work well on my environment(armv8, RAM is 8G) based on vm_multi with Linux Guest OS(512M) and Android Guest OS(<= 3G) But I meet an error(vm_ram_touch@guest_ram.c:157 Failed to touch ram region: Not registered RAM region) when assign for a VM(Android Guest OS) more than 3G memory. 1. Some logs are added for debugging this issue： +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c @@ -86,6 +86,7 @@ static int emul_io_out(virtio_emul_t *emul, unsigned int offset, unsigned int si assert(size == 4); int queue = emul->virtq.queue; emul->virtq.queue_pfn[queue] = value; + printf("[hjl] queue_size:%d desc:%p\n", emul->virtq.queue_size[queue], (void *)(uintptr_t)(value << 12)); vring_init(&emul->virtq.vring[queue], emul->virtq.queue_size[queue], (void *)(uintptr_t)(value << 12), VIRTIO_PCI_VRING_ALIGN); break; +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul_helpers.c @@ -25,10 +25,43 @@ static int write_guest_mem(vm_t *vm, uintptr_t phys, void *vaddr, size_t size, s int vm_guest_write_mem(vm_t *vm, void *data, uintptr_t address, size_t size) { + bool is_inram = false; + vm_mem_t *guest_memory = &vm->mem; + for (int i = 0; i < guest_memory->num_ram_regions; i++) { + if (guest_memory->ram_regions[i].start <= address && + guest_memory->ram_regions[i].start + guest_memory->ram_regions[i].size >= address + size) { + /* We are within a ram region*/ + is_inram = true; + } + } + + if (!is_inram) { + printf("[hjl] write mem addr:%p size:0x%lx\n", address, size); + for (int index = 0; index < guest_memory->num_ram_regions; index++) { + printf("[hjl] write mem ram_regions start:%p size:0x%lx\n", guest_memory->ram_regions[index].start, guest_memory->ram_regions[index].size); + } + } + return vm_ram_touch(vm, address, size, write_guest_mem, data); } int vm_guest_read_mem(vm_t *vm, void *data, uintptr_t address, size_t size) { + bool is_inram = false; + vm_mem_t *guest_memory = &vm->mem; + for (int i = 0; i < guest_memory->num_ram_regions; i++) { + if (guest_memory->ram_regions[i].start <= address && + guest_memory->ram_regions[i].start + guest_memory->ram_regions[i].size >= address + size) { + /* We are within a ram region*/ + is_inram = true; + } + } + + if (!is_inram) { + printf("[hjl] read mem addr:%p size:0x%lx\n", address, size); + for (int index = 0; index < guest_memory->num_ram_regions; index++) { + printf("[hjl] read mem ram_regions start:%p size:0x%lx\n", guest_memory->ram_regions[index].start, guest_memory->ram_regions[index].size); + } + } return vm_ram_touch(vm, address, size, read_guest_mem, data); } 2. The detailed log is as follows: [hjl] queue_size:128 desc:0x8eb6000 [hjl] queue_size:128 desc:0x8eb8000 [hjl] read mem addr:0x8eb8802 size:0x2 [hjl] read mem ram_regions start:0x80000000 size:0x80000 [hjl] read mem ram_regions start:0x80080000 size:0x17cda00 [hjl] read mem ram_regions start:0x8184da00 size:0xa5b2600 [hjl] read mem ram_regions start:0x8be00000 size:0x83ae98 [hjl] read mem ram_regions start:0x8c63ae98 size:0x29c5168 [hjl] read mem ram_regions start:0x8f000000 size:0x26d35 [hjl] read mem ram_regions start:0x8f026d35 size:0xc0fd92cb vm_ram_touch@guest_ram.c:157 Failed to touch ram region: Not registered RAM region 3. devices.camkes configuration reference is as follows: #define VM1_RAM_BASE 0x80000000 #define VM1_RAM_SIZE 0xD0000000 #define VM1_DTB_ADDR 0x8F000000 //VM1_RAM_BASE + 0xF000000 #define VM1_INITRD_ADDR 0x8BE00000 //VM1_DTB_ADDR - VM1_INITRD_MAX_SIZE vm1.untyped_mmios = [ "0x80000000:28", // RAM "0x90000000:28", // RAM "0xa0000000:28", // RAM "0xb0000000:28", // RAM "0xc0000000:28", // RAM "0xd0000000:28", // RAM "0xe0000000:28", // RAM "0xf0000000:28", // RAM "0x100000000:28", // RAM "0x110000000:28", // RAM "0x120000000:28", // RAM "0x130000000:28", // RAM "0x140000000:28", // RAM /* "0x150000000:28", // RAM "0x160000000:28", // RAM "0x170000000:28", // RAM "0x180000000:28", // RAM "0x190000000:28", // RAM "0x1a0000000:28", // RAM "0x1b0000000:28", // RAM */ ]; 4. Present situation: At present, I tracked and found that When the Guest OS's virtio_console driver do the probe, it created the vring and iowrite to notify VMM of the virtqueue desc 's physical address in setup_vq() /* create the vring */ static void *vring_alloc_queue(struct virtio_device *vdev, size_t size, dma_addr_t *dma_handle, gfp_t flag) { ...... void *queue = alloc_pages_exact(PAGE_ALIGN(size), flag); if (queue) { phys_addr_t phys_addr = virt_to_phys(queue); *dma_handle = (dma_addr_t)phys_addr; /* activate the queue */ iowrite32(virtqueue_get_desc_addr(vq) >> VIRTIO_PCI_QUEUE_ADDR_SHIFT, vp_dev->ioaddr + VIRTIO_PCI_QUEUE_PFN); I'm very confused why is the physical memory allocated for virtqueue desc not within the effective memory range of VM when assign the memory to it exceeds 3G? BR. Allen 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

A question about capability derivation tree
by Chang Liu 18 Mar '22

18 Mar '22

Hi list, Here is a question about capability derivation trees, in particular when it comes to seL4_CNode_Copy and seL4_CNode_Mint. Suppose I have an untyped cap Untyped0, and I create a page cap by retyping Untyped0 into Frame0 (with seL4_AllRights). I then call CNode_Mint to mint Frame0 into Frame1 with restricted rights (say read-only). Finally, I call CNode_Copy to copy Frame1 into Frame2. What would the capability derivation tree look like at the end? Case 1: |--------| |Untyped0| |--------| / | \ / | \ / | \ |------| |------| |------| |Frame0| |Frame1| |Frame2| |------| |------| |------| Case 2: |--------| |Untyped0| |--------| | |------| |Frame0| |------| | |------| |Frame1| |------| | |------| |Frame2| |------| Case 3: |--------| |Untyped0| |--------| | |------| |Frame0| |------| / \ / \ |------| |------| |Frame1| |Frame2| |------| |------| Which one of the above is the correct answer? I suspect it's case 3, but I'm not sure. Best, Chang

1 0

Sel4 VMM Virtio Net Related Porting on Other SOC
by Tao Heng 陶恒-SW 11 Mar '22

11 Mar '22

Finally, I figured out the root cause of this issue. It happened when I changed the mac address of the virtio net probed for the vm guest. According to the issue, It seemed that the virtio_net driver of the libsel4vmmsupport did not support emulating the io control for changing the mac addess of the virtio net in the guest. 发件人: Tao Heng 陶恒-SW 发送时间: 2022年3月9日 14:49 收件人: 'devel(a)sel4.systems' <devel(a)sel4.systems> 主题: Sel4 VMM Virtio Net Related Porting on Other SOC Hi everyone , Background: I was porting vm_virtio_net project on other platforms with Cortex-A55. I met a run error with : ----------------------------------------- Unhandled offset of 0x14 of size 1, writing 0x2 Assertion failed: !"panic" (/home/kuang/workspace/penoy/system/core/seL4_projects_libs/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c: emul_io_out: 109) --------------------------------------------------- While it ran well on qemu with linux kernel version 4.9.189, my linux kernel version for the SOC is 4.14.61. If I replaced the qemu linux kernel with my kernel, the vm_virtio_net project also ran well on the qemu platform. To my analyzation, your virtio_net driver should be able to support for my platform. Is this related to my dts configuration for PCI node? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

2 1

Sel4 VMM Virtio Net Related Porting on Other SOC
by Tao Heng 陶恒-SW 09 Mar '22

09 Mar '22

Hi everyone , Background: I was porting vm_virtio_net project on other platforms with Cortex-A55. I met a run error with : ----------------------------------------- Unhandled offset of 0x14 of size 1, writing 0x2 Assertion failed: !"panic" (/home/kuang/workspace/penoy/system/core/seL4_projects_libs/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c: emul_io_out: 109) --------------------------------------------------- While it ran well on qemu with linux kernel version 4.9.189, my linux kernel version for the SOC is 4.14.61. If I replaced the qemu linux kernel with my kernel, the vm_virtio_net project also ran well on the qemu platform. To my analyzation, your virtio_net driver should be able to support for my platform. Is this related to my dts configuration for PCI node? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

Does the CSpace needs to have a cap to the TCB
by Sid Agrawal 09 Mar '22

09 Mar '22

Hi, We roughly do the following steps when setting up a new process in seL4: - Allocate a new TCB - Allocate new CSpace - Make the TCB point to the CSpace - Construct the VSpace and add the relevant caps in the new CSpace - Update the VSpace cap in the TCB. - Add a copy of the TCB cap in the new CSpace. (I am looking at the process spawn function in libesel4utils at: https://github.com/seL4/seL4_libs/blob/master/libsel4utils/src/process.c#L4…) My question is about the last point i.e. copying of TCB to the new CSpace. If I want to restrict the new domain from changing its VSpace, suspend itself, and change its fault handlers, I would simply not do the last step. Will that work? Is there any fundamental need for the TCB cap to be in the cspace it points to? Thanks, Sidhartha Agrawal

2 1

vm_multi usage
by Michael Neises 08 Mar '22

08 Mar '22

Hi, I'm just beginning to use multiple VMs at once, and I have a simple question. When I simulate my image, two VMs are running, and I get a terminal interface to one of them. Can I also switch my terminal to interface with the second VM? Cheers, Michael Neises

2 1

Re: I Have some questions about the domain mechanism in the seL4
by Isaac Beckett 08 Mar '22

08 Mar '22

> Date: Sat, 5 Mar 2022 19:15:05 +1100 > From: Kent Mcleod <kent.mcleod72(a)gmail.com> > Subject: [seL4] Re: I Have some questions about the domain mechanism > in the seL4 > To: 603644559(a)qq.com > Cc: devel <devel(a)sel4.systems> > Message-ID: > <CA+-ozWdgMgBin34WBUoVL+uHSNfU=e852ekPgrNGZ5J7+nyN0g(a)mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > >> On Sat, Mar 5, 2022 at 6:11 PM 603644559--- via Devel >> <devel(a)sel4.systems> wrote: >> >> For some reason, i m learning the scheduling module in seL4. I have read the manual and the source code, and i have already read the answer in the link https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/VYRTG3… >> But i still do not know the purpose of adding the domain mechanism in seL4, >> Can anyone explain what kind of requirement led to the design of the domain mechanism? >> Please explain it more specifically, and it would be best if there were relevant documents and papers on the domain mechanism. > > It was added in order to enable the completion of the info-flow proofs. > >> From the infoflow proof paper > (https://trustworthy.systems/publications/nicta_full_text/6464.pdf) > where it is called the partition scheduler: > "Similarly, the original seL4 scheduler, before partition > scheduling was implemented, was known not to enforce > isolation. We could not prove information flow security until > we had fully and correctly specified the partition scheduler > in the updated abstract specification. Proving information > flow security then required us to show that the scheduler’s > choice about which partition to schedule next can never be > affected by any other partition, as one would expect." Hello! It was my understanding that seL4 used to not have an in-kernel scheduler, and scheduling was up to the root task. How did that work? And why was the choice made to add the MCS features? Basically, why the change from having scheduling in the kernel vs. in userspace? It’s probably more convenient, especially since most operating systems are used to having scheduling in the kernel itself (so easier for people to think about). There are probably more technical reasons too. What are those?

2 3

I Have some questions about the domain mechanism in the seL4
by 603644559＠qq.com 07 Mar '22

07 Mar '22

For some reason, i m learning the scheduling module in seL4. I have read the manual and the source code, and i have already read the answer in the link https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/VYRTG3… But i still do not know the purpose of adding the domain mechanism in seL4, Can anyone explain what kind of requirement led to the design of the domain mechanism? Please explain it more specifically, and it would be best if there were relevant documents and papers on the domain mechanism.

2 2

Reminder: sel4 developer hangout
by Birgit Brecknell 07 Mar '22

07 Mar '22

Hi all A friendly reminder that the seL4 developer hangout is on this week: Tue, Mar 22, 9pm (UTC), Topics: (open) * Sydney: Wed, Mar 23, 8am * Central Europe: Tue, Mar 22, 10pm * US Pacific Time: Tue, Mar 22, 1pm (There are too many time zones in the world to cite them all :)) Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au seL4 Foundation, birgit(a)sel4.systems 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Questions about shared page tables and Intel's MPK
by Sid Agrawal 06 Mar '22

06 Mar '22

Hi, I have a couple of questions about the virtual memory subsystem in seL4. 1. Intel's Memory Protection keys let a process restrict the access to given virtual address ranges based on a key. This key is the bit 62:59 of the virtual address. It is stored in the PTE of the level 4/5 Page Table. I want to use this feature in my project. Does seL4 support the setting of Memory Protection keys for virtual addresses? I couldn't find any mention of it in the source. I understand that if I use the current API of "seL4_X86_PageTable_Map" with those higher bits of the vaddr set, the kernel will ignore them. Is my understanding correct? Furthermore, was a decision made not to support MPK at some point? 2. As per section 7.3 of the seL4 manual, seL4 doesn't allow sharing of page tables. I am trying to understand the reasoning behind this. Was this done to aid verification? Thanks, Sidhartha S Agrawal

3 4

libsel4muslcsys: Error attempting syscall 215
by skydivebcn＠gmail.com 05 Mar '22

05 Mar '22

Hi guys, I was trying to boot a custom Linux 4.9.302 Kernel and fot this horrible message: "libsel4muslcsys: Error attempting syscall 215" hugo@dev:~/seL4/sel4webserver_hugusmaximus_fork/build$ 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,disable-modern=on,disable-legacy=off" [sudo] contraseña para hugo: ./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic -m size=2048 -netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01,disable-modern=on,disable-legacy=off -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[61bf9000..631120af] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 61d3a2b8. Loaded DTB from 61d3a2b8. paddr=[60243000..60244fff] ELF-loading image 'kernel' to 60000000 paddr=[60000000..60242fff] vaddr=[ff8060000000..ff8060242fff] virt_entry=ff8060000000 ELF-loading image 'capdl-loader' to 60245000 paddr=[60245000..617fdfff] vaddr=[400000..19b8fff] virt_entry=408f38 Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/205 T0xff80bf815400 "rootserver" @4006f8]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>> Loading Linux: 'linux' dtb: 'linux-dtb' install_linux_devices@main.c:655 module name: map_frame_hack install_linux_devices@main.c:655 module name: init_ram install_linux_devices@main.c:655 module name: cross_vm_connections libsel4muslcsys: Error attempting syscall 215 libsel4muslcsys: Error attempting syscall 215 _utspace_split_alloc@split.c:266 Failed to find any untyped capable of creating an object at address 0x8020000 as this is purely an seL4 error message (musl libc seL4 code?) then I would appreciate any hint about what can be going on. P.S.: I have run my seL4 qemu aarch64 with several Linux kernel versions and never had this problem until now.

2 1

Sel4 VMM Virtio Net Related Porting on Other SOC
by Tao Heng 陶恒-SW 04 Mar '22

04 Mar '22

Hi everyone , Background: I was porting vm_virtio_net project on other platforms with Cortex-A55. I met a run error with : ----------------------------------------- Unhandled offset of 0x14 of size 1, writing 0x2 Assertion failed: !"panic" (/home/kuang/workspace/penoy/system/core/seL4_projects_libs/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c: emul_io_out: 109) --------------------------------------------------- While it ran well on qemu with linux kernel version 4.9.189, my linux kernel version for the SOC is 4.14.61. If I replaced the qemu linux kernel with my kernel, the vm_virtio_net project also ran well on the qemu platform. To my analyzation, your virtio_net driver should be able to support for my platform. Is this related to my dts configuration for PCI node? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

seL4 Native Web-browser
by Daniel Douglas Dyrseth 04 Mar '22

04 Mar '22

Hi, everyone What parts are needed besides seL4 to get a fully functioning Chromium browser running in a Wayland server? (No virtual OS inside seL4). I'm talking native seL4 OS capable of running Chromium with all features. Hoping for some insightful answers, and at least a list from a Pro - of the minimum parts needed for this. Regards, Daniel Douglas Dyrseth

2 1

Call for support contract to the seL4 Foundation
by Birgit Brecknell 25 Feb '22

25 Feb '22

A friendly reminder that bids are due before March 4th, 2022 AOE: The seL4 foundation is seeking to contract support for the following duties: - address open github issues in the seL4 organisation repositories, with prioritisation directed by the TSC delegates; this includes: - documentation, tutorials - bugs - tests - docsite and possibly website in coordination with Foundation people - help keeping an eye on making sure questions on mailing lists, discourse and github issues are answered (by someone) Requirement for the person working on these tasks are: - multiple years of experience with seL4, both at kernel level and user-level code - good familiarity with the seL4 organisation repositories - active contributor to one or more seL4 repositories - fluent in written and spoken English The seL4 foundation would contract a service company, initially for 6 months. The service company should identify the person that will be performing the work, ideally on a full-time basis. To bid for the contract, send email to foundation(a)sel4.systems before March 4th, 2022 AOE, with the resume of the person that will be performing the work and a cover letter addressing the requirements. --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au seL4 Foundation, birgit(a)sel4.systems 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Re: Announcing Neptune OS release v0.1.1: A Windows NT personality for seL4
by Chang Liu 24 Feb '22

24 Feb '22

Thank you both for the discussion on licensing. Seems that GPLv3 is a good choice for now. Wikipedia seems to claim that ReactOS is licensed under "GPLv2 or any later version" but I didn't find this on the reactos source code itself. If the ReactOS foundation has an objection later I can always change it to v2. Best, Chang On Wed, Feb 23, 2022 at 12:09 AM G. Branden Robinson < g.branden.robinson(a)gmail.com> wrote: > Hi Chamg, > > At 2022-02-22T23:29:21-0500, Chang Liu wrote: > > I just added a LICENSE file which is GPLv3. > > Good choice! > > > I'm honestly not sure what the difference between GPLv2 and GPLv3 > > There are modest differences, but the general thrust of both versions of > the license is the same: guaranteed access to source code under a "share > and share alike" principle. > > > is so I went with the latest version (I assume they are compatible?) > > Technically, no. But most GPLv2 software is licensed under terms that > allow promotion of the license to "any later version". One famous > example of an exception that is GPLv2-only is the Linux kernel. > So is seL4 itself[1]. Consider whether you expect to need to share code > with a GPLv2-only project. (Even if you do, I would only revisit your > decision once concrete code-sharing is imminent.) > > You're not stuck with a choice of a single license forever. The GPLv3 > is a good selection to start with (in my opinion) because most > organizations that would like to exploit a work for proprietary > advantage are allergic to that license. > > You can always relicense a work under more permissive terms later if > doing so would align better with your goals. Going from more permissive > terms (like a BSD-style license) to a copyleft (like any version of the > GPL) can be impractical, or result in unintended consequences, because > it is arguably impossible to rescind the permissive license on the older > versions of the code--unless you have an Apple- or Oracle-sized budget > for lawyers to intimidate rivals maintaining the old code base. > > There is probably a better forum for licensing discussions, but my view > is that you've made a perfectly reasonable choice, one that situates > your project squarely and clearly within the Free Software community, > while still leaving you the option to reconsider later. > > Regards, > Branden > > [1] https://microkerneldude.org/2019/12/09/what-does-sel4s-license-imply/ >

1 0

Announcing Neptune OS release v0.1.1: A Windows NT personality for seL4
by Chang Liu 23 Feb '22

23 Feb '22

Hi list, For the past several months I have been working on a project which is to implement a Windows NT personality for the seL4 microkernel, which I have now taken to call “Neptune OS”, named after the codename for Windows 2000. The project has reached the point where I have implemented enough NT primitives such that a keyboard driver stack (taken from the ReactOS source code) can be loaded (as a user process), as well as a command prompt (shell), which is also taken from the ReactOS source code (albeit a very early version of ReactOS). These are all kernel-mode Windows device drivers that I’m running as user processes under seL4. The project is now on github: github.com/cl91/NeptuneOS. The entire system fits in a floppy (download link: github.com/cl91/NeptuneOS/releases/tag/v0.1.0001) Check it out! I think it’s cool! For the next release I’m planning to port the PCI stack, the AHCI stack, and a basic file system (probably fastfat.sys).

4 5

seL4 developer hangout/video call
by Birgit Brecknell 21 Feb '22

21 Feb '22

Hi all A friendly reminder that the seL4 developer hangout is on this week: * Sydney: Wed, Feb 23, 8am * Central Europe: Tue, Feb 22, 10pm * US Pacific Time: Tue, Feb 22, 1pm (There are too many time zones in the world to cite them all :)) Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au seL4 Foundation, birgit(a)sel4.systems 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Ability to change bench app options for RiscV
by Nataliya Korovkina 12 Feb '22

12 Feb '22

Hi, Does anyone remember why sel4bench configuration for RiscV was not allowed to change bench app options? If it was skipped because it was not necessary then I'd like to fix it. I would add a line to https://github.com/seL4/sel4bench/blob/master/apps/sel4bench/CMakeLists.txt --- a/apps/sel4bench/CMakeLists.txt +++ b/apps/sel4bench/CMakeLists.txt @@ -35,14 +35,15 @@ config_string( # Default dependencies on kernel benchmarking features. Declared here so that # all the benchmark applications can use it if( (KernelArchX86 AND KernelExportPMCUser AND KernelX86DangerousMSR) OR (KernelArchARM AND KernelArmExportPMUUser) OR (KernelArchArmCortexA8 AND KernelDangerousCodeInjection) + OR (KernelArchRiscV) ) set(DefaultBenchDeps TRUE) else() set(DefaultBenchDeps FALSE) endif() find_package(musllibc REQUIRED) Thanks, Nataliya

2 1

How to build compile seL4 along with another C++ project that includes <stdlib.h>
by christinefragoso＠protonmail.com 12 Feb '22

12 Feb '22

I want to run my C++ project in a camkes image for i.mx6. This image should be statically linked. I have a camkes app in https://github.com/seL4/camkes-manifest. The app's CMakeLists.txt includes my project with add_subdirectory("${CMAKE_CURRENT_LIST_DIR}/workspace_DDSHelloWorld"), which is a simple DDS example https://fast-dds.docs.eprosima.com/en/latest/fastdds/getting_started/simple… that also uses CMake as its build system. The entire app is built with ../init-build.sh -DPLATFORM=sabre -DCAMKES_APP=dds. However, the build fails. 1. My project includes <stdint.h>, but sel4 uses the -nostdinc and -nostdinc++ flags, so I get the error "stdint.h: No such file or directory". How do I make my C++ project include seL4's musllibc instead? 2. My project includes other C++ headers like <functional>. Is there any way to build seL4 with C++ headers?

2 1

testing rust program in sel4webserver example project
by lfern70＠gmail.com 12 Feb '22

12 Feb '22

Hi, I am trying to compile a simple rust web server to be executed in the virtual machine (as lighthttpd works in this webserver project). This server works perfect (I am using qemu for testing -aarch64), but when I try to get some random bytes using the rand crate the program hangs: .... let mut key = vec![0u8; 32]; rand::thread_rng().fill_bytes(&mut key); ... Do anybody knows if this could be related to some missing settings (in qemu command line or in some device.camkes file) or some rust features that don't work in a sel4 VM?? Thanks

2 1

Call for support contract to the seL4 Foundation
by June Andronick (seL4 Foundation) 11 Feb '22

11 Feb '22

The seL4 foundation is seeking to contract support for the following duties: - address open github issues in the seL4 organisation repositories, with prioritisation directed by the TSC delegates; this includes: - documentation, tutorials - bugs - tests - docsite and possibly website in coordination with Foundation people - help keeping an eye on making sure questions on mailing lists, discourse and github issues are answered (by someone) Requirement for the person working on these tasks are: - multiple years of experience with seL4, both at kernel level and user-level code - good familiarity with the seL4 organisation repositories - active contributor to one or more seL4 repositories - fluent in written and spoken English The seL4 foundation would contract a service company, initially for 6 months. The service company should identify the person that will be performing the work, ideally on a full-time basis. To bid for the contract, send email to foundation(a)sel4.systems before March 4th, 2022 AOE, with the resume of the person that will be performing the work and a cover letter addressing the requirements.

1 0

picoserver and qemu
by lfern70＠gmail.com 08 Feb '22

08 Feb '22

Hi, I am trying to test picoserver app in qemu, but I am not able to connect to the echo component on port 1234. These are the steps I am following, please, let me know if I am doing something wrong. Thanks in advance: $ repo init -u https://github.com/seL4/camkes-manifest.git $ repo sync # use docker container to compile $ container @in-container:/host$ mkdir build @in-container:/host$ cd build @in-container:/host$ ../init_build.sh -DCAMKES_APP=picoserver -DPICOSERVER_IP_ADDR=127.0.0.1 -DSIMULATION=1 @in-container:/host$ ninja Everything seems to be ok, but when I tried to execute in qemu: $ sudo ./simulate --machine q35,accel=kvm,kernel-irqchip=split --mem-size 2G --extra-cpu-opts "+vmx" --extra-qemu-args="--enable-kvm -device intel-iommu,intremap=on,caching-mode=on -netdev user,id=network0,hostfwd=tcp::1234-:1234 -device e1000e,netdev=network0" It seems the echo component is listening on port 1234, but if I try to send data with "netcat 127.0.0.1 1234" I can't reach the echo component ...... IOMMU 0x0: enabling... enabled Booting all finished, dropped to user space Protocol ethernet registered (layer: 2). Protocol ipv4 registered (layer: 3). Protocol ipv6 registered (layer: 3). Protocol icmp4 registered (layer: 4). Protocol icmp6 registered (layer: 4). Protocol igmp registered (layer: 4). Protocol udp registered (layer: 4). Protocol tcp registered (layer: 4). listener instance starting up, going to be listening on 192.168.0.21:4321 echo instance starting up, going to be listening on 192.168.0.21:1234

2 3

seL4 developer hangout/video call
by June Andronick (seL4 Foundation) 07 Feb '22

07 Feb '22

Friendly reminder that the seL4 developer hangout is on this week: - Sydney: Wed, Feb 9, 8am - Central Europe: Tue, Feb 8, 10pm - US Pacific Time: Tue, Feb 8, 1pm (There are too many time zones in the world to cite them all :)) Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, June

1 0

seL4 on TX1
by yjy 31 Jan '22

31 Jan '22

Help me! I am running sel4test on my TX1 according to the official tutorial, but I get a problem again and again. For the newly purchased TX1, I directly connected my Ubuntu host with UART serial port. At the same time, I follow this instruction ( https://docs.sel4.systems/Hardware/jetsontx1.html ), pulled the latest sel4test project code, successfully ran ninja command and built images "sel4test-driver-image-arm-tx1". Everything seemed to be going very smoothly. I use the newly purchased SanDisk 64GB SD card to boot my image, which has been formatted in ext4 format. Then I use command `sudo screen / dev / ttyusb0 115200` to open the UART serial port. After pressing and holding the power key for 1 second, and TX1 starts. Then I hit the Enter key to make TX1 cancel the auto boot default image and enter the u-boot interactive command line. Then, according to the instruction, under uboot, I typed the following command to load the image and start from the address 0x82000000: ``` ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1 go 0x82000000 ``` Finally, I failed to start sel4test as I wanted. After many repetitions, I got the same error. This is my output： ------------------------------------------------------------------------------------------------------------------------------------------ Tegra210 (P2371-2180) # ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1 5247256 bytes read in 260 ms (19.2 MiB/s) Tegra210 (P2371-2180) # go 0x82000000 ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p1 paddr=[80a57000..80f58117] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 80b825e0. Loaded DTB from 80b825e0. paddr=[8023d000..8024afff] ELF-loading image 'kernel' to 80000000 paddr=[80000000..8023cfff] vaddr=[ffffff8080000000..ffffff808023cfff] virt_entry=ffffff8080000000 ELF-loading image 'sel4test-driver' to 8024b000 paddr=[8024b000..80661fff] vaddr=[400000..816fff] virt_entry=40f0b8 Enabling MMU and paging Jumping to kernel-image entry point... Warning: gpt_cntfrq 19200000, expected 12000000 Bootstrapping kernel available phys memory regions: 2 [80000000..ff000000] [100000000..180000000] reserved virt address space regions: 3 [ffffff8080000000..ffffff808023d000] [ffffff808023d000..ffffff808024b000] [ffffff808024b000..ffffff8080662000] seL4 failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap' at /home/yjy/Desktop/sel4-rpi/sel4test_newv2/kernel/src/object/cnode.c:426 in function cteInsert halting... Kernel entry via Interrupt, irq 0 ------------------------------------------------------------------------------------------------------------------------------------------ I'm about to collapse. I really need your help. How can I solve this problem? 1. Why did I get this warning？ "Warning: gpt_cntfrq 19200000, expected 12000000" , It exists in this file "/sel4test/kernel/src/drivers/timer/generic_timer.c:21" 2. About reporting errors "failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap'". I found that the variable "(slot_ptr_t) (rootserver.tcb) ) -> cap.words[0] " is equals to 0xffffffffffffffff, so that the cap_get_capType(destSlot->cap) <=> (slot_ptr_t) (rootserver.tcb) ) -> cap.words[0] & 0x1full != 0 . I guess it caused the mistake, but i don't know why. I'm about to collapse. I really need your help. How can I solve this problem? I'm sorry for sending this email again!

2 3

Re: seL4 on TX1
by 杨竣轶 30 Jan '22

30 Jan '22

I did’t get any difference about my error except the address. Is my Uboot precedure errored? 从 Windows 版邮件发送

1 0

seL4test on Nvidia TX1
by yjy7894＠126.com 28 Jan '22

28 Jan '22

Help me! I am running sel4test on my TX1 according to the official tutorial, but I get a problem again and again. For the newly purchased TX1, I directly connected my Ubuntu host with UART serial port. At the same time, I follow this instruction ( https://docs.sel4.systems/Hardware/jetsontx1.html ), pulled the latest sel4test project code, successfully ran ninja command and built images "sel4test-driver-image-arm-tx1". Everything seemed to be going very smoothly. I use the newly purchased SanDisk 64GB SD card to boot my image, which has been formatted in ext4 format. Then I use command `sudo screen / dev / ttyusb0 115200` to open the UART serial port. After pressing and holding the power key for 1 second, and TX1 starts. Then I hit the Enter key to make TX1 cancel the auto boot default image and enter the u-boot interactive command line. Then, according to the instruction, under uboot, I typed the following command to load the image and start from the address 0x82000000: ``` ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1 go 0x82000000 ``` Finally, I failed to start sel4test as I wanted. After many repetitions, I got the same error. This is my output： ------------------------------------------------------------------------------------------------------------------------------------------ Tegra210 (P2371-2180) # ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1 5247256 bytes read in 260 ms (19.2 MiB/s) Tegra210 (P2371-2180) # go 0x82000000 ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p1 paddr=[80a57000..80f58117] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 80b825e0. Loaded DTB from 80b825e0. paddr=[8023d000..8024afff] ELF-loading image 'kernel' to 80000000 paddr=[80000000..8023cfff] vaddr=[ffffff8080000000..ffffff808023cfff] virt_entry=ffffff8080000000 ELF-loading image 'sel4test-driver' to 8024b000 paddr=[8024b000..80661fff] vaddr=[400000..816fff] virt_entry=40f0b8 Enabling MMU and paging Jumping to kernel-image entry point... Warning: gpt_cntfrq 19200000, expected 12000000 Bootstrapping kernel available phys memory regions: 2 [80000000..ff000000] [100000000..180000000] reserved virt address space regions: 3 [ffffff8080000000..ffffff808023d000] [ffffff808023d000..ffffff808024b000] [ffffff808024b000..ffffff8080662000] seL4 failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap' at /home/yjy/Desktop/sel4-rpi/sel4test_newv2/kernel/src/object/cnode.c:426 in function cteInsert halting... Kernel entry via Interrupt, irq 0 ------------------------------------------------------------------------------------------------------------------------------------------ Help me! I am running sel4test on my TX1 according to the official tutorial, but I get a problem again and again. For the newly purchased TX1, I directly connected my Ubuntu host with UART serial port. At the same time, I follow this instruction ( https://docs.sel4.systems/Hardware/jetsontx1.html ), pulled the latest sel4test project code, successfully ran ninja command and built images "sel4test-driver-image-arm-tx1". Everything seemed to be going very smoothly. I use the newly purchased SanDisk 64GB SD card to boot my image, which has been formatted in ext4 format. Then I use command `sudo screen / dev / ttyusb0 115200` to open the UART serial port. After pressing and holding the power key for 1 second, and TX1 starts. Then I hit the Enter key to make TX1 cancel the auto boot default image and enter the u-boot interactive command line. Then, according to the instruction, under uboot, I typed the following command to load the image and start from the address 0x82000000: ``` ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1 go 0x82000000 ``` Finally, I failed to start sel4test as I wanted. After many repetitions, I got the same error. This is my output： ------------------------------------------------------------------------------------------------------------------------------------------ Tegra210 (P2371-2180) # ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1 5247256 bytes read in 260 ms (19.2 MiB/s) Tegra210 (P2371-2180) # go 0x82000000 ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p1 paddr=[80a57000..80f58117] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 80b825e0. Loaded DTB from 80b825e0. paddr=[8023d000..8024afff] ELF-loading image 'kernel' to 80000000 paddr=[80000000..8023cfff] vaddr=[ffffff8080000000..ffffff808023cfff] virt_entry=ffffff8080000000 ELF-loading image 'sel4test-driver' to 8024b000 paddr=[8024b000..80661fff] vaddr=[400000..816fff] virt_entry=40f0b8 Enabling MMU and paging Jumping to kernel-image entry point... Warning: gpt_cntfrq 19200000, expected 12000000 Bootstrapping kernel available phys memory regions: 2 [80000000..ff000000] [100000000..180000000] reserved virt address space regions: 3 [ffffff8080000000..ffffff808023d000] [ffffff808023d000..ffffff808024b000] [ffffff808024b000..ffffff8080662000] seL4 failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap' at /home/yjy/Desktop/sel4-rpi/sel4test_newv2/kernel/src/object/cnode.c:426 in function cteInsert halting... Kernel entry via Interrupt, irq 0 ------------------------------------------------------------------------------------------------------------------------------------------ I'm about to collapse. I really need your help. How can I solve this problem? 1. Why did I get this warning？ "Warning: gpt_cntfrq 19200000, expected 12000000" , It exists in this file "/sel4test/kernel/src/drivers/timer/generic_timer.c:21" 2. About reporting errors "failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap'". I found that the variable "(slot_ptr_t) (rootserver.tcb) ) -> cap.words[0] " is equals to 0xffffffffffffffff, so that the cap_get_capType(destSlot->cap) <=> (slot_ptr_t) (rootserver.tcb) ) -> cap.words[0] & 0x1full != 0 . I guess it caused the mistake, but i don't know why. I'm about to collapse. I really need your help. How can I solve this problem?

1 0

Re: seL4 developer hangout/video call
by Isaac Beckett 27 Jan '22

27 Jan '22

Hello all! If you’re reading this at the time it was sent, then the developer hangout is in roughly an hour. See you there! > > On Jan 25, 2022, at 8:02 PM, devel-request(a)sel4.systems wrote: > > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via email, send a message with subject or > body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > Today's Topics: > > 1. Re: seL4 developer hangout/video call (Gerwin Klein) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Tue, 25 Jan 2022 06:52:21 +0000 > From: Gerwin Klein <kleing(a)unsw.edu.au> > Subject: [seL4] Re: seL4 developer hangout/video call > To: devel <devel(a)sel4.systems> > Message-ID: <7F36F76C-E596-4A51-9419-785AB723CC03(a)unsw.edu.au> > Content-Type: text/plain; charset="us-ascii" > > Just a reminder that seL4 dev hangout is not tomorrow, but shifted by one day. > > Cheers, > Gerwin > >> On 23 Jan 2022, at 18:13, Gerwin Klein <kleing(a)unsw.edu.au> wrote: >> >> An earlier-than-usual heads-up that the seL4 developer hangout this week will be shifted by one day, because of the public holiday in Australia. >> >> This means, we're meeting on Wed for Europe/US and on Thu for Australia: >> >> - Sydney: Thu, Jan 27, 8am >> - Central Europe: Wed, Jan 26, 10pm >> - US West Coast: Wed, Jan 26, 1pm >> >> Zoom link: https://unsw.zoom.us/j/82640784431 >> >> Cheers, >> Gerwin >> > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems > To unsubscribe send an email to devel-leave(a)sel4.systems > > > ------------------------------ > > End of Devel Digest, Vol 135, Issue 2 > *************************************

3 2

📣 2022 SUMMIT - Trusted Computing Center of Excellence
by Griffiss Institute 27 Jan '22

27 Jan '22

NEXT WEEK! Register TODAY! NEXT WEEK! | SUMMIT 2022 View email in browser https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498… https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498… REGISTER NOW! (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) NEXT WEEK! 2022 SUMMIT BEGINS JAN 31! The Trusted Computing Center of Excellence (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) (TCCoE) is excited to announce that our annual Summit (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) will be held virtually on January 31 - February 3, 2022! The TCCoE has been established with support from DARPA (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) , AFRL (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) , and the Griffiss Institute (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) . Many of you may be familiar with the annual seL4® Summit, which we’ve successfully hosted for the past three years in coordination with the seL4 Foundation. Planning for the next annual seL4 Summit has begun under the leadership of seL4 Foundation, tentatively scheduled for October 2022 at a site in Europe. Beginning in January 2022, the TCCoE will host an annual Summit in the US, a complementary multi-day event focused on trusted computing technologies with a current emphasis on the secure embedded L4 (seL4) microkernel. seL4 is the world’s first open source operating system kernel with an end-to-end proof of implementation correctness and security enforcement. The main theme of this year’s TCCoE Summit is to provide a forum to discuss measurable security, resilience and assurance, via organic integration of hardware and software security features, for current and future platforms and systems. Specifically, the Summit scope includes, (but is not limited to), discussions on hardware security features, kernel, hypervisor and Virtual Machine Managers (VMMs), operating systems, containers, software security, etc. The TCCoE Summit will provide attendees the opportunity to attend presentations by government, industry, and academia experts; interact with discussion panels; and obtain tutorial training related to the seL4 microkernel. Come join us for 4 days packed with thought provoking keynotes, insightful presentations, lively panel discussions, and educational tutorials - an event that anyone interested in embedded systems and trust-based computing cannot miss! We look forward to your attendance! REGISTRATION IS LIVE! Registration | 13 January 2022 - 3 Feb 2022 | $250 (US) REGISTER NOW! (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) REMINDER #1: Some levels of TCCoE Membership include discounted and free attendance at the Summit, so check with your organization about membership status! REMINDER #2: Tutorials will take place on Monday, January 31, starting at 8:00 am EST. These tutorials are included with your 2022 TCCoE Summit registration. You can join these one day tutorials for free just by registering below. TUTORIAL REGISTRATION (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) MEMBERSHIP Have you and/or your company considered Trusted Computing Center of Excellence membership? Through membership, you gain an opportunity to influence the CoE’s priorities and technical direction, share ideas and network among peers in our community, and gain leverage from the latest trusted computing (e.g. seL4®) based innovations. The specific member benefits vary by membership class, but in general, membership benefits include: * Complimentary (or discounted) registration fee for CoE workshops and events * Advertising on the CoE’s website, in CoE publications, and at CoE sponsored events * Voting privileges for the election of the CoE Board of Directors, and other matters * Representation on CoE Committees * Tutorials for developers of trusted systems * Connect and collaborate securely and privately with other CoE members (chat, etc.) * Curated Software Distributions * Access to the CoE Private Code Repository (ITAR restrictions may apply) JOIN NOW! (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498… seL4 is a trademark of LF Projects, LLC. ============================================================ Copyright © 2022 Griffiss Institute, All rights reserved. You are receiving this email because of your interest in the Trusted Computing Center of Excellence.. Our mailing address is: Griffiss Institute 592 Hangar Rd Rome, NY 13441-4506 USA Want to change how you receive these emails? You can ** update your preferences (https://griffissinstitute.us6.list-manage.com/profile?u=f0470275265f4981c83…) or ** unsubscribe from this list (https://griffissinstitute.us6.list-manage.com/unsubscribe?u=f0470275265f498…)

1 0

seL4 developer hangout/video call
by Gerwin Klein 25 Jan '22

25 Jan '22

Hi seL4 devs, a few of us thought it might be nice to talk more directly from time to time rather than only via pull requests, so we're trialling a seL4 developer hangout/video chat. The idea for this is to be: - informal, about 1h - for technical discussions about seL4 and related repositories - anyone can join - every two weeks, initially for 3 times, then we can decide how we like it At least one or two technical steering committee (TSC) members will try to be at every one of these, but these are not TSC meetings where formal decisions are made, just technical discussions about whatever people have on their minds. To provide a starting topic, one thing we'd be interested in is: seL4 boot code There have been quite a few pull requests in that area, and it'd be nice to know what people's plans are and how we can keep this part of seL4 high assurance while making it more flexible. Other topics for future meetings could be better support for other language bindings (e.g. Rust), any RFCs that are open or people are thinking about opening, or just discussions about current pull requests or issues. The first hangout is on - Sydney: Wed, Nov 3, 8am - Central Europe: Tue, Nov 2, 10pm - US East Coast: Tue, Nov 2, 2pm Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

2 9

Re: seL4 developer hangout/video call
by Isaac Beckett 25 Jan '22

25 Jan '22

Other US time zones: PST (West Coast): 1pm MST (Mountain Time): 2pm CST (Central Time): 3pm EST (East Coast): 4pm We have a lot of time zones here, it’s a bit of a pain sometimes. > > On Jan 23, 2022, at 8:01 PM, devel-request(a)sel4.systems wrote: > > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via email, send a message with subject or > body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > Today's Topics: > > 1. Re: seL4 developer hangout/video call (Gerwin Klein) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sun, 23 Jan 2022 07:13:27 +0000 > From: Gerwin Klein <kleing(a)unsw.edu.au> > Subject: [seL4] Re: seL4 developer hangout/video call > To: devel <devel(a)sel4.systems> > Message-ID: <678C2D4C-EEE5-4D79-82BD-256BC78B3BFC(a)unsw.edu.au> > Content-Type: text/plain; charset="us-ascii" > > An earlier-than-usual heads-up that the seL4 developer hangout this week will be shifted by one day, because of the public holiday in Australia. > > This means, we're meeting on Wed for Europe/US and on Thu for Australia: > > - Sydney: Thu, Jan 27, 8am > - Central Europe: Wed, Jan 26, 10pm > - US West Coast: Wed, Jan 26, 1pm > > Zoom link: https://unsw.zoom.us/j/82640784431 > > Cheers, > Gerwin > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems > To unsubscribe send an email to devel-leave(a)sel4.systems > > > ------------------------------ > > End of Devel Digest, Vol 134, Issue 1 > *************************************

2 1

Sel4 Vmm Project Supporting on memory resources configure
by Tao Heng 陶恒-SW 19 Jan '22

19 Jan '22

Hi Sel4: While portinging Android Guest based on Sel4 Vmm project, I met some problems .In my porting steps, I increased the reserved memory for Android Guest to 2G on my platform. Then there were some parts of Sel4 Vmm project that confused me. 1. the principle to determin the static pool size for bootstrap with allocman n In bootstrap.h, I found your explanation for the value that it is based on the work with trial and error.Is that still the case? n If I incease this size, the frame_vm0_group_bin showed in vm_minimal.cdl file will obviously increase together.What’s the relationship of the two value? 2. How is the staic memory pool created? Is this memory pool created from untyped memory, so as treated untyped object? 3. the principle to determin the vm.simple_untyped24_pool size and nums n What’s the usage of the untyped_pool memory? n How can I make sure a reasonable size and nums of this value ? Much apprecitated, if you can give some feedbacks. Tao Heng | Taoer * +8618800230581 * taoheng(a)saicmotor.com<mailto:taoheng@saicmotor.com> Basic Software Platform SAIC Motor Z-ONE Software Company Auto Innovation Park | 201 Anyan Road, Jiading, Shanghai 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

Virtual Machine and scheduling query
by Sidhartha 12 Jan '22

12 Jan '22

Hi, I am a 2nd-year grad student at the Systopia Lab in UBC. I am using seL4 for the OS research project at I have a few independent questions: 1. Virtual Machines can be implemented with different levels of support from the hardware. If we talk about x86_64, in the most basic terms, you could have VMs without or without VT-X extensions. Looking at the resources available on the seL4 site, I think the given VMM libraries assume VT-X. Is there an example that does not use VT-X? 2. The scheduler inside seL4 is relatively simple. I have heard(Thanks Nick!) that if a complicated scheduling policy is desired, it can be done in userspace. A user-level component that has the capabilities to all the TCB's can play with the priority, resume/pause, and achieve any arbitrary scheduling. Is there an example available which I could look at? 3. I would like to implement a new functionality of memory quota, where different user-apps can be assigned memory quota and not just the physical pages. Does such a functionality belong in the kernel or the userspace component(say memory quota manager)? In the latter case, it would be just an endPoint capability to the quota manager service, so how does one split it - say split a quota of 100MB into two separate 50MB quotas. This is more a generic micro-kernel query rather than seL4 specific, but any insights would help. Thanks, Sid sid-agrawal.ca

1 0

sel4test AARCH64 on imx8mm-evk
by Zippy Manaic 07 Jan '22

07 Jan '22

Hi, I have tried running sel4test built for AARCH64 (https://docs.sel4.systems/Hardware/imx8mm.html) on my imx8mm-evk dev board. I am on the 12.1.0 branch of sel4test-manifest.git. Firstly I have to add "set(KernelAArch64SErrorIgnore ON)" to my build config in order to get the tests running and unfortunately things go awry during the test run ... Starting test 47: FRAMEEXPORTS0001 Running test FRAMEEXPORTS0001 (Test that we can access all exported frames) Pagefault from [FRAMEEXPORTS0001]: read fault at PC: 0x41c4ec vaddr: 0x11000000, FSR 0x92000210 Register of root thread in test (may not be the thread that faulted) Register dump: pc: 0x41c4ec sp: 0x100118a0 spsr: 0x80000040 x0: 0x11000000 x1: 0x11000000 x2: 0x55 x3: 0x15 x4: 0xe6 x5: 0x0 x6: 0x0 x7: 0xffffffffffffffff x8: 0x10011a48 x16: 0x0 x17: 0x0 x18: 0x0 x29: 0x100118a0 x30: 0x41c9f0 x9: 0x2b x10: 0x2b x11: 0xffffffff x12: 0x0 x13: 0x0 x14: 0x0 x15: 0x0 x19: 0xe7 x20: 0x8 x21: 0x11000000 x22: 0x0 x23: 0x0 x24: 0x0 x25: 0x0 x26: 0x0 x27: 0x0 x28: 0x0 tpidr_el0: 0x616f60 tpidrro_el0: 0x0 Failure: result == SUCCESS at line 291 of file /host/projects/sel4test/apps/sel4test-driver/src/testtypes.c Error: result == SUCCESS at line 217 of file /host/projects/sel4test/apps/sel4test-driver/src/main.c ... Starting test 55: IPC1001 Running test IPC1001 (Test SMP inter-AS seL4_Send + seL4_Recv) KERNEL DATA ABORT! Faulting instruction: 0xffffff804001e2ac FAR: 0xffffff80bf800020 ESR (DFSR): 0x96000210 halting... Kernel entry via Syscall, number: 1, Call Cap type: 10, Invocation tag: 20 Is this something that should just work? Or am I missing something. Cheers, Zippy

3 9

答复: Devel Digest, Vol 130, Issue 2
by yadong.li 03 Jan '22

03 Jan '22

Hi Matthew: Firstly, thank you for your information. form your answer, we understand the design intention of group, we Iook at compilation proces and may be find the probelm of compiler, we the assume the following scenario: The client A and client B are in the same group, they all have the same global variable like "global_buf", when use objcopy with "--keep-global-symbol" param, it will change the "global_buf" symbol form "gloabl" to "local", this change make the same name global variable of different client in same space can work well, they can access their own global variable as local variable. But In out test, we find if the "global_buf" not be initialized, in the group, there is only one "global_buf", if client A change the value of "global_buf", client B also can see the change, this is may be wrong, we find the gcc objcopy with "--keep-global-symbol" can only affect ".data" and ".bss" section, but "global_buf" which not be initialized, will place in ".common" section, "--keep-global-symbol" will not change the symbol of ".common" form global to local, this may be solved by add "-fno-common" when linker in camkes project related to "group" scenario ________________________________ 发件人: devel-request(a)sel4.systems <devel-request(a)sel4.systems> 发送时间: 2021年12月28日 9:00:05 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 130, Issue 2 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: Some questions about group of camkes (adjust the format) (Matthew Fernandez) ---------------------------------------------------------------------- Message: 1 Date: Mon, 27 Dec 2021 16:26:26 -0800 From: Matthew Fernandez <matthew.fernandez(a)gmail.com> Subject: [seL4] Re: Some questions about group of camkes (adjust the format) To: "yadong.li" <yadong.li(a)horizon.ai> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems>, "xiaonan.wang" <xiaonan.wang(a)horizon.ai>, "lei.mao" <lei.mao(a)horizon.ai> Message-ID: <DA97FC78-B670-4CF7-88AC-9810B31D1015(a)gmail.com> Content-Type: text/plain; charset=utf-8 > On Dec 23, 2021, at 08:50, yadong.li <yadong.li(a)horizon.ai> wrote: > > Hi > > * We learn the group of camkes from the https://github.com/seL4/camkes-tool/blob/master/docs/index.md > * group can colocate two component instances in a single address space, we want to use the share var by this way, like directcall transfer string virtual address, But we feel confused about the global symbols who have the same symbol name include function and variable in a single address space, Their behavior seems undefined 。 My information on how this works is out of date and I can’t answer all your questions, but I can tell you how this feature was originally implemented. Single address space components were originally implemented using post-compilation symbol mangling. As you’ve noticed, naive linking of two component instances together presents two problems: 1. Unrelated homonyms between the instances now conflict. A symbol called `foo` in component instance A and a symbol called `foo` in component instance B now refer to the same thing when linked together. 2. References to glue code have the opposite problem: their names may differ in component instance A and component instance B, but need to refer to the same functions when the two are linked together. Both problems were solved with the same mechanism: GNU objcopy. The invocations to objcopy were template-generated so they could take advantage of knowledge about the system begin compiled. A generated objcopy invocation would do the following: 1. Adjust all non-generated symbols to have internal visibility. Component instance A and component instance B have already been (partially) linked, so at this point the only unresolved symbols that need to remain externally visible are those related to the connection(s) between them. This solves problem 1 above. 2. Name-mangle all remaining symbols to something prefixed with the relevant connection instance’s name. IIRC the name mangling scheme was something like ‘<connection instance name><space><original symbol name>’. This guaranteed uniqueness because <space> is not a character that existed in C or assembly symbols. Whether using a space in a symbol name is legal or not, I don’t know, but all the binutils seemed fine with this. 3. Rename the second component in the name mangling above to a common name. I don’t recall exactly how this name was chosen, but this solves problem 2 above. This sounds pretty unorthodox and brittle, but it actually worked surprisingly well. All combinations of single address space component systems seemed to Just Work, with a few notable sharp edges: * Anything involving MMIO was tricky. These symbols frequently needed to remain externally visible and the two component instances would often have differing names but the same addresses for them. * GNU ld was more or less required. The multiple steps involving partial linking was only supported by GNU ld and Gold at the time. LLVM’s lld may have caught up in the interim years. * The objcopy name mangling broke cross-section references used by GCC’s implementation of Link-Time Optimization. As a result, any LTO compilation degraded to LTO being disabled. This wouldn’t have been a big deal except that one of the primary reasons to put two components in a single address space is to enable cross-component inlining, usually facilitated by LTO. AFAICT this (playing objcopy tricks and expecting LTO to still work) was simply not a supported use case. We explored how to work around this and got some one-off efforts working for benchmarking, but proper support would have involved altering the way binutils work. ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems ------------------------------ End of Devel Digest, Vol 130, Issue 2 *************************************

2 1

Question about the Real-time of the SEL4.
by 刘跃 Jeff Liu 01 Jan '22

01 Jan '22

Hi; As we know, seL4 is a non preemptive kernel. Is it because the kernel of seL4 is an event based model? Then why not use the thread based kernel? As far as I know, VxWorks and QNX are thread based. SeL4's view is that for non preemptive kernel, real-time performance focuses on WCET, and the faster kernel does not guarantee the real-time performance of the system. I partially agree with this view. I want to know if there are real-time comparison data?, The comparison test with VxWorks or QNX is about the real-time performance of the system. the worst case interrupt latency is the sum of both the longest region with interrupts disabled, and the time to dispatch an interrupt to a user thread. How are these two parts of time calculated? Is it the method of WCET static analysis? And Then how to improve the interrupt response time, What is the specific method to reduce interrupt latency? I think most users of seL4 are more concerned about this. I look forward to communicating and discussing with you, experts. Thanks;

2 1

Some questions about group of camkes (adjust the format)
by yadong.li 28 Dec '21

28 Dec '21

Hi * We learn the group of camkes from the https://github.com/seL4/camkes-tool/blob/master/docs/index.md * group can colocate two component instances in a single address space, we want to use the share var by this way, like directcall transfer string virtual address, But we feel confused about the global symbols who have the same symbol name include function and variable in a single address space, Their behavior seems undefined 。 * Our camkes project test below, clien1 and client2 in the same group: " import <std_connector.camkes>; procedure MyInterface { void print(in string message); } component Client { control; uses MyInterface iface; } component Server { provides MyInterface iface; } assembly { composition { group g { component Client client_1; component Client client_2; } component Server server; connection seL4RPCCall conn(from g.client_1.iface, from g.client_2.iface, to server.iface); } configuration { client_1.iface_attributes = 11; client_2.iface_attributes = 22; } } * 1. We test function in group (a single address space): * the client code below: " #include <camkes.h> int run(void) { char *name = get_instance_name(); iface_print(name); return 0; } " * the server code below: " #include <camkes.h> #include <stdio.h> void iface_print(const char *name) { printf("[%s] ping, the badge is [%d]\n", name, iface_get_sender_id()); } " * From the cameks project, we have two client, they are client_1 and client_2, they have the same they can all “iface_print” to access server function，In this scene，we have two quesiton: * Question 1. After compiled the test project, we found in the symbol table of g_group_bin, we have two "iface_print" symbol, they have different address even though they have the same name, it look like the componet can call their own "iface_print", I think in a single address space, component like thread, Why two symbols with the same name(iface_print) will not conflict in one address space * Question 2: when client access server, we offer the _attributes(badge) for the interface of client, by test, the two client can call their own "iface_print", but the server can only recevice one badge 22, below is our test: " [client_2] ping, the badge is [22] [client_1] ping, the badge is [22] " * The attribute(badge) of client1 is covered by the attribute(badge) of client2, The iface_print of two client have only one capability to access IPC endpoint object * We can not understand in single address space,the "iface_print" of two component is behavior as one or two different ? * 2. We test function in global variable (a single address space): * We found whether global variables are initialized will have completely different behavior， out test code below: * scene1 :Client code below: " int temp_value; int run(void) { char *name = get_instance_name(); iface_print(name); printf("at start, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); if (strcmp(name, "client_1") == 0) { int count = 1000000000; while(count--) { asm volatile(""); } /* client1 read the temp_value*/ printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } else { /* client2 change the val of temp_value */ temp_value = 0x12345; printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } return 0; } " * Phenomenon: client1 and client2 are different instances of the same code in same group，form the above code，the symbol of "temp_value" is bss section, the temp_value of client1 and the temp_value of client2 have the same virtual address, and if the client2 change the value, client1 can perceive the change， test as below： " at start, in client_1, the temp_value address is [0x659e70], value is [0x0] at start, in client_2, the temp_value address is [0x659e70], value is [0x0] at last, in client_2, the temp_value address is [0x659e70], value is [0x12345] at last, in client_1, the temp_value address is [0x659e70], value is [0x12345] " * scene2 :Client code below: " int temp_value = 1; int run(void) { char *name = get_instance_name(); iface_print(name); printf("at start, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); if (strcmp(name, "client_1") == 0) { int count = 1000000000; while(count--) { asm volatile(""); } /* client1 read the temp_value*/ printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } else { /* client2 change the val of temp_value */ temp_value = 0x12345; printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } return 0; } " * Phenomenon: client1 and client2 are different instances of the same code in same group，form the above code，the symbol of "temp_value" is data section, the temp_value of client1 and the temp_value of client2 have the different virtual address, and if the client2 change the value, client1 can not get the change， test as below： " at last, in client_2, the temp_value address is [0x445ba8], value is [0x12345] at last, in client_1, the temp_value address is [0x444008], value is [0x1] " * The code of scene1 and scene2 are almost the same, except whether temp_value is initialized， the bss section or data section，but the symbol table completely different, scene1 the symbol table of g_group_bin has only one "temp_value" symbol, But scene1 the symbol table of g_group_bin has two symbols named temp_value, we also do not understand why the same name symbols of global variable should be one or two in a single address of group. It looks like random. Thank you very much

2 1

Some questions about group of camkes
by yadong.li 24 Dec '21

24 Dec '21

Hi * We learn the group of camkes from the https://github.com/seL4/camkes-tool/blob/master/docs/index.md * group can colocate two component instances in a single address space, we want to use the share var by this way, like directcall transfer string virtual address, But we feel confused about the global symbols who have the same symbol name include function and variable in a single address space, Their behavior seems undefined 。 * Our camkes project test below, clien1 and client2 in the same group: import <std_connector.camkes>; procedure MyInterface { void print(in string message); } component Client { control; uses MyInterface iface; } component Server { provides MyInterface iface; } assembly { composition { group g { component Client client_1; component Client client_2; } component Server server; connection seL4RPCCall conn(from g.client_1.iface, from g.client_2.iface, to server.iface); } configuration { client_1.iface_attributes = 11; client_2.iface_attributes = 22; } } * 1. We test function in group (a single address space): * the client code below: #include <camkes.h> int run(void) { char *name = get_instance_name(); iface_print(name); return 0; } * the server code below: #include <camkes.h> #include <stdio.h> void iface_print(const char *name) { printf("[%s] ping, the badge is [%d]\n", name, iface_get_sender_id()); } * From the cameks project, we have two client, they are client_1 and client_2, they have the same they can all “iface_print” to access server function，In this scene，we have two quesiton: * Question 1. After compiled the test project, we found in the symbol table of g_group_bin, we have two "iface_print" symbol, they have different address even though they have the same name, it look like the componet can call their own "iface_print", I think in a single address space, component like thread, Why two symbols with the same name(iface_print) will not conflict in one address space * Question 2: when client access server, we offer the _attributes(badge) for the interface of client, by test, the two client can call their own "iface_print", but the server can only recevice one badge 22, below is our test: [client_2] ping, the badge is [22] [client_1] ping, the badge is [22] * The attribute(badge) of client1 is covered by the attribute(badge) of client2, The iface_print of two client have only one capability to access IPC endpoint object * We can not understand in single address space,the "iface_print" of two component is behavior as one or two different ? * 2. We test function in global variable (a single address space): * We found whether global variables are initialized will have completely different behavior， out test code below: * scene1 :Client code below: int temp_value; int run(void) { char *name = get_instance_name(); iface_print(name); printf("at start, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); if (strcmp(name, "client_1") == 0) { int count = 1000000000; while(count--) { asm volatile(""); } /* client1 read the temp_value*/ printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } else { /* client2 change the val of temp_value */ temp_value = 0x12345; printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } return 0; } * Phenomenon: client1 and client2 are different instances of the same code in same group，form the above code，the symbol of "temp_value" is bss section, the temp_value of client1 and the temp_value of client2 have the same virtual address, and if the client2 change the value, client1 can perceive the change， test as below： at start, in client_1, the temp_value address is [0x659e70], value is [0x0] at start, in client_2, the temp_value address is [0x659e70], value is [0x0] at last, in client_2, the temp_value address is [0x659e70], value is [0x12345] at last, in client_1, the temp_value address is [0x659e70], value is [0x12345] * scene2 :Client code below: int temp_value = 1; int run(void) { char *name = get_instance_name(); iface_print(name); printf("at start, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); if (strcmp(name, "client_1") == 0) { int count = 1000000000; while(count--) { asm volatile(""); } /* client1 read the temp_value*/ printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } else { /* client2 change the val of temp_value */ temp_value = 0x12345; printf("at last, in %s, the temp_value address is [%p], value is [0x%lx]\n", name, &temp_value, temp_value); } return 0; } * Phenomenon: client1 and client2 are different instances of the same code in same group，form the above code，the symbol of "temp_value" is data section, the temp_value of client1 and the temp_value of client2 have the different virtual address, and if the client2 change the value, client1 can not get the change， test as below： at last, in client_2, the temp_value address is [0x445ba8], value is [0x12345] at last, in client_1, the temp_value address is [0x444008], value is [0x1] * The code of scene1 and scene2 are almost the same, except whether temp_value is initialized， the bss section or data section，but the symbol table completely different, scene1 the symbol table of g_group_bin has only one "temp_value" symbol, But scene1 the symbol table of g_group_bin has two symbols named temp_value, we also do not understand why the same name symbols of global variable should be one or two in a single address of group. It looks like random.

1 0

Can't locate VM at virtual 0?
by Richard Clark 22 Dec '21

22 Dec '21

My VM's can't seem to be untied from actual physical memory.... I've got a nice old moldy version of sel4, around version 8 I think, but it's got some life left if we can figure out how to remap our VMs to 0 instead of mapping virtual directly equal physical... In other words, for some reason, we map virtual == physical, and have to tell the VM that it is up at some high-level address. We would like to be able to pick a physical patch of memory, and map it to zero in the VM, so the VM can believe it is at 0. Honestly I don't understand why that isn't the default anyway... But I've found examples where I can specify a physical address and get back an arbitrary virtual address, and other examples where I can specify a virtual address and get back an arbitrary physical page. What I need, is a way to specify both the physical and the virtual addresses into my VM vspace. Would you happen to have an example or two on hand? For a little more context, I've got the following code, which appears to map the first page ok, but then fails trying to map the next page when called a second time: map_ram_to(vspace_t *vspace, vspace_t *vmm_vspace, vka_t* vka, uintptr_t paddr, uintptr_t vaddr) { vka_object_t frame_obj; cspacepath_t frame[2]; reservation_t res; int err; /* reserve vspace */ printf("map_ram_to, reserve phys mem at %p to vaddr %p\n", (void *)paddr, (void *)vaddr); res = vspace_reserve_range_at(vspace, (void *)paddr, 0x1000, seL4_AllRights, 1); if (!res.res) { ZF_LOGF("Failed to reserve range"); return NULL; } /* map phys addr ro frame obj */ printf("map_ram_to, alloc phys mem at %p\n", (void *)paddr); err = vka_alloc_frame_at(vka, 12, paddr, &frame_obj); if (err) { printf("ERROR VKA alloc ptr: %p\n", vka->data); ZF_LOGF("Failed vka_alloc_frame_maybe_device in devices.c"); vspace_free_reservation(vspace, res); return NULL; } vka_cspace_make_path(vka, frame_obj.cptr, &frame[0]); printf("map_ram vka_cspace_alloc_path\n"); err = vka_cspace_alloc_path(vka, &frame[1]); if (err) { ZF_LOGF("Failed vka_cspace_alloc_path"); vka_free_object(vka, &frame_obj); vspace_free_reservation(vspace, res); return NULL; } printf("map_ram vka_cnode_copy\n"); err = vka_cnode_copy(&frame[1], &frame[0], seL4_AllRights); if (err) { ZF_LOGF("Failed vka_cnode_copy"); vka_cspace_free(vka, frame[1].capPtr); vka_free_object(vka, &frame_obj); vspace_free_reservation(vspace, res); return NULL; } err = map_page(vspace, frame_obj.cptr, (void *)vaddr, seL4_AllRights, 1, 12); vspace_free_reservation(vspace, res); if (err) { printf("FAILED Failed vspace_map_pages_at_vaddr\n"); vka_cspace_free(vka, frame[1].capPtr); vka_free_object(vka, &frame_obj); return NULL; } printf("map_ram_to, worked and zeroed at %p\n", (void *)paddr); return (void *)paddr; } Help is greatly appreciated! Richard H. Clark

2 1

vm physaddr != virtual?
by Richard Clark 22 Dec '21

22 Dec '21

My VM's can't seem to be untied from actual physical memory.... I've got a nice old moldy version of sel4, around version 8 I think, but it's got some life left if we can figure out how to remap our VMs to 0 instead of mapping virtual directly equal physical... In other words, for some reason, we map virtual == physical, and have to tell the VM that it is up at some high-level address. We would like to be able to pick a physical patch of memory, and map it to zero in the VM, so the VM can believe it is at 0. Honestly I don't understand why that isn't the default anyway... But I've found examples where I can specify a physical address and get back an arbitrary virtual address, and other examples where I can specify a virtual address and get back an arbitrary physical page. What I need, is a way to specify both the physical and the virtual addresses into my VM vspace. Would you happen to have an example or two on hand? For a little more context, I've got the following code, which appears to map the first page ok, but then fails trying to map the next page when called a second time: map_ram_to(vspace_t *vspace, vspace_t *vmm_vspace, vka_t* vka, uintptr_t paddr, uintptr_t vaddr) { vka_object_t frame_obj; cspacepath_t frame[2]; reservation_t res; int err; /* reserve vspace */ printf("map_ram_to, reserve phys mem at %p to vaddr %p\n", (void *)paddr, (void *)vaddr); res = vspace_reserve_range_at(vspace, (void *)paddr, 0x1000, seL4_AllRights, 1); if (!res.res) { ZF_LOGF("Failed to reserve range"); return NULL; } /* map phys addr ro frame obj */ printf("map_ram_to, alloc phys mem at %p\n", (void *)paddr); err = vka_alloc_frame_at(vka, 12, paddr, &frame_obj); if (err) { printf("ERROR VKA alloc ptr: %p\n", vka->data); ZF_LOGF("Failed vka_alloc_frame_maybe_device in devices.c"); vspace_free_reservation(vspace, res); return NULL; } vka_cspace_make_path(vka, frame_obj.cptr, &frame[0]); printf("map_ram vka_cspace_alloc_path\n"); err = vka_cspace_alloc_path(vka, &frame[1]); if (err) { ZF_LOGF("Failed vka_cspace_alloc_path"); vka_free_object(vka, &frame_obj); vspace_free_reservation(vspace, res); return NULL; } printf("map_ram vka_cnode_copy\n"); err = vka_cnode_copy(&frame[1], &frame[0], seL4_AllRights); if (err) { ZF_LOGF("Failed vka_cnode_copy"); vka_cspace_free(vka, frame[1].capPtr); vka_free_object(vka, &frame_obj); vspace_free_reservation(vspace, res); return NULL; } err = map_page(vspace, frame_obj.cptr, (void *)vaddr, seL4_AllRights, 1, 12); vspace_free_reservation(vspace, res); if (err) { printf("FAILED Failed vspace_map_pages_at_vaddr\n"); vka_cspace_free(vka, frame[1].capPtr); vka_free_object(vka, &frame_obj); return NULL; } printf("map_ram_to, worked and zeroed at %p\n", (void *)paddr); return (void *)paddr; } Help is greatly appreciated! Richard H. Clark

1 0

mapping tutorial answers?
by Richard Clark 22 Dec '21

22 Dec '21

I'm interested in the ANSWERS to the MAPPING tutorial. I have my own virtual/physical memory management system and need only the ability to map a specific physical address to a specific virtual address. I can find no such thing in all the sel4 code that I have, but it appears that the mapping tutorial is what I need. Does anyone have this? (preferably arm64 and/or x64) Richard Clark

1 0

sel4-sys support
by kgugala＠antmicro.com 16 Dec '21

16 Dec '21

Hi All, We’ve been working on reviving the sel4-sys Rust crate and getting it usable again. Currently, we have it working correctly with RISC-V, we’re working on ARM (including aarch64) and X86. We’d like to contribute this work, but to have it landed we need to extend the test suite to include crate tests - especially the syscalls API. During the build, the crate generates the syscalls functions accessible from Rust code based on seL4 config. We use standard sel4test-tests suite to handle the tests: * We build the crate as static library * Sel4test is built with `-DLibSel4FunctionAttributes=public` and while linking we overwrite the original symbols with the ones from a static library from the crate This allows us to run the standard test suite against Rust syscall stubs. For now the crate generates the syscall stubs with Rust flavor, so functions signatures between Rust and C do not match. To handle this we additionally generate a thin glue code adopting Rust signatures to the C ones. We generate the Rust syscalls with a slightly modified version of the `syscall_stub_gen.py` script - we copied it into the crate’s codebase. Copying the code doesn’t seem to be the best idea - we’d need to maintain the code in both places - seL4 kernel and the crate. We’d like to merge the Rust generator with the current set of tools - is this something you’d be willing to land in the kernel code? If not, how would you see the way forward here? Thanks and best regards Karol

4 5

Re: seL4 developer hangout/video call
by Isaac Beckett 15 Dec '21

15 Dec '21

This is 4pm east coast US/EST. > The next instalment of the seL4 developer hangout is happening as planned tomorrow. It's the last one for this year: > > - Sydney: Wed, Dec 15, 8am > - Central Europe: Tue, Dec 14, 10pm > - US West Coast: Tue, Dec 14, 1pm > > Zoom link: https://unsw.zoom.us/j/82640784431 > > (There is also a separate meeting of the technical steering committee end of this week) > > Cheers > Gerwin

1 0

two questions about cteDelete of sel4 kernel 12.0.0 ?
by yadong.li 12 Dec '21

12 Dec '21

Hi： I have two questions about cteDelete of sel4 kernel 12.0.0？ IF I want to delete slot that slot->cap is cnode object(I called it level 1 cnode). The finaliseSlot function will create zombie capability and call reduceZombie(), param "immediate" is ture. the reduceZombie() call cteDelete() delete the endSlot, if the endSlot->cap is cnode capability again(I call it level 2 cnode), this time param "immediate" is false. and cteDelete() will call reduceZombie again, but because param "immediate " is false ,this time reduceZombie will not call cteDelete recursively. the reduceZombie will call capSwapForDelete, if Swap cap is not cnode or tcb, when it return to finaliseSlot, finaliseSlot will check finaliseCap, because swap cap is not cnode or tcb, almost it capRemovable, and it return directly. 1. I think when call capSwapForDelete in reduceZombie, the level 2 cnode become Cyclic zombie, but when return finaliseSlot, I do not think it will deal with below branch: if (!immediate && capCyclicZombie(fc_ret.remainder, slot)) { } because this time ,slot ->cap is not cnode or tcb, it will not create zombie cap. Who will delete level 2 cnode ? Is it lost as "Cyclic zombie", memory leak? 2. when delete cnode, it will check "preemptionPoint", if our delete is beak, even though fs_ret.success is false, but this false is not deliver to caller, who will delete cnode object again? Thank you very much

2 3

seL4 kernel does not receive PCI interrupts
by hamed_ganji＠aut.ac.ir 12 Dec '21

12 Dec '21

Hi all, I have created a simple CAMKES-VM-x86 app for a PC but its PCI devices are not working due to not receiving corresponding interrupts. By adding a printf to the function "handleInterrupt" inside the seL4 kernel I found that only some limited interrupts such as timer and serial are received. However, capdl_spec.c file contains all necessary declaration of capabilities and objects for the required interrupts such as follows, ... [19625] = { #ifdef CONFIG_DEBUG_BUILD .name = "vm0_irq_10", #endif .type = CDL_IOAPICInterrupt, .slots.num = 1, .slots.slot = (CDL_CapSlot[]) { {0, {.type = CDL_NotificationCap, .obj_id = 19567 /* vm0_irq_notification_obj_10 */, .is_orig = true, .rights = (CDL_CanRead), .data = { .tag = CDL_CapData_Badge, .badge = 0}}}, }, .ioapicirq_extra = { .ioapic = 0, .ioapic_pin = 10, .level = 1, .polarity = 1, }, }, ... and the host endpoint of the VMM thread is properly set to receive IRQ notifications and route them to VM, and the IOAPIC pin number (source) is also true, I checked. How can I solve the problem? Any pointers would be appreciated. Kind regards, Hamed

1 0

Nvidia Tegra SoCs: Has anyone tried running seL4 on them?
by Isaac Beckett 12 Dec '21

12 Dec '21

Has anyone experimented with running seL4 on Tegra SoCs? I’m interested mainly because I own a Nintendo Switch console that is vulnerable to an exploit in the boot rom that allows for booting arbitrary payloads. Most people use it to run modified versions of the official firmware, or to run Linux or Android, so the hardware is at least decently well reverse engineered at this point, and there are even proper Linux drivers for the joy-con detachable controllers. I’m interested in attempting to run seL4 on this device, mostly to see if I can, but I figured I’d ask here first to see if anyone’s attempted similar hardware.

2 2

next seL4 TSC meeting on Fri 17 Dec (16 Dec in US and Europe)
by Gerwin Klein 11 Dec '21

11 Dec '21

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Fri, 17 Dec, 8am - Central Europe: Tue, 16 Dec, 10pm - US West Coast: Tue, 16 Dec, 1pm The meeting is by Zoom, and you can join from here: https://unsw.zoom.us/j/82827057586 Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. The agenda for the meeting so far is: - update on GitHub status, test stability, etc - release schedule - change main verification platform to imx8? - RFCs: - Core Platform https://sel4.atlassian.net/browse/RFC-5 - Removing CNode Mutate https://sel4.atlassian.net/browse/RFC-7 - SMC calls https://sel4.atlassian.net/browse/RFC-9 If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.html

1 0

two questions about cteDelete of sel4 kernel？
by yadong.li 11 Dec '21

11 Dec '21

Hi： I have two questions about cteDelete of sel4 kernel？ IF I want to delete slot that slot->cap is cnode object(I called it level 1 cnode). The finaliseSlot function will create zombie capability and call reduceZombie(), param "immediate" is ture. the reduceZombie() call cteDelete() delete the endSlot, if the endSlot->cap is cnode capability again(I call it level 2 cnode), this time param "immediate" is false. and cteDelete() will call reduceZombie again, but because param "immediate " is false ,this time reduceZombie will not call cteDelete recursively. the reduceZombie will call capSwapForDelete，it will swap zombie cap with slot 0 of level 2 cnode, if Swap cap(slot0 of level 2 cnode) is not cnode or tcb(the cnode object slot 0 must point to cnode self ? I did not find this limitation), when it return to finaliseSlot, finaliseSlot will check finaliseCap, because swap cap is not cnode or tcb, almost it call be capRemovable, and it return directly. 1. I think when call capSwapForDelete in reduceZombie, the level 2 cnode become Cyclic zombie, but when return finaliseSlot, I do not think it will deal with below branch: if (!immediate && capCyclicZombie(fc_ret.remainder, slot)) { } because this time ,slot ->cap is not cnode or tcb, it will not create zombie cap. then Who will delete level 2 cnode ? Is it lost as "Cyclic zombie", memory leak? 2. when delete cnode, it will check "preemptionPoint", if our delete is beak, even though fs_ret.success is false, but this false is not deliver to caller who will delete it again? thank you for your help

1 0

How can I port the seL4 microkernel to my unofficially verified hardware？
by yjy 10 Dec '21

10 Dec '21

Does the document provide relevant information or project? I read related articles and I can be sure that my instruction set is common. Thank you.

2 1

Troubles booting VM with large memory(e.g VM_RAM_SIZE >= 2048MB)
by Han JingLong 韩景龙 09 Dec '21

09 Dec '21

Hello all, Reference to seL4 Docs/Projects/CAmkES ARM VMM, I have successfully run a VM (a Linux guest OS and config VM_RAM_SIZE = 1024MB) on a new ARM(ArmV8a CortexA55) platform. But when I tried to increase the ram size assigned to VM, I encountered the following error: ============================================================================== ram_ut_alloc_iterator@guest_ram.c:295 Failed to allocate page map_vm_memory_reservation@guest_memory.c:470 Failed to get frame for reservation address 0xae7c0000 reservation_size:60000000 …… vm_ram_touch@guest_ram.c:160 Failed to touch ram region: Not registered RAM region 32 bit ARM insts not decoded Pagefault from [Linux]: write fault @ PC: 0xffff000008d9132c IPA: 0xaffff000, FSR: 0x92000046 Context: x0: 0xffff7dfffe639000 x1: 0x0 x2: 0xfc0 x3: 0x4 x4: 0x0 x5: 0x40 x6: 0x3f x7: 0x0 x8: 0xffff7dfffe639000 x9: 0x0 x10: 0x1000 x11: 0x6f01c3b8 x12: 0xc0000000 pc: 0xffff000008d9132c x14: 0x0 sp: 0xffff000009668d80 spsr: 0x40000085 x13: 0x60000000 x15: 0x4 x16: 0x1800 x17: 0xffff7dfffe81c3b4 x18: 0x8 x19: 0xaffff000 x20: 0xffff0000096a1fd0 x21: 0xffff7dfffe80009c x22: 0x58389df x23: 0xffff0000091ce000 x24: 0x4b78e0 x25: 0x47b87c x26: 0x0 x27: 0xa0000000047b818 x28: 0x614f0018 x29: 0xffff000009643eb0 x30: 0xffff0000094f7ad0 m-------- Assertion failed: rt >= 0 (/home/hjl/workdir/vmm_sel4_sdx_android/projects/seL4_projects_libs/libsel4vm/src/arch/arm/fault.c: fault_get_width: 623) Attach config file for reference： 1. overlay dts reserved-memory { #address-cells = < 0x02 >; #size-cells = < 0x02 >; ranges; vm-memory@60000000 { reg = < 0x00 0x60000000 0x00 0x60000000 >; no-map; }; }; 1. devices.camkes #define VM_INITRD_MAX_SIZE 0x5000000 //80 MB #define VM_RAM_BASE 0x60000000 #define VM_RAM_OFFSET 0 #define VM_RAM_SIZE 0x60000000 #define VM_DTB_ADDR 0x6F000000 #define VM_INITRD_ADDR 0x6A000000 vm0.untyped_mmios = [ “0x35436000:12”, // Interrupt Controller Virtual CPU interface (Virtual Machine view) /* The purpose of these untyped regions is to force the untyped * allocator to treat this memory region as reserved so that when we * try to ensure that the VMM is placed into this region in RAM, it * will definitely be available for placement. * * This address pertains to vm-memory@60000000 in the overlay DTS */ “0x60000000:28”, // RAM “0x70000000:28”, // RAM “0x80000000:28”, // RAM “0x90000000:28”, // RAM “0xa0000000:28”, // RAM “0xb0000000:28”, // RAM ]; 1. guest linux dts memory@60000000 { device_type = “memory”; reg = <0x00 0x60000000 0x00 0x60000000>; }; ============================================================================== In contrast, I tried to expand the VM memory based on QEMU and encountered the same problem. Attach config file for reference： 1. settings.cmake if(${PLATFORM} STREQUAL “qemu-arm-virt”) set(QEMU_MEMORY “4096”) set(KernelArmCPU cortex-a53 CACHE STRING “” FORCE) set(VmInitRdFile ON CACHE BOOL “” FORCE) endif() 1. overlay-reserve-vm-memory.dts reserved-memory { #address-cells = < 0x02 >; #size-cells = < 0x02 >; ranges; vm-memory@40000000 { reg = <0x0 0x40000000 0x0 0x50000000>; no-map; }; }; 1. devices.camkes #define VM_INITRD_MAX_SIZE 0x1900000 //25 MB #define VM_RAM_BASE 0x40000000 #define VM_RAM_SIZE 0x50000000 #define VM_RAM_OFFSET 0x00000000 #define VM_DTB_ADDR 0x4F000000 #define VM_INITRD_ADDR 0x4D700000 vm0.untyped_mmios = [ “0x8040000:12”, // Interrupt Controller Virtual CPU interface (Virtual Machine view) “0x40000000:29”, // Linux kernel memory regions “0x60000000:29”, // Linux kernel memory regions “0x80000000:28”, // Linux kernel memory regions ]; 1. guest linux dts memory@40000000 { reg = <0x0 0x40000000 0x0 0x50000000>; device_type = “memory”; }; Is there any memory limit for VM? or Configuration problem? Anyways anyone any help can provide would be awesome and thanks in advance for any help! 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

getKernelWcetUs: where does the 10us return value come from?
by Jack Chen 09 Dec '21

09 Dec '21

Hi all, Quick questions regarding the return value of getKernelWcetUs(): 1. For ARM the value is assigned during build process taking config.cmake files, where KERNEL_WCET's are all 10us (except for tk1 it's 100us, typo?) For x86 the function returns 10 directly, and for risc-v, comment suggests it's copied from x86 hoping it's an overestimate. Where does this "10us" come from? Based on static estimate done previously on Armv6 (imx31)? AOS lecture mentioned a "378us" kernel WCET estimate and 99.5us observed WCET for Armv6. 2. Is this 10us WCET value the one used as padding in the Temporal Partitioning routine? ("worst-case flushing time"?) Regards, Jack

3 5

Incorporating seL4 into your project, risc-v architecture
by so_s＠gmx.de 08 Dec '21

08 Dec '21

Dear seL4 devs and community. I try to create a simple project using the seL4 micro kernel. For setting up my environment I followed this (https://github.com/manu88/SeL4_101) and this (https://docs.sel4.systems/projects/buildsystem/incorporating.html) article. As kernel I'm using the last release of SeL4 (https://github.com/seL4/seL4/releases/tag/12.1.0) I created some kind of user application, like Manu88 did with a simple Hello World C-Program. While building with the delivered init-build.sh script I got a lot of repeating errors like this: CMake Error at tools/cmake-tool/helpers/simulation.cmake:179 (add_custom_command): Error evaluating generator expression: $<TARGET_PROPERTY:rootserver_image,KERNEL_IMAGE_NAME> Target "rootserver_image" not found. Call Stack (most recent call first): CMakeLists.txt:22 (GenerateSimulateScript) While going through Manu88s guide I saw that he also got this errors. But after adding a CMakeList.txt file inside his user code, and declaring it as rootserver inside the CMakeList.txt file (I just copied the contents from here: https://github.com/manu88/SeL4_101/blob/master/projects/Hello/CMakeLists.txt) he got rid of the errors. I still get them and searching through the internet could not find a solution for me. Bellow I added the folder structure of my project. Project/ ├── kernel/ ├── projects/ │ ├── Hello/ │ ├── musllibc/ │ ├── utils_libs/ │ ├── seL4_libs/ ├── build/ ├── tools/ │ └── cmake-tool/ │ └── elfloader-tool/ ├── init-build.sh -> tools/cmake-tool/init-build.sh ├── CMakeLists.txt ├── application_settings.cmake -> tools/cmake-tool/helpers/application_settings.cmake ├── settings.cmake So I cannot tell where the issue lies. Any pointers would be appreciated. Kind regards, Sophia

2 3

capdl-loader questions
by Sam Leffler 08 Dec '21

08 Dec '21

I've been investigating how capd-loader works and have some questions. My apologies if these were previously discussed. 1. CDL_Model is mutable. The capDL specification looks like a perfect candidate for being in .rodata but it's stored+treated as mutable. Why? I see capdl-loader uses the mutability to store mapped page frame caps and, for risc-v, VSpace roots, but both can be easily handled w/o modifying the spec. Having this immutable has many benefits. 2. All page frames are treated as shared. CAPDL_SHARED_FRAMES is #define'd in the code so every frame is treated as shared. This inflates the size of the orig_caps array and the kernel capabilities table but seems unnecessary. Why? I've verified that instead of doing the Copy op on each page you can just check the return of the seL4_Page_Map call and if necessary clone the cap. Better would be for camkes to identify shared page frames so this doesn't require 2x syscalls (which spam's the console w/ CONFIG_PRINTING enabled). 3. Why does copy_addr_with_pt exist? There are two memory regions created for mapping page frames into the rootserver address space for doing fill ops. One is 64KB and the other is 1 page (nominally 4KB). init_frame tries the 4KB region first then falls back to the 64K region if mapping into the 4KB region fails. Why (i.e. why would the 1st mapping call fail)? On my risc-v system I never use the 64K region and I'm not sure when it might be used? Even if it were used, why is 64K always allocated; seems like the region should be sized according to the target platform. Having this extra region has a cost that can be significant on small systems. 4. console output. Why is sel4_DebugPutChar (or similar) not a standard part of the kernel? This forces capdl-loader to depend on libsel4platsupport for console output which in turn affects cap space. I can't imagine an seL4 system that cannot write to the console and I think it's entirely reasonable to have a critical system service like the rootserver use that. 5. duplicate_caps. The scheme for constructing a running system from a spec is straightforward except for duplicating caps. Why are all TCB's and CNode caps dup'd? Why does init_tcbs call init_tcb on the original object but immediately configure_tcb on the dup? There are other places where the dup cap is used instead of the original cap (e.g. init_cnode_slot). None of this seems to matter on risc-v; maybe this matters on some other architectures? 6. On risc-v all pages appear to be marked executable--including ipc buffers! This seems just wrong and a potential security hole. 7. Why does seL4_TCB_WriteRegisters take a _mutable_ seL4_UserContext? I'm guessing this is a mistake in the xml spec (but haven't looked). 8. init_cspaces mystifies me. There are two loops over all CNodes; one that does "COPY" operations and one that does "MOVE" operations. I see nothing explaining what's happening. I've read this code many times and still don't get it; please explain. 9. According to comments, the use of a global static to setup the UserContext for a new TCB is done because one cannot take the address of a local variable. On what architecture is this true? On risc-v the context is copied into "registers" before calling the kernel so this doesn't appear to be an issue with crossing the user-kernel protection boundary. 10. Memory reclamation. I'm unclear what happens to the memory used by capdl-loader. The process does a TCB_Suspend call when it's done. Does this cause the CSpace & VSpace to be reclaimed? For CAmkES this doesn't matter as there's no support for allocating memory but I'm building a system where this isn't true. How do I release memory (in particular) back to the untyped pool? I have a bunch of niggly code complaints/questions but let's start with the above. -Sam

2 4

Re: some performance problem when test 4 cores SMP答复: Devel Digest, Vol 127, Issue 5
by yadong.li 07 Dec '21

07 Dec '21

Hi: > So you would expect that the reported metric would scale following Amdahl's law based on the proportion of an operation that is serialized inside the kernel lock which would potentially vary across platforms. > It cannot simply be throughput, else the doubled delay should be reflected in a significantly reduced throughput, but it has almost no effect. 1. This is what I also feel confused, I think whether it is depend on the implementation of ipc_normal_delay ipc_normal_delay will call below code: delay = OVERHEAD_FIXUP(REXP(id) * current_delay_cycle, overhead); insert a command such as 'zigset(...)'for every core, The ziggurat method for generating random variables, when double delay, the random variables coefficient will reduce the delay influence? 2. " the proportion of an operation that is serialized inside the kernel lock ", CLH lock is serialized between cores, if 4 cores will have big different performance on different ARM platform? > For 3 or 4 cores the combined latency of two IPCs is larger than the 500cy delay and you expect lock contention, resulting in reduced scaling, while it should still scale almost perfectly with the 1000cy delay. > > > Addition： > > Our seL4_Call performance is same with other platform > > XXXX IMX8MM_EVK_64 TX2_64 > > seL4_Call 367(0) 378(2) 492(16) client->server, same vspace, ipc_len is 0 > > seL4_ReplyRecv 396(0) 402(2) 513(16) server->client, same vspace, ipc_len is 0 1. the seL4_Call and seL4_ReplyRecv are measured on SMP kernel 2. or 3 or 4 cores the combined latency of two IPCs is larger than the 500cy delay and you expect lock contention ---- that's what I thought at first, But It can't be explained very well on IMX8MM_EVK_64, base on the test seL4_Call data, when run on 3 cores and 4cores, IMX8MM_EVK_64 still have a good scalability, so I think not all seL4_Call and ReplyRecv flow which cost maybe 300 or 400 is locked(like el trap), TX2 should have a good scalability as expected when run on 3 or 4 cores, but it did not show good, from data below：1497740（3core， 500cycles），1545872（4core） > > My test results below: > > ARM platform > > Test item XXX IMX8MM_EVK_64 TX2 > > mean(Stddev) > > 500 cycles, 1 core 636545(46) 625605(29) 598142(365) > > 500 cycles, 2 cores 897900(2327) 1154209(44) 994298(94) > > 500 cycles, 3 cores 1301679(2036) 1726043(65) 1497740(127) > > 500 cycles, 4 cores 1387678(549) 2172109(12674) 1545872(109) > > 1000 cycles, 1 core 636529(42) 625599(22) 597627(161) > > 1000 cycles, 2 cores 899212(3384) 1134110(34) 994437(541) > > 1000 cycles, 3 cores 1297322(5028) 1695385(45) 1497547(714) > > 1000 cycles, 4 cores 1387149(456) 2174605(81) 1545716(614) > I notice your standard deviations for 2 and 3 cores are surprisingly high (although still small in relative terms). > > Did you try running the same again? Are the numbers essentially the same or are multiple runs all over the shop? 1. Yes，I test several times，I always get the same results, have little different 2. I think the stddev is small relative to our test results, IMX8MM_EVK_64 also have a big stddev(500 cycles, 3core) from the data. -----邮件原件----- 发件人: devel-request(a)sel4.systems [mailto:devel-request@sel4.systems] 发送时间: 2021年12月7日 11:45 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 127, Issue 5 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: Use TimeServer by Group Components Questions (Kent Mcleod) 2. Re: Incorporating seL4 into your project, risc-v architecture (Kent Mcleod) 3. Re: some performance problem when test 4 cores SMP benchmark of seL4bench project 答复: Devel Digest, Vol 127, Issue 1 (Kent Mcleod) 4. Re: Use TimeServer by Group Components Questions (15852538526(a)139.com) 5. Re: Use TimeServer by Group Components Questions (Kent Mcleod) 6. Re: some performance problem when test 4 cores SMP benchmark of seL4bench project 答复: Devel Digest, Vol 127, Issue 1 (Gernot Heiser) ---------------------------------------------------------------------- Message: 1 Date: Tue, 7 Dec 2021 13:03:00 +1100 From: Kent Mcleod <kent.mcleod72(a)gmail.com> Subject: [seL4] Re: Use TimeServer by Group Components Questions To: 15852538526(a)139.com Cc: devel <devel(a)sel4.systems> Message-ID: <CA+-ozWeJgZm3B902EKBU6dUGxy6wU3Cp92jEUYwRKNFcVS=7DA(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" On Fri, Dec 3, 2021 at 2:51 PM <15852538526(a)139.com> wrote: > > I got an problem when I use TimeServer with Group Components. I wish more than one component in the same Group Components, that can use TimeServer. While the cdl only have one ep for all components in the Group to communicate to TimeServer with an badge value that not equal to zero. And TimeServer must to distinguish requester by the badge, so only one component can receive TimeServer's response. How can I resolve this problem? The TimeServer component cannot be used as part of a Group component. The Group component mechanism isn't designed to transparently work for any component and the Connection types that the TimeServer uses are not compatible with the Group mechanism. > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email > to devel-leave(a)sel4.systems ------------------------------ Message: 2 Date: Tue, 7 Dec 2021 13:14:30 +1100 From: Kent Mcleod <kent.mcleod72(a)gmail.com> Subject: [seL4] Re: Incorporating seL4 into your project, risc-v architecture To: so_s(a)gmx.de Cc: devel <devel(a)sel4.systems> Message-ID: <CA+-ozWeU7Bi-byXhsvo9jnQ_tcn90U7QRa8_hh39p2rVgUcKzA(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" On Fri, Dec 3, 2021 at 8:14 AM <so_s(a)gmx.de> wrote: > > Dear seL4 devs and community. > > I try to create a simple project using the seL4 micro kernel. For setting up my environment I followed this (https://github.com/manu88/SeL4_101) and this (https://docs.sel4.systems/projects/buildsystem/incorporating.html) article. As kernel I'm using the last release of SeL4 (https://github.com/seL4/seL4/releases/tag/12.1.0) I created some kind of user application, like Manu88 did with a simple Hello World C-Program. While building with the delivered init-build.sh script I got a lot of repeating errors like this: > CMake Error at tools/cmake-tool/helpers/simulation.cmake:179 (add_custom_command): > Error evaluating generator expression: > > $<TARGET_PROPERTY:rootserver_image,KERNEL_IMAGE_NAME> > > Target "rootserver_image" not found. > Call Stack (most recent call first): > CMakeLists.txt:22 (GenerateSimulateScript) While going through > Manu88s guide I saw that he also got this errors. But after adding a CMakeList.txt file inside his user code, and declaring it as rootserver inside the CMakeList.txt file (I just copied the contents from here: https://github.com/manu88/SeL4_101/blob/master/projects/Hello/CMakeLists.txt) he got rid of the errors. I still get them and searching through the internet could not find a solution for me. Bellow I added the folder structure of my project. > Project/ > ├── kernel/ > ├── projects/ > │ ├── Hello/ > │ ├── musllibc/ > │ ├── utils_libs/ > │ ├── seL4_libs/ > ├── build/ > ├── tools/ > │ └── cmake-tool/ > │ └── elfloader-tool/ > ├── init-build.sh -> tools/cmake-tool/init-build.sh > ├── CMakeLists.txt > ├── application_settings.cmake -> > tools/cmake-tool/helpers/application_settings.cmake > ├── settings.cmake > > So I cannot tell where the issue lies. Any pointers would be appreciated. If you are using https://github.com/manu88/SeL4_101/blob/master/projects/Hello/CMakeLists.txt inside projects/Hello/ then you need to make sure that the top level CMakeLists inside Project/ is either a symlink to tools/cmake-tool/default-CMakeLists.txt or is similar to https://github.com/manu88/SeL4_101/blob/master/CMakeLists.txt. With this file layout, ../init-build.sh will end up calling the following CMake invocation: `cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DSEL4_CACHE_DIR=../.sel4_cache -C "../settings.cmake" "../"`. What is the contents of your settings.cmake file? > > Kind regards, > Sophia > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email > to devel-leave(a)sel4.systems ------------------------------ Message: 3 Date: Tue, 7 Dec 2021 13:43:48 +1100 From: Kent Mcleod <kent.mcleod72(a)gmail.com> Subject: [seL4] Re: some performance problem when test 4 cores SMP benchmark of seL4bench project 答复: Devel Digest, Vol 127, Issue 1 To: Gernot Heiser <gernot(a)unsw.edu.au> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <CA+-ozWcihN6my4WOyPbpCcfp3=rksYSnnEgZE2kc6c-BV4Kymw(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" On Thu, Dec 2, 2021 at 9:28 PM Gernot Heiser <gernot(a)unsw.edu.au> wrote: > > > > > On 2 Dec 2021, at 16:17, yadong.li <yadong.li(a)horizon.ai> wrote: > > > > First, I got the data of IMX8MM_EVK_64 and TX2 from > > https://github.com/seL4/sel4bench/actions/runs/1469475721#artifacts, > > the sel4bench-results-imx8mm_evk file and sel4bench-results-tx2 file, unpack the file out, I find xxxx_SMP_64.json Secondly, the test is the smp benchmark form sel4bench-manifest project, the source file is sel4bench/apps/smp/src/main.c The test scenario look like below: > > A pair thread of ping-pong on the same core, the ping thread will > > wait for "ipc_normal_delay" time then send 0 len ipc message to pong > > thread, then return. I think the 500 cycles mean how long > > ipc_normal_delay will really delay > > > The above scenario will test on one core, or mutil core. If we run 4 cores, every core will have a ping thread and a pong thread run like above description, then record the sum of all cores ping-pong counts. > > ok, but what is the metric reported? [Apologies for not being on top > of the details of our benchmarking setups.] Looking at the sel4bench smp benchmark implementation, the metric is the total number of "operations" in a single second. An operation is a round trip intra address space seL4_Call + seL4_ReplyRecv between 2 threads on the same core with each thread delaying for the cycle count before performing the next operation. After 1 second of all cores performing these operations continuously and maintaining a core-local (on a separate cache line) count, the total number of operations is added together and reported as the final number. So you would expect that the reported metric would scale following Amdahl's law based on the proportion of an operation that is serialized inside the kernel lock which would potentially vary across platforms. > > It cannot simply be throughput, else the doubled delay should be reflected in a significantly reduced throughput, but it has almost no effect. > > > I think this experiment is used to illustrate in multi core, our seL4 kernel big lock will not affect mutli-core performance, am I right ? > > Not quite. As there’s only one big lock, only one core can execute the kernel at any time. If one core is in the IPC while another core is trying to IPC, even though both IPCs are core-local, the second will have to wait until the first gets out of the lock. > > As the delay is higher than the syscall latency, you’d expect perfect scalability from one core to two (with the lock essentially synchronising the threads). For 3 or 4 cores the combined latency of two IPCs is larger than the 500cy delay and you expect lock contention, resulting in reduced scaling, while it should still scale almost perfectly with the 1000cy delay. This is exactly what you see for the i.MX8 and the TX2. > > > Addition： > > Our seL4_Call performance is same with other platform > > XXXX IMX8MM_EVK_64 TX2_64 > > seL4_Call 367(0) 378(2) 492(16) client->server, same vspace, ipc_len is 0 > > seL4_ReplyRecv 396(0) 402(2) 513(16) server->client, same vspace, ipc_len is 0 > > OK, so baseline performance is good. But are these measured on a single-core or SMP kernel (i.e. is locking included)? > > > My test results below: > > ARM platform > > Test item XXX IMX8MM_EVK_64 TX2 > > mean(Stddev) > > 500 cycles, 1 core 636545(46) 625605(29) 598142(365) > > 500 cycles, 2 cores 897900(2327) 1154209(44) 994298(94) > > 500 cycles, 3 cores 1301679(2036) 1726043(65) 1497740(127) > > 500 cycles, 4 cores 1387678(549) 2172109(12674) 1545872(109) > > 1000 cycles, 1 core 636529(42) 625599(22) 597627(161) > > 1000 cycles, 2 cores 899212(3384) 1134110(34) 994437(541) > > 1000 cycles, 3 cores 1297322(5028) 1695385(45) 1497547(714) > > 1000 cycles, 4 cores 1387149(456) 2174605(81) 1545716(614) > > I notice your standard deviations for 2 and 3 cores are surprisingly high (although still small in relative terms). > > Did you try running the same again? Are the numbers essentially the same or are multiple runs all over the shop? > > There are some issues with our benchmarking methodology. Fixing up sel4bench is one of the projects I’d like to do if I got a student for it, or maybe someone from the community would want to help? > > But just from looking at the data I’m not sure that’s the issue here. > > Gernot > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email > to devel-leave(a)sel4.systems ------------------------------ Message: 4 Date: Tue, 07 Dec 2021 03:06:38 -0000 From: 15852538526(a)139.com Subject: [seL4] Re: Use TimeServer by Group Components Questions To: devel(a)sel4.systems Message-ID: <163884639883.1070957.2394639262660252936(a)mattermost.seL4.systems> Content-Type: text/plain; charset="utf-8" Thank you very much for answering my question. I still have a doubt about the TimeServer. I can manually modify the cdl file and then I get the the expected source file(capdl_spec.c) from using capdl-parse. I also need to change the return value of timeserver <IF>_notification API. I have try and I can run the program as I expected. Is there any way to create adapted cdl file automatic by modifying the ADL parse project? I am looking forward to getting your answer again. Thank you very much. my ADL file: import <std_connector.camkes>; import <global-connectors.camkes>; import <TimeServer/TimeServer.camkes>; component Client { control; uses Timer timeout; } assembly { composition { group grp { component Client c1; component Client c2; } component TimeServer time_server; connection seL4TimeServer ts1( from grp.c1.timeout, to time_server.the_timer); connection seL4TimeServer ts2( from grp.c2.timeout, to time_server.the_timer); } configuration { time_server.timers_per_client = 1; } } ------------------------------ Message: 5 Date: Tue, 7 Dec 2021 14:23:54 +1100 From: Kent Mcleod <kent.mcleod72(a)gmail.com> Subject: [seL4] Re: Use TimeServer by Group Components Questions To: 15852538526(a)139.com Cc: devel <devel(a)sel4.systems> Message-ID: <CA+-ozWestyqAM4wy+x359CLZLf13PzdCRBNFSfPY-3nyo9Y6wA(a)mail.gmail.com> Content-Type: text/plain; charset="UTF-8" On Tue, Dec 7, 2021 at 2:09 PM <15852538526(a)139.com> wrote: > > Thank you very much for answering my question. I still have a doubt about the TimeServer. I can manually modify the cdl file and then I get the the expected source file(capdl_spec.c) from using capdl-parse. I also need to change the return value of timeserver <IF>_notification API. I have try and I can run the program as I expected. Is there any way to create adapted cdl file automatic by modifying the ADL parse project? There isn't a supported way to modify the generated cdl file as CAmkES expects to generate a full system specification. What is your motivation for trying to make the timeserver a group component instead of a separate component? As part of a group component it will still have its own kernel objects for its threads, code, data and heap memories so you still have the costs of isolation but without the benefits because it still shares the virtual address space and capability space with other components in the same group. > I am looking forward to getting your answer again. Thank you very much. > > my ADL file: > import <std_connector.camkes>; > import <global-connectors.camkes>; > import <TimeServer/TimeServer.camkes>; > > component Client { > control; > uses Timer timeout; > } > > assembly { > composition { > group grp { > component Client c1; > component Client c2; > } > component TimeServer time_server; > > connection seL4TimeServer ts1( > from grp.c1.timeout, to time_server.the_timer); > connection seL4TimeServer ts2( > from grp.c2.timeout, to time_server.the_timer); > } > > configuration { > time_server.timers_per_client = 1; > } > } > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email > to devel-leave(a)sel4.systems ------------------------------ Message: 6 Date: Tue, 7 Dec 2021 03:45:09 +0000 From: Gernot Heiser <gernot(a)unsw.edu.au> Subject: [seL4] Re: some performance problem when test 4 cores SMP benchmark of seL4bench project 答复: Devel Digest, Vol 127, Issue 1 To: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <17FC6BC4-3407-44AE-B7AA-4623EFF76988(a)unsw.edu.au> Content-Type: text/plain; charset="utf-8" On 7 Dec 2021, at 13:43, Kent Mcleod <kent.mcleod72(a)gmail.com> wrote: > > Looking at the sel4bench smp benchmark implementation, the metric is > the total number of "operations" in a single second. An operation is > a round trip intra address space seL4_Call + seL4_ReplyRecv between 2 > threads on the same core with each thread delaying for the cycle count > before performing the next operation. After 1 second of all cores > performing these operations continuously and maintaining a core-local > (on a separate cache line) count, the total number of operations is > added together and reported as the final number. So you would expect > that the reported metric would scale following Amdahl's law based on > the proportion of an operation that is serialized inside the kernel > lock which would potentially vary across platforms. Thanks for the explanation, Kent. Observations: 1) The metric is essentially independent of the delay. Looking at the single-core figures for the i/MX8, I get 1598.5 ns in both cases, the difference being 15ps. Doesn’t make sense to me. 2) Assuming this processor runs at the 1.8GHz it seems speced for, this corresponds to 2877 cycles, which is huge, even if the 1000cy delay is subtracted! 3) As I said before, intra-AS IPC is a meaningless metric we should never use (but that’s incidental to the particular thing we want to measure here). 4) Having to do these calculations to understand the numbers is a sure indication that the results are presented in an unsuitable form. I can’t see how these figures make sense. Gernot ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems ------------------------------ End of Devel Digest, Vol 127, Issue 5 *************************************

1 0

CfP: Microkernel and Component-based OS Devroom at FOSDEM 2022
by Alexander Boettcher 07 Dec '21

07 Dec '21

Hello seL4 community, FOSDEM 2022 will be an online event (again) with the traditional Microkernel devroom as part of it. Thanks to Martin Decky & my colleague Sebastian Sumpf for engagement! The original Call for Papers follows. Best regards, Alexander. -- Alexander Boettcher Genode Labs https://www.genodians.org - https://www.genode.org ------------------------------------------------------------------------------------------------------ Microkernel and Component-based OS Devroom at FOSDEM 2022 CALL FOR PARTICIPATION On-line version of this CfP: http://fosdem.microkernel.info/ The developers and users of several free and open source microkernel-based and component-based operating systems will meet on-line as part of FOSDEM 2022 [1] and will share a developer room. The devroom is currently looking for content in the form of talks and activities related to the area of microkernel-based, unikernel-based, component-based operating systems and similar topics. The devroom has been preliminarily scheduled to Saturday February 5th 2022. The devroom will take place during European day hours. Possible topics of the devroom include, but are not limited to: * introduction of a specific OS or framework * design of subsystems and the general architecture of an OS * languages, tools and toolchains used * enabling support for hardware (architectures, device drivers) and programming languages * development processes, debugging * maintenance, testing and release engineering * safety, security and robustness * trends and challenges * research and open questions * community and governance * use cases, experiences and status updates * best practices and lessons learned * demos This is a call for your participation. We kindly ask you to submit your proposals no later than on December 28th 2021. Please use the Pentabarf web site [2] to submit your proposals. If you already have a user account in Pentabarf, please do not create a new one. Addtionally, make sure to select the Microkernel and Component-based OS Devroom as the track when submitting your talk and include at least the following information in your proposal: * title of your talk * your full name * short abstract of your talk (one or two paragraphs) * duration of your talk (at least 20 minutes and no longer than 50 minutes) * your short bio * your photo The talks will be pre-recorded in advance in January and streamed automatically during the event. This means that you will need to complete and submit your talk recording by January 15th 2022. However, each speaker should be also present on-line just after the streaming of their talk for a live Q&A. You can specify your prefered time slot of your talk. The communication language of the devroom is English. The official devroom schedule (along with the accepted talks) will be announced on December 31st 2021 on the devroom's mailing list [3] and the speakers will be notified via e-mail. The schedule will also be published on the FOSDEM web site. For any comments, questions and suggestions (e.g. suggestions for a different type of event during the devroom), please do not hesitate to use the devroom's mailing list [3]. About the Devroom Since the first Microkernel OS Devroom at FOSDEM 2012 [4], this devroom has been a part of each following FOSDEM (with slight variations of the name). The focus gradually widened to include component-based, unikernel-based and other operating systems. By now, it has become a somewhat institutionalized tradition for the open source operating systems community and it is one of the few places where microkernel enthusiasts and people with different views on how operating systems should work meet regularly. To this date, over a dozen projects have participated in one way or another. Many of the projects face similar challenges but come up with partially different solutions. Therefore, the goal of the devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. Extraordinary Circumstances in 2022 (Again) Due to the extraordinary mode of organization of FOSDEM 2022 (being an on-line event again), the devroom talks will be required to be pre-recorded in January and streamed during the event (with a live Q&A). The talk videos will be published under Creative Commons license by FOSDEM. By submitting a recorded talk, the speaker agrees to have it made available publicly indefinitively. For organizational purposes, we also need contact information of the speakers of accepted talks. Please check the official CfP page [5] of the devroom regularly. We will keep updating it as technical guidelines will be set by the FOSDEM organizers. Microkernel Dinner Sadly, it will not be possible to arrange our traditional microkernel dinner and other in-person social gatherings in Brussels this time again. However, we plan a closing event of the devroom as a loose approximation of the microkernel dinner. The details will be announced later. We encourage the on-line participats to bring their own food and beverages. About FOSDEM FOSDEM [6] is a two-day event organized by volunteers to promote the widespread use of free and open source software. FOSDEM is widely recognized as one of the best such conferences worldwide. FOSDEM covers a wide spectrum of free and open source software and hardware projects and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present latest directions, lightning talks, news and proposals. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, certification exams and project stands. In recent years, FOSDEM has been hosting more than 5000 developers annually at the ULB Solbosch campus. Due to the circumstances, FOSDEM 2022 will be organized as an on-line event. The participation in FOSDEM is totally free, although the organizers gratefully accept donations and sponsorship. No registration is necessary, but attendees are expected to follow the FOSDEM's code of conduct [7]. Important Dates Recap * 2021-12-28: Deadline for talk proposal submission * 2021-12-31: Schedule published and speakers notified of acceptance * 2022-01-15: Deadline for talk pre-recoding submission * 2022-02-05: Devroom taking place on-line Contact In case of any comments, questions and suggestions, please do not hesitate to contact the devroom organizers via the devroom's mailing list [3]. The primary organizers of the devroom in 2022 are: * Sebastian Sumpf * Martin Decky Links [1] https://fosdem.org/2022/ [2] https://penta.fosdem.org/submission/FOSDEM22/ [3] https://lists.fosdem.org/listinfo/microkernel-devroom [4] https://archive.fosdem.org/2012/schedule/track/microkernel_os_devroom.html [5] http://fosdem.microkernel.info/ [6] https://fosdem.org/ [7] https://fosdem.org/2022/practical/conduct/

1 0

Use TimeServer by Group Components Questions
by 15852538526＠139.com 07 Dec '21

07 Dec '21

I got an problem when I use TimeServer with Group Components. I wish more than one component in the same Group Components, that can use TimeServer. While the cdl only have one ep for all components in the Group to communicate to TimeServer with an badge value that not equal to zero. And TimeServer must to distinguish requester by the badge, so only one component can receive TimeServer's response. How can I resolve this problem?

2 4

Re: some performance problem when test 4 cores SMP benchmark of seL4bench project 答复: Devel Digest, Vol 127, Issue 1
by yadong.li 07 Dec '21

07 Dec '21

Hi professor Heiser： To understand what’s going on I’d need to know what these numbers are: - what is being measured, and what’s the 500/100cy parameter? - which web site are the “official” numbers from, they aren’t at https://sel4.systems/About/Performance/ First, I got the data of IMX8MM_EVK_64 and TX2 from https://github.com/seL4/sel4bench/actions/runs/1469475721#artifacts, the sel4bench-results-imx8mm_evk file and sel4bench-results-tx2 file, unpack the file out, I find xxxx_SMP_64.json Secondly, the test is the smp benchmark form sel4bench-manifest project, the source file is sel4bench/apps/smp/src/main.c The test scenario look like below: A pair thread of ping-pong on the same core, the ping thread will wait for "ipc_normal_delay" time then send 0 len ipc message to pong thread, then return. I think the 500 cycles mean how long ipc_normal_delay will really delay The above scenario will test on one core, or mutil core. If we run 4 cores, every core will have a ping thread and a pong thread run like above description, then record the sum of all cores ping-pong counts. I think this experiment is used to illustrate in multi core, our seL4 kernel big lock will not affect mutli-core performance, am I right ? Addition： Our seL4_Call performance is same with other platform XXXX IMX8MM_EVK_64 TX2_64 seL4_Call 367(0) 378(2) 492(16) client->server, same vspace, ipc_len is 0 seL4_ReplyRecv 396(0) 402(2) 513(16) server->client, same vspace, ipc_len is 0 Thank you for your help -----邮件原件----- 发件人: devel-request(a)sel4.systems [mailto:devel-request@sel4.systems] 发送时间: 2021年12月2日 9:00 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 127, Issue 1 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Subscription (Xin Wang) 2. some performance problem when test 4 cores SMP benchmark of seL4bench project (yadong.li) 3. Re: some performance problem when test 4 cores SMP benchmark of seL4bench project (Gernot Heiser) ---------------------------------------------------------------------- Message: 1 Date: Wed, 1 Dec 2021 06:52:45 +0000 From: Xin Wang <xin.wang(a)bst.ai> Subject: [seL4] Subscription To: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <BL0PR18MB2146092BCA3DBADBC26984ADF7689(a)BL0PR18MB2146.nam prd18.prod.outlook.com> Content-Type: text/plain; charset="gb2312" Hi sirs, Subscription Thanks, 从 Windows 版邮件<https://go.microsoft.com/fwlink/?LinkId=550986>发送 ------------------------------ Message: 2 Date: Wed, 1 Dec 2021 14:58:17 +0000 From: yadong.li <yadong.li(a)horizon.ai> Subject: [seL4] some performance problem when test 4 cores SMP benchmark of seL4bench project To: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <2ae9929de02e481796d3d697182842c3(a)horizon.ai> Content-Type: text/plain; charset="gb2312" Hi, Now, I meet some performance problem when test 4 cores SMP benchmark of seL4bench on our platform. Out platform is XXX, But I get the test data of IMX8MM_EVK_64 and TX2 platform from seL4 website, I think they are official statistics. My test results below: ARM platform Test item XXX IMX8MM_EVK_64 TX2 mean(Stddev) 500 cycles, 1 core 636545(46) 625605(29) 598142(365) 500 cycles, 2 cores 897900(2327) 1154209(44) 994298(94) 500 cycles, 3 cores 1301679(2036) 1726043(65) 1497740(127) 500 cycles, 4 cores 1387678(549) 2172109(12674) 1545872(109) 1000 cycles, 1 core 636529(42) 625599(22) 597627(161) 1000 cycles, 2 cores 899212(3384) 1134110(34) 994437(541) 1000 cycles, 3 cores 1297322(5028) 1695385(45) 1497547(714) 1000 cycles, 4 cores 1387149(456) 2174605(81) 1545716(614) From these compare data: 1. When test smp bench on one core, the performance of several platform is similar 2. When test smp bench on muti core, the result of IMX8MM_EVK_64 is beauty, the result of 4 cores is 3.47 times as good as 1 core, I think it’s good 3. But the platform of TX2 has some different performance, the result of 2 cores is 1.66 times as good as 1 core, I still think is good, But the result of 3 cores almost have the same ping-pong count with 4 cores, why add one core, the count result not add as our expected ? 4. The performance of our platform is badly, on our platform, the result of 3 cores almost also have the same ping-pong count with 4 cores, and our count result of 4 cores just 2 times as good as one core, I think it is very bad 5. I want to know what are the possible causes of the badly performance about our platform XXX and TX2 ? ------------------------------ Message: 3 Date: Wed, 1 Dec 2021 21:09:41 +0000 From: Gernot Heiser <gernot(a)unsw.edu.au> Subject: [seL4] Re: some performance problem when test 4 cores SMP benchmark of seL4bench project To: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <720E9728-1079-4455-BB0E-34A7C5CE88F4(a)unsw.edu.au> Content-Type: text/plain; charset="utf-8" Hi Yandong, To understand what’s going on I’d need to know what these numbers are: - what is being measured, and what’s the 500/100cy parameter? - which web site are the “official” numbers from, they aren’t at https://sel4.systems/About/Performance/ Gernot On 2 Dec 2021, at 01:58, yadong.li<http://yadong.li/> <yadong.li(a)horizon.ai<mailto:yadong.li@horizon.ai>> wrote: Hi, Now, I meet some performance problem when test 4 cores SMP benchmark of seL4bench on our platform. Out platform is XXX, But I get the test data of IMX8MM_EVK_64 and TX2 platform from seL4 website, I think they are official statistics. My test results below: ARM platform Test item XXX IMX8MM_EVK_64 TX2 mean(Stddev) 500 cycles, 1 core 636545(46) 625605(29) 598142(365) 500 cycles, 2 cores 897900(2327) 1154209(44) 994298(94) 500 cycles, 3 cores 1301679(2036) 1726043(65) 1497740(127) 500 cycles, 4 cores 1387678(549) 2172109(12674) 1545872(109) 1000 cycles, 1 core 636529(42) 625599(22) 597627(161) 1000 cycles, 2 cores 899212(3384) 1134110(34) 994437(541) 1000 cycles, 3 cores 1297322(5028) 1695385(45) 1497547(714) 1000 cycles, 4 cores 1387149(456) 2174605(81) 1545716(614) From these compare data: 1. When test smp bench on one core, the performance of several platform is similar 2. When test smp bench on muti core, the result of IMX8MM_EVK_64 is beauty, the result of 4 cores is 3.47 times as good as 1 core, I think it’s good 3. But the platform of TX2 has some different performance, the result of 2 cores is 1.66 times as good as 1 core, I still think is good, But the result of 3 cores almost have the same ping-pong count with 4 cores, why add one core, the count result not add as our expected ? 4. The performance of our platform is badly, on our platform, the result of 3 cores almost also have the same ping-pong count with 4 cores, and our count result of 4 cores just 2 times as good as one core, I think it is very bad 5. I want to know what are the possible causes of the badly performance about our platform XXX and TX2 ? _______________________________________________ Devel mailing list -- devel(a)sel4.systems<mailto:devel@sel4.systems> To unsubscribe send an email to devel-leave(a)sel4.systems<mailto:devel-leave@sel4.systems> ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems ------------------------------ End of Devel Digest, Vol 127, Issue 1 *************************************

3 3

some performance problem when test 4 cores SMP benchmark of seL4bench project
by yadong.li 02 Dec '21

02 Dec '21

Hi, Now, I meet some performance problem when test 4 cores SMP benchmark of seL4bench on our platform. Out platform is XXX, But I get the test data of IMX8MM_EVK_64 and TX2 platform from seL4 website, I think they are official statistics. My test results below: ARM platform Test item XXX IMX8MM_EVK_64 TX2 mean(Stddev) 500 cycles, 1 core 636545(46) 625605(29) 598142(365) 500 cycles, 2 cores 897900(2327) 1154209(44) 994298(94) 500 cycles, 3 cores 1301679(2036) 1726043(65) 1497740(127) 500 cycles, 4 cores 1387678(549) 2172109(12674) 1545872(109) 1000 cycles, 1 core 636529(42) 625599(22) 597627(161) 1000 cycles, 2 cores 899212(3384) 1134110(34) 994437(541) 1000 cycles, 3 cores 1297322(5028) 1695385(45) 1497547(714) 1000 cycles, 4 cores 1387149(456) 2174605(81) 1545716(614) From these compare data: 1. When test smp bench on one core, the performance of several platform is similar 2. When test smp bench on muti core, the result of IMX8MM_EVK_64 is beauty, the result of 4 cores is 3.47 times as good as 1 core, I think it’s good 3. But the platform of TX2 has some different performance, the result of 2 cores is 1.66 times as good as 1 core, I still think is good, But the result of 3 cores almost have the same ping-pong count with 4 cores, why add one core, the count result not add as our expected ? 4. The performance of our platform is badly, on our platform, the result of 3 cores almost also have the same ping-pong count with 4 cores, and our count result of 4 cores just 2 times as good as one core, I think it is very bad 5. I want to know what are the possible causes of the badly performance about our platform XXX and TX2 ?

2 1

Subscription
by Xin Wang 01 Dec '21

01 Dec '21

Hi sirs, Subscription Thanks, 从 Windows 版邮件<https://go.microsoft.com/fwlink/?LinkId=550986>发送

1 0

VM Kernel Modules
by Michael Neises 20 Nov '21

20 Nov '21

Hello all, I recently spent a lot of time getting the camkes-vm-linux tutorial to work, because it is the only example I could find of compiling a kernel module for the linux vm as a part of the camkes build process. Unfortunately, the kernel module doesn't seem to work. For more information, see the previous email chain as well as https://github.com/NeisesResearch/vm_measure/wiki/Building-the-camkes_vm_li… . In lieu of doing things the right way, I believe I could compile a kernel module for the linux kernel that is provided as part of the camkes build system. I believe this is how the introspect-app accomplishes its work. However, I need to have the exact kernel and exact configuration in order to compile the kernel module correctly. Can anyone point me to the correct kernel version and configuration, so that I can target the provided linux kernel for module compilation? Or if there's a better way to get a kernel module in there, please let me know. Cheers, Michael Neises

4 5

the security whiltelist of smc call 答复: Devel Digest, Vol 124, Issue 1
by yadong.li 19 Nov '21

19 Nov '21

Hi: In our ARMv8 platform，we access secure world not only from the VM guest OS， but also form native compont like config clk register In ARMv8 platform, SMC instructions are not allowed from EL0. So in camkes-vm project, I create a new smc capability and a new syscall as a temporary solution, like below: "LIBSEL4_INLINE seL4_ARM_SMC_CallFunc_t seL4_ARM_SMC_CallFunc(seL4_ARM_SMC _service, seL4_Word function_id, seL4_Word arg0, seL4_Word arg1, seL4_Word arg2)" But I did not pay much attention to security, it is just meet our current work. I didnot really understand the essence of kernel whitelist mentioned by "https://sel4.atlassian.net/browse/RFC-9"? I have some question below, I feel the smc cap should like schedcontrol cap belong every core. 1. what is the whiltelist describe ? sip command smc function id? 2. how are the members of whilelist represented in the kernel , check the invLabel of syscall in kernel if we provide one smc cap not every function id? or just check the range of function id ? 3. Does each TCB have its own whitelist or does the entire system have a whitelist? thank you very much. -----邮件原件----- 发件人: devel-request(a)sel4.systems [mailto:devel-request@sel4.systems] 发送时间: 2021年11月10日 9:00 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 124, Issue 1 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. RFC-9: new capability for seL4 SMC Forwarding on Arm (Gerwin Klein) ---------------------------------------------------------------------- Message: 1 Date: Tue, 9 Nov 2021 21:52:58 +0000 From: Gerwin Klein <kleing(a)unsw.edu.au> Subject: [seL4] RFC-9: new capability for seL4 SMC Forwarding on Arm To: devel <devel(a)sel4.systems> Message-ID: <613858AC-3DB1-4D7C-A892-9ABDB5B31D58(a)unsw.edu.au> Content-Type: text/plain; charset="utf-8" I’d like to solicit discussion on the new RFC on forwarding Secure Monitor Calls on Arm: https://sel4.atlassian.net/browse/RFC-9 Relevant Arm documentation (SMC calling conventions): https://developer.arm.com/documentation/den0028/latest?_ga=2.116565828.3903… Any opinions, concerns, alternative designs? Cheers, Gerwin ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems ------------------------------ End of Devel Digest, Vol 124, Issue 1 *************************************

1 0

Got it, Thank you for your help. 答复: Devel Digest, Vol 125, Issue 2
by yadong.li 18 Nov '21

18 Nov '21

-----邮件原件----- 发件人: devel-request(a)sel4.systems [mailto:devel-request@sel4.systems] 发送时间: 2021年11月18日 5:56 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 125, Issue 2 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: some question about seL4 performance (Gerwin Klein) 2. Re: some question about seL4 performance (Gernot Heiser) 3. Re: some question about seL4 performance (Gerwin Klein) ---------------------------------------------------------------------- Message: 1 Date: Wed, 17 Nov 2021 21:24:57 +0000 From: Gerwin Klein <kleing(a)unsw.edu.au> Subject: [seL4] Re: some question about seL4 performance To: yadong.li <yadong.li(a)horizon.ai> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <CA210292-C334-42C1-9FB4-48CAFDE8CCC6(a)unsw.edu.au> Content-Type: text/plain; charset="utf-8" > On 18 Nov 2021, at 02:06, yadong.li <yadong.li(a)horizon.ai> wrote: > > Hi： > I learn the sel4 performance form > https://sel4.systems/About/Performance/ > I focus on the ARMv8 platform, from the website, the parameters are as follows: > ISA Mode Core/SoC/Board Clock IRQ Invoke IPC call IPC reply > "Armv8a 64 A57/Tx1/Jetson 1.9 GHz 863 (18) 396(15) 397(4)" > > I want to know what is the length of IPC for the record provided on the web page , when test IPC call and reply? 0 or 10? The page reports the 0-length numbers. The idea is that IPC should fit into registers, the 10 case is the one that make it spill into memory deliberately. That number is good to know for development, but should not be the main performance characteristic. Cheers, Gerwin ------------------------------ Message: 2 Date: Wed, 17 Nov 2021 21:36:39 +0000 From: Gernot Heiser <gernot(a)unsw.edu.au> Subject: [seL4] Re: some question about seL4 performance To: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <9885F4AB-61C0-46CD-B239-595E38482673(a)unsw.edu.au> Content-Type: text/plain; charset="utf-8" On 18 Nov 2021, at 08:24, Gerwin Klein <kleing(a)unsw.edu.au> wrote: > > The page reports the 0-length numbers. The idea is that IPC should fit into registers, the 10 case is the one that make it spill into memory deliberately. That number is good to know for development, but should not be the main performance characteristic. Note that whether data is transferred solely in registers or using a memory buffer does not make a big difference on contemporary hardware. However, our present implementation reverts to the slow path as soon as the message size overflows the physical message registers, which will make the PIC much slower. This is something that could be fixed by widening the fastpath conditions without much complications. However, we haven’t yet come across an important use case where this matters, so there isn’t much motivation for investing time in it. Gernot ------------------------------ Message: 3 Date: Wed, 17 Nov 2021 21:56:06 +0000 From: Gerwin Klein <kleing(a)unsw.edu.au> Subject: [seL4] Re: some question about seL4 performance To: Gernot Heiser <gernot(a)unsw.edu.au> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Message-ID: <FFD95815-9F62-4A90-A3D0-59671152494D(a)unsw.edu.au> Content-Type: text/plain; charset="us-ascii" On 18 Nov 2021, at 08:36, Gernot Heiser <gernot(a)unsw.edu.au<mailto:gernot@unsw.edu.au>> wrote: On 18 Nov 2021, at 08:24, Gerwin Klein <kleing(a)unsw.edu.au<mailto:kleing@unsw.edu.au>> wrote: The page reports the 0-length numbers. The idea is that IPC should fit into registers, the 10 case is the one that make it spill into memory deliberately. That number is good to know for development, but should not be the main performance characteristic. Note that whether data is transferred solely in registers or using a memory buffer does not make a big difference on contemporary hardware. However, our present implementation reverts to the slow path as soon as the message size overflows the physical message registers, which will make the PIC much slower. Yes I should have mentioned that. If you look at the raw numbers for x86, eg. at https://github.com/seL4/sel4bench/actions/runs/1469475721#artifacts, fast path/no fast path is almost equal for length 10. You get a tiny bit better performance for length 10 when the fast path is switched off completely, because it doesn't first have to test whether to take the fast path or not. Cheers, Gerwin ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems ------------------------------ End of Devel Digest, Vol 125, Issue 2 *************************************

1 0

some question about seL4 performance
by yadong.li 18 Nov '21

18 Nov '21

Hi： I learn the sel4 performance form https://sel4.systems/About/Performance/ I focus on the ARMv8 platform, from the website, the parameters are as follows: ISA Mode Core/SoC/Board Clock IRQ Invoke IPC call IPC reply "Armv8a 64 A57/Tx1/Jetson 1.9 GHz 863 (18) 396(15) 397(4)" I want to know what is the length of IPC for the record provided on the web page , when test IPC call and reply? 0 or 10? thank you very much

3 3

Crash problem, CAmkES-VM app with Ethernet passthrough
by hamed_ganji＠aut.ac.ir 18 Nov '21

18 Nov '21

Hello everyone, I attempt to make a simple CAmkES-VM app to load a Linux VM with Ethernet passthrough. After running, Linux kernel crashes while initializing the device (e1000). Can anyone guide me how to fix the problem, please. Thanks in advance. The used qemu command: ------------------------------------------------------------ $ qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu Nehalem,+vme,+pdpe1gb,+xsave,+xsaveopt,+xsavec,+fsgsbase,+pcid,+invpcid,enforce,+vmx -nographic -serial mon:stdio -m size=4G -enable-kvm -device intel-iommu,intremap=off -net nic,model=e1000 -net tap,script=no,ifname=tap0 -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 ------------------------------------------------------------ Here is my CAmkES app definition: ------------------------------------------------------------ import <VM/vm.camkes>; #include <configurations/vm.h> #define VM_GUEST_CMDLINE "earlyprintk=ttyS0,115200 console=ttyS0,115200 i8042.nokbd=y i8042.nomux=y \ i8042.noaux=y io_delay=udelay noisapnp pci=nomsi debug root=/dev/mem" // nosmap acpi=off" component Init0 { VM_INIT_DEF() } assembly { composition { VM_COMPOSITION_DEF() VM_PER_VM_COMP_DEF(0) } configuration { VM_CONFIGURATION_DEF() VM_PER_VM_CONFIG_DEF(0) vm0.simple_untyped25_pool = 75; vm0.cnode_size_bits = 24; vm0.heap_size = 0x2000000; vm0.guest_ram_mb = 2048; vm0.kernel_cmdline = VM_GUEST_CMDLINE; vm0.kernel_image = "bzimage"; vm0.kernel_relocs = "bzimage"; vm0.initrd_image = "rootfs.cpio"; vm0.iospace_domain = 0x0f; vm0.pci_devices_iospace = 1; vm0.vm_ioports = [ {"start":0xc000, "end":0xc040, "pci_device":2, "name":"eth"}, ]; vm0.pci_devices = [ { "name":"eth", "bus":0, "dev":2, "fun":0, "irq":"eth_irq", "memory":[ {"paddr":0xfeb00000, "size":0x80000, "page_bits":12}, {"paddr":0xfeb80000, "size":0x20000, "page_bits":12} ] }, ]; vm0.vm_irqs = [ {"name":"eth_irq", "source":1, "level_trig":1, "active_low":1, "dest":11}, ]; } } ------------------------------------------------------------ The output lines: ------------------------------------------------------------ Booting from ROM..Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0xa1f000 end=0x1edbe18 size=0x14bce18 name='images/capdl-loader-image-x86_64-pc99' Parsing GRUB physical memory map Physical Memory Region from 0 size 9fc00 type 1 Physical Memory Region from 9fc00 size 400 type 2 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size 7fedf000 type 1 Adding physical memory region 0x100000-0x7ffdf000 Physical Memory Region from 7ffdf000 size 21000 type 2 Physical Memory Region from b0000000 size 10000000 type 2 Physical Memory Region from fed1c000 size 4000 type 2 Physical Memory Region from feffc000 size 4000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 Physical Memory Region from 100000000 size 80000000 type 1 Adding physical memory region 0x100000000-0x180000000 Multiboot gave us no video information ACPI: RSDP paddr=0xf5ac0 ACPI: RSDP vaddr=0xf5ac0 ACPI: RSDT paddr=0x7ffe2140 ACPI: RSDT vaddr=0x7ffe2140 Kernel loaded to: start=0x100000 end=0xa1e000 size=0x91e000 entry=0x1012db ACPI: RSDT paddr=0x7ffe2140 ACPI: RSDT vaddr=0x7ffe2140 ACPI: FADT paddr=0x7ffe1f18 ACPI: FADT vaddr=0x7ffe1f18 ACPI: FADT flags=0x84a5 ACPI: DMAR paddr=0x7ffe20f8 ACPI: DMAR vaddr=0x7ffe20f8 ACPI: IOMMU host address width: 39 ACPI: 1 IOMMUs detected ACPI: MADT paddr=0x7ffe200c ACPI: MADT vaddr=0x7ffe200c ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd ACPI: 1 CPU(s) detected ELF-loading userland images from boot modules: size=0x294b000 v_entry=0x408619 v_start=0x400000 v_end=0x2d4b000 p_start=0x1edc000 p_end=0x4827000 Moving loaded userland images to final location: from=0x1edc000 to=0xa1e000 size=0x294b000 Starting node #0 with APIC ID 0 Mapping kernel window is done IOMMU 0x0: 16-bit domain IDs supported IOMMU: Using 3 page-table levels (max. supported: 3) IOMMU: Create VTD context table for PCI bus 0x0 (pptr=0xffffff817e01d000) IOMMU: Create VTD context table for PCI bus 0x1 (pptr=0xffffff817e01e000) IOMMU: Create VTD context table for PCI bus 0x2 (pptr=0xffffff817e01f000) IOMMU: Create VTD context table for PCI bus 0x3 (pptr=0xffffff817e020000) IOMMU: Create VTD context table for PCI bus 0x4 (pptr=0xffffff817e021000) IOMMU: Create VTD context table for PCI bus 0x5 (pptr=0xffffff817e022000) IOMMU: Create VTD context table for PCI bus 0x6 (pptr=0xffffff817e023000) IOMMU: Create VTD context table for PCI bus 0x7 (pptr=0xffffff817e024000) IOMMU: Create VTD context table for PCI bus 0x8 (pptr=0xffffff817e025000) IOMMU: Create VTD context table for PCI bus 0x9 (pptr=0xffffff817e026000) IOMMU: Create VTD context table for PCI bus 0xa (pptr=0xffffff817e027000) IOMMU: Create VTD context table for PCI bus 0xb (pptr=0xffffff817e028000) IOMMU: Create VTD context table for PCI bus 0xc (pptr=0xffffff817e029000) IOMMU: Create VTD context table for PCI bus 0xd (pptr=0xffffff817e02a000) IOMMU: Create VTD context table for PCI bus 0xe (pptr=0xffffff817e02b000) IOMMU: Create VTD context table for PCI bus 0xf (pptr=0xffffff817e02c000) IOMMU: Create VTD context table for PCI bus 0x10 (pptr=0xffffff817e02d000) IOMMU: Create VTD context table for PCI bus 0x11 (pptr=0xffffff817e02e000) IOMMU: Create VTD context table for PCI bus 0x12 (pptr=0xffffff817e02f000) IOMMU: Create VTD context table for PCI bus 0x13 (pptr=0xffffff817e030000) IOMMU: Create VTD context table for PCI bus 0x14 (pptr=0xffffff817e031000) IOMMU: Create VTD context table for PCI bus 0x15 (pptr=0xffffff817e032000) IOMMU: Create VTD context table for PCI bus 0x16 (pptr=0xffffff817e033000) IOMMU: Create VTD context table for PCI bus 0x17 (pptr=0xffffff817e034000) IOMMU: Create VTD context table for PCI bus 0x18 (pptr=0xffffff817e035000) IOMMU: Create VTD context table for PCI bus 0x19 (pptr=0xffffff817e036000) IOMMU: Create VTD context table for PCI bus 0x1a (pptr=0xffffff817e037000) IOMMU: Create VTD context table for PCI bus 0x1b (pptr=0xffffff817e038000) IOMMU: Create VTD context table for PCI bus 0x1c (pptr=0xffffff817e039000) IOMMU: Create VTD context table for PCI bus 0x1d (pptr=0xffffff817e03a000) IOMMU: Create VTD context table for PCI bus 0x1e (pptr=0xffffff817e03b000) IOMMU: Create VTD context table for PCI bus 0x1f (pptr=0xffffff817e03c000) IOMMU: Create VTD context table for PCI bus 0x20 (pptr=0xffffff817e03d000) IOMMU: Create VTD context table for PCI bus 0x21 (pptr=0xffffff817e03e000) IOMMU: Create VTD context table for PCI bus 0x22 (pptr=0xffffff817e03f000) IOMMU: Create VTD context table for PCI bus 0x23 (pptr=0xffffff817e040000) IOMMU: Create VTD context table for PCI bus 0x24 (pptr=0xffffff817e041000) IOMMU: Create VTD context table for PCI bus 0x25 (pptr=0xffffff817e042000) IOMMU: Create VTD context table for PCI bus 0x26 (pptr=0xffffff817e043000) IOMMU: Create VTD context table for PCI bus 0x27 (pptr=0xffffff817e044000) IOMMU: Create VTD context table for PCI bus 0x28 (pptr=0xffffff817e045000) IOMMU: Create VTD context table for PCI bus 0x29 (pptr=0xffffff817e046000) IOMMU: Create VTD context table for PCI bus 0x2a (pptr=0xffffff817e047000) IOMMU: Create VTD context table for PCI bus 0x2b (pptr=0xffffff817e048000) IOMMU: Create VTD context table for PCI bus 0x2c (pptr=0xffffff817e049000) IOMMU: Create VTD context table for PCI bus 0x2d (pptr=0xffffff817e04a000) IOMMU: Create VTD context table for PCI bus 0x2e (pptr=0xffffff817e04b000) IOMMU: Create VTD context table for PCI bus 0x2f (pptr=0xffffff817e04c000) IOMMU: Create VTD context table for PCI bus 0x30 (pptr=0xffffff817e04d000) IOMMU: Create VTD context table for PCI bus 0x31 (pptr=0xffffff817e04e000) IOMMU: Create VTD context table for PCI bus 0x32 (pptr=0xffffff817e04f000) IOMMU: Create VTD context table for PCI bus 0x33 (pptr=0xffffff817e050000) IOMMU: Create VTD context table for PCI bus 0x34 (pptr=0xffffff817e051000) IOMMU: Create VTD context table for PCI bus 0x35 (pptr=0xffffff817e052000) IOMMU: Create VTD context table for PCI bus 0x36 (pptr=0xffffff817e053000) IOMMU: Create VTD context table for PCI bus 0x37 (pptr=0xffffff817e054000) IOMMU: Create VTD context table for PCI bus 0x38 (pptr=0xffffff817e055000) IOMMU: Create VTD context table for PCI bus 0x39 (pptr=0xffffff817e056000) IOMMU: Create VTD context table for PCI bus 0x3a (pptr=0xffffff817e057000) IOMMU: Create VTD context table for PCI bus 0x3b (pptr=0xffffff817e058000) IOMMU: Create VTD context table for PCI bus 0x3c (pptr=0xffffff817e059000) IOMMU: Create VTD context table for PCI bus 0x3d (pptr=0xffffff817e05a000) IOMMU: Create VTD context table for PCI bus 0x3e (pptr=0xffffff817e05b000) IOMMU: Create VTD context table for PCI bus 0x3f (pptr=0xffffff817e05c000) IOMMU: Create VTD context table for PCI bus 0x40 (pptr=0xffffff817e05d000) IOMMU: Create VTD context table for PCI bus 0x41 (pptr=0xffffff817e05e000) IOMMU: Create VTD context table for PCI bus 0x42 (pptr=0xffffff817e05f000) IOMMU: Create VTD context table for PCI bus 0x43 (pptr=0xffffff817e060000) IOMMU: Create VTD context table for PCI bus 0x44 (pptr=0xffffff817e061000) IOMMU: Create VTD context table for PCI bus 0x45 (pptr=0xffffff817e062000) IOMMU: Create VTD context table for PCI bus 0x46 (pptr=0xffffff817e063000) IOMMU: Create VTD context table for PCI bus 0x47 (pptr=0xffffff817e064000) IOMMU: Create VTD context table for PCI bus 0x48 (pptr=0xffffff817e065000) IOMMU: Create VTD context table for PCI bus 0x49 (pptr=0xffffff817e066000) IOMMU: Create VTD context table for PCI bus 0x4a (pptr=0xffffff817e067000) IOMMU: Create VTD context table for PCI bus 0x4b (pptr=0xffffff817e068000) IOMMU: Create VTD context table for PCI bus 0x4c (pptr=0xffffff817e069000) IOMMU: Create VTD context table for PCI bus 0x4d (pptr=0xffffff817e06a000) IOMMU: Create VTD context table for PCI bus 0x4e (pptr=0xffffff817e06b000) IOMMU: Create VTD context table for PCI bus 0x4f (pptr=0xffffff817e06c000) IOMMU: Create VTD context table for PCI bus 0x50 (pptr=0xffffff817e06d000) IOMMU: Create VTD context table for PCI bus 0x51 (pptr=0xffffff817e06e000) IOMMU: Create VTD context table for PCI bus 0x52 (pptr=0xffffff817e06f000) IOMMU: Create VTD context table for PCI bus 0x53 (pptr=0xffffff817e070000) IOMMU: Create VTD context table for PCI bus 0x54 (pptr=0xffffff817e071000) IOMMU: Create VTD context table for PCI bus 0x55 (pptr=0xffffff817e072000) IOMMU: Create VTD context table for PCI bus 0x56 (pptr=0xffffff817e073000) IOMMU: Create VTD context table for PCI bus 0x57 (pptr=0xffffff817e074000) IOMMU: Create VTD context table for PCI bus 0x58 (pptr=0xffffff817e075000) IOMMU: Create VTD context table for PCI bus 0x59 (pptr=0xffffff817e076000) IOMMU: Create VTD context table for PCI bus 0x5a (pptr=0xffffff817e077000) IOMMU: Create VTD context table for PCI bus 0x5b (pptr=0xffffff817e078000) IOMMU: Create VTD context table for PCI bus 0x5c (pptr=0xffffff817e079000) IOMMU: Create VTD context table for PCI bus 0x5d (pptr=0xffffff817e07a000) IOMMU: Create VTD context table for PCI bus 0x5e (pptr=0xffffff817e07b000) IOMMU: Create VTD context table for PCI bus 0x5f (pptr=0xffffff817e07c000) IOMMU: Create VTD context table for PCI bus 0x60 (pptr=0xffffff817e07d000) IOMMU: Create VTD context table for PCI bus 0x61 (pptr=0xffffff817e07e000) IOMMU: Create VTD context table for PCI bus 0x62 (pptr=0xffffff817e07f000) IOMMU: Create VTD context table for PCI bus 0x63 (pptr=0xffffff817e080000) IOMMU: Create VTD context table for PCI bus 0x64 (pptr=0xffffff817e081000) IOMMU: Create VTD context table for PCI bus 0x65 (pptr=0xffffff817e082000) IOMMU: Create VTD context table for PCI bus 0x66 (pptr=0xffffff817e083000) IOMMU: Create VTD context table for PCI bus 0x67 (pptr=0xffffff817e084000) IOMMU: Create VTD context table for PCI bus 0x68 (pptr=0xffffff817e085000) IOMMU: Create VTD context table for PCI bus 0x69 (pptr=0xffffff817e086000) IOMMU: Create VTD context table for PCI bus 0x6a (pptr=0xffffff817e087000) IOMMU: Create VTD context table for PCI bus 0x6b (pptr=0xffffff817e088000) IOMMU: Create VTD context table for PCI bus 0x6c (pptr=0xffffff817e089000) IOMMU: Create VTD context table for PCI bus 0x6d (pptr=0xffffff817e08a000) IOMMU: Create VTD context table for PCI bus 0x6e (pptr=0xffffff817e08b000) IOMMU: Create VTD context table for PCI bus 0x6f (pptr=0xffffff817e08c000) IOMMU: Create VTD context table for PCI bus 0x70 (pptr=0xffffff817e08d000) IOMMU: Create VTD context table for PCI bus 0x71 (pptr=0xffffff817e08e000) IOMMU: Create VTD context table for PCI bus 0x72 (pptr=0xffffff817e08f000) IOMMU: Create VTD context table for PCI bus 0x73 (pptr=0xffffff817e090000) IOMMU: Create VTD context table for PCI bus 0x74 (pptr=0xffffff817e091000) IOMMU: Create VTD context table for PCI bus 0x75 (pptr=0xffffff817e092000) IOMMU: Create VTD context table for PCI bus 0x76 (pptr=0xffffff817e093000) IOMMU: Create VTD context table for PCI bus 0x77 (pptr=0xffffff817e094000) IOMMU: Create VTD context table for PCI bus 0x78 (pptr=0xffffff817e095000) IOMMU: Create VTD context table for PCI bus 0x79 (pptr=0xffffff817e096000) IOMMU: Create VTD context table for PCI bus 0x7a (pptr=0xffffff817e097000) IOMMU: Create VTD context table for PCI bus 0x7b (pptr=0xffffff817e098000) IOMMU: Create VTD context table for PCI bus 0x7c (pptr=0xffffff817e099000) IOMMU: Create VTD context table for PCI bus 0x7d (pptr=0xffffff817e09a000) IOMMU: Create VTD context table for PCI bus 0x7e (pptr=0xffffff817e09b000) IOMMU: Create VTD context table for PCI bus 0x7f (pptr=0xffffff817e09c000) IOMMU: Create VTD context table for PCI bus 0x80 (pptr=0xffffff817e09d000) IOMMU: Create VTD context table for PCI bus 0x81 (pptr=0xffffff817e09e000) IOMMU: Create VTD context table for PCI bus 0x82 (pptr=0xffffff817e09f000) IOMMU: Create VTD context table for PCI bus 0x83 (pptr=0xffffff817e0a0000) IOMMU: Create VTD context table for PCI bus 0x84 (pptr=0xffffff817e0a1000) IOMMU: Create VTD context table for PCI bus 0x85 (pptr=0xffffff817e0a2000) IOMMU: Create VTD context table for PCI bus 0x86 (pptr=0xffffff817e0a3000) IOMMU: Create VTD context table for PCI bus 0x87 (pptr=0xffffff817e0a4000) IOMMU: Create VTD context table for PCI bus 0x88 (pptr=0xffffff817e0a5000) IOMMU: Create VTD context table for PCI bus 0x89 (pptr=0xffffff817e0a6000) IOMMU: Create VTD context table for PCI bus 0x8a (pptr=0xffffff817e0a7000) IOMMU: Create VTD context table for PCI bus 0x8b (pptr=0xffffff817e0a8000) IOMMU: Create VTD context table for PCI bus 0x8c (pptr=0xffffff817e0a9000) IOMMU: Create VTD context table for PCI bus 0x8d (pptr=0xffffff817e0aa000) IOMMU: Create VTD context table for PCI bus 0x8e (pptr=0xffffff817e0ab000) IOMMU: Create VTD context table for PCI bus 0x8f (pptr=0xffffff817e0ac000) IOMMU: Create VTD context table for PCI bus 0x90 (pptr=0xffffff817e0ad000) IOMMU: Create VTD context table for PCI bus 0x91 (pptr=0xffffff817e0ae000) IOMMU: Create VTD context table for PCI bus 0x92 (pptr=0xffffff817e0af000) IOMMU: Create VTD context table for PCI bus 0x93 (pptr=0xffffff817e0b0000) IOMMU: Create VTD context table for PCI bus 0x94 (pptr=0xffffff817e0b1000) IOMMU: Create VTD context table for PCI bus 0x95 (pptr=0xffffff817e0b2000) IOMMU: Create VTD context table for PCI bus 0x96 (pptr=0xffffff817e0b3000) IOMMU: Create VTD context table for PCI bus 0x97 (pptr=0xffffff817e0b4000) IOMMU: Create VTD context table for PCI bus 0x98 (pptr=0xffffff817e0b5000) IOMMU: Create VTD context table for PCI bus 0x99 (pptr=0xffffff817e0b6000) IOMMU: Create VTD context table for PCI bus 0x9a (pptr=0xffffff817e0b7000) IOMMU: Create VTD context table for PCI bus 0x9b (pptr=0xffffff817e0b8000) IOMMU: Create VTD context table for PCI bus 0x9c (pptr=0xffffff817e0b9000) IOMMU: Create VTD context table for PCI bus 0x9d (pptr=0xffffff817e0ba000) IOMMU: Create VTD context table for PCI bus 0x9e (pptr=0xffffff817e0bb000) IOMMU: Create VTD context table for PCI bus 0x9f (pptr=0xffffff817e0bc000) IOMMU: Create VTD context table for PCI bus 0xa0 (pptr=0xffffff817e0bd000) IOMMU: Create VTD context table for PCI bus 0xa1 (pptr=0xffffff817e0be000) IOMMU: Create VTD context table for PCI bus 0xa2 (pptr=0xffffff817e0bf000) IOMMU: Create VTD context table for PCI bus 0xa3 (pptr=0xffffff817e0c0000) IOMMU: Create VTD context table for PCI bus 0xa4 (pptr=0xffffff817e0c1000) IOMMU: Create VTD context table for PCI bus 0xa5 (pptr=0xffffff817e0c2000) IOMMU: Create VTD context table for PCI bus 0xa6 (pptr=0xffffff817e0c3000) IOMMU: Create VTD context table for PCI bus 0xa7 (pptr=0xffffff817e0c4000) IOMMU: Create VTD context table for PCI bus 0xa8 (pptr=0xffffff817e0c5000) IOMMU: Create VTD context table for PCI bus 0xa9 (pptr=0xffffff817e0c6000) IOMMU: Create VTD context table for PCI bus 0xaa (pptr=0xffffff817e0c7000) IOMMU: Create VTD context table for PCI bus 0xab (pptr=0xffffff817e0c8000) IOMMU: Create VTD context table for PCI bus 0xac (pptr=0xffffff817e0c9000) IOMMU: Create VTD context table for PCI bus 0xad (pptr=0xffffff817e0ca000) IOMMU: Create VTD context table for PCI bus 0xae (pptr=0xffffff817e0cb000) IOMMU: Create VTD context table for PCI bus 0xaf (pptr=0xffffff817e0cc000) IOMMU: Create VTD context table for PCI bus 0xb0 (pptr=0xffffff817e0cd000) IOMMU: Create VTD context table for PCI bus 0xb1 (pptr=0xffffff817e0ce000) IOMMU: Create VTD context table for PCI bus 0xb2 (pptr=0xffffff817e0cf000) IOMMU: Create VTD context table for PCI bus 0xb3 (pptr=0xffffff817e0d0000) IOMMU: Create VTD context table for PCI bus 0xb4 (pptr=0xffffff817e0d1000) IOMMU: Create VTD context table for PCI bus 0xb5 (pptr=0xffffff817e0d2000) IOMMU: Create VTD context table for PCI bus 0xb6 (pptr=0xffffff817e0d3000) IOMMU: Create VTD context table for PCI bus 0xb7 (pptr=0xffffff817e0d4000) IOMMU: Create VTD context table for PCI bus 0xb8 (pptr=0xffffff817e0d5000) IOMMU: Create VTD context table for PCI bus 0xb9 (pptr=0xffffff817e0d6000) IOMMU: Create VTD context table for PCI bus 0xba (pptr=0xffffff817e0d7000) IOMMU: Create VTD context table for PCI bus 0xbb (pptr=0xffffff817e0d8000) IOMMU: Create VTD context table for PCI bus 0xbc (pptr=0xffffff817e0d9000) IOMMU: Create VTD context table for PCI bus 0xbd (pptr=0xffffff817e0da000) IOMMU: Create VTD context table for PCI bus 0xbe (pptr=0xffffff817e0db000) IOMMU: Create VTD context table for PCI bus 0xbf (pptr=0xffffff817e0dc000) IOMMU: Create VTD context table for PCI bus 0xc0 (pptr=0xffffff817e0dd000) IOMMU: Create VTD context table for PCI bus 0xc1 (pptr=0xffffff817e0de000) IOMMU: Create VTD context table for PCI bus 0xc2 (pptr=0xffffff817e0df000) IOMMU: Create VTD context table for PCI bus 0xc3 (pptr=0xffffff817e0e0000) IOMMU: Create VTD context table for PCI bus 0xc4 (pptr=0xffffff817e0e1000) IOMMU: Create VTD context table for PCI bus 0xc5 (pptr=0xffffff817e0e2000) IOMMU: Create VTD context table for PCI bus 0xc6 (pptr=0xffffff817e0e3000) IOMMU: Create VTD context table for PCI bus 0xc7 (pptr=0xffffff817e0e4000) IOMMU: Create VTD context table for PCI bus 0xc8 (pptr=0xffffff817e0e5000) IOMMU: Create VTD context table for PCI bus 0xc9 (pptr=0xffffff817e0e6000) IOMMU: Create VTD context table for PCI bus 0xca (pptr=0xffffff817e0e7000) IOMMU: Create VTD context table for PCI bus 0xcb (pptr=0xffffff817e0e8000) IOMMU: Create VTD context table for PCI bus 0xcc (pptr=0xffffff817e0e9000) IOMMU: Create VTD context table for PCI bus 0xcd (pptr=0xffffff817e0ea000) IOMMU: Create VTD context table for PCI bus 0xce (pptr=0xffffff817e0eb000) IOMMU: Create VTD context table for PCI bus 0xcf (pptr=0xffffff817e0ec000) IOMMU: Create VTD context table for PCI bus 0xd0 (pptr=0xffffff817e0ed000) IOMMU: Create VTD context table for PCI bus 0xd1 (pptr=0xffffff817e0ee000) IOMMU: Create VTD context table for PCI bus 0xd2 (pptr=0xffffff817e0ef000) IOMMU: Create VTD context table for PCI bus 0xd3 (pptr=0xffffff817e0f0000) IOMMU: Create VTD context table for PCI bus 0xd4 (pptr=0xffffff817e0f1000) IOMMU: Create VTD context table for PCI bus 0xd5 (pptr=0xffffff817e0f2000) IOMMU: Create VTD context table for PCI bus 0xd6 (pptr=0xffffff817e0f3000) IOMMU: Create VTD context table for PCI bus 0xd7 (pptr=0xffffff817e0f4000) IOMMU: Create VTD context table for PCI bus 0xd8 (pptr=0xffffff817e0f5000) IOMMU: Create VTD context table for PCI bus 0xd9 (pptr=0xffffff817e0f6000) IOMMU: Create VTD context table for PCI bus 0xda (pptr=0xffffff817e0f7000) IOMMU: Create VTD context table for PCI bus 0xdb (pptr=0xffffff817e0f8000) IOMMU: Create VTD context table for PCI bus 0xdc (pptr=0xffffff817e0f9000) IOMMU: Create VTD context table for PCI bus 0xdd (pptr=0xffffff817e0fa000) IOMMU: Create VTD context table for PCI bus 0xde (pptr=0xffffff817e0fb000) IOMMU: Create VTD context table for PCI bus 0xdf (pptr=0xffffff817e0fc000) IOMMU: Create VTD context table for PCI bus 0xe0 (pptr=0xffffff817e0fd000) IOMMU: Create VTD context table for PCI bus 0xe1 (pptr=0xffffff817e0fe000) IOMMU: Create VTD context table for PCI bus 0xe2 (pptr=0xffffff817e0ff000) IOMMU: Create VTD context table for PCI bus 0xe3 (pptr=0xffffff817e100000) IOMMU: Create VTD context table for PCI bus 0xe4 (pptr=0xffffff817e101000) IOMMU: Create VTD context table for PCI bus 0xe5 (pptr=0xffffff817e102000) IOMMU: Create VTD context table for PCI bus 0xe6 (pptr=0xffffff817e103000) IOMMU: Create VTD context table for PCI bus 0xe7 (pptr=0xffffff817e104000) IOMMU: Create VTD context table for PCI bus 0xe8 (pptr=0xffffff817e105000) IOMMU: Create VTD context table for PCI bus 0xe9 (pptr=0xffffff817e106000) IOMMU: Create VTD context table for PCI bus 0xea (pptr=0xffffff817e107000) IOMMU: Create VTD context table for PCI bus 0xeb (pptr=0xffffff817e108000) IOMMU: Create VTD context table for PCI bus 0xec (pptr=0xffffff817e109000) IOMMU: Create VTD context table for PCI bus 0xed (pptr=0xffffff817e10a000) IOMMU: Create VTD context table for PCI bus 0xee (pptr=0xffffff817e10b000) IOMMU: Create VTD context table for PCI bus 0xef (pptr=0xffffff817e10c000) IOMMU: Create VTD context table for PCI bus 0xf0 (pptr=0xffffff817e10d000) IOMMU: Create VTD context table for PCI bus 0xf1 (pptr=0xffffff817e10e000) IOMMU: Create VTD context table for PCI bus 0xf2 (pptr=0xffffff817e10f000) IOMMU: Create VTD context table for PCI bus 0xf3 (pptr=0xffffff817e110000) IOMMU: Create VTD context table for PCI bus 0xf4 (pptr=0xffffff817e111000) IOMMU: Create VTD context table for PCI bus 0xf5 (pptr=0xffffff817e112000) IOMMU: Create VTD context table for PCI bus 0xf6 (pptr=0xffffff817e113000) IOMMU: Create VTD context table for PCI bus 0xf7 (pptr=0xffffff817e114000) IOMMU: Create VTD context table for PCI bus 0xf8 (pptr=0xffffff817e115000) IOMMU: Create VTD context table for PCI bus 0xf9 (pptr=0xffffff817e116000) IOMMU: Create VTD context table for PCI bus 0xfa (pptr=0xffffff817e117000) IOMMU: Create VTD context table for PCI bus 0xfb (pptr=0xffffff817e118000) IOMMU: Create VTD context table for PCI bus 0xfc (pptr=0xffffff817e119000) IOMMU: Create VTD context table for PCI bus 0xfd (pptr=0xffffff817e11a000) IOMMU: Create VTD context table for PCI bus 0xfe (pptr=0xffffff817e11b000) IOMMU: Create VTD context table for PCI bus 0xff (pptr=0xffffff817e11c000) IOMMU 0x0: enabling... enabled Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/212 T0xffffff817e11d400 "rootserver" @4014bf]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>> <<seL4(CPU 0) [decodeUntypedInvocation/212 T0xffffff817e11d400 "rootserver" @4014bf]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>> <<seL4(CPU 0) [decodeUntypedInvocation/212 T0xffffff817e11d400 "rootserver" @4014bf]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>> <<seL4(CPU 0) [decodeUntypedInvocation/212 T0xffffff817e11d400 "rootserver" @4014bf]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>> <<seL4(CPU 0) [decodeUntypedInvocation/212 T0xffffff817e11d400 "rootserver" @4014bf]: Untyped Retype: Insufficient memory (1 * 33554432 bytes needed, 0 bytes available).>> Single bus detected lib_pci_scan_dev found pci device 0 0 PCI :: 00.00.00 : intel Unknown device ID. (vid 0x8086 did 0x29c0) line0 pin0 lib_pci_scan_dev found pci device 0 1 PCI :: 00.01.00 : Unknown vendor ID. Unknown device ID. (vid 0x1234 did 0x1111) line0 pin0 BAR0 : [ mem 0xfd000000 sz 0x1000000 szmask 0xff000000 prefetch ] BAR2 : [ mem 0xfebb0000 sz 0x1000 szmask 0xfffff000 ] lib_pci_scan_dev found pci device 0 2 PCI :: 00.02.00 : intel Unknown device ID. (vid 0x8086 did 0x100e) line11 pin1 BAR0 : [ mem 0xfeb80000 sz 0x20000 szmask 0xfffe0000 ] BAR1 : [ io 0xc000 sz 0x40 szmask 0xffffffc0 ] lib_pci_scan_dev found pci device 0 31 PCI :: 00.1f.00 : intel intel_ich9_8 (vid 0x8086 did 0x2918) line0 pin0 lib_pci_scan_dev found multi function device 0 31 PCI :: 00.1f.02 : intel Unknown device ID. (vid 0x8086 did 0x2922) line10 pin1 BAR4 : [ io 0xc080 sz 0x20 szmask 0xffffffe0 ] BAR5 : [ mem 0xfebb1000 sz 0x1000 szmask 0xfffff000 ] PCI :: 00.1f.03 : intel intel_ich9_6 (vid 0x8086 did 0x2930) line10 pin1 BAR4 : [ io 0x700 sz 0x40 szmask 0xffffffc0 ] Guest page dir allocated at 0x10000000. Creating 1-1 entries sel4utils_reserve_range_at_no_alloc@vspace.c:601 Range not available at 0x7e00, size 0x78200 vm_reserve_memory_at@guest_memory.c:328 Failed to allocate vm reservation: Unable to create vspace reservation at address 0x7e00 of size 492032 vm_ram_register_at@guest_ram.c:355 Unable to reserve ram region at addr 0x7e00 of size 0x78200 guest_elf_relocate@guest_image.c:129 50000 relocs done. guest_elf_relocate@guest_image.c:129 100000 relocs done. Constructing guest cmdline at 0x500 of size 142 Guest boot info allocated at 0x58f. Populating... Final e820 map is: 0x0 - 0x500 type 2 0x500 - 0x7c00 type 1 0x7c00 - 0x80000 type 2 0x80000 - 0x9fc00 type 1 0x9fc00 - 0x10001000 type 2 0x10001000 - 0x90001000 type 1 Initializing guest to start running at 0x10400000 [ 0.000000] Linux version 4.8.16 (alisonf@carbon) (gcc version 7.4.0 (Ubuntu 7.4.0-1ubuntu1~18.04.1) ) #1 Wed Oct 23 17:26:59 AEDT 2019 [ 0.000000] Disabled fast string operations [ 0.000000] x86/fpu: Legacy x87 FPU detected. [ 0.000000] x86/fpu: Using 'eager' FPU context switches. [ 0.000000] e820: BIOS-provided physical RAM map: [ 0.000000] BIOS-e820: [mem 0x0000000000000000-0x00000000000004ff] reserved [ 0.000000] BIOS-e820: [mem 0x0000000000000500-0x0000000000007bff] usable [ 0.000000] BIOS-e820: [mem 0x0000000000007c00-0x000000000007ffff] reserved [ 0.000000] BIOS-e820: [mem 0x0000000000080000-0x000000000009fbff] usable [ 0.000000] BIOS-e820: [mem 0x000000000009fc00-0x0000000010000fff] reserved [ 0.000000] BIOS-e820: [mem 0x0000000010001000-0x0000000090000fff] usable [ 0.000000] bootconsole [earlyser0] enabled [ 0.000000] Notice: NX (Execute Disable) protection missing in CPU! [ 0.000000] DMI not present or invalid. [ 0.000000] e820: update [mem 0x00000000-0x00000fff] usable ==> reserved [ 0.000000] e820: remove [mem 0x000a0000-0x000fffff] usable [ 0.000000] e820: last_pfn = 0x90001 max_arch_pfn = 0x100000 [ 0.000000] MTRR: Disabled [ 0.000000] x86/PAT: MTRRs disabled, skipping PAT initialization too. [ 0.000000] x86/PAT: Configuration [0-7]: WB WT UC- UC WB WT UC- UC [ 0.000000] Warning only 895MB will be used. [ 0.000000] Use a HIGHMEM enabled kernel. [ 0.000000] Scanning 1 areas for low memory corruption [ 0.000000] initial memory mapped: [mem 0x00000000-0x10ffffff] [ 0.000000] Base memory trampoline at [c009b000] 9b000 size 16384 [ 0.000000] BRK [0x10b8f000, 0x10b8ffff] PGTABLE [ 0.000000] BRK [0x10b90000, 0x10b90fff] PGTABLE [ 0.000000] RAMDISK: [mem 0x10c71000-0x11279fff] [ 0.000000] 895MB LOWMEM available. [ 0.000000] mapped low ram: 0 - 37fe2000 [ 0.000000] low ram: 0 - 37fe2000 [ 0.000000] Zone ranges: [ 0.000000] DMA [mem 0x0000000000001000-0x0000000000ffffff] [ 0.000000] Normal [mem 0x0000000001000000-0x0000000037fe1fff] [ 0.000000] Movable zone start for each node [ 0.000000] Early memory node ranges [ 0.000000] node 0: [mem 0x0000000000001000-0x0000000000006fff] [ 0.000000] node 0: [mem 0x0000000000080000-0x000000000009efff] [ 0.000000] node 0: [mem 0x0000000010001000-0x0000000090000fff] [ 0.000000] Initmem setup node 0 [mem 0x0000000000001000-0x0000000090000fff] [ 0.000000] On node 0 totalpages: 163846 [ 0.000000] free_area_init_node: node 0, pgdat d0a7ce40, node_mem_map f7466020 [ 0.000000] DMA zone: 32 pages used for memmap [ 0.000000] DMA zone: 0 pages reserved [ 0.000000] DMA zone: 37 pages, LIFO batch:0 [ 0.000000] Normal zone: 1760 pages used for memmap [ 0.000000] Normal zone: 163809 pages, LIFO batch:31 [ 0.000000] e820: [mem 0x90001000-0xffffffff] available for PCI devices [ 0.000000] clocksource: refined-jiffies: mask: 0xffffffff max_cycles: 0xffffffff, max_idle_ns: 19112604462750000 ns [ 0.000000] pcpu-alloc: s0 r0 d32768 u32768 alloc=1*32768 [ 0.000000] pcpu-alloc: [0] 0 [ 0.000000] Built 1 zonelists in Zone order, mobility grouping on. Total pages: 162054 [ 0.000000] Kernel command line: earlyprintk=ttyS0,115200 console=ttyS0,115200 i8042.nokbd=y i8042.nomux=y i8042.noaux=y io_delay=udelay noisapnp pci=nomsi debug root=/dev/mem [ 0.000000] PID hash table entries: 4096 (order: 2, 16384 bytes) [ 0.000000] Dentry cache hash table entries: 131072 (order: 7, 524288 bytes) [ 0.000000] Inode-cache hash table entries: 65536 (order: 6, 262144 bytes) [ 0.000000] Initializing CPU#0 [ 0.000000] Memory: 632784K/655384K available (4590K kernel code, 339K rwdata, 1744K rodata, 284K init, 496K bss, 22600K reserved, 0K cma-reserved) [ 0.000000] virtual kernel memory layout: [ 0.000000] fixmap : 0xfffe4000 - 0xfffff000 ( 108 kB) [ 0.000000] vmalloc : 0xf87e2000 - 0xfffe2000 ( 120 MB) [ 0.000000] lowmem : 0xc0000000 - 0xf7fe2000 ( 895 MB) [ 0.000000] .init : 0xd0a88000 - 0xd0acf000 ( 284 kB) [ 0.000000] .data : 0xd087bcae - 0xd0a86d40 (2092 kB) [ 0.000000] .text : 0xd0400000 - 0xd087bcae (4591 kB) [ 0.000000] Checking if this processor honours the WP bit even in supervisor mode...Ok. [ 0.000000] SLUB: HWalign=32, Order=0-3, MinObjects=0, CPUs=1, Nodes=1 [ 0.000000] NR_IRQS:16 nr_irqs:16 16 [ 0.000000] CPU 0 irqstacks, hard=f7008000 soft=f700a000 [ 0.000000] Console: colour dummy device 80x25 [ 0.000000] console [ttyS0] enabled [ 0.000000] console [ttyS0] enabled [ 0.000000] bootconsole [earlyser0] disabled [ 0.000000] bootconsole [earlyser0] disabled [ 0.000000] tsc: Fast TSC calibration failed [ 0.000000] tsc: Unable to calibrate against PIT [ 0.000000] tsc: No reference (HPET/PMTIMER) available [ 0.000000] tsc: Marking TSC unstable due to could not calculate TSC khz [ 0.040000] Calibrating delay loop... 7023.82 BogoMIPS (lpj=35119104) [ 0.070000] pid_max: default: 32768 minimum: 301 [ 0.080000] Security Framework initialized [ 0.080000] Mount-cache hash table entries: 2048 (order: 1, 8192 bytes) [ 0.090000] Mountpoint-cache hash table entries: 2048 (order: 1, 8192 bytes) [ 0.100000] Disabled fast string operations [ 0.100000] Last level iTLB entries: 4KB 0, 2MB 0, 4MB 0 [ 0.110000] Last level dTLB entries: 4KB 0, 2MB 0, 4MB 0, 1GB 0 [ 0.110000] CPU: Intel Core i7 9xx (Nehalem Class Core i7) (family: 0x6, model: 0x1a, stepping: 0x3) [ 0.150000] Performance Events: unsupported p6 CPU model 26 no PMU driver, software events only. [ 0.160000] devtmpfs: initialized [ 0.160000] clocksource: jiffies: mask: 0xffffffff max_cycles: 0xffffffff, max_idle_ns: 19112604462750000 ns [ 0.170000] kworker/u2:0 (11) used greatest stack depth: 7308 bytes left [ 0.180000] NET: Registered protocol family 16 [ 0.190000] cpuidle: using governor ladder [ 0.190000] cpuidle: using governor menu [ 0.200000] clocksource: pit: mask: 0xffffffff max_cycles: 0xffffffff, max_idle_ns: 1601818034827 ns [ 0.210000] PCI: Using configuration type 1 for base access [ 0.220000] vgaarb: loaded [ 0.220000] SCSI subsystem initialized [ 0.230000] libata version 3.00 loaded. [ 0.230000] usbcore: registered new interface driver usbfs [ 0.240000] usbcore: registered new interface driver hub [ 0.240000] usbcore: registered new device driver usb [ 0.250000] pps_core: LinuxPPS API ver. 1 registered [ 0.250000] pps_core: Software ver. 5.3.6 - Copyright 2005-2007 Rodolfo Giometti <giometti(a)linux.it> [ 0.260000] PTP clock support registered [ 0.270000] dmi: Firmware registration failed. [ 0.270000] PCI: Probing PCI hardware [ 0.280000] PCI: root bus 00: using default resources [ 0.280000] PCI: Probing PCI hardware (bus 00) [ 0.290000] PCI host bridge to bus 0000:00 [ 0.290000] pci_bus 0000:00: root bus resource [io 0x0000-0xffff] [ 0.300000] pci_bus 0000:00: root bus resource [mem 0x00000000-0xffffffff] [ 0.310000] pci_bus 0000:00: No busn resource found for root bus, will use [bus 00-ff] [ 0.320000] pci 0000:00:00.0: [5e14:0042] type 00 class 0x060000 [ 0.330000] pci 0000:00:01.0: [1234:1111] type 00 class 0x030000 [ 0.340000] pci 0000:00:01.0: reg 0x10: [mem 0x90001000-0x90001fff pref] [ 0.350000] pci 0000:00:01.0: reg 0x14: [mem 0x91001000-0x91001fff] [ 0.370000] pci 0000:00:01.0: reg 0x30: [mem 0xfeba0000-0xfebaffff pref] [ 0.380000] vgaarb: setting as boot device: PCI:0000:00:01.0 [ 0.380000] vgaarb: device added: PCI:0000:00:01.0,decodes=io+mem,owns=io+mem,locks=none [ 0.400000] pci 0000:00:02.0: [8086:100e] type 00 class 0x020000 [ 0.400000] pci 0000:00:02.0: reg 0x10: [mem 0x91002000-0x91003fff] [ 0.410000] pci 0000:00:02.0: reg 0x14: [io 0xc000-0xc03f] [ 0.420000] pci 0000:00:02.0: reg 0x30: [mem 0xfeb00000-0xfeb7ffff pref] [ 0.430000] pci 0000:00:03.0: [8086:2918] type 00 class 0x060100 [ 0.440000] pci 0000:00:03.0: quirk: [io 0x0600-0x067f] claimed by ICH6 ACPI/GPIO/TCO [ 0.450000] pci 0000:00:04.0: [8086:2922] type 00 class 0x010601 [ 0.460000] pci 0000:00:04.0: reg 0x10: [io 0xc080-0xc09f] [ 0.470000] pci 0000:00:04.0: reg 0x14: [mem 0x91022000-0x91022fff] [ 0.490000] pci 0000:00:05.0: [8086:2930] type 00 class 0x0c0500 [ 0.490000] pci 0000:00:05.0: reg 0x10: [io 0x0700-0x073f] [ 0.510000] pci_bus 0000:00: busn_res: [bus 00-ff] end is updated to 00 [ 0.520000] PCI: pci_cache_line_size set to 32 bytes [ 0.520000] e820: reserve RAM buffer [mem 0x00007c00-0x0000ffff] [ 0.530000] e820: reserve RAM buffer [mem 0x0009fc00-0x0009ffff] [ 0.540000] e820: reserve RAM buffer [mem 0x90001000-0x93ffffff] [ 0.540000] NetLabel: Initializing [ 0.550000] NetLabel: domain hash size = 128 [ 0.550000] NetLabel: protocols = UNLABELED CIPSOv4 [ 0.560000] NetLabel: unlabeled traffic allowed by default [ 0.570000] clocksource: Switched to clocksource pit [ 0.570000] VFS: Disk quotas dquot_6.6.0 [ 0.580583] VFS: Dquot-cache hash table entries: 1024 (order 0, 4096 bytes) [ 0.580583] hugetlbfs: disabling because there are no supported hugepage sizes [ 0.608902] pci_bus 0000:00: resource 4 [io 0x0000-0xffff] [ 0.622439] pci_bus 0000:00: resource 5 [mem 0x00000000-0xffffffff] [ 0.629178] NET: Registered protocol family 2 [ 0.629178] TCP established hash table entries: 8192 (order: 3, 32768 bytes) [ 0.643721] TCP bind hash table entries: 8192 (order: 3, 32768 bytes) [ 0.651068] TCP: Hash tables configured (established 8192 bind 8192) [ 0.651068] UDP hash table entries: 512 (order: 1, 8192 bytes) [ 0.664304] UDP-Lite hash table entries: 512 (order: 1, 8192 bytes) [ 0.673571] NET: Registered protocol family 1 [ 0.679034] RPC: Registered named UNIX socket transport module. [ 0.679034] RPC: Registered udp transport module. [ 0.691033] RPC: Registered tcp transport module. [ 0.691033] RPC: Registered tcp NFSv4.1 backchannel transport module. [ 0.702947] pci 0000:00:01.0: Video device with shadowed ROM at [mem 0x000c0000-0x000dffff] [ 0.713872] PCI: CLS 0 bytes, default 32 [ 0.719115] Unpacking initramfs... [ 0.728865] Freeing initrd memory: 6180K (d0c71000 - d127a000) [ 0.740017] platform rtc_cmos: registered platform RTC device (no PNP device found) [ 0.749380] Scanning for low memory corruption every 60 seconds [ 0.749380] futex hash table entries: 256 (order: -1, 3072 bytes) [ 0.765067] workingset: timestamp_bits=30 max_order=18 bucket_order=0 [ 0.788927] squashfs: version 4.0 (2009/01/31) Phillip Lougher [ 0.798908] NFS: Registering the id_resolver key type [ 0.798908] Key type id_resolver registered [ 0.812867] Key type id_legacy registered [ 0.818762] Block layer SCSI generic (bsg) driver version 0.4 loaded (major 250) [ 0.831896] io scheduler noop registered [ 0.831896] io scheduler deadline registered [ 0.841111] io scheduler cfq registered (default) [ 0.841111] intel_idle: does not run on family 6 model 26 [ 0.854361] Serial: 8250/16550 driver, 4 ports, IRQ sharing enabled [ 0.877337] serial8250: ttyS0 at I/O 0x3f8 (irq = 4, base_baud = 115200) is a 16550A [ 0.888811] Non-volatile memory driver v1.3 [ 0.888811] [drm] Initialized drm 1.1.0 20060810 [ 0.900611] loop: module loaded [ 0.910483] lpc_ich 0000:00:03.0: I/O space for GPIO uninitialized [ 0.919536] ahci 0000:00:04.0: version 3.0 [ 0.919536] ahci: probe of 0000:00:04.0 failed with error -22 [ 0.931932] pcnet32: pcnet32.c:v1.35 21.Apr.2008 tsbogend(a)alpha.franken.de [ 0.940722] e100: Intel(R) PRO/100 Network Driver, 3.5.24-k2-NAPI [ 0.940722] e100: Copyright(c) 1999-2006 Intel Corporation [ 0.953860] e1000: Intel(R) PRO/1000 Network Driver - version 7.3.21-k8-NAPI [ 0.962047] e1000: Copyright (c) 1999-2006 Intel Corporation. [ 1.029745] BUG: unable to handle kernel paging request at f87f9820 [ 1.029745] IP: [<d06ecf45>] e1000_reset_hw+0x10f/0x180 [ 1.029745] *pde = 37021067 *pte = 00000000 [ 1.029745] Oops: 0000 [#1] [ 1.029745] Modules linked in: [ 1.029745] CPU: 0 PID: 1 Comm: swapper Not tainted 4.8.16 #1 [ 1.029745] task: f704c000 task.stack: f7050000 [ 1.029745] EIP: 0060:[<d06ecf45>] EFLAGS: 00210202 CPU: 0 [ 1.029745] EIP is at e1000_reset_hw+0x10f/0x180 [ 1.029745] EAX: f87f4000 EBX: f73f274c ECX: 00000000 EDX: 00000060 [ 1.029745] ESI: 04140240 EDI: 0000c000 EBP: f7051e38 ESP: f7051e2c [ 1.029745] DS: 007b ES: 007b FS: 0000 GS: 0000 SS: 0068 [ 1.029745] CR0: 80050033 CR2: f87f9820 CR3: 10ad2000 CR4: 00000680 [ 1.029745] Stack: [ 1.029745] f73f2000 00000000 00000000 f7051e78 d06e97c0 f7051e54 f73f2400 00000043 [ 1.029745] f73f274c 00000000 f7083800 00000000 f7051e78 d05bb85a f7051e6c d0a696d4 [ 1.029745] f7083800 f7083868 d0a69694 f7051e90 d05bbb48 d0a69660 f7083868 d0a69694 [ 1.029745] Call Trace: [ 1.029745] [<d06e97c0>] e1000_probe+0x556/0xb18 [ 1.029745] [<d05bb85a>] ? pci_match_device+0x5f/0x7c [ 1.029745] [<d05bbb48>] pci_device_probe+0x51/0x98 [ 1.029745] [<d06a48ed>] driver_probe_device+0xc9/0x1aa [ 1.029745] [<d06a4a26>] __driver_attach+0x58/0x74 [ 1.029745] [<d06a352c>] bus_for_each_dev+0x4f/0x63 [ 1.029745] [<d06a44c1>] driver_attach+0x14/0x16 [ 1.029745] [<d06a49ce>] ? driver_probe_device+0x1aa/0x1aa [ 1.029745] [<d06a4216>] bus_add_driver+0xab/0x18a [ 1.029745] [<d06a4e77>] driver_register+0x6e/0xa0 [ 1.029745] [<d05bb5a0>] __pci_register_driver+0x27/0x2a [ 1.029745] [<d0aa34b0>] ? e100_init_module+0x4d/0x4d [ 1.029745] [<d0aa34e8>] e1000_init_module+0x38/0x6e [ 1.029745] [<d0aa34b0>] ? e100_init_module+0x4d/0x4d [ 1.029745] [<d0400465>] do_one_initcall+0x7c/0xed [ 1.029745] [<d043744a>] ? parse_args+0x1b3/0x27d [ 1.029745] [<d0a88b40>] ? kernel_init_freeable+0xdf/0x17d [ 1.029745] [<d0a88b5d>] kernel_init_freeable+0xfc/0x17d [ 1.029745] [<d0878103>] kernel_init+0x8/0xcb [ 1.029745] [<d087a4e2>] ret_from_kernel_thread+0xe/0x24 [ 1.029745] [<d08780fb>] ? rest_init+0x59/0x59 [ 1.029745] Code: 8b 03 8b 40 18 80 cc 20 8b 13 89 42 18 8b 03 8b 40 08 b8 02 00 00 00 eb 05 b8 05 00 00 00 e8 22 d8 d5 ff 83 7b 0c 04 76 13 8b 03 <8b> 80 20 58 00 00 80 e4 df 8b 13 89 82 20 58 00 003 [ 1.029745] EIP: [<d06ecf45>] e1000_reset_hw+0x10f/0x180 SS:ESP 0068:f7051e2c [ 1.029745] CR2: 00000000f87f9820 [ 1.029745] ---[ end trace f9705abe48180ae4 ]--- [ 1.042868] Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000009 [ 1.042868] [ 1.042868] Kernel Offset: disabled [ 1.042868] ---[ end Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000009 [ 1.042868] [ 2.558940] random: fast init done [ 133.760986] random: crng init done ------------------------------------------------------------

1 0

PicoServer attributes
by christinefragoso＠protonmail.com 16 Nov '21

16 Nov '21

I am running on an i.MX6 the picoserver app https://github.com/seL4/camkes/tree/master/apps/picoserver Both the echo and listener components print out to serial: listener instance starting up, going to be listening on 10.0.0.2:4321 echo instance starting up, going to be listening on 10.0.0.2:1234 but only the echo component receives PicoTCP events: Assigned ipv4 10.0.0.2 to device eth0 IPv6: DAD verified valid address. echo: Connection established with 10.0.0.1 on socket 1 echo: Received a message on socket 3, going to echo to Listener echo: Received a message on socket 3, going to echo to Listener echo: Received a message on socket 3, going to echo to Listener Note that the listener component does not even print out "Connection established". I tried to figure out why, and found out that by editing this part of picoserver.camkes: /* * The attributes of the *_(control/send/recv) interfaces should be the same and unique between * different components, this determines the client ID of this component with respect to * the PicoServer component */ echo.echo_control_attributes = "1"; echo.echo_recv_attributes = "1"; echo.echo_recv_shmem_size = 0x1000; echo.echo_send_attributes = "1"; echo.echo_send_shmem_size = 0x1000; echo.ip_addr = PICOSERVER_IP_ADDR; /* * Listener config */ listener.listener_control_attributes = "2"; listener.listener_recv_attributes = "2"; listener.listener_recv_shmem_size = 0x1000; listener.listener_send_attributes = "2"; listener.listener_send_shmem_size = 0x1000; listener.ip_addr = PICOSERVER_IP_ADDR; and changing the attributes to this: /* * The attributes of the *_(control/send/recv) interfaces should be the same and unique between * different components, this determines the client ID of this component with respect to * the PicoServer component */ echo.echo_control_attributes = "0"; echo.echo_recv_attributes = "0"; echo.echo_recv_shmem_size = 0x1000; echo.echo_send_attributes = "0"; echo.echo_send_shmem_size = 0x1000; echo.ip_addr = PICOSERVER_IP_ADDR; /* * Listener config */ listener.listener_control_attributes = "1"; listener.listener_recv_attributes = "1"; listener.listener_recv_shmem_size = 0x1000; listener.listener_send_attributes = "1"; listener.listener_send_shmem_size = 0x1000; listener.ip_addr = PICOSERVER_IP_ADDR; then listener will print that it has connected to echo, but now echo will not print out anything. How do I make both echo and listener print out on the serial port? Which part of the code looks at echo.echo_recv_attributes = "1"; and listener.listener_recv_attributes = "2"; in order to determine the client ID of the echo and listener components with respect the PicoServer component? From what I can tell, attributes was not declared as an actual attribute.

1 0

RFC-9: new capability for seL4 SMC Forwarding on Arm
by Gerwin Klein 13 Nov '21

13 Nov '21

I’d like to solicit discussion on the new RFC on forwarding Secure Monitor Calls on Arm: https://sel4.atlassian.net/browse/RFC-9 Relevant Arm documentation (SMC calling conventions): https://developer.arm.com/documentation/den0028/latest?_ga=2.116565828.3903… Any opinions, concerns, alternative designs? Cheers, Gerwin

2 4

Camkes VMM configuration
by Jose Martins 10 Nov '21

10 Nov '21

Hello. I've been playing around with the camkes Arm VMM. However, the meaning of some of the configuration fields is not completely clear to me. For example: - what is the difference between "linux_ram_base" and "linux_ram_paddr_base" in the linux_address_config attribute? Are these supposed to define the virtual and physical addresses of the guest's ram region base, respectively? If so, can we have non-identity mappings by setting them to different values? From my experiments having different addresses on those does not always work (even if both are aligned to a 2M superpage boundary) . - what is the difference between the untyped_mmios and mmios attributes? They seem to serve pretty similar purposes. For example, in different vm-examples they are both used for assigning the virtual gic cpu interface to the guest. I probably have a few other questions. I couldn't find it, but I was hoping there was more thorough documentation for the vm configuration detailing the meaning of these fields (and others)? Best regards, José

2 1

Re: Runtime Measurement Hiccup
by Hugo V.C. 08 Nov '21

08 Nov '21

BTW, regarding to the nice trick suggested by Kent (using expect language to interact with console) just wanted to show you this expect script I wrote on 2007 (page 210 of https://www.pentest.es/checkpoint_hack.pdf) to exploit a vulnerability via interactive SSH shell in a very hardened device at that time (Check Point Secure Platform) which was an EAL4+ certified appliance with a locked down custom Linux, and patched kernel (Exec-Shield) with a painful set of memory protections, ASCII Armor, etc + a creative protection in their custom interactive shell (called CPSHELL) that only allowed a restricted set of ASCII chars... It took me 6 months to figure out how to bypass every single protection of that target, and chain all the different bypass techniques into a fully functional exploit. It was hard but I did it and I'm pretty sure anyone with somewhat creative offensive mind (there are thousands out there) would have achieved the same, after or before. Two things I want to highlight here is: 1) Anyone that is tempted to build "insecure" software solutions (Linux/non_verified_code) on top of secure solutions (seL4) must assume for the global design of the architecture that the "insecure" solution (Linux/non_verified_code) should be considered already broken. If you don't do this and expect other low level layers of security to solve root security issues, things may go horribly wrong. This is what happened in the case of Check Point Secure Platform, at that time, all the security was relying in the low level, multiple layers of the OS protections, but the source code of the vendor specific command line tools were full of security bugs... So, let's not expect seL4 host to solve the security problems of the guests (Linux, etc). seL4 can guarantee isolation of guests and it's own security, but as long there's an interaction with the guest (i.e. via console) there's lot of room for exploitation of the guest. 2) Going a step ahead, console interaction is just the most simple, but there are other ways to interact with guests as they are not physically isolated entities of the Universe.... I mean, if we consider chain supply attacks as a real possibility (i.e. an open source tool integrated into a Linux guest on top of seL4) we should be aware that it is not difficult to create a covert channel attack to extract information from the "isolated" guest... So even without any I/O available, the guest can play with multiple physical low level hardware details and physical environment variables to create a funny reliable stealth communication channel. I was just thinking loud but hope it helps someone else to have a wide vision of low level security. Expect scripting interaction with console suggestion by Kent reminded me about this old exploit I wrote and then I extrapolated it to any interaction in our beloved seL4 environments. Have a nice day. El mié, 3 nov 2021 a las 13:00, Hugo V.C. (<skydivebcn(a)gmail.com>) escribió: Very nice trick Kent! Thank you for sharing. That kind of information, from you guys the seL4 experts, is invaluable. El mié, 3 nov 2021 a las 12:15, Kent Mcleod (<kent.mcleod72(a)gmail.com>) escribió: Hi Michael, Just trying to answer your question about how to get data from a simulated system to a host system, the way we do it for sel4test and sel4bench is to use the serial console and grep for magic escape strings. It isn't foolproof but having something like: printf("<digest>%s</digest>\n", digest); from the simulated machine can be captured automatically by the host via matching the input character stream from the console looking to match <digest>.*</digest>. We use expect (https://en.wikipedia.org/wiki/Expect) or the python wrapper pexpect for scripting this and it's how we extract seL4test results and the sel4bench benchmark results that are automatically posted to https://sel4.systems/About/Performance/ via capturing the serial stream. ( https://github.com/seL4/sel4bench/runs/4064401581?check_suite_focus=true shows the output where the benchmark results are just dumped to the console). Kent.

1 0

Graph-refine Toolset Usability Issues (for WCET analysis)
by Jack Chen 06 Nov '21

06 Nov '21

Greetings I'm recently conducting research on WCET analysis of seL4-based systems. Graph-to-graph seems to be a good starting point. However the toolset doesn't seem to be fully working in my setup. My setup: x86, 16GB RAM, Windows10 WSL Ubuntu 20.04 Goal: To replicate the static WCET analysis decribed in the paper [Sewell et al. 2016], using graph-to-graph and graph-refine/seL4-example build. Steps taken: - repo setup with "verification-manifest" - fetched 2 versions: defalut (10/21/2021), and 12.1.0 - followed READMEs: preparing isabelle, HOL4, standalone c-parser, and their dependencies (according to graph-refine/seL4-example/readme) - L4V_ARCH=ARM - [./run_tests] in l4v - [make tar] in graph-refine/seL4-example - [python graph-refine.py <targetdir> all] Results (default version) : --------------------------- - seL4-example [make tar]: all things seem normal except - Graph spec failed in _start for pos 0xe0000008. - Graph spec failed in _start for pos 0xe0000008. - l4v run_tests: 43/51 passed - HaskellKernel STUCK (probably due to internet access issue for my region), CParserTest Failed - graph-refine: KeyError: 'kernel_devices' - This one is interesting. The seL4 code fetched with this "default" manifest contains a "kernel_device_frames", which I think is called "kernel_devices" in previous versions of seL4 kernel code. In kernel.elf.rodata they seem to be associated with the same block of assembly code. Results (12.1.0): --------------------------- - seL4-example [make tar]: same as default, graph spec fails - l4v run_tests: 29/51 passed - HaskellKernel STUCK as usual, CParserTest Failed, CBaseRefine TIMEOUT, AInvs TIMEOUT, a lot others SKIPPED due to dependency - graph-refine: There's no KeyError now because "kernel_devices" is present in this version of seL4 code, but I got this instead: ###======================================= ### Doing stack analysis for 'cap_get_capPtr'. (48 of 575) ### Traceback (most recent call last): ### File "graph-refine.py", line 31, in <module> ### args = target_objects.load_target_args () ### ... ### ... ### File "stack_logic.py", line 223, in get_ptr_offsets ### assert not fail_early, (v, ptr) ### AssertionError: ((3758178040, Expr ('Var', Type ('Word', 32), name = 'r13')), 'r13_after_3758178040_3758178040=i+0') ###===================================== Here are my questions: - Are these issues common, or is my setup & installations just wrong? Any way to resolve these issues? (big questions, and hence the long email, and hence I'm here asking the experts) - Is solver.py currently broken? (dug up some clues in seL4-example/Makefile) - for graph-to-graph, phantom_preempt.py seems required in the convert_loop_bounds step: Any guide on how to write this file, e.g. format, content? - To replicate the WCET experiment in the 2016 paper, should I download the specific version of the verification repo of that time? - static vs. measurement-based WCET analysis: Going forward, on more advanced ARM archs (e.g., Armv8), is static WCET analysis still worth it (or even feasible)? Is hybrid approach the way to go? Is the TS team still working on WCET tools for seL4 on ARM systems? (saw papers from the team many years ago discussing the combination of static cache analysis and probabilistic measurement) Regards, Jack

3 3

Too large messages
by Peter Chubb 05 Nov '21

05 Nov '21

There've been a few messages stuck in the queue recently because they're too large for the list. Please remember when sending to the Devel(a)sel4.systems list -- trim what you're replying to, to just the relevant bits -- reply in-line (no top-posting) -- send only plain text (not screen shots or HTML). Serial port output can be pasted in-line. This will maximise your chance of getting email through on first attempt. -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW

1 0

Re: Runtime Measurement Hiccup
by Hugo V.C. 05 Nov '21

05 Nov '21

Hi Michael! Adding the full list to the thread again (we missed them at some point...). "I appreciate the complete lack of partial credit, and I consider you find my work to be a waste." I don't think anyone thinks your work is a waste. Personally, I just gave my opinion about the architecture, but of course the final decision is yours, as it is your baby :) Maybe someone on the list can answer you with a more specific example you require (even if they already gave some hints...). Cheers, El lun, 25 oct 2021 a las 19:11, Michael Neises (<neisesmichael(a)gmail.com>) escribió: > Hugo (and Everyone), > > Thank you for the reminders. > > I believe it's trivial to provide or restrict caps to any IO device. So, > yes, I believe with the board's reference manual it should theoretically be > quite easy to restrict them all. > > I appreciate the complete lack of partial credit, and I consider you find > my work to be a waste. So with that in mind I'll ask once more: > > Has anyone on the planet ever performed such an independent measurement of > a virtual machine, or is seL4 really as unusable as indicated? > > I don't want to spend any amount of time barking up a tree that doesn't > exist. > > Cheers, > Michael Neises > > > > > > On Mon, Oct 25, 2021, 01:02 Hugo V.C. <skydivebcn(a)gmail.com> wrote: > >> Hi Michael, >> >> as I commented, it depends on the runtime environment. The scenario I >> described, even if challenging, it is just one of many you could face. Let >> me explain myself. >> >> Really, it is irrelevant if the full Linux (or whatever OS) VM is >> "inmutable". At some point you need to load code into memory and run it. >> Then, only formal verified code (like seL4) is reasonably secure. Being >> pedant, anything else simply it is not. >> Why? >> >> The reason is you will never be sure what interactions the VM OS (in your >> example Linux) will have with the outside World. Do you have NTP client...? >> HTTP clients...(wget)? DNS clients...? Are you absolutely sure you know >> every line of this VM OS (Linux) and can guarantee there will be no out of >> control interaction with the outside Word? >> >> Let's go a step ahead in the offensive mindset. Even in the case you are >> building a siloed "air gap" machine (no networking), do you have full >> awareness of all the I/O mechanisms of the device so you can guarantee >> there will be no interaction with the outside World...? >> >> For that reasons code is formally verified. That is the only way to be >> sure things are reasonably secure. >> >> If we accept the last statement as true, any integrity check done from >> inside of unverified code, is, by definition, not trustable. But of course >> you can do it. >> >> On the other side, what I don't get is, if you consider (for whatever >> reason) your guest OS is inmutable... then why you want to check integrity >> from inside...? >> >> In embedded World, integrity checks always need something (theoretically) >> really inmutable (i.e. CPU fuses). You need to check/anchor from the most >> trustable source you have. That's why in embedded devices there are those >> "funny" boot sequences with chain of trust where different parts of the >> system (from most simple to most complex) are used to verify the next step >> in the boot chain. >> >> Having said that, of course you can do integrity checks from inside the >> VM itself, but IMHO will be a waste of trusted computing power of seL4 >> platform. >> >> Please excuse me in advance if I misunderstood your message. >> >> A very interesting topic. >> >> Cheers, >> >> >> El lun., 25 oct. 2021 2:34, Michael Neises <neisesmichael(a)gmail.com> >> escribió: >> >>> Hugo and Everyone, >>> >>> Thanks for the response. This is something I've worried about as well. >>> >>> I've been under the impression that once I compile a seL4 image, that >>> image should be static no matter how many times I boot it. That is, I've >>> looked around for persistent storage to use, and my solution has so far >>> been to recompile the entire seL4 image in order to insert new data. So >>> even when I "touch" files in the Linux virtual machine, they are completely >>> forgotten when I reboot the system. For a time I thought of this as an >>> impediment, but I soon came to realize it as a benefit. So I suppose I >>> should clarify that when I said "Linux kernel" in that quote, I really >>> meant this particular Linux image which is prepared at compile-time and >>> virtualized by seL4 at runtime. >>> >>> For the last several months, I've been operating under the assumption >>> that there is no way for me, even as a developer, to "manipulate the seL4 >>> image I used to boot myself." Namely, I've been trying to jump through all >>> these virtual network hoops because I couldn't figure out a way to make >>> persistent changes to the image. So, as I said, I had taken it for granted >>> that a seL4 image was immutable in this way, but I recognize your point >>> that maybe it is not. My argument has been that the seL4 image is loaded >>> onto an SD card, and I can forbid access to that SD card, which means the >>> image should be guaranteed to be untouchable except maybe by the seL4 >>> kernel itself. >>> >>> I believe seL4's proofs uphold my argument regarding "capabilities" to >>> the SD card, but I admit a slim understanding of seL4's "caps." I will be >>> happy as always to be edified. >>> >>> Cheers and Good Evening to you, >>> Michael Neises >>> >>> On Sun, Oct 24, 2021 at 4:32 PM Hugo V.C. <skydivebcn(a)gmail.com> wrote: >>> >>>> Hi Michael, >>>> >>>> "Please correct me if I am wrong, but I think if the very first thing >>>> the Linux kernel does is measure itself, before it is even connected >>>> to a network, then there is simply no attack surface" >>>> >>>> My 5 cents: it is not so simple... it depends on the specfic run time >>>> environment. >>>> Anyway, just as an example, some years ago I was challenged with a >>>> similar scenario: an appliance running Linux firmware with an embedded >>>> integrity mechanism in the kernel code that checked its own integrity and >>>> also the integrity of all loaded kernel modules (that were doing integrity >>>> checks of the file system). Once initial modules were loaded no more were >>>> allowed to be loaded. >>>> Anyway, the running kernel was very outdated, so I was able to find a >>>> vulnerability that allowed me to inject my own data/code in the kernel >>>> space. The problem was persistence: most of the file system was read >>>> only... with the exception of some config files in the compact flash >>>> storage... a second bug in the parsing of the config files (that allowed >>>> user space command execution to trigger the kernel vuln) gave me the >>>> persistence I wanted for my kernel level vulnerability in that "inmutable" >>>> system. Game over. >>>> >>>> So, it really depends on your environment. As long you have I/O data >>>> operation were an attacker can interact to some persistent storage, then >>>> there's room for persistent intrusion no matter the runtime checks you do >>>> on the kernel or the file system. There have been plenty of even more >>>> elaborated attacks/tricks on heavily siloed and isolated and "inmutable" >>>> systems that have been carried out in the computing history. In fact, those >>>> are the interesting ones... :-) >>>> >>>> Hopes this helps. >>>> >>>> >>>> El dom., 24 oct. 2021 19:46, Michael Neises <neisesmichael(a)gmail.com> >>>> escribió: >>>> >>>>> Hello seL4 developers, >>>>> >>>>> Thank you for the replies. >>>>> >>>>> For the sake of clarity, the system works like this: >>>>> At compile time, some expected digest values are made available only >>>>> to a >>>>> distinct CAmkES component. At the time of first-Linux-boot, a kernel >>>>> module >>>>> takes several measurements of the other kernel modules present >>>>> (including >>>>> itself). It reports these digests outwards to CAmkES, where they are >>>>> compared against the expected values. It is the "pre-compile-time >>>>> provisioning of these expected digests" in which I am interested. At >>>>> this >>>>> time, I can simulate the system and compute these digests, but the >>>>> only way >>>>> I have to extract them is to copy them by hand off the screen. To be >>>>> totally explicit, I want to extract these values in order to re-compile >>>>> them into a system that knows its expected digest values. I want to >>>>> have an >>>>> initial simulation where I extract these digests, so that in the >>>>> subsequent compilation and simulations, the system is aware what values >>>>> these digests are required to take. >>>>> >>>>> Please correct me if I am wrong, but I think if the very first thing >>>>> the >>>>> Linux kernel does is measure itself, before it is even connected to a >>>>> network, then there is simply no attack surface. Of course I'm very >>>>> happy >>>>> to be wrong, but I don't see who the attacker is in this situation. >>>>> Certainly, there remains an open question of how to extend these >>>>> measurements meaningfully into the space where there is a viable attack >>>>> surface (after enabling a network adapter), but I consider that >>>>> question to >>>>> be beside the point for now (some future work). If there is some way >>>>> for me >>>>> to inspect the run-time data of the Linux system without relying >>>>> somewhat >>>>> on a tool inside the Linux instance, I would very much like to know >>>>> about >>>>> it. My strategy follows the same path as the vm-introspect example app >>>>> (which I'm under the impression was created for this explicit purpose), >>>>> which itself trusts implicitly the Linux instance. Again, to be >>>>> entirely >>>>> explicit, there does not appear to be any information anywhere on a >>>>> way to >>>>> meaningfully inspect a virtualized Linux system without trusting it >>>>> even >>>>> the slightest bit. I would be elated to be corrected; if someone can >>>>> show >>>>> me how to scrape (from the seL4 side exclusively) all the bits from a >>>>> virtual Linux system and reassemble those bits into >>>>> semantically-valuable >>>>> information, I'm sure you will not hear from me for several months >>>>> while I >>>>> rebuild everything I have. At this time that does not appear to be >>>>> possible. >>>>> >>>>> Cheers, >>>>> Michael Neises >>>>> >>>>> On Tue, Oct 19, 2021 at 3:46 PM Michael Neises < >>>>> neisesmichael(a)gmail.com> >>>>> wrote: >>>>> >>>>> > Hello seL4 developers, >>>>> > >>>>> > I want to be able to retrieve data from seL4's virtual Linux >>>>> machine, in >>>>> > order to store it in a persistent way. Namely, I want to be able to >>>>> > simulate a seL4 kernel, boot its Linux virtual machine, compute some >>>>> hash >>>>> > digests, and then export those hash digests. These digests are >>>>> valuable >>>>> > because they represent the "clean room" runtime-state of the linux >>>>> machine. >>>>> > Currently I can export these digests by way of hand-eye >>>>> coordination, but I >>>>> > consider this unusable as a piece of software. >>>>> > >>>>> > To date I've taken two main approaches: CAmkES FileServer or virtual >>>>> > networking. I'm under the impression that the FileServer changes are >>>>> not >>>>> > persistent through reboot, and even if they were, to change the boot >>>>> image >>>>> > after compile-time would seem to fly in the face of seL4's >>>>> principles. >>>>> > Virtual networking seems to promise I can host my digests on a >>>>> webpage that >>>>> > is visible to my "root host" machine; that is, the simulated seL4's >>>>> linux >>>>> > instance hosts a site available on my 192.168.x.x network. I know >>>>> there is >>>>> > a seL4webserver app as part of the seL4 repositories which claims to >>>>> do >>>>> > this, but unfortunately its prose is unhelpful and it doesn't seem >>>>> to work >>>>> > even when it compiles and simulates. >>>>> > >>>>> > I've taken two distinct strategies to investigate the virtual network >>>>> > approach. First, I tried to get it to work on my normal stack: >>>>> Windows 10 >>>>> > using WSL2 using a Docker container to simulate the seL4 image. The >>>>> problem >>>>> > with this approach is that it appears I'm required to blindly thread >>>>> 3 or 4 >>>>> > needles all at once, without getting feedback more descriptive than >>>>> "you >>>>> > didn't do it." In other words, there does not appear to be a partial >>>>> > success available, and without ICMP ping, I honestly have no idea >>>>> how to >>>>> > debug these "virtual" networks. >>>>> > >>>>> > Next, I tried simplifying my stack by installing the dependencies >>>>> natively >>>>> > on a Debian 10 machine, which should bypass several layers of the >>>>> virtual >>>>> > network I was suggesting in my first strategy. Unfortunately, I met >>>>> with >>>>> > the same "AttributeError: module 'yaml' has no attribute >>>>> 'FullLoader'" >>>>> > error that inspired me to begin using Docker several years ago. Of >>>>> course I >>>>> > should note that "pip/pip2/pip3 install pyyaml" all report that >>>>> pyyaml is >>>>> > already installed, so I would be in debt to anyone who has an idea >>>>> about >>>>> > that error. >>>>> > >>>>> > To conclude, I find virtual networks opaque, and I would be grateful >>>>> for >>>>> > any guidance. If you have a different idea how I might achieve my >>>>> goal, I >>>>> > would be similarly effusive in my thanks. >>>>> > >>>>> > Cheers, >>>>> > Michael Neises >>>>> > >>>>> _______________________________________________ >>>>> Devel mailing list -- devel(a)sel4.systems >>>>> To unsubscribe send an email to devel-leave(a)sel4.systems >>>>> >>>>

4 7

Pine64 PinePhone with seL4: any prior attempts?
by Isaac Beckett 03 Nov '21

03 Nov '21

Hello! I recently received a PinePhone for my birthday, and it finally arrived a few weeks later. It’s been fun to tinker with so far, although I haven’t yet replaced the Linux distro it came with yet, which I plan to do soon. But thinking about my options for that made me wonder, has anyone attempted to run seL4, even just a test program, on one of these before? It’s an aarch64 device using a quad-core Allwinner A64 SOC, so four Cortex CPU cores and an Arm Mali GPU. I don’t have any experience bringing up an OS in new hardware. It runs Linux fine, and while the included software setup is a bit sluggish, I’m pretty sure that’s just from Plasma mobile being very resource hungry. So, I’m curious, has anyone experimented with this in the past? I think this platform could be very useful, personally I’m hoping that as hobbyist type phones like this become more mature, that people will have more choices for software to run on it.

3 2

CAmkES: dataports larger than 4k
by Fabrizio Bertocci 01 Nov '21

01 Nov '21

Is it possible to use dataports that are larger than 4k? I tried with both typed dataports and "Buf" dataport but I can't find a way to do it. In the hello-camkes-2 tutorial, I tried to add a configuration for my dataports in the main assembly file to increase its size like this: // Typed dataport name: 'd_image' // Buf dataport name: 'd' configuration { echo.d_size=65536; // Buf dataport echo.d_image_size=65536; // Typed dataport } unfortunately that doesn't seem to do anything as d_get_size() keep returning 4k, and for the typed dataport, the build system triggers the static assert "typeof(from_0_d_image_data) size greater than dataport size" Thanks, Fabrizio

2 1