- Devel - lists.sel4.systems

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