- Devel - lists.sel4.systems

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

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

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

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

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

2 1

Support for Intel x86-64?
by Yes Man 13 Jan '15

13 Jan '15

2 1

(good faq entries to add?) re-proving after code commits?
by Raoul Duke 09 Jan '15

09 Jan '15

hi, When does seL4 get re-proven? When code gets pulled into the master branch on github? Once a year? Something in-between? Is it clear what code is actually proven? Is everything in github under the proofs? Or are there things that fall outside the proven kernel? How would anybody see that? :-) Thanks!

2 4

simple_default_cap_count doesn't contain seL4_CapDomain
by Pei.XiLong(裴喜龙) 05 Jan '15

05 Jan '15

Hi PM, The logic in these 2 functions doesn’t contain capability seL4_CapDomain int simple_default_cap_count(void *data) seL4_CPtr simple_default_nth_cap(void *data, int n) So, these sentense cause error: // ……/sel4tes-drivers/src/main.c env.init->domain = copy_cap_to_process(&test_process, simple_get_init_cap(&env.simple, seL4_CapDomain)); Xilong Pei Tongji University 2014/12/31

2 4

Day-to-day usability of seL4
by Marc Hans 31 Dec '14

31 Dec '14

seL4 as a kernel is complete, as far as I can tell, but what about the userspace and hardware support? As soon as this formally verified OS boots into a graphical interface and one can get a simple web browser and media player working, it will be pretty much ready for day-to-day use for most users. I normally wouldn't expect such a thing, but since NICTA has showed excellence in the past and is so intensively powered, I got my hopes up. Will users soon be able to use a completely formally verified OS (kernel, userspace and everything)? Or is that something too far fetched to dream about? Best wishes, Marc Collin

4 3