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
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
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.
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
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
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
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#L92https://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
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
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