- Devel - lists.sel4.systems

U-boot help sabrelite
by Andrew Shruhan 12 Aug '15

12 Aug '15

Hi, I am attempting to follow the tutorial booting from SPI for the sabrelite https://sel4.systems/Hardware/sabreLite/ when booting I obtain this output and am not able to run "run bootsel4_mmc" U-Boot 2009.08-dirty (Jun 27 2013 - 16:26:46) 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 In: serial Out: serial Err: serial Net: got MAC address from IIM: 00:19:b8:01:fd:6d FEC0 Hit any key to stop autoboot: 0 AHCI 0000.0000 1 slots 1 ports ? Gbps 0x0 impl SATA mode flags: No port device detected! Unknown command 'load' - try 'help' SATA device 1: unknown device Unknown command 'load' - try 'help' Card did not respond to voltage select! mmc0(part 0) is current device Unknown command 'load' - try 'help' mmc1 is current device Unknown command 'load' - try 'help' Unknown command 'usb' - try 'help' Unknown command 'usb' - try 'help' Unknown command 'load' - try 'help' Unknown command 'usb' - try 'help' Unknown command 'load' - try 'help' 6x_bootscript not found serial console at 115200, 8N1 details at http://boundarydevices.com/6q_bootscript AHCI 0000.0000 1 slots 1 ports ? Gbps 0x0 impl SATA mode flags: No port device detected! AHCI 0000.0000 1 slots 1 ports ? Gbps 0x0 impl SATA mode flags: No port device detected! Card did not respond to voltage select! mmc0(part 0) is current device expose mmc drive 0 over USB Unknown command 'ums' - try 'help' Card did not respond to voltage select! no block devices found ERTOS MX6Q SABRELITE U-Boot > -- -Andrew Andrew P. Shruhan Research and Development Engineer III DocBox, Inc. 320 Nevada St Newton MA, 02460 Work: 857-598-2819 ext. 117 www.docboxinc.com

2 2

Upstream seL4/RISC-V work?
by Hesham ALMatary 10 Aug '15

10 Aug '15

Hi, The seL4/RISC-V port is now working on Spike (emulator), Rocket Chip (FPGA), and jor1k (online emulator). I've also written a recent blog post how to build/run the port with SOS project [1] from my repos). The code is pretty much like the ARM port, and following the same bootstrapping procedure (more on this on my blog). MMU code provides 4KiB and 4MiB pages (like IA-32). I'd like to ask if there are special requirements to upstream this work: * All libraries that are target-dependant. * seL4 microkernel. * Tools (elf loader, build system). * SOS project? I understand it won't be an easy process because this work is the first "foreign" code that big, of course apart from formal verification. But it wouldn't hurt to ask. [1] http://heshamelmatary.blogspot.co.uk/2015/07/howto-build-and-run-sel4-on-ri… Best, -- Hesham

4 4

Porting Linux driver into Sel4
by Shabnam Engineer 09 Aug '15

09 Aug '15

HiI have a question about porting Linux drivers in Sel4.Can I port Linux drivers into Sel4? I know that DDEKit provides such functionality for L4-based systems and I could find the implementation of that in fiasco.OC microkernel, but I can not find same works for Sel4. I want to implement Sel4 on a board and test some features, At first I want to be sure that if I need a driver for our special tests and the Sel4 does not support that, Could I choose it from Linux drivers and port it to Sel4 microkernel? Thank you for your considering my question.Regards,Shabnam

1 0

Wandboard Port
by Robert Kaiser 30 Jul '15

30 Jul '15

Hello, in an attempt to familiarize myself with the seL4 code, I am trying to "port" it to the Wandboard (see www.wandboard.org) This should be an easy task for a beginner (thought I) since the board is very similar to the SabeLite, and seL4 is already running well on that board. I have access to a SabreLite and a Wandboard Quad, both (according to U-boot) have the same revision of the iMX6 SoC installed. Differences between the Sabre and the Wand I have noticed so far are: - 2GB of RAM from (0x10000000 to 0x90000000) on the Wand (Sabrelite has 1GB) - Wand uses UART1 for debug output, Sabrelite: UART2 I compiled an sel4test project where I adapted the UART port in kernel/include/plat/imx6/plat/machine/devices.h and elfloader/src/arch-arm/plat-imx6/platform.h and the RAM size in kernel src/plat/imx6/machine/hardware.c. When I boot this system, I get: 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 0x9f11c2e0 with status 0x1c06 in thread 0xffdfad00 at address 0x13294 (Needless to say, "all is well in the universe" on the SabreLite... ) What is not shown here are a ton of other debug messages which I have added to convince myself that kernel initialization completes as expected. The crash seems to happen upon entry into user code. The address 0x13294 is the virtual address of the entry point: $ nm build/arm/imx6/sel4test-driver/sel4test-driver.bin | grep 13294 00013294 T _sel4_start I suspect that this fault happens on opcode fetch, because the user code is not properly mapped when invoked. Does "status 0x1c06" confirm this? If so, *should* the code be mapped at this point or are these mappings expected to be installed "on demand", i.e. through page fault handling? Thanks for any help... Robert -- Robert Kaiser Computer Engineering RheinMain University of Applied Sciences

3 14

Happy Birthday, Developers!
by Gernot Heiser 29 Jul '15

29 Jul '15

Hi everyone, Today is the anniversary of the open-sourcing of seL4. At NICTA we’re celebrating, I hope you’ll virtually join us ;-) Let me add that I quite enjoy this mailing list. Traffic has a high signal-noise ratio (apologies for degrading it with this message ;-) people generally seem to know what they are doing, and the community is clearly growing. Presently there are over 300 addresses on the list. Many thanks from all of us at NICTA, and keep it up! Gernot [cid:1374281D-B193-431C-AA3F-D6EE049C461A@keg.ertos.in.nicta.com.au] ________________________________ 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.

2 1

CMake and seL4
by Wink Saville 29 Jul '15

29 Jul '15

In my opinion the edit/compile/test loop with the standard build system seeed slow, so I thought I'd try to see if CMake might be any better. Here <https://github.com/winksaville/sel4-newlibs-manifest> is repo manifest which uses CMake for building my sel4-newlibs helloworld application and I'm happy to report there is some improvement. For a "clean" build it is about 2x faster, 8 seconds as compared to 14 seconds. And for a small change to apps/helloworld/src/main.c it is 20x faster, 0.3 seconds as compared to 7 seconds. Is there any interest in using CMake or other build system to reduce the builds times for seL4? -- Wink

2 2

seL4 runs on Rocket Chip (RISCV/FPGA)
by Hesham ALMatary 18 Jul '15

18 Jul '15

Hi all, This is a status update of the seL4/RISC-V project. It can run now on Rocket Chip (FPGA) and jor1k (online emulator), for more details have a look at this link [1]. [1] http://heshamelmatary.blogspot.co.uk/2015/07/sel4-runs-on-rocket-chip-riscv… Thanks, -- Hesham

1 0

Some questions about seL4 operating system
by Qing Wei 16 Jul '15

16 Jul '15

Hi, I am a beginner to seL4 as well as microkernel, and very interested in it. I think it is great in terms of its minimality and formally verified security. However, I have some questions about it, (1) How is its performance compared to other monolithic kernel, say, Linux. Could it make use of multicore, multiprocessor to enjoy the performance scalability? (2) How is its ecosystem, fox example, how to support new hardware, does it need write the driver from scratch or could it make use of Linux driver? And how to write application on it, or, could it run Linux application without modification? (3) How is its virtualization support, could it run Linux vm, and does it need any modification to the guest os? Cheers, Qing Wei

1 0

what are these comments meaning
by Pei.XiLong(裴喜龙) 15 Jul '15

15 Jul '15

Hi, In recent seL4 commit https://github.com/seL4/seL4/commit/67d8d041de0c435a1cc59ef8c237be6e39beb1c6 , A lot of comments like these: /** AUXUPD: "(True, ptr_retyps (2 ^ (unat \<acute>userSize)) (Ptr (ptr_val \<acute>regionBase) :: cte_C ptr))" */ /** GHOSTUPD: "(True, gs_new_cnodes (unat \<acute>userSize) (ptr_val \<acute>regionBase) (4 + unat \<acute>userSize))" */ have been added into source code, What is their meaning? I don't know isablle, and just know a little about haskell. thanks! Xilong Pei Tongji University 2015/7/14

2 1

Raspberry Pi version for learning about seL4
by Simon Apperley 14 Jul '15

14 Jul '15

Hi, I wondered if there was any news on the Raspberry Pi 2 port of seL4 which I saw mentioned when I did a search? I am interested in using the Raspberry Pi to learn about seL4 - not as a target for a full system (as I know there is an issue with trusting the boot mechanism). I just thought it would be a nice platform to use to get my head around seL4 and experiment with virtualising Linux and maybe Android? Simon Sent from my iPad

2 1

reply: This checkin cause a build error
by XilongPei(裴喜龙) 13 Jul '15

13 Jul '15

Hi, Adria, I have fix this build error, it is because I use an old version of apps/sel4test-driver/scripts/extract-test-names.sh I am developing an operating system which can support Microsoft COM like component programing module based on seL4, so I have to sync every repository manually. Xilong Pei Tongji University 2015/7/13

1 0

This checkin cause a build error
by XilongPei(裴喜龙) 13 Jul '15

13 Jul '15

Hi, This checkin cause a build error: Drop static qualifier from tests so that C++ compilers will use extern C linkage instead of name mangling https://github.com/seL4/libsel4test/commit/930744eaf43260ceb37ce2793eefbe77c d808ff0 the error information: .../libs/libsel4test/src/test.c:161: undefined reference to `__start__test_case' .../libs/libsel4test/src/test.c:161: undefined reference to `__stop__test_case' Xilong Pei Tongji University 2015/7/13

2 1

Streamline seL4/libsel4 and make it not depend on libc
by Wink Saville 10 Jul '15

10 Jul '15

I've got sel4test running with libsel4 not having a dependency on libc. I've pulled out libsel4assert, libsel4benchmark, libsel4printf and libsel4putchar from libsel4 and they are separate libraries The biggest change is to seL4/libsel4 and sel4/tools/bitfield_gen.py. The changes to bitfield_gen.py allow it to generate the same code as before for the kernel but uses the new names for entities in user space. Please let me know what you think. -- Wink https://github.com/winksaville/seL4/tree/libsel4-no-libc-dependency https://github.com/winksaville/libsel4test/tree/libsel4-no-libc-dependency https://github.com/winksaville/libsel4allocman/tree/libsel4-no-libc-depende… https://github.com/winksaville/libsel4utils/tree/libsel4-no-libc-dependency https://github.com/winksaville/sel4test/tree/libsel4-no-libc-dependency https://github.com/winksaville/libsel4assert https://github.com/winksaville/libsel4benchmark https://github.com/winksaville/libsel4printf https://github.com/winksaville/libsel4putchar

