- Devel - lists.sel4.systems

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