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
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
> Easier to keep the generator simple and let the compiler do the optimisations it already understands.
Based on things like the experiences of Tahoe LAFS with compiler
optimizations vs. security - let alone plain bugs - I am scared if
anybody uses any optimizations at all, especially for serious
business. I have not researched the position se4L takes on this. Are
the proofs about the before-optimization code, or do they consider the
after-optimization assembly output?
thanks.
One more and then I'll stop .. I promise.
There appear to be numerous instances of the following design pattern:
struct message_info {
uint32_t words[1];
};
Where the above structure is then allocated locally, initialized and
returned by a procedure.
Seems like a lot of work to return a uint32_t.
I originally assumed that all/much of this code was generated
automatically from Haskell .. so I figured it was some odd corner case in
the translator. Subsequent discussions, however, have suggested that this
assumption is false and that the code was actually written by hand.
I could understand using structures to present a unique, statically
checkable procedure type signature .. but I can't rationalize the use of
the single element array.
So .. is there a reason for this curious design pattern?
Thanks,
Dave
I ran the sel4 kernel source through the CIL infrastructure front end:
http://kerneis.github.io/cil/
CIL reported two warnings:
../../../../seL4/src/object/cnode.c:867: Warning: Body of function
isMDBParentOf falls-through. Adding a return statement
../../../../seL4/src/object/objecttype.c:261: Warning: Body of function
recycleCap falls-through and cannot find an appropriate return value
The first warning looks like a weakness in CIL code analysis .. every
branch of the condition has a return so the procedure doesn't need a
fall-through return.
The same is not true for the second .. the first branch halt()'s but it
doesn't return .. thus the procedure is not "obviously" type safe.
I'm curious about the this from a reasoning perspective.
Perhaps the argument is that halt() never terminates (or it "exits"),
thus it is OK if the procedure doesn't return a value in that case. But
that argument only works if the logic somehow captures the semantics of
halt().
Are halt() semantics baked into the correctness proofs? If not, how is
this procedure justified?
Thanks,
Dave
Hello,
I am attempting to boot the seL4 kernel (only the kernel, not the
platform library) on an AM335x chip and am running into difficulties
when the elfloader enables the MMU. Debug statements indicate that the
enable_mmu function is not returned from, thus I believe a fault is
occuring when the processor attempts to execute the first instruction
following the MMU being enable. Unfortunately I do not have access to
a JTAG debugger at the moment, so I will relay what information I can.
I should also mention that I have made no changes to the elfloader
source code except where noted for debugging purposes.
I have verified that the page table is being setup for supervisor
access (access protection bit 10 set, bit 11 clear) and that the
domain is set to 0 for all pages. As I understand it, this means that
the permissions set in the domain access control register are checked.
I am booting the elfloader through uboot and since the co-processor
registers are accessible, I believe I am already in supervisor mode.
Thus it would seem the elfloader code should work without
modification. However, the only way I have found to get the kernel to
boot is by setting access control for domain 0 to manager (write 3
instead of 1 at
https://github.com/seL4/elfloader-tool/blob/803b92c7a3c9b48bd474b3de7ac9b8c…).
>From my examination of the code, I don't believe this should be
necessary, so I think I have probably configured the project
incorrectly or am loading the image with uboot somehow incorrectly
(for the record, I objcopy the elfloader elf to a bin and load the
image through uboot to memory address 0x82000000 and perform a go
command).
What confuses me is that if I leave access to the domain set as client
(no change from what is on the master branch) and instead set the
permission on the page to bit 10 and bit 11 both set, the processor
still faults. I would expect this configuration to not produce a fault
since these permissions should allow supervisor and non-supervisor
read/write access.
Finally, the code is executing in a region that is 1:1 mapped after
the MMU is enabled, so I don't think this is a problem.
With all that said, does anyone have any idea why the elfloader isn't
working out of the box for me? As I understand things, using the
elfloader is the standard way to boot the kernel on an arm processor.
I have included the options of my build configuration at the end of
this message.
Thank you for your time,
Jordan
CONFIG_ARCH_ARM_V7A=y
CONFIG_ARCH_ARM=y
CONFIG_ARM_CORTEX_A8=y
CONFIG_PLAT_AM335X=y
CONFIG_ROOT_CNODE_SIZE_BITS=16
CONFIG_TIMER_TICK_MS=2
CONFIG_TIME_SLICE=5
CONFIG_RETYPE_FAN_OUT_LIMIT=256
CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION=100
CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS=199
CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS=167
CONFIG_FASTPATH=y
CONFIG_NUM_DOMAINS=1
CONFIG_DOMAIN_SCHEDULE=""
CONFIG_NUM_PRIORITIES=256
CONFIG_DEBUG_BUILD=y
CONFIG_IRQ_REPORTING=y
CONFIG_OPTIMISATION_O2=y
CONFIG_LIB_SEL4=y
CONFIG_LIB_MUSL_C=y
CONFIG_HAVE_LIBC=y
CONFIG_HAVE_CRT=y
CONFIG_LIB_CPIO=y
CONFIG_LIB_ELFLOADER=y
CONFIG_ARM_ERRATA_764369=y
CONFIG_CROSS_COMPILER_PREFIX="arm-none-eabi-"
CONFIG_KERNEL_COMPILER=""
CONFIG_KERNEL_CFLAGS=""
CONFIG_KERNEL_EXTRA_CPPFLAGS=""
CONFIG_USER_EXTRA_CFLAGS=""
CONFIG_USER_CFLAGS=""
CONFIG_USER_OPTIMISATION_O2=y
CONFIG_USER_DEBUG_BUILD=y
Gerwin,
On Tue, Jan 20, 2015 at 3:02 PM, Gerwin Klein <Gerwin.Klein(a)nicta.com.au>
wrote:
> Hi David,
>
> yes, it seems the Isabelle installation step failed already. The command
> ./isabelle/bin/isabelle components -a should print the list of missing
> components as it did, but should then start downloading them. Instead it
> printed an error message about dirname.
>
Isabelle did go on to download and install the components (sorry: the
ellipsis was supposed to suggest that). I did not see any other warnings
or errors after the message about dirname.
Is there any way I could test to make sure this installation succeeded?
> It's possible that it is picking up the wrong kind of shell to run the
> script. Do you have bash installed? The script is trying to run bash using
> "#!/usr/bin/env bash"
>
Bash is installed. When I type /usr/bin/env bash at my prompt I get a
new bash shell prompt.
> The wrong path out of run_tests also seems to be related to dirname. It's
> this line that seems to be going wrong:
>
> DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
>
> in this case DIR should just become ".", but it seems to return the empty
> string instead.
>
I added a line to echo DIR in the run_scripts and it prints out my
current working directory, as I would expect.
The nature of the failure makes me think there might some environment
variable that I am supposed to set .. could that be?
It looks like the test failure was generated by "make" .. can you tell me
where (the directory in which) make is run and/or tell me where to find the
Makefile it is using?
> Cheers,
> Gerwin
>
> > On 21.01.2015, at 05:41, David Greve <david.greve(a)rockwellcollins.com>
> wrote:
> >
> >
> > I am attempting to run the sel4 proofs on linux Mint 17.1 (64-bit).
> >
> > I have a copy of the "verification" project and have walked through
> all of the setup steps up to the point of running run_test. When I do, I
> encounter numerous failures, the first of which says:
> >
> > ------------------------------------------------------------------------
> > TEST FAILURE: CamkesAdlSpec
> >
> > /isabelle/bin/isabelle build -b -v -d "" CamkesAdlSpec
> > make: /isabelle/bin/isabelle: Command not found
> > /bin/sh: /isabelle/bin/isabelle: No such file or directory
> > make: *** [CamkesAdlSpec] Error 127
> >
> > ------------------------------------------------------------------------
> >
> > Note that the isabelle command appears to be missing a leading path.
> >
> > I think the script is somehow failing to pick up my working directory.
> >
> > Now, when I was setting up isabelle, I did see the following message:
> >
> > $ ./isabelle/bin/isabelle components -a
> > ### Missing Isabelle component:
> "/home/dagreve/.isabelle/contrib/cvc3-2.4.1"
> > ...
> > ### Missing Isabelle component:
> "/home/dagreve/.isabelle/contrib/xz-java-1.2-1"
> > dirname: missing operand
> > Try 'dirname --help' for more information.
> > ...
> >
> > The setup completed without further errors, but I wonder if this is a
> contributing factor?
> >
> > Thanks,
> > Dave
> >
> > _______________________________________________
> > Devel mailing list
> > Devel(a)sel4.systems
> > https://sel4.systems/lists/listinfo/devel
>
>
> ________________________________
>
> 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.
>
I am attempting to run the sel4 proofs on linux Mint 17.1 (64-bit).
I have a copy of the "verification" project and have walked through all
of the setup steps up to the point of running run_test. When I do, I
encounter numerous failures, the first of which says:
------------------------------------------------------------------------
TEST FAILURE: CamkesAdlSpec
/isabelle/bin/isabelle build -b -v -d "" CamkesAdlSpec
make: /isabelle/bin/isabelle: Command not found
/bin/sh: /isabelle/bin/isabelle: No such file or directory
make: *** [CamkesAdlSpec] Error 127
------------------------------------------------------------------------
Note that the isabelle command appears to be missing a leading path.
I think the script is somehow failing to pick up my working directory.
Now, when I was setting up isabelle, I did see the following message:
$ ./isabelle/bin/isabelle components -a
### Missing Isabelle component: "/home/dagreve/.isabelle/contrib/cvc3-2.4.1"
...
### Missing Isabelle component:
"/home/dagreve/.isabelle/contrib/xz-java-1.2-1"
dirname: missing operand
Try 'dirname --help' for more information.
...
The setup completed without further errors, but I wonder if this is a
contributing factor?
Thanks,
Dave