4 11

can IPC be concurrent running?
by Pei.XiLong(裴喜龙) 07 Jul '15

07 Jul '15

Hi, We can get the definition of IPCBuffer from here https://github.com/seL4/seL4/blob/master/libsel4/arch_include/arm/sel4/arch… enum { seL4_GlobalsFrame = 0xffffc000, }; It is fixed in one virtual space, that means the IPC in seL4's thread cann't be concurrent, we can't prepare more than 1 IPC request at the same time, for we call these function: seL4_SetTag, seL4_SetMR, seL4_SetUserData wil use this buffer, but there is no locker to protect the buffer. Is my understanding correct? Xilong Pei Tongji University 2015/7/6

1 0

Where is the definition of seL4_TCB_BindAEP and seL4_TCB_UnbindAEP?
by XilongPei(裴喜龙) 07 Jul '15

07 Jul '15

Hi, In test program binding.c https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/src/tests/b inding.c , there are two functions, seL4_TCB_BindAEP and seL4_TCB_UnbindAEP, where can I get their definitions? Xilong Pei Tongji University 2015/7/6

2 1

Try two for libsel4 not having a dependency on libc
by Wink Saville 04 Jul '15

04 Jul '15

Here <https://github.com/winksaville/sel4-min-sel4/tree/new-libs> is a different approach for removing the libc dependency, it seemed like people thought libsel4 was to big and that as part of the effort of breaking the dependency it should be made smaller. Basically libsel4 does nothing expect satisfy dependency needed for the kernel for some xml files. And I've broken libsel4 into basically 8 other libraries. see here <https://github.com/winksaville/sel4-min-sel4/tree/new-libs/libs>. This maybe taking things to far, but it does mean people can use only what they need, which I like. The smallest example is app/min-hw which only uses libsel4_gen, libsel4_startup. libsel4_bootinfo and libsel4_putchar. At the other extreme apps/test-newlibs uses everything. Anyway other organizations are certainly possible. Currently there is at least one known problem, I modified bitfield_gen.py so types_gen.h has no asserts since at the moment the kernel uses assert and userspace is libsel4_assert. We could either do something like I've done and remove them or change the kernel to use libsel4_assert or something else. Anyway, before creating a pull request I'd like to know what people think. -- Wink

4 12

Who can give me a sample program using sel4platsupport_new_io_ops
by XilongPei(裴喜龙) 01 Jul '15

01 Jul '15

Hi, sel4platsupport_new_io_ops is defined in libsel4platsupport/include/sel4platsupport/io.h , it creates a new implementation of the platsupport io_ops interface using a provided simple, vspace and vka, Here is its protocol: /* * @param simple Simple interface for getting the physical frames * @param vspace VSpace interface to use for mapping * @param vka VKA interface for allocating any extra objects or cslots * @param io_ops Interface to fill in * * @return returns 0 on success */ int sel4platsupport_new_io_ops(simple_t simple, vspace_t vspace, vka_t vka, ps_io_ops_t *io_ops); Who can give me a sample program using this function? I guess it will be used in I/O DMA program, but I don't know much about DMA program. Xilong Pei Tongji University 2015/7/1

1 0

Make seL4/libsel4 not depend upon libc
by Wink Saville 29 Jun '15

29 Jun '15

