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
I just noticed the web page says
"we have Haskell sort-of running on seL4 (thanks or
friends from Galois for their help), should be released
in the near future"
This is great news. Are you able to share any details
such as when any of this will be public, what the
porting strategy was (is this similar to HalVM?),
what dependencies haskell compiled code requires,
if there are sel4 bindings, etc?
Tim
I am working on a UART device driver in camkes for AM335x.
When I load the image on the board I get this error:
Creating object frame_drv_group_bin_42 in slot 596, from untyped 1f6...
device frame, paddr = 0x48022000, size = 12 bits
capDL-loader :: << Error: Failed to find device frame at paddr = 0x48022000
>>
I am reasonably confident the address is correct,
(https://github.com/seL4/libplatsupport/blob/master/plat_include/am335x/plat…)
Looking at the source It seems capDL-Loader wants to find this device
frame in bootinfo
https://github.com/seL4/capdl-loader-app/blob/master/src/main.c#L731
Any help on how capDL-loader builds bootinfo would be appreciated.
Jeff
--
Jeffrey L. Hieb
Department of Engineering Fundamentals
University of Louisville
Louisville Kentucky 40292
(502) 852 0465
Hi,
I'm trying to implement a "create endpoint" syscall as a continuation of my
AOS project last year. I'm using the following code to create and endpoint
in the current threads's cspace (using libsel4cspace):
https://gist.github.com/anonymous/8294aa47ad351e4d4066
When this code runs, seL4 prints the following during the
cspace_ut_retype_addr call:
<<seL4 [decodeUntypedInvocation/128 Tffeead00 @b330]: Untyped Retype:
Invalid destination address.>>
This error comes from inside libsel4cspace, specifically where it calls
seL4_Untyped_RetypeAtOffset(). I've read the libsel4cspace documentation
and enabled CSPACE_DEBUG, but nothing from the output looks amiss (I'm not
an expert though, and I can post the relevant debug output).
Have I done anything wrong in the code above?
Thanks,
- Will
I want to transplant the Refos into the ZYNQ board,Now everything is ok,except the timer server. Could you give me some advices about how to modify timer server's file device_timer.c .
------------------ Original ------------------
From: "devel-request";<devel-request(a)sel4.systems>;
Date: Thu, Sep 24, 2015 10:00 AM
To: "devel"<devel(a)sel4.systems>;
Subject: Devel Digest, Vol 16, Issue 12
Send Devel mailing list submissions to
devel(a)sel4.systems
To subscribe or unsubscribe via the World Wide Web, visit
https://sel4.systems/lists/listinfo/devel
or, via email, send a message with subject or body 'help' to
devel-request(a)sel4.systems
You can reach the person managing the list at
devel-owner(a)sel4.systems
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Devel digest..."
Today's Topics:
1. Reminder: Developers Day registration closes Monday
(Gernot Heiser)
----------------------------------------------------------------------
Message: 1
Date: Wed, 23 Sep 2015 05:58:01 +0000
From: Gernot Heiser <gernot(a)nicta.com.au>
To: seL4 <devel(a)sel4.systems>
Subject: [seL4] Reminder: Developers Day registration closes Monday
Message-ID: <FD16E4F0-FD7A-494C-9432-AF1C4903E750(a)nicta.com.au>
Content-Type: text/plain; charset="us-ascii"
Details at https://sel4.systems/Community/Devdays/
Gernot
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
------------------------------
Subject: Digest Footer
_______________________________________________
Devel mailing list
Devel(a)sel4.systems
https://sel4.systems/lists/listinfo/devel
------------------------------
End of Devel Digest, Vol 16, Issue 12
*************************************
Details at https://sel4.systems/Community/Devdays/
Gernot
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Hello, I am attempting to create a simple program opening up a serial port
on the Sabrelight. Attached is the source code and below is the console
output. On other sel4 blogs with this problem uboot may have been the
issue. I have used the u-boot as discribed on the supported
hardware->sabrelight page with the same outcome. Any help would be
appreciated. Thanks,
U-Boot 2009.08-dirty (Sep 17 2015 - 14:58:04)
CPU: Freescale i.MX6 family TO1.2 at 792 MHz
Temperature: 36 C, calibration data 0x56a4bc7d
mx6q pll1: 792MHz
mx6q pll2: 528MHz
mx6q pll3: 480MHz
mx6q pll8: 50MHz
ipg clock : 66000000Hz
ipg per clock : 66000000Hz
uart clock : 80000000Hz
cspi clock : 60000000Hz
ahb clock : 132000000Hz
axi clock : 264000000Hz
emi_slow clock: 132000000Hz
ddr clock : 528000000Hz
usdhc1 clock : 198000000Hz
usdhc2 clock : 198000000Hz
usdhc3 clock : 198000000Hz
usdhc4 clock : 198000000Hz
nfc clock : 24000000Hz
Board: MX6Q-SABRELITE:[ POR]
Boot Device: I2C
I2C: ready
DRAM: 1 GB
MMC: FSL_USDHC: 0,FSL_USDHC: 1
JEDEC ID: 0xbf:0x25:0x41
Reading SPI NOR flash 0xc0000 [0x2000 bytes] -> ram 0x276009b8
SUCCESS
*** Warning - bad CRC, using default environment
In: serial
Out: serial
Err: serial
Net: got MAC address from IIM: 00:19:b8:01:fd:6d
FEC0 [PRIME]
Hit any key to stop autoboot: 0
mmc1 is current device
-- Trying fat on SD 1, partition 1
reading sel4-image
344564 bytes read
## Starting application at 0x20000000 ...
ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10
paddr=[20000000..2004c01f]
ELF-loading image 'kernel'
paddr=[10000000..10031fff]
vaddr=[e0000000..e0031fff]
virt_entry=e0000000
ELF-loading image 'hello-1'
paddr=[10032000..1003ffff]
vaddr=[8000..15fff]
virt_entry=803c
Enabling MMU and paging
Jumping to kernel-image entry point...
Bootstrapping kernel
Caught cap fault in send phase at address 0x0
while trying to handle:
vm fault on data at address 0x0 with status 0x7
in thread 0xffdfd900 "rootserver" at address 0x804
--
-Andrew
Andrew P. Shruhan
Research and Development Engineer III
DocBox, Inc.
320 Nevada St
Newton MA, 02460
Work: 857-598-2819 ext. 117
www.docboxmed.com <http://www.docboxinc.com/>
Hi. I came across seL4 yesterday and have not spent too much time on it. I
have not found anything specific to my question in the FAQ yet, so I am posing
it here: has the work done by seL4 been accepted upstream? If not, any reason
why it has not been accepted yet?
Thanks.
Harish
Dear developers,
Those of you who aren’t (yet) subscribed to announce(a)sel4.systems might have missed this: we announced
- the seL4 roadmap: https://sel4.systems/pipermail/announce/2015/000007.html
- the second Developers Day: https://sel4.systems/pipermail/announce/2015/000008.html
Gernot
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
