- Devel - lists.sel4.systems

Capability unwrapping
by Norman Feske 14 Feb '15

14 Feb '15

Hello, after a rather long break, I picked up my work with porting Genode to seL4. More specifically, I try to find a good way to realize Genode's RPC mechanism with seL4 IPC. But admittedly, I am struggling a bit. Ideally, each Genode RPC should be realized as a seL4 IPC call. Unfortunately, however, I find the kernel interface too restrictive to do that. There are two issues. 1. Delegation of multiple capabilities at once According to Chapter 4.2.2 of the manual, the kernel allows the … [View More]

8 18

Network stack support
by Andy Helten 13 Feb '15

13 Feb '15

1 0

Status of supporting Beaglebone?
by Kun Cheng 06 Feb '15

06 Feb '15

Hi guys, I happened to find out that beaglebone was listed in the menuconfig. After that I immediately bought a Beaglebone black (Yeah I know beaglebone is different from bb black, but it might succeed. LOL.) and tried to build a image for my bb black . But I found code errors during compilation. I use arm-none-eabi tool chains and the gcc version is 4.8. Errors occurred in sel4test/libs/libplatsupport/src/clock.c which includes platsupport/plat/clock.h but it doesn't exist sel4test/libs/… [View More]

2 4

Optimizations?
by Raoul Duke 30 Jan '15

30 Jan '15

> 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.

4 4

curious design pattern
by David Greve 29 Jan '15

29 Jan '15

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,… [View More]

3 2

Haskell error comments
by David Greve 28 Jan '15

28 Jan '15

What is the significance of the various "Haskell error:" comments found throughout the kernel code?

3 6

fall-through procedures
by David Greve 27 Jan '15

27 Jan '15

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 … [View More]

2 2

Elfloader faults when MMU activated
by Jordan Woehr 24 Jan '15

24 Jan '15

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 … [View More]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 [View Less]

2 2

Re: [seL4] run_test failures
by David Greve 22 Jan '15

22 Jan '15

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 … [View More]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. > [View Less]

3 8

run_test failures
by David Greve 21 Jan '15

21 Jan '15

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/… [View More]

2 1