I noticed that seL4/libsel4 was dependent upon libc and so I created a patch ( https://github.com/winksaville/seL4/commit/fc91a1f68c054fdb41aaa42a7b56a80f…) which removes the dependency. If there is interest I can submit a pull request, and of course will make any changes deemed necessary to make it suitable for acceptance. Please advise, Wink

6 11

How to edit RefOS libs c file
by ぷ风过无痕?? 22 Jun '15

22 Jun '15

Hi, I am using RefOS to develop a small applicaiton(interprocess comunicaion).I need to edit some c files in RefOS/libs/librefos directory,But comments say that do not edit these files,these files were generated by CIDL.CIDL is a simple C IDL compiler which is made to save the trouble of manually implementing RPC interface stubs to marshal C style arguments and return value. It uses a simple XML-based IDL language. I search on the google，but just got some introduction. So where can I got some useful infomation about CIDL? Can you recommend some books or websites? ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Sun, Jun 21, 2015 10:00 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 13, Issue 11 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. Re: Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC (da Tyga) ---------------------------------------------------------------------- Message: 1 Date: Sat, 20 Jun 2015 16:26:46 +1000 From: da Tyga <cyberfonic(a)gmail.com> To: devel(a)sel4.systems Subject: Re: [seL4] Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC Message-ID: <CALj3Nd3+CFFQF41BOwW+-bwFNOEZS9HyVLHDwVssTyMAcsU3ig(a)mail.gmail.com> Content-Type: text/plain; charset="utf-8" > > > Hi Yuxin, I don't think you need to modify GCC, it is the compiler that you can use to generate required executables. Making changes to it is a massive undertaking. Instead of trying to reinvent stuff that has already been done, you really should read the Genode documentation and download and read the source code referenced by Norman Feske's suggestions. >From my reading of the Genode documents and source code, I would expect that you would find a considerable amount of code that you could you re-purpose for your specific requirements. Cheers, Tyga > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 19 Jun 2015 22:46:40 +0800 > From: Yuxin Ren <ryx(a)gwmail.gwu.edu> > To: Norman Feske <norman.feske(a)genode-labs.com> > Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] Does sel4 support c++ > Message-ID: > <CAAKbDrcbyh0YV+nHzhziiiXavn-= > P_tW5bS2LUfPzHcBF-iMKg(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Thank you all! > > If modifying the tool chain is the easiest way, I want to try it. > But I definitely want to avoid creating the tool chain from "bare metal". > I still prefer to reuse the existing tool chain like gcc > with minimal modification. > > Could you give me some guidance how to create a custom tool chain, which > part I need to modify? > I am not familiar with gcc. So if I have to modify gcc, where can I get > more information or documentation? > > Thanks a lot!! > Yuxin > > On Thu, Jun 18, 2015 at 9:50 PM, Norman Feske < > norman.feske(a)genode-labs.com> > wrote: > > > Hello, > > > > > The easiest approach is possibly to create a custom tool chain, and > port > > > the GCC C++ library that way. I know the people behind Genode did some > > > of this (http://genode.org/download/tool-chain) although I'm not sure > > > how much of the C++ standard library they actually support. > > > > more in-depth information about Genode's tool chain are provided by > > Section 7.2 of the documentation [1]. In short, the tool chain is a > > "bare metal" tool chain that does not depend on a C library, yet it > > still supports C++ (including exceptions and runtime type information). > > > > On Genode, the libc and STL (aka stdcxx) can be used optionally whereas > > the STL depends on the libc. The libc is based on FreeBSD's libc. The > > STL is GCC's version. Both libraries are available via Genode's ports > > mechanism. > > > > That said, as both the libc and stdcxx are shared libraries, they cannot > > be used on the seL4 version of Genode as of now. Shared libraries don't > > work on seL4 (at least on x86_32) because the system-call bindings > > cannot be compiled with -fPIC. > > > > [1] http://genode.org/documentation/genode-foundations-15-05.pdf > > > > 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 > > > > _______________________________________________ > > Devel mailing list > > Devel(a)sel4.systems > > https://sel4.systems/lists/listinfo/devel > > > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: < > http://sel4.systems/pipermail/devel/attachments/20150619/5b4ce704/attachmen… > > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > ------------------------------ > > End of Devel Digest, Vol 13, Issue 10 > ************************************* > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20150620/c72cfc07/attachmen…> ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 13, Issue 11 *************************************

4 3

Re: [seL4] Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC
by da Tyga 22 Jun '15

22 Jun '15

> > > Hi Yuxin, I don't think you need to modify GCC, it is the compiler that you can use to generate required executables. Making changes to it is a massive undertaking. Instead of trying to reinvent stuff that has already been done, you really should read the Genode documentation and download and read the source code referenced by Norman Feske's suggestions. >From my reading of the Genode documents and source code, I would expect that you would find a considerable amount of code that you could you re-purpose for your specific requirements. Cheers, Tyga > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 19 Jun 2015 22:46:40 +0800 > From: Yuxin Ren <ryx(a)gwmail.gwu.edu> > To: Norman Feske <norman.feske(a)genode-labs.com> > Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] Does sel4 support c++ > Message-ID: > <CAAKbDrcbyh0YV+nHzhziiiXavn-= > P_tW5bS2LUfPzHcBF-iMKg(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Thank you all! > > If modifying the tool chain is the easiest way, I want to try it. > But I definitely want to avoid creating the tool chain from "bare metal". > I still prefer to reuse the existing tool chain like gcc > with minimal modification. > > Could you give me some guidance how to create a custom tool chain, which > part I need to modify? > I am not familiar with gcc. So if I have to modify gcc, where can I get > more information or documentation? > > Thanks a lot!! > Yuxin > > On Thu, Jun 18, 2015 at 9:50 PM, Norman Feske < > norman.feske(a)genode-labs.com> > wrote: > > > Hello, > > > > > The easiest approach is possibly to create a custom tool chain, and > port > > > the GCC C++ library that way. I know the people behind Genode did some > > > of this (http://genode.org/download/tool-chain) although I'm not sure > > > how much of the C++ standard library they actually support. > > > > more in-depth information about Genode's tool chain are provided by > > Section 7.2 of the documentation [1]. In short, the tool chain is a > > "bare metal" tool chain that does not depend on a C library, yet it > > still supports C++ (including exceptions and runtime type information). > > > > On Genode, the libc and STL (aka stdcxx) can be used optionally whereas > > the STL depends on the libc. The libc is based on FreeBSD's libc. The > > STL is GCC's version. Both libraries are available via Genode's ports > > mechanism. > > > > That said, as both the libc and stdcxx are shared libraries, they cannot > > be used on the seL4 version of Genode as of now. Shared libraries don't > > work on seL4 (at least on x86_32) because the system-call bindings > > cannot be compiled with -fPIC. > > > > [1] http://genode.org/documentation/genode-foundations-15-05.pdf > > > > 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 > > > > _______________________________________________ > > Devel mailing list > > Devel(a)sel4.systems > > https://sel4.systems/lists/listinfo/devel > > >

2 1

Does sel4 support c++
by Yuxin Ren 20 Jun '15

20 Jun '15

Hi, Can I run C++ programs on sel4? I am not familiar with programming language. I do not know the relationship between the OS and the C++ language. In order to run C++, does the OS need to provide some support or what user level library are needed? Thanks a lot. Yuxin

4 6

Virtualization extensions
by Nick Betteridge 16 Jun '15

16 Jun '15

Hi I'm very interested in working with the virtualization extensions on sel4 - is there any rough timeline for when these will be available. Thanks Nick

1 0

high-availability system should have these software services
by XilongPei(裴喜龙) 15 Jun '15

15 Jun '15

Hi, In general, a high-availability system should have the following software services http://electronicdesign.com/boards/high-availability-rtoss-deliver-five-nine s-reliability : - Heartbeat support for each server and each application. - Event management capability for change notification. - Alarm management for error handling. - Transactions capability for check-pointing and rollback/restart. - Clustering for server management and applications links. - Reliable storage support for RAIDs and for journaling file systems. I want to develop a high-availability system on seL4, can anyone give me some suggestions? QNX has high availability support http://www.qnx.com/developers/docs/6.3.0SP3/neutrino/sys_arch/ham.html , can we learn something from them? Xilong Pei Tongji University 2015/6/11

6 7

[sel4] seL4 on RISC-V is running SOS (Simple Operating System)
by Hesham ALMatary 09 Jun '15

09 Jun '15

Hi all, This is the second status update of the project (Porting seL4 to RISC-V). Please have a look at the blog post [1] for more details, and feel free to ask and/or comment. You feedback would be appreciated. [1] http://heshamelmatary.blogspot.co.uk/2015/06/sel4-on-risc-v-is-running-sos-… Thanks, -- Hesham

2 1

Sel4 and Network
by Haselauer Lukas - S1410304006 03 Jun '15

03 Jun '15

Hello, My name is Lukas and I am currently studying in Austria. I am currently using sel4 in a student's project. We are using CAmkES to develop a small application (on the imx6-platform), and some things already work fine :-) But when it comes to networking, we are totally without results. We tried using some of the excisting libraries (libethdrivers + libplatsupport + liblwip) - but without success. My question is: Which way can I go if I want my CAmkES Apps to communicate via ethernet? Do I have to implement a driver as part of the App? As an additional library? Or somewhere else? I really couldn't figure out how to do it properly... Is there some sort of documentation or example on how to get a IP-stack up and running on sel4? Thank you for reading and helping! Lukas

2 1

Hello world - simple example thread creation
by Piotr 31 May '15

31 May '15

I would like to start from scratch - simple thread or process creation helloworld in seL4. I saw there are some examples in "sel4test/app" of seL4 application, but I am looking for something smaller. I have found here on page 39 "Creating a Thread in Own AS and cspace_t" http://www.cse.unsw.edu.au/~cs9242/14/lectures/01-intro.pdf example of thread creation. Unfortunetly I cannot find header file with " cspace_ut_retype_addr" or "ut_alloc". Are they obsolete, any replacements? Are there any small and simple hello-world tutorials or examples avaliable?

1 0

why do there are some differences between camkes branch and master branch in lib seL4/libsel4muslcsys
by Pei.XiLong(裴喜龙) 29 May '15

29 May '15

Hi, Siwei Zhuang, Why do there are some differences between camkes branch and master branch in lib seL4/libsel4muslcsys? The lib seL4/libsel4muslcsys is the foundation of libmuslc, it shoud be a libc for any seL4 program, and there should be no diference among any branches. https://github.com/seL4/libsel4muslcsys/commits/camkes Xilong Pei Tongji University 2015/5/29

3 3

[sel4] Porting seL4 to RISC-V - Status Report 1
by Hesham ALMatary 26 May '15

26 May '15

Hi all, As a warm up, I've written a blog entry [1] of the project giving some introductory details for both RISC-V and seL4 microkernel and what has been done so far. Open to questions/suggestions. [1] http://heshamelmatary.blogspot.co.uk/2015/05/porting-sel4-to-risc-v-status-… Thanks, -- Hesham

2 3

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

Virtual address space (kernelBase) restriction
by Hesham ALMatary 23 May '15

23 May '15

Hi all, Is it a must that every platform/architecture mapped to virtual addresses higher than 0xF0000000? Thanks -- Hesham

1 0

lowRISC Google Summer of Code
by Stefan Wallentowitz 19 May '15

19 May '15

Hi all, I just wanted to take the chance to introduce Hesham ALMatary and myself. Hesham participates in Google's Summer of Code in the lowRISC organization and I am his mentor. During summer, Hesham will port seL4 to the RISC-V architecture, specifically for the lowRISC project. Please find more details here: http://www.lowrisc.org/blog/2015/05/summer-of-code-students-for-lowrisc/ Hesham and I will keep you updated about the progress, I believe he will also give updates in his blog: http://heshamelmatary.blogspot.it/. Best Regards, Stefan

2 1

sel4 example compilation - cygwin
by Piotr 12 May '15

12 May '15

Hi, I am trying to compile example from 'Download' tutorial under Cygwin. http://sel4.systems/Download/ What I get is: [KERNEL] [BF_GEN] arch/object/structures_gen.h [BF_GEN] plat/machine/hardware_gen.h [BF_GEN] api/types_gen.h [CPP] src/arch/ia32/machine_asm.s [AS] src/arch/ia32/machine_asm.o /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S: Assembler messages: /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:15: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:15: Error: junk at end of line, first unrecognized character is `o' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:20: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:20: Error: junk at end of line, first unrecognized character is `o' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:22: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:22: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:26: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:26: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:30: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:30: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:34: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:34: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:36: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:36: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:41: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:41: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:43: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:43: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:49: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:49: Error: junk at end of line, first unrecognized character is `i' .......... What to do with it?

4 3

CSpace: resolveAddressBits
by Norman Feske 04 May '15

04 May '15

Hello, I am trying to construct a custom CSpace for my root task using seL4's guarded page-table concept. At the 1st level, there is a CNode with a radix of 12 and a guard of 0. At the 2nd level, there is a CNode with a radix of 14 and a guard of 6. After copying the initial capabilities to the 2nd-level CNode, switching to this CSpace, and invoking a system call that takes a capability as argument (seL4_TCB_Suspend), the kernel tells me: <<seL4 [decodeInvocation/609 Te3ffa880 @10245c2]: Attempted to invoke a null cap #1.>> The problem seems to be a failed 'lookupCapAndSlot', which internally calls 'resolveAddressBits': https://github.com/seL4/seL4/blob/experimental/src/kernel/cspace.c#L138 While inspecting the function, it does not appeared to me why it does not consider any guard bits within the while loop. The 'levelBits' variable is simply set to 'radixBits'. Interestingly, the same function in the master branch looks different. Here, the 'guardBits' are taken into account, which is consistent with the documentation. I wonder, why differs the experimental branch to the master branch in this respect? Is there a way to construct the scenario above with the experimental branch? The only work-around I see is to allocate an intermediate CNode with a size of 2^6 that sits between the 1st and 2nd level. Or is there a better way? 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

2 2

Does sel4 support pthread?
by 小健 24 Apr '15

24 Apr '15

I am using sel4 to develop a multi-thread program on ARM platform. I know that sel4 support musl libc. But when I call __pthread_create the program returns an error. Does sel4 support pthread on ARM platform? By the way, I get the libmuslc from seL4test. So if there is a musl libc which has pthread inside that can be used by sel4, please tell me where I can get it. Thank you.

2 1

Port seL4 to allwinnerA20
by Jensen Zhang 20 Apr '15

20 Apr '15

Hello everyone, We have ported seL4 to allwinnerA20, although the cache cannot still work well. All tests passed, except for CACHEFLUSH0001 and CACHEFLUSH0002. A git clone can be gotten from here [1]. And the 'zener' directory in this project has a similar structure to sel4test. But there is a problem about TIMER API. For allwinnerA20, there are several registers (Timer IRQ Enable/Status Register) used by all timers. Both kernel and libsel4platsupport will use timers, and they have to use different timers. But some registers can be accessed by both kernel and libsel4platsupport. That's very dangerous! Because libsel4platsupport can disable the timer of kernel by modifying the register. How to solve this problem? [1] git clone http://elastos.org/review/HD-Elastos -- Jensen Zhang Tongji University

2 1

am335x patches - refos working
by Tim Newsham 14 Apr '15

14 Apr '15

RefOS is now working fine on am335x / beaglebone black. Patches attached. Tim

4 3

How to get a helper thread's TCB?
by Kun Cheng 11 Apr '15

11 Apr '15

Hi guys, Currently I'm working on something that requires threads can be moving between domains. I can run two domains now (trying to run more) and I'm trying to understand the content of domain.cxx in sel4-test. Each thread has TCB which contains the domain id of it. But after running through *struct helper_thread* and relevant data structures, I'm curious about how to retrieve a helper thread's domain id, which could help me verify that they're indeed moved to another domain. Best regards, Kun Cheng

1 0

Regarding Bootstrapping the Kernel
by Sebastian Lau 08 Apr '15

08 Apr '15

On the http://sel4.systems website, it says that like qnx, sel4 expects to be elf-loaded. Could you please explain what that means?

2 1

SeL4 As Hypervisor
by CACook＠quantum-sci.com 03 Apr '15

03 Apr '15

After weeks trying to make Xen pass through an Intel IGP to the VM, I've finally found that it simply doesn't work. That's enough time spent on that.... My goal is to use a microkernel for hypervisor, which supports up to 10 VMs that perform various functions. The most challenging one is a VM which plays video using hardware accel of the integrated graphics processor, and sends and receives commands over a USB device. All my VMs will be CentOS. >From the FAQ I infer that it requires coding skills to do anything more than install base seL4. True? If not, have others set up an seL4 machine with multiple VMs and written how they did it and how it went? I should note that I am not a coder, although I am well experienced with Linux admin and scripting.

3 3

libsel4cspace?
by Ted Cooper 27 Mar '15

27 Mar '15

I'm adapting the aos-2014 exercises from http://www.cse.unsw.edu.au/~cs9242/14/project/index.shtml so I can run them under IA32 qemu. Milestone 0's sos project depends on stuff from libsel4space, e.g. cspace_root_task_bootstrap(). From a cursory search, it seems like this library isn't on the seL4 github account. Is this because its functionality has been rolled into one of the other libsel4*, or because it's a course-specific library not intended to see the light of day?

2 1

Cannot run on more than 1 domian?
by Kun Cheng 26 Mar '15

26 Mar '15

Hey guys, It seems that sel4test can only run on 1 domian (with CONFIG_NUM_DOMAINS=1 in .config), I tried to set it to 4 or a larger one (<=16) but when I ran the image with qemu it gave me an error "seL4 failed assertion '_ndks_end - _ndks_start <= NDKS_SIZE' at /home/kenneth/sel4/sel4current/kernel/src/arch/ia32/kernel/boot_sys.c:447 in function try_boot_sys". Is there any other configurations or code that I have to change? PS: I've been suffering a problem that I can only receive devel digests recently but none of your emails could reach me. This is weird because I set no filter in gmail. Best regards, Kun Cheng

1 0

Getting Started
by Fred 25 Mar '15

25 Mar '15

>From the main page. "If you would like to learn how to build a system on seL4, you might want to follow the lectures and especially the seL4-based project of UNSW's Advanced Operating Systems course <http://cs9242.web.cse.unsw.edu.au/>." Request: Is it possible to obtain access to the recorded lectures as well as the notes? Also assignment templates appear to be only available to enrolled students. I understand that publicly posting solutions to the assignments may be a problem. e.g. git clone ssh:// YOURLOGIN@login.cse.unsw.edu.au//home/cs9242/public_html/current/project/files/aos-2014 Background: Our project is in the internally funded phase of an open-source platform for medical simulation and training (similar to SimMan). The system consists of intercommunicating modules where each module runs a minimal OS. Thanks

4 5

beagle bone docs on page?
by Tim Newsham 21 Mar '15

21 Mar '15

Now that sel4, sel4test and refos work on beaglebone, perhaps it could be mentioned on the sel4 web page? If there's anything I can do to help make that happen, please let me know. Tim

2 1

seL4 + Qubes OS Project
by WhonixQubes 21 Mar '15

21 Mar '15

Hello, I am the maintainer of the Qubes + Whonix project... https://www.whonix.org/wiki/Qubes Which is the port of Whonix OS (think a more secure Tor proxied VM) to Qubes OS, which has upstream integration into the Qubes codebase now. I am very interested in secure minimal kernels and hypervisors, and have been discussing these topics publicly and privately with other interested developers and investors recently. And I am also positioning to bring development resources to low-level projects that can achieve a more optimal (and verifiable) secure TCB than bloated Linux-based systems, as Qubes Dom0 is currently based upon. Actually being able to read through and know all the code that is running on a mission critical machine, a novel thought, huh. ;) I am most interested in this Qubes blurb on the seL4 website... https://sel4.systems/GettingStarted "Qubes is an open source operating system designed to provide strong security for desktop computing using virtualisation to provide isolation. Qubes is based on Xen. seL4 is a much better fit for Qubes. The project is to port Qubes to seL4 (or develop an alternative Qubes-like system for seL4)." I absolutely agree with this and would like to know more about what Qubes development project might already underway be in the seL4 community in order to consider the opportunity of providing some real assistance in the future. What's the status of this seL4 Qubes port project and who can I get in touch with to talk more about accomplishing it? Thanks! :) WhonixQubes

7 7

Emit debugging info
by Hesham ALMatary 19 Mar '15

19 Mar '15

Hi all, This is most likely a straight forward question: how can I get debugging symbols for the final image (if possible)? I am configuring/compiling seL4tests for example with "make kzm_simulation_debug_xml_defconfig", etc. And when I try to dump the generated "sel4test-driver-image-arm-imx31" content with "arm-none-eabi-objdump" command, I can't find any debugging symbols (function/variable names) although debugging flags are set. If the previous question is not valid, then how can I debug the generated image using QEMU/gdb if possible? and trace the program execution beginning from _start? Other solutions for debugging are appreciated. Thanks in advance. -- Hesham

2 2

About the latest commit of seL4 kernel
by Jensen Zhang 16 Mar '15

16 Mar '15

Hello, I found there are several little changes on the latest commit of seL4 kernel [1]. And you just changed the define of function "map_it_frame_cap" for arm, but not for ia32. I just wonder whether there are any further considerations, or it's just a mistake :) Thanks, [1] https://github.com/seL4/seL4/commit/4f12acd2703183c9f44fe097589b53eb53c599eb -- Jensen Zhang Tongji University

2 1

refos and sel4-test questions
by Tim Newsham 16 Mar '15

16 Mar '15

Is it possible to build and run sel4-test against the "experimental" kernel tree? if so, whats the process? On RefOS for my port, I'm seeing a weird problem with the timer code. It is mapping in the right phys addr for my timer device, and I can read the right ID register out, so it appears to be mapping the right memory, but the code to do a timer reset, which sets a reset bit then polls for the bit to return to zero, is getting stuck in an infinite loop. I verified that the loop isn't being altered by the compiler, and I verified that the same code runs fine in sel4 test. At this point I suspect one of two things 1) refos is allowing the mapping to happen with caching on (even though I asked it not to) or 2) something is wrong elsewhere with the "experimental" kernel (sel4-test is running on the "master" tree, and refos is using the kernel from the "experimental" tree). is there anything else I could be missing? any thoughts? -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com

3 2

Porting seL4 to RISC-V
by Hesham ALMatary 15 Mar '15

15 Mar '15

Hi all, I'm Hesham ALMatary a computer science research student at the University of York. I am considering porting L4 microkernel variants to RISC-V [2] (for both my research and Google Summer of Code), and Fiasco.OC is one of these variants, but I want to extend the options here by asking about seL4. Is this project would be: first applicable, and second of interest to you? And if yes, would you offer some help (guidance)? I am sending this message as suggested here [1] that I should contact you if I'm willing to port seL4 to a new platform. [1] http://sel4.systems/GettingStarted/ [2] http://riscv.org/ Thanks, -- Hesham

4 4

seL4 on Raspberry Pi
by da Tyga 11 Mar '15

11 Mar '15

> > IMHO, the biggest problem with the Raspberry Pi is that most of its I/O > (even the NIC) is connected through USB. A serial port is available > (albeit without level shifters). So, running the seL4test should be > possible without a USB stack, but as soon as you want to access a > keyboard, network or filesystem, you'll need one. You should keep in mind that seL4 is a microkernel. So the USB stack and drivers that depend on that stack should all be implemented as processes/tasks running on top of seL4. I know it is not cool to mention Minix here, but it and Plan9 suggest ideas as to how the layers above seL4 could be structured. As far as I can understand, seL4 is not an operating system, it is a microkernel upon which one or more operating systems could be built. The key reason to use seL4 would be due to it providing capabilities based isolation between the layers that run on top of it and thus preventing rogue processes from interfering with other processes.

3 2

A port to the Raspberry Pi 2?
by Sebastian Lau 10 Mar '15

10 Mar '15

Would a port of seL4 to the raspberry pi 2 be welcome because I'm interested in buying a raspberry pi 2 and building sel4 for it?

5 9

docker compatible? (was Re: MySQL - seL4)
by Raoul Duke 07 Mar '15

07 Mar '15

> wouldn't provide you much. What sel4 could buy > you is isolation between mysql and other applications > if you chose to run several processes on the same > machine. The processes themselves, including mysql, > would still be vulnerable to any internal vulnerabilities > they might have (sel4 is not a magic bullet). There's a lot of noise around Docker. I find it annoying for many reasons, including security -- although I do understand some of the attraction. It would be super keen in my mind if seL4 could offer something in that vein, could present itself as a nice alternative.

5 6

MySQL - seL4
by André Bispo 06 Mar '15

06 Mar '15

Hello guys,Do you think it is feasible to have MySQL running on top of seL4 and take advantage of the isolation mechanisms?I was looking into the microkernel, the CamKES project and the mailinglist, to find some answers but i think it would be very difficult, if not impossible to run MySQL on seL4.I'm trying to explore this possibility and i want to know your opinion before continue. Best regards,André Bispo.

3 2

USB booting problem
by André Bispo 05 Mar '15

05 Mar '15

Hello guys, i'm building myself a system for my thesis and i'm currently testing out the seL4.I was trying to boot the sel4test by USB following the tutorial described in another question on this mailing list.But syslinux seems to load the kernel and the test but nothing appears afterwards.This is the message shown: MBRLoading sel4kernel... okLoading rootserver... ok _ If anyone could help me out i'd be very grateful. Best regards,André Bispo.

3 3

am335x - configs and refos
by Tim Newsham 04 Mar '15

04 Mar '15

Attached are some patches for am335x support. I've started to play with refos, and can build it for am335x and run some of the startup (with release mode) but it hangs at some point.. still a work in progress. Also there's a few minor proofread tweaks on the refos doc. By the way, sel4test runs pretty well now in debug and release modes. Instructions are pretty straightforward: - build the project using the debug or release config - use objcopy to extract a raw binary from the ELF image - load the binary with uboot (I use "tftp", it defaults to the proper load address) - run it in uboot with "go 82000000" Tim

2 1

Joint a formally verified C compiler with seL4?
by Grissiom 02 Mar '15

02 Mar '15

Hi all, I've heard a formally verified optimizing C compiler: CompCert recently: http://www.absint.com/compcert/ HN: https://news.ycombinator.com/item?id=9130934 . So what benefit will there be if some one use CompCert as the compiler for seL4? -- Cheers, Grissiom

3 2

Re: [seL4] How are capabilities assigned
by Sebastian Lau 02 Mar '15

02 Mar '15

Hi, sorry if this sounds stupid but are address spaces and threads directly managed by the kernel as in are they allocated and identified by the kernel or is there another that helps the kernel?

2 2

ifc6410 loading instructions
by Joel Nider 26 Feb '15

26 Feb '15

Hi, I'm trying to follow the instructions for loading the test image for ifc6410 on this page: http://sel4.systems/Hardware/IFC6410/ I'm not clear about the second instruction "> ramdisk". It looks to me like this is a redirection with some missing parts. Can you please help me fill in the blanks? Thanks, Joel

2 2

question about repo
by Tim Newsham 21 Feb '15

21 Feb '15

This is slightly tangential to sel4.. but.. sel4 uses "repo" to tie together projects that span multiple github repos. I'm really unclear on the proper workflow for using repo. I would like to keep my local patches (and be able to pull down updates from the master repositories), and I would like to pick patches to contribute back. What would the normal flow for these be? Should I be forking each github project that I work with and then fork a master "repo" project to reference my versions, somehow? Is there a good online guide that covers this? Tim

2 1

[PATCH] - fix am335x spurious interrupt issue
by Tim Newsham 21 Feb '15

21 Feb '15

patch for seL4 kernel attached.

1 0

How are capabilities assigned
by Sebastian Lau 17 Feb '15

17 Feb '15

I have a question, how are capabilities assigned or given to processes? Is it through the kernel or can the root process (like init etc.) assign capabilities as well? Also is IPC managed by calls to the kernel? I have in mind to base something off of seL4 in the future but I'm not quite ready to start though and just want to get an understanding of how things work.

2 3

am335x patches
by Tim Newsham 17 Feb '15

17 Feb '15

This set of fixes pushes AM335x support closer to working. With these patches and the previously submitted bootloader fix (https://github.com/seL4/elfloader-tool/issues/2) sel4 can boot and the sel4test project can run through some of the test cases. There are still some notable ommissions like missing timer and uart features and lack of uart IRQ support. - sel4 kernel - fix up sel4 kernel support for the am335x timer - note: this still receives lots of spurious interrupts - libplatsupport - bring code into line with conventions used by other ports - bring the uart code to life. PIO only for now - support multiple timers - libsel4platsupport - bring code into line with conventions used by other ports -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com

2 2

am335x test PREEMPT_REVOKE hanging
by Tim Newsham 16 Feb '15

16 Feb '15

while running the am335x port through the sel4 test suite I'm getting a hang in the PREEMPT_REVOKE test. It appears the revoke_thread is getting created but it is never getting executed and hence the wait_for_helper on the revoke thread is hanging indefinitely.. Any idea what would cause this behavior? Tim

2 1

am335x and question
by Tim Newsham 14 Feb '15

14 Feb '15

I'm playing around with the am335x code now and have the sel4 test building but not working properly. If anyone else is interested in playing with this, let me know. I have a question about the boot loader, I'm seeing: if (UART_PPTR < kernel_info.virt_region_start) { printf("Jumping to kernel-image entry point...\n\n"); } else { /* Our serial port is no longer accessible */ } is this necessary? It looks like init_boot_pd established a 1:1 mapping for all addresses lower than the kernel vaddr (which for me is 0xf0000000). Shouldnt the UART be accesible here? I'm seeing the bootloader run up to mmu is turned on but nothing after that and trying to track down where the failure is happening. printf's after arm_enable_mmu are not working for me, and I don't understand if this is due to mmu bringup problems or something else. By the way, I started a "#seL4" channel on freenode IRC. -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com

2 2

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 delegation of merely a single capability for each IPC whereas the Genode API does not have such a restriction. It effectively renders my idea for working around the capability re-identification problem [1] by representing each Genode capability by a tuple (or triple) of seL4 endpoint capabilities moot. [1] http://sel4.systems/pipermail/devel/2014-November/000112.html Is there a fundamental reason for this restriction? If not, would you be open to make the kernel more flexible with regard to the maximum number of delegations per IPC? 2. Aliasing of unwrapped capabilities with delegated capabilities I understand that the kernel will automatically "unwrap" capabilities if the receiver imprinted a badge into the received capability. In my experiments, the mechanism works as expected. However, how can the receiver determine, which capability got unwrapped if multiple capabilities were transferred? For example, if the sender specifies three capabilities, two of them "unwrappable" and one delegated, the receiver will see 3 capabilities. The delegated cap is written to the specified 'ReceivePath' whereas the badges of the two unwrapped caps can be read from the message buffer. But I see no way for the receiver to decide, which of the three capability arguments got unwrapped and which got delegated. How could the receiver determine this information? 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

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/libplatsupport/src/plat/am335x/dm.c has several coding mistakes, like: in function dm_stop_timer() the 'timer' is undeclared in function dm_periodic() dm is undeclared in function dm_get_timer() timer->properties.upcounter = false; but 'false' is undeclared timer->properties.bitwidth = 32; should probably be timer->properties.bit_width = 32; and timer->start = dm_timer_start; timer->stop = dm_timer_stop; should probably be: timer->start = dm_start_timer; timer->stop = dm_stop_timer; also I got a redundant redeclaration of 'ki_end' in sel4test/kernel/src/plat/am335x/machine/hardware.c which the compiler thought the previous declaration of ki_end was in : sel4test/kernel/src/arch/arm/kernel/boot.c So I am just wandering if beaglebone support is still under development? If any of you run sel4 successfully on beaglebone black, please give me some instructions. Currently I removed building platform independent libraries from menuconfig and the compilation went well. But I don't think it's a good idea. And I also find the cross tool chains which is recommend for Debian Wheezy on the http://sel4.systems/Download/DebianToolChain.pml seems to be not working well for compiling beagle configs. I got cc1 options error during compiling which is due to that some of the options are supported by gcc 4.5 or later while the recommended one is based on gcc 4.4. Best regards, Kun Cheng

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

i.MX6 quad booting problems
by Will Korteland 25 Dec '14

25 Dec '14

Hi everyone, I hope I'm using the correct list for this type of thing... I've bought my own Sabre Lite (identical to the AOS boards), and I've been trying for a few days now to get it to boot from tftp. I've downloaded the prebuilt u-boot.bin from the Sabre Lite hardware page, but it still doesn't seem to be working - it keeps timing out when trying to do the transfer. I think my tftp server is set up correctly, since it is the same as it was during AOS last semester. Could someone please boot a Sabre Lite set up for TFTP, interrupt the default boot process, type "printenv" into the U-Boot prompt and paste the results? Sorry if this is the wrong place to ask. Thanks, - Will

2 4

page permissions - execute?
by Tim Newsham 24 Dec '14

24 Dec '14

Is there no "execute" permission that can be set (or not set) on mapped pages in sel4?

4 3

(no subject)
by Jensen Zhang 24 Dec '14

24 Dec '14

Hi Will, About the message, "Unknown command 'bootelf'", it seems that this command wasn't configured and compiled. You'd better recompile th u-boot image. You can modify the source code to config this command. Add a macro define "#define CONFIG_CMD_ELF" in the file "include/config_cmd_default.h" to enable the command "bootelf". This link can help you, http://elastos.org/redmine/issues/17472#change-34139. Lucky! -- Jensen Zhang Tongji University

1 0

Run seL4 on OMAP4
by 张静轩 22 Dec '14

22 Dec '14

Hi, We have run the seL4 on pandaboard[1] (omap4 platform). It seems that the kernel works well, excpet for some tests about timer. Is there anyone interested in it or helping us? The source code can be got from the following link[2] now. (We will upload to github latter.) btw. I think the devices and platforms supported by seL4 are too few. How to make it easy to let seL4 support more devices? Can anyone give me some suggestion? I suggest to write a document to port seL4 easier. :) --- Jensen Zhang Tongji University 2014/12/22 [1] http://pandaboard.org/ [2] http://elastos.org/review/#/admin/projects/HD-Elastos

2 1

Re: [seL4] Devel Digest, Vol 7, Issue 3
by Kenneth 20 Dec '14

20 Dec '14

Hi Pei, Maybe you could make it happen on cmkes. As far as I know it's a set of OS' services for sel4, just like Iguana for OKL4. FS should be a service, so I think it's better ported into cmkes. This email is typed on my iPhone. I'd like to apologize for any mistake in it. > 在 2014年12月20日，9:00，devel-request@sel4.systems 写道： > > 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. I want to port a filesystem onto seL4 (XilongPei (???)) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 19 Dec 2014 14:20:22 +0800 > From: XilongPei(???) <pei_xilong(a)tongji.edu.cn> > To: <devel(a)sel4.systems> > Subject: [seL4] I want to port a filesystem onto seL4 > Message-ID: <01c401d01b53$e054be30$a0fe3a90$(a)tongji.edu.cn> > Content-Type: text/plain; charset="gb2312" > > Hi, > I want to port a filesystem onto seL4, the source code is here: > https://github.com/RT-Thread/rt-thread/tree/master/components/dfs Can anyone > give me some suggestion? > > > Xilong Pei > Tongji University > 2014/12/19 > > > > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > ------------------------------ > > End of Devel Digest, Vol 7, Issue 3 > ***********************************

3 2

I want to port a filesystem onto seL4
by XilongPei(裴喜龙) 19 Dec '14

19 Dec '14

Hi, I want to port a filesystem onto seL4, the source code is here: https://github.com/RT-Thread/rt-thread/tree/master/components/dfs Can anyone give me some suggestion? Xilong Pei Tongji University 2014/12/19

1 0

what is fastpath
by Pei.XiLong(裴喜龙) 17 Dec '14

17 Dec '14

Hi, Who can give me some description about seL4 fastpath? Xilong Pei 2014/12/17

2 1

wrong word spelling in program
by XilongPei(裴喜龙) 27 Nov '14

27 Nov '14

Hi, Who wrote the program in file $/libplatsupport/plat_include/omap4/platsupport/plat/gpt_constants.h , GPT4_DEFICE_PADDR is wrong spelled, it should be GPT1_DEVICE_PADDR. static void *paddrs[] = {(void *) GPT1_DEVICE_PADDR, (void *) GPT2_DEFICE_PADDR, (void *) GPT3_DEFICE_PADDR, (void *) GPT4_DEFICE_PADDR, (void *) GPT5_DEFICE_PADDR, (void *) GPT6_DEFICE_PADDR, (void *) GPT7_DEFICE_PADDR, (void *) GPT8_DEFICE_PADDR, (void *) GPT9_DEFICE_PADDR, (void *) GPT10_DEFICE_PADDR, (void *) GPT11_DEFICE_PADDR}; Xilong Pei Tongji University 2014/11/19

2 1

Confused on porting/using musl lib c
by chengkunck＠gmail.com 27 Nov '14

27 Nov '14

Hi All, I want to use musl lib c but I'm a little confused on the following two projects: libmuslc and musllibc. I went through their Kconfig and brief intros, so my question now is do I need them both to port/use musl lib c on sel4? It might be a dumb question but I'm stuck here, any help is appreciated. Best regards, Kenneth

2 2

where can I get beagle_run_elf program
by XilongPei(裴喜龙) 21 Nov '14

21 Nov '14

Hi, In the Makefile, a program beagle_run_elf is referred, Where can I get it? --------------------------------------- # This relies on a helper script to build a bootable image simulate-beagle: beagle_run_elf images/sel4test-driver-image-arm-omap3 --------------------------------------- Xilong Pei Tongji University 2014/11/19

2 1

run seL4 on pandaboard
by Pei.XiLong(裴喜龙) 14 Nov '14

14 Nov '14

Hi, I have built an image for my pandaboard, but I have no bootelf u-boot command, I use go command instead, get the following error: Panda # fatload mmc 0 0x82000000 sel4test-driver-image-arm-omap3 Panda # go 0x82008000 ## Startting application at 0x82008000 ... after this message, the system is dead. How to do next? Xilong Pei Tongji University 2014/11/14

1 0

Re-identification of capabilities
by Norman Feske 13 Nov '14

13 Nov '14

Hello, I hope you don't mind me spamming the list with my problems. I have a question about the association of capabilities with process-local meta data. As far as I understand, the "badging" of capabilities is the recommended mechanism for servers to attach a server-local meaningful value to a capability. After having handed out the capability to a client, it gets this value reported each time the client (or any other process to which the capability was delegated to) invokes the capability or delegates the capability back to the server (e.g., as RPC argument). Now, I have the following scenario: There are three processes, a factory (F), a mediator (M), and a client (C). The factory is responsible for physically allocating objects (e.g., in Genode's case, one example would be the core process that hands out dataspaces). The mediator is a process that sits in-between the client and the factory (in the Genode world, this could the the init process). It keeps records about the allocation and may use this information to implement a policy. The client is the designated user of the object. To create an object, C will call M, which, in turn, will call F on behalf of C: alloc create F <-------- M <--------- C F will create the actual object and a corresponding badged capability and returns the badged capability as return value to M. Because M wants to keep records about the lifetime and parameters of the created objects, it needs to associate a process-local meta-data structure to the capability. badged cap F ---------> M C : (meta data <-> cap) M stores the meta data in a process-local data base using the cap as key. It then hands out the cap to the actual client. Sometime later, the client decides to destroy the object (or perform another operation at M that takes the cap as argument): badged cap F M ---------> C | | uses object (e.g., invoking the cap) destroy | (cap arg) | ? <----------+ When M receives the destroy request with the cap of the to-be-destroyed object as argument, it wants to look up the corresponding meta data from its data base. But unfortunately, the cap argument of the destroy function got assigned a new local name within M (some number within the receive window of M). How can M find the meta data associated with the allocated object? 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

