Devel

devel@sel4.systems

9 participants
1390 discussions

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

Memory Management
by Mark Reus 22 Nov '16

22 Nov '16

Hi I have a general case about memory allocation in particular with that of the Vspace. I have been reading some documents and trying to compare how it is in Linux Kernel. Any program Virtual memory in a Linux kernel is as shown in picture below where all processes have 1GB of virtual memory which is mapped to kernel space for faster context switches and system calls. _____________________ | Kernel Space (1GB) | |_____________________| | | | User Mode Space | | (3 GB) | | | |_____________________| I have come across this this link http://os.inf.tu-dresden.de/pipermail/l4-hackers/2014/006262.html detailing a little about the sel4 memory management. But I haven't been able to completely comprehend it . I wanted to know if the seL4 kernel also has a similar mapping of kernel space. Regards Mark

2 1

Syscall errors with musl
by Rinat Dobrokhotov 21 Nov '16

21 Nov '16

Hi all, I have written simple programme which gets system time. I get syscall errors when programm is calling gettimeofday function: *main.c:* #include <time.h> #include <sys/time.h> #include <stdlib.h> #include <stdio.h> int main(int argc, char *argv[]) { int iterations = 1000000; struct timeval start, end; gettimeofday(&start, NULL); for (int i = 0; i < iterations; i++) { } gettimeofday(&end, NULL); printf("%ld\n", ((end.tv_sec * 1000000 + end.tv_usec) - (start.tv_sec * 1000000 + start.tv_usec))); return 0; *Errors:* libsel4muslcsys: Error attempting syscall 263 libsel4muslcsys: Error attempting syscall 78 Could you tell me where I mistook? -- Best regards, Rinat Dobrokhotov

2 1

seL4RPC vs seL4RPCCall?
by Andrew Gacek 18 Nov '16

18 Nov '16

What's the difference between seL4RPC and seL4RPCCall in CAmkES? Is there documentation on the various connectors somewhere? Thanks, Andrew

2 1

Send input to seL4 in QEMU
by Andrew Gacek 18 Nov '16

18 Nov '16

Hi, We are developing an seL4 application that will process UDP packets coming in over a network connection. Eventually, we'll be running this on real hardware with real drivers, but for now we are using QEMU. We have a python script that can generate packet payloads. Is there a way to send this information into QEMU so that we can develop our seL4 application without having the drivers and hardware in place? If it matters, we are using CAmkES as well. Thanks, Andrew

2 3

seL4 Kernel Profiler
by Chris Guikema 18 Nov '16

18 Nov '16

Hello, I am working on a Code Profiler for use in seL4 Systems. I see that the Kernel already has some form of profiling/benchmarking functionality built in. However, I do not see anything in the documentation that covers how this is used. Is there a guide that I can follow to get the kernel profile functional? Thanks Chris Guikema

2 1

Will seL4_Word ever be anything but uintptr_t?
by Corey Richardson 17 Nov '16

17 Nov '16

I guess this is a somewhat philosophical question. It's come up a bit in the Rust libs I've been writing. Casting from pointer-sized things to *specifically* u32/u64 is bit tiresome for the places where I can't abstract over that. -- cmr http://octayn.net/ +16038524272

2 1

seL4 on i.MX53
by Yevgeny Lavrov 15 Nov '16

15 Nov '16

Hello. I've multiple ARM devices at my disposal that I want to use to experiment with seL4, one of them is USB Armory (Architecture: ARMv7 Cortex-A8 Processor: i.MX53 800MHz). Before I get into it, I would like to know if seL4 supports this ARM device. Thanks

2 1

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel