Devel October 2014

devel@sel4.systems

20 participants
15 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

Make Error : seL4 kernel
by Yashwardhan Singh 29 Oct '14

29 Oct '14

Hi I downloaded the latest repository of seL4 from GitHub. When I am trying to build the kernel using make for ia32 architecture and pc99 platform I am getting this error : *yashward@macaroni-09:~/cs736-proj/seL4$ make ARCH=ia32 PLAT=pc99* * [CC] kernel_final.s* *src/arch/ia32/kernel/boot_sys.c:75:26: error: ‘CONFIG_MAX_NUM_IOAPIC’ undeclared here (not in a function)* * paddr_t ioapic_paddr[CONFIG_MAX_NUM_IOAPIC];* * ^* *src/plat/pc99/machine/hardware.c: In function ‘maskInterrupt’:* *src/plat/pc99/machine/hardware.c:54:9: error: implicit declaration of function ‘pic_mask_irq’ [-Werror=implicit-function-declaration]* * pic_mask_irq(mask, irq);* * ^* *src/plat/pc99/machine/hardware.c:54:9: error: nested extern declaration of ‘pic_mask_irq’ [-Werror=nested-externs]* *cc1: all warnings being treated as errors* *make: *** [kernel_final.s] Error 1* I am trying to compile it on a 64 bit machine with red hat linux machine operating system on it. Please help me with this issue. Regards Yash

2 1

A missing function?
by chengkunck＠gmail.com 29 Oct '14

29 Oct '14

Hello everyone, Currently I'm going through the source code of seL4. I find function in seL4\src\object\Tcb.c that I can't find it's definition. In line 59, tcbSchedEnqueue calls a function 'thread_state_ptr_set_tcbQueued(&tcb->tcbState, true)'. However, even with the help of Source Insight I still can't locate the definition of 'thread_state_ptr_set_tcbQueued' . Does anyone know where it is ? Thanks in advance. Best regards, Kenneth.

3 4

Dynamic number of arguments in interface method
by Lukas Masek 27 Oct '14

27 Oct '14

Hello Everyone, I'm trying to implement interface which will accept similar syntax like printf method in c is accepting. syntax of function in c: void printer(int i,char* format,...){ } However I have problem to create valid syntax in idl4 interface definition for CAmkES. Can somebody help me to create valid syntax for procedure definition used in interface? procedure Test { void printer(in int i,in string format,in ...); }; Or is this approach even supported? Also If there is more complex reference guide for idl4 used by CAmkES which I can use to find answers like this? Thank you for help and if question is stupid please accept my apologize I'm just starting to play with this project. BR, Casper

2 1

sel4 on multi-core
by Yuxin Ren 21 Oct '14

21 Oct '14

Hi All, I think, on IA-32, sel4 supports multi-core machine. But I do not how to use that. Here I have two specfic questions. 1. How to assign a specific core to a process/thread? And can I change this affinity? 2. How to two process/threads communicate via IPC on different cores? I want to know some implementation details in kernel to support cross-core IPC. Could anyone explain its logic or tell me the code for it in the kernel? Thank you very much. Best, Yuxin

6 6

IPC performance for slowpath
by Yuxin Ren 19 Oct '14

19 Oct '14

Hi All, I find there have slow and fast path for IPC. I want to know the performance difference between those two. More accurate, on x86, how many cycles for slow path round-trip ipc between two address space?(on single core) And how many for fast path? Thank you very much. Yuxin

2 3

How to get a capability of a virtual address
by Yuxin Ren 18 Oct '14

18 Oct '14

Hi All, In sel4, how can a process/thread get the capability of its virtual address? I know there is function vspace_get_cap(vspace_t *vspace, void *vaddr) But how can I know the current vspace the process/thread is in? Thank you very much. Yuxin

3 5

Where to begin for Linux on seL4 x86?
by Robert Brewer 16 Oct '14

16 Oct '14

I'm new to seL4 (and L4 generally). I'd like to initially run my application functionality in Linux on top of seL4 (x86) and then over time migrate pieces of its functionality to run directly on seL4 to achieve finer-grained confinement. I'm having trouble finding any instructions on how to run a Linux environment on top of seL4. Either paravirtualized or hardware virtualized would be ok. So far I found pointers to L4Linux but it appears to need L4Re. Can anyone point me in the right direction? Thanks, Rob

3 3

Get a mapping for physical memory
by Yuxin Ren 14 Oct '14

14 Oct '14

Hi All, I am a very beginner for sel4, and I very little about its APIs. Now I have a physical address of memory, I want to know if this address is mapped into my virtual address space. And if so, how can I know what virtual address t is mapped in? Furthermore, how can I share this piece of memory with another process/thread? I find there is a function "simple_get_frame_mapping_f“ in libsel4simple-default library. Its comment is "Request mapped address to a region of physical memory.” It is very similar to what I need, but its implementation just returns NULL.(in sel4\libs\libsel4simple-stable\src\libsel4simple-stable.c) Thank you very much. Yuxin

1 0

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel October 2014