5 8

the omap3 image can't run on pandaboard
by XilongPei(裴喜龙) 13 Nov '14

13 Nov '14

Hi, The OMAP3 Beagle board is too out of date, I buy a pandaboard http://omappedia.org/wiki/PandaBoard , but the omap3 image can't run on this board. The error information look like these: ----------------------------------------------------------------- Panda # Panda # fatls mmc 0 31644 mlo 208784 u-boot.img 4782336 uimage 208273 uinitrd 449 boot.scr 3092757 sel4test-driver-image-arm-omap3 9 file(s), 0 dir(s) Panda # fatload mmc 0 0x81ff8000 omap3 reading sel4test-driver-image-arm-omap3 3092757 bytes read Panda # go 0x82000000 ## Starting application at 0x82000000 ... data abort MAYBE you should read doc/README.arm-unaligned-accesses pc : [<820024bc>] lr : [<82002194>] sp : 822d7f78 ip : 00000000 fp : 822d7f84 r10: 00000002 r9 : 00000000 r8 : bfefdf68 r7 : bffabd14 r6 : 82000000 r5 : bfeffd5c r4 : 00000002 r3 : 49020014 r2 : 00000001 r1 : 00000000 r0 : 0000000a Flags: Nzcv IRQs off FIQs off Mode SVC_32 Resetting CPU ... resetting ... ----------------------------------------------------------------- Who can give me some help? thanks first! Xilong Pei Tongji University Shanghai China 2014/11/13

1 0

seL4 : Queries
by Yashwardhan Singh 10 Nov '14

10 Nov '14

Hi I am trying to modify the seL4 scheduler as a part of my project. I was wondering if there is any function present in the library OS like scanf which can help me in writing an interactive process , to measure the response time of the scheduler for interactive process. I was also curious if there is any shell like framework for sel4, from which multiple processes can be started concurrently and so that they run in background. Is there a benchmark suite for generation of performance metrics using the data structures present in /kernel/src/arch/ia32/api/benchmark. Please help. Thanks and Regards Yash

2 1

Clang & LLVM
by da Tyga 08 Nov '14

08 Nov '14

Hi ! There seems to be a general trend towards using Clang / LLVM in the ARM area. AFAIK ARM are going LLVM for V8. Is it viable to do seL4 work with that environment? Cheers!

1 0

Reasoning behind the root cnode's guard value
by Norman Feske 06 Nov '14

06 Nov '14

Hello, the seL4 kernel constructs the root task's CNode (in kernel/boot.c) by using the configurable number CONFIG_ROOT_CNODE_SIZE_BITS as size and a guard value calculated as 32 - CONFIG_ROOT_CNODE_SIZE_BITS. I understand that it makes the capability name space nicely linear. But on the hand, doesn't it impede the number of kernel objects addressable by root task? When using Genode's core as root task on seL4, I will need to maintain a large number of capabilities to kernel objects, in particular one for each page managed by the core process. Naturally. I would like to organize the root task's capability namespace hierarchically, allocating CNodes depending on the dynamic work load. As far as I understand, however, root task would have no way to address slots within such additional CNodes because all address bits are already consumed by the root CNode indices + guard. For example, how is root task supposed to specify capabilities that are not contained in the root CNode as "service" argument to functions like 'seL4_TCB_WriteRegisters'? One way I see would be to move capabilities back and forth between the root CNode and other CNodes using 'seL4_CNode_Copy', effectively using the root CNode as a kind of CNode cache. But this solution seems overly complicated. Another way would be to dimension CONFIG_ROOT_CNODE_SIZE_BITS pessimistically. But introducing such an upper bound a-priory would somehow contradict with seL4's otherwise nicely dynamic resource management. Yet another way would be to let root task use a smaller guard value that leaves enough bits available to be used for second-level or third-level CNodes. But since that would require a change of the kernel code, I suspect that this approach is not in line with right seL4 way. Could you share the reasoning behind the guard-value calculation and help me to get on the right track? Or would you consider a configurable guard value for root task as a reasonable feature request? 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

