July 2016 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 30 Jan '25

30 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

IA32 syscall bindings
by Norman Feske 26 Aug '16

26 Aug '16

Dear seL4 developers, first, I'd like to thank you for publishing seL4 under GPL. I am very happy that I can finally get my hands dirty with working with the kernel of your group. :-) Currently, I am taking the first baby steps to bring the Genode OS framework (http://genode.org) to seL4. For reference, I am using the experimental branch. The first smallish issue I stumbled upon stems from the fact that Genode is written in C++. By compiling the seL4 syscall bindings with a C++ compiler, I got the following error: error: inconsistent operand constraints in an ‘asm’ It can be reproduced by putting the following code snippet into a cc file and compiling it with 'g++ -m32 -c' (tested with the Genode tool chain as well as with GCC 4.8.1): typedef enum { seL4_SysDebugPutChar = -9, _enum_pad_seL4_Syscall_ID = (1U << ((sizeof(int)*8) - 1)) } seL4_Syscall_ID; void seL4_DebugPutChar(char c) { asm volatile ( "pushl %%ebp \n" "movl %%esp, %%ecx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "popl %%ebp \n" : : "a" (seL4_SysDebugPutChar), "b" (c) : "%ecx", "%edx", "%esi", "%edi", "memory" ); } When compiling the same code snippet with 'gcc' instead of 'g++', everything is fine. It turns out that the C++ compiler does not like the enum value to be specified as input argument. I found the following ways to circumvent this problem: * Changing the enum value 'SysDebugPutChar' to a positive value, * Removing the definition of '_enum_pad_seL4_Syscall_ID', * Casting 'seL4_SysDebugPutChar' to an integer: : "a" ((int)seL4_SysDebugPutChar), In any case, I seem to have to change the bindings. Do you see a way around it? If not, would you consider one of the solutions above for the seL4 headers? On another note, I noticed that the bindings use the EBX register. Unfortunately, this makes it impossible to compile seL4 userland software as position-independent code (PIC). E.g., when compiling the above code snippet via 'g++ -m32 -fPIC -c', the following error occurs: error: inconsistent operand constraints in an ‘asm’ However, PIC is required in order to use shared libraries. The solution would be to not use EBX to pass arguments to the 'asm' statements, save EBX on the stack prior moving the respective kernel argument to the register, and, of course, restoring it after sysenter returns. Before I start changing the bindings, I'd like to know: is there anyone else working on the same problem? Would you be open to accept a change of the bindings to become PIC compliant on the costs of a few added instructions? Or do you have another suggestion how I should go about it? Best regards Norman -- Dr.-Ing. Norman Feske Genode Labs http://www.genode-labs.com · http://genode.org Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

4 7

syscalls and tlb
by Vasily A. Sartakov 26 Aug '16

26 Aug '16

Greetings. I am working on MIPS port of seL4. Now I can run very simple hello world application which reads and dumps bootinfo page. In other words, I modified elfloader, added platform and architecture support to the kernel, add _sel4_start for mips in libsel4platsupport, adopted mips support of libmuslc to work with __sysinfo in mips and more. Now I have some questions. I see that for different ‘syscalls' muslc uses different routes but with the same end. For example, SYS_ioctl from __stdout_write uses __syscall, provided by libmuslc/arch/<arch>/syscall_arch.h (implemented as CALL_SYSINFO). In the same time, syscall_cp function from __stdio_write is implemented inside libmuslc/src/internal/<arch>/syscall.s which uses __sysinfo in turn. So, that question is why? The second question is about the kernel. Now I am using static configuration of TLB in kerne: I have one region for rootserver aligned to 2MB, and one region for boot info page (also aligned). Thus, I do not have tlb traps since everything is in the TLB. In future, of course, I should add a processing of TLB misses somewhere in the plat/arch part of kernel. I am not familiar with memory support in seL4 yet, is there any syscall for delivery tlb traps? (I see nothing similar) Is there any check inside, for example, SEND call, about a presence of page in TLB? thank you. -- Vasily A. Sartakov sartakov(a)ksyslabs.org

4 5

beaglebone ethernet support
by Julien Delange 27 Jul '16

27 Jul '16

