January 2017 - Devel - lists.sel4.systems

config-independent object type numbers
by Corey Richardson 10 Jan '17

10 Jan '17

Right now, object type numbers vary based on the kernel config (eg, CONFIG_VTX) etc. This is a huge source of pain for the Rust userspace libraries which don't integrate with seL4's build system. Is it possible for those enums to explicitly label every potential object type for a given architecture with a fixed number? -- cmr http://octayn.net/ +16038524272

2 2

seL4 as Xen guest / AWS
by Tony Arcieri 10 Jan '17

10 Jan '17

Has anyone managed to run seL4 as a Xen HVM guest? I was more specifically curious about running seL4 on an EC2 instance. I was curious about the possibility of using seL4 as the host OS for a "unikernel"-like deployment of a Rust application split into a small set of services living in different capability spaces (e.g. network, key storage / crypto) -- Tony Arcieri

3 3

sel4test 4.0.x.xml broken?
by Corey Richardson 09 Jan '17

09 Jan '17

It seems that the line <project name="seL4.git" path="kernel" revision="4.0.x-compatible"/> should be <project name="seL4.git" path="kernel" revision="4.0.0"/> Either that, or a tag is missing from the kernel repo. -- cmr http://octayn.net/ +16038524272

2 1

questions about the vgic maintenance for sel4 TK1 ARM VMM
by PX 09 Jan '17

09 Jan '17

Hi, all I have questions about the vgic maintenance for sel4 tk1 ARM VMM. When the VM acknowledges an IRQ, an exception is raised and is delivered to the VMM. Could someone explain how seL4 intercepts the VM ack? How is this exception is raised ? I am confused because the VM is supposed to totally control the MMIO of the device and can write any thing to the device. How can seL4 be triggered in this case? Which part of source code allows seL4 to intercept the VM ack? Thanks Peng

2 1

Interest in 32-bit x86 Rust userspace?
by Corey Richardson 07 Jan '17

07 Jan '17

Is anyone interested at all in the 32-bit x86 Rust userspace libraries? I'm considering dropping support for them, as I don't personally plan to have any support for them in Robigalia, instead focusing on x86_64. Note that this wouldn't impact any Rust CAmkES components using the support in the sel4 buildsystem, just the sel4-sys, rust-sel4, etc crates. -- cmr http://octayn.net/ +16038524272

1 0

DMA driver in VM
by PX 07 Jan '17

07 Jan '17

Hi, I have a generic question about DMA driver in the VM on sel4. How does the device driver in the vm put physical address in the DMA controller given that there is no emulation in sel4? I worked on TK1 sel4 hypervisor extention version, but cannot find any address translation from vmm. Thanks Peng

1 0

pic/no-pic and some other questions
by Vasily A. Sartakov 06 Jan '17

06 Jan '17

Greetings. I have merged MIPS port with 4.0.0 release. Now I would like to clean up my code and need to remove many small issues that I did not fix during the porting before making the code public. In fact, most of the current problems are related to toolchains: 1. The first problem is a position independent code. Could you please describe me seL4' vision about it? muclibs is building with -fPIC, but everything else doesn't, right? I have a very tricky set of GCC’ flags, related to MIPS’ GOT, small data, abicalls, pic/non-pic, etc, and many of them are not working together. 2. MIPS assembler has several features, one of them is that the -O0 code requires having an addition space above the top of the stack for 4 registers: > 43b610: 27bdffe8 addiu sp,sp,-24 <— start of the function > 43b614: afbf0014 sw ra,20(sp) > 43b618: afbe0010 sw s8,16(sp) > 43b61c: afb0000c sw s0,12(sp) > 43b620: 03a0f021 move s8,sp <— frame stack > 43b624: afc40018 sw a0,24(s8) <— save 1st arg for a subroutine call > 43b628: afc5001c sw a1,28(s8) <— save 2nd arg for the subroutine > 43b62c: afc60020 sw a2,32(s8) <— save 3rd arg for the subroutine So, each time when I am allocating new stack I should return not top of the stack, but top_of_the_stack - 4*sizeof(seL4_Word). As result, sel4utils_configure_thread_config becomes platform specific. Could you please consider a possibility to put it into the «arch» as sel4utils_arch_init_context, or add something like «sel4utils_arch_configure». Also, it is important: this is an issue only for -O0 code, as far I see, -O2 uses different methods for arguments passing. I am trying to build toolchains which do not use frame pointer this style for -O0 code, but I am not sure about the result. 3. I really like how you redesigned declaration syscalls. Now I have a freedom to modify syscalls and do not care about the mainline declarations because now there are syscall wrappers. However, my toolchain generates very poor code for CONFIG_LIB_SEL4_PUBLIC_SYMBOLS and «DEFAULT» — I have proper working code only for CONFIG_LIB_SEL4_INLINE_INVOCATIONS. What is the conceptual difference of these declaration attributes, what they affect? 4. Could you please tell me what was the C equivalent of this asm code: .global __syscall .type __syscall,%function __syscall: sub sp, sp, #4 push {r5,r6} adr r5, 1f ldr r6, 1f ldr r5, [r5,r6] str r5, [sp, #8] pop {r5, r6} pop {pc} .hidden __sysinfo 1: .word __sysinfo-1b something similar to __syscall6 from libmuslc/arch/<arch>_sel4/syscall_arch.h, right? Thank you. P/s Happy new year/merry xmass/happy holidays! -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 2

xsave region size for haswell/broadwell?
by Corey Richardson 06 Jan '17

06 Jan '17

Does anyone have a "maximal" xsave region size big enough for all the xsave-supporting features seL4 enables on Broadwell or Haswell? I don't have access to a machine with these features, so I can't run a program to get them with cpuid. -- cmr http://octayn.net/ +16038524272

2 1

questions about the address translation for a DMA driver in the ARM VM
by PX 05 Jan '17

05 Jan '17

Hi, all Happy new year! I have some urgent questions about address translation for a DMA driver in the ARM seL4-based VM. Your quick response is highly appreciated! 1. In the ARM sel4-based VM, the MMIO of a device is directly exposed to the device driver in the VM. When the DMA device driver allocates a DMA buffer to a device controller, the device driver can directly tell the real controller the IPA of the buffer starting address, instead of the real physical address. In other words, the device controller can only get the IPA of the buffer starting address. How can this device controller perform DMA without knowing the real PA of the buffer? Does seL4 perform some emulation here? How? 2. A closely related question to 1: when we develop a DMA driver in the VMM space, we put the real physical address of the device descriptor and real physical address of the DMA buffer in the controller registers through its MMIO. We found that the controller cannot find the correct place for the descriptor and the buffer. Do the seL4 hypervisor perform the address translation? If so, which source code does that? Thanks Peng

2 3

Build Error
by Daniel Romero 05 Jan '17

05 Jan '17

Hi, I am currently on a BeagleBone running Ubuntu 14.04 using gcc-arm-none-eabi. However I am getting the following error running 'make' after 'make menuconfig'. I am wondering if someone can guide me in the right direction [libs/libsel4] building... [GEN] include/sel4/types_gen.h Traceback (most recent call last): File "/home/ubuntu/seL4test/libs/libsel4/tools/bitfield_gen.py", line 26, in <module> from six.moves import range ImportError: No module named six.moves make[1]: *** [include/sel4/types_gen.h] Error 1 make: *** [libsel4] Error 2 Thank you, Hector Daniel Romero hdromero93(a)gmail.com

2 1