2 2

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

x86 Bootable USB install
by Matthew Scaperoth 14 Oct '14

14 Oct '14

Hello, I am at the George Washington University working on benchmarking the seL4 system. I am new to systems, and I am having a hard time building a bootable USB image On Ubuntu 14.04 x86. I understand that there is a Grub2 stanza on the Downloads page <https://sel4.systems/Download/> on the SeL4 website, but I cannot find the sel4kernel and sel4rootserver files in the system to build into a boot image. I would like to build an image using a process similar to the one in Pistachio (see https://www.l4ka.org/120.php) except for using Grub2 of course. Are there instructions for booting on full hardware such as a PC? Regards, Matthew Scaperoth Jr. Programmer Analyst The George Washington University Academic Technologies Tel: 202-994-6907

5 7

How is the sel4test-driver process created?
by Yuxin Ren 14 Oct '14

14 Oct '14

Hi All, Now I am working on sel4test project. I know there is a process for sel4test-driver, and it will spawn new process which does the actual testing. But I want to know how the sel4test-driver process is created, especially how its memory and capability is set up. Could anyone show me the code for those stuff and it is great if give me some explanation or comments about it? Thank you very much Yuxin

4 3

Console Output for Test Files in seL4test-manifest?
by Matthew Scaperoth 12 Oct '14

12 Oct '14

Hey All, First, thank you for your responses so far. This message board has been helpful with learning seL4. While we have been working to benchmark the seL4 system on bare metal we have run into some trouble trying to figure out how to get output to the console instead of serial. For our tests we are using the existing seL4test-manifest files and defining custom tests within the apps/sel4test-tests/src/tests/ipc.c file. We noticed that the test output will only go to serial. We have tested with and without the debug configuration. We would like to see all output go to console. We have tried to remove debug defines on the system call path for __arch_putchar() which seems to only affect the serial output. These system calls don't seem to affect the direction of the output, but only what is being output to serial. Is there a driver missing from the test libraries that defines the console output? Is there a specific way to output to console when working with tests. To test these settings we are working with a 32-bit build and are using syslinux to create a bootable USB to test on bare metal. Regards, Matthew Scaperoth Jr. Programmer Analyst The George Washington University Academic Technologies Tel: 202-994-6907

2 1

Is this path wrong?
by Harry Butterworth 05 Oct '14

05 Oct '14