Hello, I noticed that there is some source code to support the ethernet driver of the beaglebone black. I look especially in projects/seL4_libs/libsel4platsupport/src/plat/am335x/cpsw_beaglebone.c According to https://github.com/seL4/seL4_libs/blob/master/libsel4platsupport/src/plat/a… the file has been introduced by NICTA - I am wondering if there is any existing example/support for it. In a nutshell, I am trying to use the ethernet driver. I started to integrate the startcode from TI on a camkes application before discovering this code. So, is there any sample application to use it? It is supported/working? Thanks for any help, Julien.

1 0

sel4 on Hikey board
by rahul mahadev 26 Jul '16

26 Jul '16

Hi , I'm trying to run sel4 on a hikey board, I'm following this wiki https://wiki.sel4.systems/Hardware/HiKey . I'm having issues as the link to the linaro-edk2 patch does not work(asks for some auth) , can someone provide another link or direct me . Thank you

2 1

Image lies outside of usable physical memory
by Alexander Boettcher 22 Jul '16

22 Jul '16

Hi, I want to boot seL4 (x86) 3.2.0 on a native machine (Lenovo X201) and I get a message like: End of loaded userland image lies outside of usable physical memory seL4 called fail at sel4/src/arch/x86/kernel/boot_sys.c: in function boot_sys, saying "boot_sys failed for some reason :( (Full log below attached) It seems that our used bootloader put the image to high in physical memory for seL4 (the other x86 kernels we use don't complain so far). Is this right that only memory below PPTR_TOP (0x1fc00000 on x86 3.2.0) can be used for the initial boot modules? Can this be changed or should we not try to touch this define (it seems to be derived from various other defines). Is there maybe a description about the required physical memory layout of the kernel and why it has to be as it is? Just in order to understand better the constraints we probably have to apply to our bootloader ;-) Thanks in advance, Alex. Parsing GRUB physical memory map Physical Memory Region from 0 size 89000 type 1 Physical Memory Region from 89000 size 17000 type 2 Physical Memory Region from d2000 size 2000 type 2 Physical Memory Region from dc000 size 24000 type 2 Physical Memory Region from 100000 size bb17c000 type 1 Adding physical memory region 0x100000-0x1fc00000 Physical Memory Region from bb27c000 size 6000 type 2 Physical Memory Region from bb282000 size dd000 type 1 Physical Memory Region from bb35f000 size 12000 type 2 Physical Memory Region from bb371000 size 81000 type 4 Physical Memory Region from bb3f2000 size 1d000 type 2 Physical Memory Region from bb40f000 size 60000 type 1 Physical Memory Region from bb46f000 size 1f9000 type 2 Physical Memory Region from bb668000 size 80000 type 4 Physical Memory Region from bb6e8000 size 27000 type 2 Physical Memory Region from bb70f000 size 8000 type 1 Physical Memory Region from bb717000 size 8000 type 2 Physical Memory Region from bb71f000 size 4c000 type 1 Physical Memory Region from bb76b000 size c000 type 4 Physical Memory Region from bb777000 size 3000 type 3 Physical Memory Region from bb77a000 size 7000 type 4 Physical Memory Region from bb781000 size 1000 type 3 Physical Memory Region from bb782000 size 9000 type 4 Physical Memory Region from bb78b000 size 1000 type 3 Physical Memory Region from bb78c000 size 13000 type 4 Physical Memory Region from bb79f000 size 60000 type 3 Physical Memory Region from bb7ff000 size 1000 type 1 Physical Memory Region from bb800000 size 800000 type 2 Physical Memory Region from bc000000 size 4000000 type 2 Physical Memory Region from e0000000 size 10000000 type 2 Physical Memory Region from feaff000 size 1000 type 2 Physical Memory Region from fec00000 size 10000 type 2 Physical Memory Region from fed00000 size 0 type 2 Physical Memory Region from fed1c000 size 4000 type 2 Physical Memory Region from fed20000 size 70000 type 2 Physical Memory Region from fee00000 size 1000 type 2 Physical Memory Region from ff000000 size 1000000 type 2 Physical Memory Region from 0 size 38000000 type 1 Kernel loaded to: start=0x100000 end=0x147000 size=0x47000 entry=0x10003e ACPI: RSDP paddr=0xf68e0 ACPI: RSDP vaddr=0xdfcf68e0 ACPI: RSDT paddr=0xbb7f07a2 ACPI: RSDT vaddr=0xdfff07a2 ACPI: DMAR paddr=0xbb781000 ACPI: DMAR vaddr=0xdff81000 ACPI: IOMMU host address width: 36 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1d fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1a fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x2 fun=0x0 ACPI: 3 IOMMUs detected ACPI: MADT paddr=0xbb7feb45 ACPI: MADT vaddr=0xdfffeb45 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_APIC apic_id=0x1 ACPI: MADT_APIC apic_id=0x4 ACPI: MADT_APIC apic_id=0x5 ACPI: MADT_IOAPIC ioapic_id=1 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: 4 CPU(s) detected Detected 4 CPUs. Only just 1 Detected 1 boot module(s): module #0: start=0x7fc7a000 end=0x7ffff338 size=0x385338 name='/image.elf' ELF-loading userland images from boot modules: size=0x385000 v_entry=0x2000000 v_start=0x2000000 v_end=0x2385000 p_start=0x80000000 p_end=0x80385000

