- Devel - lists.sel4.systems

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 04 Oct '14

04 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 04 Oct '14

04 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 22 Sep '14

22 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 18 Sep '14

18 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