diff --git a/lib/WPTutorial.thy b/lib/WPTutorial.thy index f6ecd0a..cd0d992 100644 --- a/lib/WPTutorial.thy +++ b/lib/WPTutorial.thy @@ -9,7 +9,7 @@ *) theory WPTutorial -imports Bits_R +imports "../proof/refine/Bits_R" begin text {*

1 0

Error in comment in abstract spec Syscall_A.thy
by Harry Butterworth 05 Oct '14

05 Oct '14

diff --git a/spec/abstract/Syscall_A.thy b/spec/abstract/Syscall_A.thy index e308501..6576f78 100644 --- a/spec/abstract/Syscall_A.thy +++ b/spec/abstract/Syscall_A.thy @@ -72,7 +72,7 @@ occured in the first operation); this second operation may result in an error; \item the error handler @{text h_error} to execute if the second operation resulted in an error; -\item the third and last operation @{text h_error} to execute (if +\item the third and last operation @{text m_finalise} to execute (if no error occured in the second operation); this operation may be interrupted. \end{itemize}

1 0

several questions about seL4
by 조현우 25 Sep '14

25 Sep '14

Hi I am new in seL4. It is really interesting OS. I would like to ask some questions even though the FAQ explains many things. 1. How different is seL4+VMM with OKL4 or codezero? If there is some performance gap between them, I am curious where the overheads are for? 2. I am wondering how well seL4 can support virtualization services. Can seL4 supports more than two linux simultaneously on the VMM layers? Moreover, can it execute different kind of guest OSes at the same time? What about RTOS? A RTOS can be executed with keeping their real time property on the seL4+VMM?? Lastly, I would like to know when new version of the VMM for A15 support will be released. 3. Did you use a code generator when you hit the steps for “Specification”, “Haskell Prototype” and “C code” In the Proof Processing? If you did it using any automatic tool, I am so curious how you verified and validated the codes. 4., According to the FAQ, current multicore support is through a multikernel configuration. Do you have any plan for one seL4 kernel to manage several processors? Thank you much in advance. Regards, Joe.

2 1

Building a Custom Test
by Matthew Scaperoth 23 Sep '14

23 Sep '14

Hello All, First I wanted to say thank you for this dev forum. The more I learn about SeL4 the more I am amazed with how well it is written. I am working on a 32-bit Ubuntu 14.04 and I would like to run your individual test suites in the sel4-manifest with a 32-bit build. Specifically some of the tests from the https://github.com/seL4/sel4test/tree/master/apps/sel4test-tests/src directory. For example, I'd like to alter the code a little bit and run qemu to output cycle time for IPC or memory mapping. So potentially I would boot up the image, the files would load and I would get an output saying "Intra-as IPC 151 cycles" or something along those lines after the test was automatically run. I was reading through the files and noticed that the main.c accepts arguments to say which test I'd like to run using the find_test() method with the argv passed in. I am now trying to find a way to use the main.c file in sel4test-tests to achieve the build I am after. I also noticed that a .bin file and a another file in stage/ia32/pc99/bin/sel4test-tests are generated when you run the first top-level make after the configuration. So I have tried booting the sel4test-tests file in qemu with qemu-system-i386 -m 512 -serial stdio -kernel images/kernel-ia32-pc99 -initrd stage/ia32/pc99/bin/sel4test-tests but nothing happens. My thought process was that it could replace the driver image for ia32 pc99 (sel4test-driver-image-ia32-pc99) . So I am missing a piece here (or pieces?). I am not sure if there is a Makefile that I can alter to include only a specific test, or if it's something else entirely. I'd be happy to clarify what I aim to achieve or details about my system if necessary. Also, I am really enjoying the code that generates these tests in the main.c file mentioned earlier. I feel like it is a much more graceful solution to running these tests than other l4 systems I've worked with. Thanks again, Matt

1 1

Re: [seL4] Fault Tolerant Operating System for ______________
by da Tyga 19 Sep '14

19 Sep '14

> > Date: Thu, 18 Sep 2014 15:58:29 +0800 >> From: XilongPei(???) <pei_xilong(a)tongji.edu.cn> >> To: "'Aniruddha Bhide'" <aniruddha.360(a)gmail.com>, "'Peter Chubb'" >> <peter.chubb(a)nicta.com.au> >> Cc: devel(a)sel4.systems >> Subject: [seL4] ??: x86 Bootable USB install >> Message-ID: <007c01cfd316$565647b0$0302d710$(a)tongji.edu.cn> >> Content-Type: text/plain; charset="utf-8" >> Hi, >> I am at Tongji University (China, http://www.tongji.edu.cn/english/ ), I >> want to build a Fault Tolerant Operating System for high speed railway. >> >> The seL4 is just a micro-kernel operating system, there is still no >> centre-service to let it work as a PC operating system, and it still can?t >> work as a virtual-machine, such as VirtualBox. There are a lot of works >> should be done before seL4 used as a really operating system. >> >> Xilong Pei >> 2014/9/18 > > > > You are correct. seL4 is a microKernel upon which an operating system could be built. Instead of writing a proprietary OS for your high speed railway (of which there are several already in operation, e.g in France, Germany) you might want to consider porting an existing OS to run on top of seL4, or even better build your specific requirements on top of a robust OS such as those found at http://cog.systems/products.shtml.

1 0

[PATCH] trivial: remove redundant newline in fail() calls.
by Eduard Nicodei 19 Sep '14

19 Sep '14

Hello, I have noticed certain fail() calls include newline. This does not seem necessary since fail() is defined as printf( "seL4 called fail at %s:%u in function %s, saying \"%s\"\n", file, line, function, s ); Which causes affected error messages to contain a single " character on a new line. Patch attached. Regards, Eduard Nicodei

1 0

Sel4 on Pi
by Robert Clove 09 Sep '14

09 Sep '14

Hi All, I am all new to this raspberry pi.I was trying to port sel4 ( https://github.com/seL4/seL4) on raspberry pi but the build instruction ( http://sel4.systems/Hardware/General/) are only for another board. Has anyone successfully ported sel4 on pi. Please guide me Another query does sel4 has networking stack? Regards

2 3

More detailed `running on hardware' instructions
by Peter Chubb 15 Aug '14

15 Aug '14

Hi Folks, I've put up reasonably detailed instructions on how to build and run seL4test on the Sabre Lite, BeagleBoard, Odroid XU and IFC6410. I'm still working on instructions for the Arndale. See http://sel4.systems/Hardware -- Dr Peter Chubb peter.chubb AT nicta.com.au http://www.ssrg.nicta.com.au Software Systems Research Group/NICTA

2 2

Is the log of seL4test right?
by Alex Chih Hu 13 Aug '14

13 Aug '14

Hi, I download seL4test, and then run it. Is the log correct? -------------------------------------------------------------------------------------------- $ make simulate-ia32 qemu-system-i386 \ -m 512 -nographic -kernel images/kernel-ia32-pc99 \ -initrd images/sel4test-driver-image-ia32-pc99 Switching to a safer, bigger stack... seL4 Test ========= INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 31 type 0 Failed to allocate object of size 2147483648, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 30 type 0 Failed to allocate object of size 1073741824, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 29 type 0 Failed to allocate object of size 536870912, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 28 type 0 Failed to allocate object of size 268435456, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 27 type 0 Failed to allocate object of size 134217728, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 26 type 0 Failed to allocate object of size 67108864, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 25 type 0 Failed to allocate object of size 33554432, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 24 type 0 Failed to allocate object of size 16777216, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 23 type 0 Failed to allocate object of size 8388608, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 22 type 0 Failed to allocate object of size 4194304, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 21 type 0 Failed to allocate object of size 2097152, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 20 type 0 Failed to allocate object of size 1048576, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 19 type 0 Failed to allocate object of size 524288, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 18 type 0 Failed to allocate object of size 262144, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 17 type 0 Failed to allocate object of size 131072, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 16 type 0 Failed to allocate object of size 65536, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 15 type 0 Failed to allocate object of size 32768, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 14 type 0 Failed to allocate object of size 16384, error 1 INFO :_allocman_utspace_alloc:301: Regular utspace alloc failed and not watermark for size 13 type 0 Failed to allocate object of size 8192, error 1 <testsuite> <testcase classname="sel4test" name="TEST_CNODEOP0001"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP0002"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP0003"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0003 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP0004"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0004 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP0005"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0005 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP0006"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0006 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP0007"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0007 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP0008"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0008 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP0009"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0009 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CSPACE0001"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CSPACE0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_DOMAINS0001"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_DOMAINS0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_DOMAINS0002"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_DOMAINS0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_DOMAINS0003"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_DOMAINS0003 </system-out> </testcase> <testcase classname="sel4test" name="TEST_FPU0000"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_FPU0000 </system-out> </testcase> <testcase classname="sel4test" name="TEST_FPU0001"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_FPU0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_FRAMEEXPORTS0001"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_FRAMEEXPORTS0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_FRAMERECYCLE0001"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_FRAMERECYCLE0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC0001"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC0002"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC0003"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC0003 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC0004"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC0004 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC0010"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC0010 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC1001"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC1001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC1002"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC1002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC1003"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC1003 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC1004"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC1004 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT0001"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT0002"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT0003"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT0003 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT0004"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT0004 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT0005"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT0005 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT1001"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT1001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT1002"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT1002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT1003"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT1003 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT1004"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT1004 </system-out> </testcase> <testcase classname="sel4test" name="TEST_RECYCLE0001"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_RECYCLE0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_RECYCLE0002"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_RECYCLE0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_REGRESSIONS0001"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_REGRESSIONS0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_RETYPE0000"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_RETYPE0000 </system-out> </testcase> <testcase classname="sel4test" name="TEST_RETYPE0001"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_RETYPE0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_RETYPE0002"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_RETYPE0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SCHED0002"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SCHED0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SCHED0003"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SCHED0003 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SCHED0004"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SCHED0004 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SCHED0005"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SCHED0005 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SCHED0006"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SCHED0006 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL0000"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0000 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL0001"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL0002"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL0003"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0003 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL0004"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0004 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL0005"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0005 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL0006"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0006 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL0010"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0010 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL0011"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0011 </system-out> </testcase> <testcase classname="sel4test" name="TEST_THREADS0004"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_THREADS0004 </system-out> </testcase> <testcase classname="sel4test" name="TEST_THREADS0005"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_THREADS0005 </system-out> </testcase> <testcase classname="sel4test" name="TEST_TRIVIAL0000"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_TRIVIAL0000 </system-out> </testcase> <testcase classname="sel4test" name="TEST_TRIVIAL0001"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_TRIVIAL0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_TRIVIAL0002"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_TRIVIAL0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_VSPACE0000"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_VSPACE0000 </system-out> </testcase> <testcase classname="sel4test" name="TEST_VSPACE00002"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_VSPACE0000 </system-out> </testcase> <testcase classname="sel4test" name="TEST_TRIVIAL00022"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_TRIVIAL0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_TRIVIAL00012"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_TRIVIAL0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_TRIVIAL00002"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_TRIVIAL0000 </system-out> </testcase> <testcase classname="sel4test" name="TEST_THREADS00052"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_THREADS0005 </system-out> </testcase> <testcase classname="sel4test" name="TEST_THREADS00042"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_THREADS0004 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL00112"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0011 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL00102"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0010 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL00062"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0006 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL00052"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0005 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL00042"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0004 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL00032"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0003 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL00022"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL00012"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SYSCALL00002"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SYSCALL0000 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SCHED00062"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SCHED0006 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SCHED00052"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SCHED0005 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SCHED00042"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SCHED0004 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SCHED00032"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SCHED0003 </system-out> </testcase> <testcase classname="sel4test" name="TEST_SCHED00022"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_SCHED0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_RETYPE00022"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_RETYPE0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_RETYPE00012"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_RETYPE0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_RETYPE00002"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_RETYPE0000 </system-out> </testcase> <testcase classname="sel4test" name="TEST_REGRESSIONS00012"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_REGRESSIONS0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_RECYCLE00022"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_RECYCLE0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_RECYCLE00012"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_RECYCLE0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT10042"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT1004 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT10032"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT1003 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT10022"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT1002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT10012"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT1001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT00052"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT0005 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT00042"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT0004 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT00032"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT0003 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT00022"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_PAGEFAULT00012"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_PAGEFAULT0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC10042"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC1004 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC10032"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC1003 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC10022"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC1002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC10012"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC1001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC00102"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC0010 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC00042"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC0004 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC00032"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC0003 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC00022"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_IPC00012"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_IPC0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_FRAMERECYCLE00012"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_FRAMERECYCLE0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_FRAMEEXPORTS00012"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_FRAMEEXPORTS0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_FPU00012"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_FPU0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_FPU00002"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_FPU0000 </system-out> </testcase> <testcase classname="sel4test" name="TEST_DOMAINS00032"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_DOMAINS0003 </system-out> </testcase> <testcase classname="sel4test" name="TEST_DOMAINS00022"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_DOMAINS0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_DOMAINS00012"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_DOMAINS0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CSPACE00012"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CSPACE0001 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP00092"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0009 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP00082"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0008 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP00072"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0007 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP00062"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0006 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP00052"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0005 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP00042"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0004 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP00032"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0003 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP00022"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0002 </system-out> </testcase> <testcase classname="sel4test" name="TEST_CNODEOP00012"> INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08048000-->0808f718 INFO :sel4utils_elf_load_record_regions:276: * Loading segment 08091000-->081a9e80 <system-out> TEST_CNODEOP0001 </system-out> </testcase> </testsuite> 122/122 tests passed. All is well in the universe. Ignoring call to sys_exit_group Ignoring call to sys_rt_sigprocmask Ignoring call to sys_gettid Ignoring call to sys_getpid sys_tgkill assuming self kill QEMU 1.5.0 monitor - type 'help' for more information (qemu) q -------------------------------------------------------------------------------------------- The "All is well in the universe" is displayed. But on boot, there are the log "Failed to allocate object of size 2147483648, error 1". Is this item log right? Why there are the these log "Failed to allocate object of size XXXXXXXXXXX, error 1"? Regards, Hu Zhi

2 1

Instructions on using the haskell simulator
by Prashanth Mundkur 10 Aug '14

10 Aug '14

These seem to be missing from the system documentation, especially on how to use it with qemu. I've built the simulator, but am unsure how to use it. The build generates a libHSSEL4-0.3.a, but I can't find an executable anywhere. Also, the simulator manual says it is out-of-date, but the manual seems to include the Haskell literate sources directly. It also says the Haskell code is kept up-to-date. That sounds a bit contradictory. Are the comments in the sources that obsolete? --prashanth [Congratulations on the open-sourcing and excellent license choices!]

2 1

seL4test suite error when compiling for AM335X beaglebone
by Jorge Ventura 07 Aug '14

07 Aug '14

I am trying to create a test for beaglebone using the seL4test suite but I am having the following error: seL4Test/libs/libplatsupport/src/plat/am335x/dm.c:56:25: error: ‘timer’ undeclared (first use in this function) dm_t *dm = (dm_t *) timer->data; I just did "make menuconfig" and change: Architecture Type (ARM) ---> ARM CPU selection (Cortex A8) ---> Platform Type (AM335X (BeagleBone)) ---> Save the configuration and "make". Ventura

3 3

experiences running sel4 test on beagleboard
by Tim Newsham 07 Aug '14

07 Aug '14

Here is my experience building and running seL4 on the BeagleBoard (original, redboard, revision D). I'm hoping the notes will be helpful for others who arent very experience with this platform, like myself. Start with a BeagleBoard, a 5volt power supply (or the USB cable for power), a SDCard and an RS232 serial connector. Note: the BeagleBoard uses RS232 serial levels, not TTL levels, so you'll need some kind of RS232 connector. I used a USB<->RS232 (9-pin D-connector) cable. The beagle board has serial on header P9, which is a 2x5 header. P9 pin 2 (RX) <--> D-connector pin 3 (TX) P9 pin 3 (TX) <--> D-connector pin 2 (RX) P9 pin 5 (GND) <--> D-connector pin 5 (GND) I use "screen" or "cu" from linux to connect to the serial line with one of the following commands (note: I'm in linux and my account has permissions on /dev/ttyUSB0): $ cu -l /dev/ttyUSB0 -s 115200 $ screen /dev/ttyUSB0 115200 Verify that when you power on the device (no SDCard necessary yet) you get the u-boot bootloader in your terminal. Next get and build your seL4 image for the beagleboard. I'm running the sel4 test project in a debug build. You'll need to have the proper prerequisites, as covered in the sel4 build notes. $ mkdir sel4/beagle $ cd sel4/beagle $ repo init -u https://github.com/seL4/sel4test-manifest.git $ repo sync $ make beagle_debug_xml_defconfig $ make menuconfig # at this point I adjusted the tools prefix to # "arm-none-eabi-" to match the arm toolchain I have $ make At this point you've got an ELF image in the images dir. It has one section at 0x82000000 starting at offset 0x8000 in the file, and the start address is 0x82000000. Mount an SDCard with a FAT filesystem and nothing else on it and copy the image to your sdcard $ cp images/sel4test-driver-image-arm-omap3 /media/SDCARD/ $ umount /media/SDCARD now power off the beagle board, move the SDCard to the beagleboard, power it on and interrupt the u-boot sequence to get a boot loader prompt. Enter the following commands to boot the image. They will load the file so that offset 0x8000 is at 0x82000000 (by loading the entire file 0x8000 bytes before 0x82000000). Then it will jump to the entry point and run the sel4 loader, kernel and tests. mmc rescan 0 fatload mmc 0 0x81ff8000 sel4test-driver-image-arm-omap3 go 0x82000000 At this point sel4 is up and running and the test program is running through its tests! The full output of the tests can be seen at http://pastebin.com/cC0FTuqM There are some errors printed during the test, but happily the test ends with: 136/136 tests passed. All is well in the universe. Tim

2 1

dma and sel4
by Tim Newsham 06 Aug '14

06 Aug '14

Does the use of DMA invalidate security guarantees in the ARM ports (and KZM in particular) currently? -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com

4 3

Thanks for seL4, plus a digital Random Bit Generator
by TAG AUTO REPLY 06 Aug '14

06 Aug '14

I would like to thank the development teams and sponsoring institutions for releasing this amazing work into the public domain. It may be some time before the importance of this is fully understood by the software industry, but I believe we finally have a reference platform for how software is to be correctly engineered. You have raised the bar for all of us. I would also like to share with you a POSIX C implementation of a non-deterministic Digital Random Bit Generator for your evaluation. It can be downloaded from http://www.tag.md/public/ Kind regards, -MK

1 0

[PATCH] Use usr/bin/env for all python bangpaths to enable virtualenv
by Max R.D. Parmer 05 Aug '14

05 Aug '14

This patch targets the core "seL4" repo. I idly submitted a PR on github before reading anything at all really (beyond checking to see if the issue was made more consistent in subsequent commits). Apologies if this is/was inconvenient. I saw some prior github discussion on whether "python2" or "python" is best'; IMHO, "python" is best as virtualenv allows the desired binary to be specified at env creation time. CLA forthcoming, I'm quite a long way from printers/scanners and all those sorts of things. -- @maximus_freeman 0x7D964D3361142ACF

3 2

seL4 boot issue
by Jorge Ventura 05 Aug '14

05 Aug '14

I am trying to boot seL4 on beaglebone white. I have an initial code just to configure the DDR2 memory at range 0x80000000-0xbfffffff. As we can see below, the start address is the virtual address 0xf0000000 but at this point I have no MMU configured. I was thinking that the segment .boot should be the code to prepare all details about MMU/D-CACHE/I-CACHE but it's not what gdb is understanding based in the elf header. Someone could explain to me how is the kernel boot; what do I have to consider. I guess that beaglebone is not supported but this is exactly my goal, to make seL4 boot on beaglebone. Any help or suggestion is very welcome. Sincerely, Jorge Ventura (gdb) load kernel.elf > Loading section .boot, size 0x10000 lma 0x80000000 > Loading section .text, size 0xf1ec lma 0x80010000 > Loading section .text.unlikely, size 0xd98 lma 0x8001f1ec > Loading section .rodata, size 0x4170 lma 0x8001ff84 > Loading section .data, size 0x8 lma 0x800240f4 > Start address 0xf0000000, load size 147708 > Transfer rate: 319 KB/sec, 3787 bytes/write. > (gdb) monitor poll background polling: on TAP: am335x.dap (enabled) target state: halted target halted in ARM state due to debug-request, current mode: System cpsr: 0x6000019f pc: 0xf0000000 MMU: disabled, D-Cache: disabled, I-Cache: disabled

1 1

active development and verification
by Tim Newsham 05 Aug '14

05 Aug '14

A question I had about how the sel4 project is run internally: What is your process of developing ongoing changes and how does verification fit into it? Do you maintain the proofs with kernel modifications on an ongoing basis? On a semi-regular basis? Is the "experimental" branch verified? When time slices are no longer global, will those changes be verified? etc... Tim

2 2

ArchLinux/Manjaro development
by stercor 03 Aug '14

03 Aug '14

Has there been any seL4 development effort for the ArchLinux or Manjaro platforms? -- GPG/PGP public key: B07F9AAE

2 1

signing git commits
by HW42 01 Aug '14

01 Aug '14

Hi, I really like to see big formally verified software. But it seems your provide no way to verify the downloads from your repositories. I think you should use signed git tags and also ensure that repo verify those. HW42

2 1

run_tests needs mlton-compiler gcc-arm-none-eabi
by Harry Butterworth 01 Aug '14

01 Aug '14

On Ubuntu 14.04, after attempting to follow the instructions, I found I needed to add two extra packages. I needed mlton-complier for CParserTools and gcc-arm-none-eabi for CBaseRefine. gcc-arm-linux-gnueabi is a documented dependency for 14.04 and was already installed when the CBaseRefine test was failing. After installing those two packages and the documented latex extras all 31 regression tests passed.

2 1

AM335X (BeagleBone) support?
by Tim Newsham 31 Jul '14

31 Jul '14

What is the state of "AM335X (BeagleBone)" support in the main and experimental branches? Tim

2 1

Running seL4 on a Raspberry Pi?
by Quigley, Joseph 31 Jul '14

31 Jul '14

Hello! My name is Joe Quigley, I found out about the project recently and want to start experimenting with it on a Rasberry Pi I have floating around. Because it uses a very similar ARMv6 CPU as the KZM-ARM11-01, am I correct in assuming it will work with that kernel? -- --Joe Quigley

2 1

(simple?) build error?
by Tim Newsham 31 Jul '14

31 Jul '14

I'm getting an error when building from Ubuntu. I'm building from: repo init -u https://github.com/seL4/sel4test-manifest.git I've configured with: make ia32_simulation_release_xml_defconfig and done "make menuconfig" accepting the defaults. Finally I run make and get errors: [KERNEL] [CC] kernel_final.s src/sel4/sel4test/kernel/src/arch/ia32/kernel/vspace.c: In function ‘init_boot_pd’: src/sel4/sel4test/kernel/src/arch/ia32/kernel/vspace.c:58:23: error: array subscript is above array bounds [-Werror=array-bounds] cc1: all warnings being treated as errors make[1]: *** [kernel_final.s] Error 1 make: *** [kernel_elf] Error 2 Attached is the output of "make V=2" (for verbosity). Tim

3 2

virtualization and linux?
by Tim Newsham 31 Jul '14

31 Jul '14

Is there any documentation on using the VMM support for x86 seL4? Also, when can we hear more about "Served by Apache on Linux on seL4."? Tim

1 0

Does the kernel build support the gold linker?
by Stephen Thomas 30 Jul '14

30 Jul '14

I tried building the kernel for ARCH=ia32 and PLAT=pc99 and I fail with a linker errror. Is there a linker script that supports the gold linker (for linux). Cheers Thomo

2 1

Initial architecture/processor support in seL4
by Peter Howard 26 Jun '14

26 Jun '14

HI, I'm wondering what CPUs the initial source release for seL4 will support. In http://www.nicta.com.au/pub?doc=6930&filename=Elphinstone_Heiser_13.pdf It references Core i7 32-bit, ARM11, and Cortex A9 - covering x86, ARMv6, and ARMv7. What else will be in there? Thanks, -- Peter Howard <pjh(a)northern-ridge.com.au>

2 2

Re: [seL4] Question about seL4 on July 29th
by Gernot Heiser 21 Jun '14

21 Jun '14

On 21 Jun 2014, at 11:59 , Jorge Ventura <jorge.araujo.ventura(a)gmail.com> wrote: > Anybody knows what kind of Open Source License is expected > to be deployed with seL4 on July 29th ? The seL4 developers mailing list (copied) is probably the better place for this question. Short answer: can’t tell you yet. Longer answer: we have a clear idea of the licenses that will be used for the various parts, but have not yet concluded all formal agreements between the various parties having a say in this, and until that is the case, we cannot reveal more. What I can say is that I expect the community will be happy with the outcome. Gernot

1 0

We're live!
by Gernot Heiser 05 Jun '14

05 Jun '14

This list is probably not of much use until 29 July, but then it will be the place for technical discussions about building systems on seL4. Enjoy, 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.

1 0