2 1

3.1.0 to 3.2.0 (x86) upgrade issue
by Alexander Boettcher 22 Jul '16

22 Jul '16

Hello, after upgrading the seL4 kernel (x86) from 3.1.0 to 3.2.0 we get for the very first invocation of seL4_X86_Page_Map an errorcode of *3* (seL4_IllegalOperation). We bisected the commits between 3.1.0 and 3.2.0 and [0] is the first bad commit for us. If we use the 3.2.0 release with [0] reverted on top than everything works as before - so no changes to Genode/seL4 as used for the 3.1.0 kernel are necessary. It's a know issue, or maybe something changed which must be adjusted in userland/roottask ? Thanks, Alex. [0] https://github.com/seL4/seL4/commit/c8819792d76ae5aecd89bcff656ca561e62959a5

2 2

Re: [seL4] [sel4utils question] stack size of the second process
by Kofidoku.Atuah＠data61.csiro.au 21 Jul '16

21 Jul '16

Hi, Our malloc currently uses mmap() for large allocations (and therefore the matching munmap() for freeing those large allocations). See https://github.com/seL4/musllibc/blob/sel4/src/malloc/malloc.c#L352. So while the mmap() call is implemented, the munmap() call is not, and this is why you're seeing this issue with "syscall 91" not being successful: https://github.com/seL4/musllibc/blob/sel4/arch/i386/bits/syscall.h#L92 https://github.com/seL4/musllibc/blob/sel4/arch/arm/bits/syscall.h#L67 ? Usually you allocate such a big chunk of memory for private use and management, so free() probably isn't a mission critical thing here (for the tutorials), unless there are factors I can't see -- let me know if this was helpful -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO E kofidoku.atuah(a)csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61

1 0

[sel4utils question] stack size of the second process
by Norrathep Rattanavipanon 21 Jul '16

21 Jul '16

Hi, So I followed hello-4 example. I can create a static array inside a second process (hello-4-app) and the second process works fine. However, when I try to increase the size of an array to 80,000 bytes, the second process wont start. I tried to increase ALLOCATOR_VIRTUAL_POOL_SIZE but it still does not work. Any help would be appreciated. Thanks, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

1 1

Re: [seL4] [sel4utils question] stack size of the second process
by Kofidoku.Atuah＠data61.csiro.au 20 Jul '16

20 Jul '16

Hi, Thanks for popping by! The answer to the question in the subject line of your email (stack size of processes spawned by sel4utils_configure_process()) is that sel4utils_configure_process() calls sel4utils_configure_thread(), which allocates the stack using vspace_new_pages(), found here: (https://github.com/seL4/seL4_libs/blob/master/libsel4vspace/include/vspace/…) The stack size is determined by CONFIG_SEL4UTILS_STACK_SIZE, which can be set in your `make menuconfig` settings. Try: `make menuconfig` -> select "seL4 Libraries" -> "libsel4utils" and change the stack size as desired. That said, > However, when I try to increase the size of an array to 80,000 bytes, the second process wont start. I tried to increase ALLOCATOR_VIRTUAL_POOL_SIZE but it still does not work. Sorry, I'll need to know a bit more about what's going on here: could you post some more detailed output, or maybe a diff, so I can try to aid you? --Yours truly, Kofi

1 0