November 2016 - Devel - lists.sel4.systems

Questions about Memory Management in seL4
by Daniel Wang 19 May '23

19 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

Bitcoin on seL4?
by Carl Dong 02 Dec '16

02 Dec '16

Hi all, I recently acquired a BD-SL-I.MX6 and will be tinkering with it to install seL4. A major use case for me is if I could run [bitcoind](https://en.bitcoin.it/wiki/Bitcoind) or at least [vanitygen](https://en.bitcoin.it/wiki/Vanitygen) on seL4. I'm very new to the system, but is there a relatively easy way of cross-compiling said software for seL4? Would love to spend some time learning. Cheers, Carl Dong accounts(a)carldong.me

4 3

Good C, bad C, verifiable C
by Jeff Waugh 30 Nov '16

30 Nov '16

Howdy, Is there a guide to the dos and don'ts of C according to the seL4 verification process? I kinda remember reading a quick summary somewhere, but can't find it on the wiki. Maybe I read it in one of the papers? I certainly remember reading the moral equivalent of "lol no strings". ;-) Thanks, Jeff

2 1

contiguous physical memory allocation for seL4
by PX 30 Nov '16

30 Nov '16

Hi, all I want to allocate a contiguous physical memory block (larger than a physical page) and map it to contiguous virtual addresses in the vspace, what's the best way to do it? Are there existing libraries allowing me to do that? thanks Peng

3 2

First International seL4 Workshop
by Gernot.Heiser＠data61.csiro.au 29 Nov '16

29 Nov '16

Hey seL4 community! We’d like to invite you to participate in the inaugural seL4 Workshop. Given the growth in the community we are starting an annual seL4 workshop where we can come together to share and learn what is being done with seL4. Unlike the previous developers days, the focus is much more on what is happening with seL4 and what interesting things are being done using seL4 rather than a learning or tutorial event. We’d like participants to join and: - present what they are doing with seL4 - demonstrate seL4-based projects - give tutorials on aspects of seL4 or tools, libraries, environments for working with seL4 - show results or progress of verification work involving seL4 - discuss interesting challenges (and possible solutions) they’ve encountered when using seL4 - discuss visions for the future of seL4 and high-assurance systems This workshop will take place on Thursday December 15, 2016 (and may be extended to December 16th if there is enough demand) in Malibu, CA, USA. Note that you are welcome to attend even if you do not present anything. Please register participation at: https://sel4.systems/Community/Devdays/ Participation is free, and we may be able to provide students with financial assistance for travel. This workshop is sponsored by the Center for Secure and Resilient Systems at HRL Laboratories, LLC, and by Data61. Gernot for the Data61 Trustworthy Systems Team

2 1

Re: [seL4] Timer for Performance Measurement
by Kofidoku.Atuah＠data61.csiro.au 29 Nov '16

29 Nov '16

?Hey Andrew, Sorry I took so long to get back to you: we have a benchmarking suite, seL4Bench (https://github.com/seL4/sel4bench/blob/master/apps/ipc/src/main.c) which should have userspace timers and precise timestamps available for most platforms. As I understand, you will just have to write a new microbenchmark of your own, and import your library, and then insert calls to the relevant timestamp counter functions (https://wiki.sel4.systems/Benchmarking%20guide)? Kofi Doku Atuah Kernel engineer DATA61 | CSIRO E kofidoku.atuah(a)data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of Andrew Mine <secondmine(a)gmail.com> Sent: 04 November 2016 16:30 To: devel(a)sel4.systems Subject: [seL4] Timer for Performance Measurement Hi Is there any inbuilt library to get the time like get_time in seL4? I want to measure IPC performance and overheads for my tasks. Regards Andrew

1 0

Re: [seL4] how to get timing information on seL4 user space
by Kofidoku.Atuah＠data61.csiro.au 29 Nov '16

29 Nov '16

??Hi Peng, Well, an atomic counter would suffice, and if you need to secure the counter, you could wrap it around with a server. You either need a hardware upcounter, or else a periodic event-timer that you can use to emulate a hardware upcounter; from there, you just use your upcounter for your jiffies. Libplatsupport has userspace timer drivers for most platforms we support: https://github.com/seL4/util_libs/tree/master/libplatsupport? Kofi Doku Atuah Kernel engineer DATA61 | CSIRO E kofidoku.atuah(a)data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of PX <seawolf.peng(a)gmail.com> Sent: 29 November 2016 08:27 To: devel(a)sel4.systems Subject: [seL4] how to get timing information on seL4 user space Hi, all I want to get number of ticks, similar to jiffies in Linux, in the ARM seL4 user space. How can I do it? Are there existing libraries I can use? If not, what's the best way to implement it? thanks Peng

1 0

how to get timing information on seL4 user space
by PX 29 Nov '16

29 Nov '16

Hi, all I want to get number of ticks, similar to jiffies in Linux, in the ARM seL4 user space. How can I do it? Are there existing libraries I can use? If not, what's the best way to implement it? thanks Peng

1 0

IPC measurements
by Neelesh Vemula 28 Nov '16

28 Nov '16

Hi I have been measuring the performance of my application and doing some comparisons with other kernels. I had a couple of queries. I am running seL4 on zynq device. I am using the given timer driver in libplatsupport to measure the clock cycles. Queries: 1) I have found the sample benchmark numbers for seL4 IPC from http://l4hq.org/docs/performance.php. Since I am running on Armv7 Cortex A9 , the time for one half way trip is 316 ns. Is this measured from system call to system call or from process to process? 2) I am trying to compare the performance on FreeRTOS and Linux, is there any such comparison on where seL4 stands? 3) Does the IPC time vary with the different api of ReplyRecv, Reply, seL4_NBRecv? I have this question because I am seeing that Reply is taking about twice the amount of clock cycles compared to Recv. In terms of my application, I am majorly looking at measuring one whole cycle which includes: 1) 1st Process sends message to 2nd Process 2) 2nd Process Reads from AXI device space 3) 2nd Process replies with Reply and waits for another command from 1st process 4) 1st process sends another message to 2nd Process 5) 2nd Process writes to the hardware 6) Time from step 1 to step 5 is measured. Results for this on seL4 : 3180 clock cycles FreeRTOS: 2414 clock cycles I am sure there is possibility of unnecessary overheads involved in my measurement, but I expected seL4 to be faster. Can someone help me in this regard. Regards Neelesh Vemula

2 1

Reading executable of the first process in kernel
by Norrathep Rattanavipanon 22 Nov '16

22 Nov '16

Hi, I want to modify the sel4 kernel to compute a checksum over the executable of the first process before executing it. The goal is to ensure that we execute the correct first process. What I'm doing right now is modify try_init_kernel() in kernel/src/archarm/kernel/boot.c by adding the following lines: for(i=ui_p_reg_start, i<ui_p_reg_end; i++) { checksum += *((char*) (i)); } My questions are the following: (1) Is this a right place to perform the checksum (inside try_init_kernel())? I assume in this function, seL4 kernel already takes over and thus this should do the job. (2) Based on my understanding, what I did was computing the checksum over the entire image (which may includes executable of other processes as well). Is there a way to just read the executable of the first process and ignore the rest in seL4 kernel? (3) I'm also curious: where/when does the seL4 kernel start the root process? I see the end of the same file (boot.c) that it just calls try_init_kernel() but does not load the root process. Best, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1