Devel November 2014

devel@sel4.systems

12 participants
11 discussions

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

Progress of bringing Genode to seL4
by Norman Feske 26 May '15

26 May '15

Hello, I have written up the first of a series of articles about using seL4 as base platform for the Genode OS framework: http://genode.org/documentation/articles/sel4_part_1 I hope that it contains useful bits of information for novices of seL4 and Genode alike. Even though the article outlines a few hurdles, the overall experience of using the kernel had been overly positive so far. For those of you interested in tracking the progress of the ongoing work, here is the corresponding topic branch: https://github.com/nfeske/genode/commits/sel4 Cheers 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

wrong word spelling in program
by XilongPei(裴喜龙) 27 Nov '14

27 Nov '14

Hi, Who wrote the program in file $/libplatsupport/plat_include/omap4/platsupport/plat/gpt_constants.h , GPT4_DEFICE_PADDR is wrong spelled, it should be GPT1_DEVICE_PADDR. static void *paddrs[] = {(void *) GPT1_DEVICE_PADDR, (void *) GPT2_DEFICE_PADDR, (void *) GPT3_DEFICE_PADDR, (void *) GPT4_DEFICE_PADDR, (void *) GPT5_DEFICE_PADDR, (void *) GPT6_DEFICE_PADDR, (void *) GPT7_DEFICE_PADDR, (void *) GPT8_DEFICE_PADDR, (void *) GPT9_DEFICE_PADDR, (void *) GPT10_DEFICE_PADDR, (void *) GPT11_DEFICE_PADDR}; Xilong Pei Tongji University 2014/11/19

2 1

Confused on porting/using musl lib c
by chengkunck＠gmail.com 27 Nov '14

27 Nov '14

Hi All, I want to use musl lib c but I'm a little confused on the following two projects: libmuslc and musllibc. I went through their Kconfig and brief intros, so my question now is do I need them both to port/use musl lib c on sel4? It might be a dumb question but I'm stuck here, any help is appreciated. Best regards, Kenneth

2 2

where can I get beagle_run_elf program
by XilongPei(裴喜龙) 21 Nov '14

21 Nov '14

Hi, In the Makefile, a program beagle_run_elf is referred, Where can I get it? --------------------------------------- # This relies on a helper script to build a bootable image simulate-beagle: beagle_run_elf images/sel4test-driver-image-arm-omap3 --------------------------------------- Xilong Pei Tongji University 2014/11/19

2 1

run seL4 on pandaboard
by Pei.XiLong(裴喜龙) 14 Nov '14

14 Nov '14

Hi, I have built an image for my pandaboard, but I have no bootelf u-boot command, I use go command instead, get the following error: Panda # fatload mmc 0 0x82000000 sel4test-driver-image-arm-omap3 Panda # go 0x82008000 ## Startting application at 0x82008000 ... after this message, the system is dead. How to do next? Xilong Pei Tongji University 2014/11/14

1 0

Re-identification of capabilities
by Norman Feske 13 Nov '14

13 Nov '14

Hello, I hope you don't mind me spamming the list with my problems. I have a question about the association of capabilities with process-local meta data. As far as I understand, the "badging" of capabilities is the recommended mechanism for servers to attach a server-local meaningful value to a capability. After having handed out the capability to a client, it gets this value reported each time the client (or any other process to which the capability was delegated to) invokes the capability or delegates the capability back to the server (e.g., as RPC argument). Now, I have the following scenario: There are three processes, a factory (F), a mediator (M), and a client (C). The factory is responsible for physically allocating objects (e.g., in Genode's case, one example would be the core process that hands out dataspaces). The mediator is a process that sits in-between the client and the factory (in the Genode world, this could the the init process). It keeps records about the allocation and may use this information to implement a policy. The client is the designated user of the object. To create an object, C will call M, which, in turn, will call F on behalf of C: alloc create F <-------- M <--------- C F will create the actual object and a corresponding badged capability and returns the badged capability as return value to M. Because M wants to keep records about the lifetime and parameters of the created objects, it needs to associate a process-local meta-data structure to the capability. badged cap F ---------> M C : (meta data <-> cap) M stores the meta data in a process-local data base using the cap as key. It then hands out the cap to the actual client. Sometime later, the client decides to destroy the object (or perform another operation at M that takes the cap as argument): badged cap F M ---------> C | | uses object (e.g., invoking the cap) destroy | (cap arg) | ? <----------+ When M receives the destroy request with the cap of the to-be-destroyed object as argument, it wants to look up the corresponding meta data from its data base. But unfortunately, the cap argument of the destroy function got assigned a new local name within M (some number within the receive window of M). How can M find the meta data associated with the allocated object? 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

5 8

the omap3 image can't run on pandaboard
by XilongPei(裴喜龙) 13 Nov '14

13 Nov '14

Hi, The OMAP3 Beagle board is too out of date, I buy a pandaboard http://omappedia.org/wiki/PandaBoard , but the omap3 image can't run on this board. The error information look like these: ----------------------------------------------------------------- Panda # Panda # fatls mmc 0 31644 mlo 208784 u-boot.img 4782336 uimage 208273 uinitrd 449 boot.scr 3092757 sel4test-driver-image-arm-omap3 9 file(s), 0 dir(s) Panda # fatload mmc 0 0x81ff8000 omap3 reading sel4test-driver-image-arm-omap3 3092757 bytes read Panda # go 0x82000000 ## Starting application at 0x82000000 ... data abort MAYBE you should read doc/README.arm-unaligned-accesses pc : [<820024bc>] lr : [<82002194>] sp : 822d7f78 ip : 00000000 fp : 822d7f84 r10: 00000002 r9 : 00000000 r8 : bfefdf68 r7 : bffabd14 r6 : 82000000 r5 : bfeffd5c r4 : 00000002 r3 : 49020014 r2 : 00000001 r1 : 00000000 r0 : 0000000a Flags: Nzcv IRQs off FIQs off Mode SVC_32 Resetting CPU ... resetting ... ----------------------------------------------------------------- Who can give me some help? thanks first! Xilong Pei Tongji University Shanghai China 2014/11/13

1 0

seL4 : Queries
by Yashwardhan Singh 10 Nov '14

10 Nov '14

Hi I am trying to modify the seL4 scheduler as a part of my project. I was wondering if there is any function present in the library OS like scanf which can help me in writing an interactive process , to measure the response time of the scheduler for interactive process. I was also curious if there is any shell like framework for sel4, from which multiple processes can be started concurrently and so that they run in background. Is there a benchmark suite for generation of performance metrics using the data structures present in /kernel/src/arch/ia32/api/benchmark. Please help. Thanks and Regards Yash

2 1

Clang & LLVM
by da Tyga 08 Nov '14

08 Nov '14

Hi ! There seems to be a general trend towards using Clang / LLVM in the ARM area. AFAIK ARM are going LLVM for V8. Is it viable to do seL4 work with that environment? Cheers!

1 0

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel November 2014