Devel

devel@sel4.systems

9 participants
1391 discussions

Latest experimental RT kernel released
by Anna Lyons 03 Jun '16

03 Jun '16

= Latest experimental RT kernel released = The RT kernel provides + periodic scheduling, + temporal isolation, + support for criticality and criticality mode changes, + temporal exceptions, .. and more. == Caveats == The RT kernel does not compile or run on all platforms, we currently support: + x86: ia32 platforms with TSC_DEADLINE mode + ARM: Sabre lite, Beagle board, and Odroid-xu (all armv7-a). The RT kernel is not verified, and as such we provide no guarantees, and there's likely still some bugs hiding in there. The other platforms require driver work at user level and in the kernel. If you are keen to get a certain platform working, contributions are welcome! == Available == + *Kernel branch* on github: https://github.com/seL4/seL4/tree/rt + *Release notes* (detailed API changes from current seL4 latest release): https://wiki.sel4.systems/seL4%201.0.0-rt-dev + *RT kernel manual* http://sel4.systems/Info/Docs/seL4-manual-1.0.0-rt-dev.pdf + *whitepaper* http://arxiv.org/abs/1606.00111 == Try it == Check out the rt branch of sel4test-manifest with repo: $ repo init -u https://github.com/seL4/sel4test-manifest.git -b rt Feedback on the API would be *extremely* valued. Enjoy! -- Anna Lyons Kernel engineer / PhD Student DATA61 | CSIRO E anna.lyons(a)nicta.com.au<mailto:anna.lyons@nicta.com.au> www.data61.csiro.au<http://www.data61.csiro.au> CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________ 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.

3 3

Memory allocation & threads
by Доброхотов Ринат 03 Jun '16

03 Jun '16

Hello, I don't understand how static and virtual pool's size related to thread's available working space. I got the example app from the sel4-tutorials project with process creation (app-4). A static pool and a virtual pool are created in this app. I have done experiments with size of this pools and size of arrays in the second thread. For example I set size of virtual pool to zero, as I understand this pool need to create kernel objects. Also I define the test array size of (1 << 23)~8,3Mb. If test array is static, static pool size must be equal to ((1 << seL4_PageBits) * 100) ~0,4Mb. If test array is no static, static pool size not limited. Why is it so? -- Best Regards, Rinat Dobrokhotov

4 4

Will the codes in branch rt be merged into master
by XilongPei 02 Jun '16

02 Jun '16

Hi, I got information from https://wiki.sel4.systems/seL4%201.0.0-rt-dev , the development branch for the seL4 realtime extensions. My question is that will the codes in branch rt be merged into master, and add some build option. If a working tree always not in the master branch, it will be very difficult to be managed. Xilong Pei Tongji University 2016/6/1

2 1

RT branch questions
by Julien Delange 27 May '16

27 May '16

I am currently trying the RT branch and have some questions: 1. What emulator to use in order to try the examples? I am trying to use x86 with qemu but it seems that it does not work. I got the following trace at execution Starting node #0 APIC: unsupported platform, TSC-deadline mode is not supported seL4 called fail at /home/sel4/camkes-sc-tests/kernel/src/arch/x86/kernel/boot_sys.c:451 in function boot_sys, saying "boot_sys failed for some reason :( So, is there an emulator (for any supported platform) to try it? 2. In the RT-camkes extensions, I have the following new attributes: _period _budget _priority What is the semantics of these attributes? Any information about them? How they are supposed to be isolated from each other then? How to define the scheduling plan for the system then? Also, how these attributes apply to all thread: a thread is created for each interface of the component, so, how can we then define the priority/budget of each thread? Do these attributes apply to all the components of the thread? Thanks for any help/clarification. Julien. assembly { composition { component Client client1; component Client client2; } configuration { client1._priority = 100; client1._period = 10000; client1._budget = 7500; client2._priority = 50; client2._period = 10000; client2._budget = 7500; } }

3 6

Advice on camkes and regular seL4 for driver components
by Norrathep Rattanavipanon 27 May '16

27 May '16

Hello, I currently had codes, implemented as regular seL4, since camkes does not support some features (i.e. transferring capabilities or accessing address space outside the process), Everything is fine up to this point but now I want to create several drivers. And I found that the best and easiest way to do that is to use camkes. So is it possible to use existing regular codes in conjunction with camkes? Or would the best way be to implement drivers as regular seL4 codes? Thanks, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

building VMM on Jetson TK1 board
by PX 26 May '16

26 May '16

Hi, all we want to build the seL4-based VMM from https://github.com/smaccm/sel4arm-vmm.git on Jetson TK1 board. However, the seL4 kernel in that project does not support TK1 board. We want to use the new version seL4 version (arm_hyp) at https://github.com/seL4/seL4.git. My questions are: 1) It is feasible to do that? 2) If so, what are the correct steps to do that? 3) we try to compile these source code, but failed. We do the following modifications: A) we add TK1 source codes (i.e. TK1 folders from https://github.com/seL4/seL4.git) to the corresponding libraries in the VMM source code from https://github.com/smaccm/sel4arm-vmm.git; and B) we add relevant config definitions to the VMM code. Currently, we can successfully compile the seL4 kernel code, but have trouble to compile the VMM libraries. Do we miss something here? thanks Peng

2 1

Availability of RT branch?
by Julien Delange 25 May '16

25 May '16

Hi all, Follow-up on our recent discussions on the RT branch: is the RT branch now available? How could I get it and access the related documentation? If not available, is there any idea of when it will be available? Thanks. Julien.

1 0

Getting timer info from seL4 kernel
by Will Klieber 19 May '16

19 May '16

Hi, Is there any way of obtaining the number of elapsed timer ticks from the seL4 kernel (using ARM / BeagleBoard platform)? I know the kernel uses this information internally for the scheduler, but I couldn't find any way of accessing it from userland. Specifically, my usage scenario is as follows. Two mutually distrustful programs are running, and each wants to run an action periodically. We want to temporally isolate the two programs using seL4 time domains. In this case, interacting with the hardware timer in userland seems difficult, since we want to get the updated time whenever a new timer tick arrives, but the userland device driver for the timer can only operate in exactly one of the seL4 time domains. Please let me know if I am misunderstanding something or if there might be a better way to approach this situation. Thanks, Will

5 6

Hello. I'm Kihyun-seo in South Korea.
by 서기현 17 May '16

17 May '16

Hello, I am a student of the Hanseo University in Korea. I want to create a UAV(drone) that uses Odroid XU4 Odroid XU4's Detailed Specifications = http://www.hardkernel.com/main/products/prdt_info.php?g_code=G143452239825 I want to install seL4 on the board for the security of the drones. The board has “ubuntu-15.04-robotics-odroid-xu4-201” 32bit linux version. I have two questions. First, I understood that after installing the seL4 first, and installing the linux later after seeing the 1.jpg. However, in the “https://wiki.sel4.systems/Getting%20started”. “Setting up your machine - These instructions are for Ubuntu. They assume you already know the basics of using the command line, compilers and GNU Make.” So then, Should I install the Linux(ubuntu) first, and install the seL4 later? I wonder what is correct. and I need more detailed explanation. Second, An error occurred during install the seL4 like 2.jpg. (command = "make menuconfig" in "Build ia32" part.) I need a solution about the error. Please answer my two questions.

3 2

multi-core support
by PX 17 May '16

17 May '16

Hi, Just want to double check if the seL4 under link https://github.com/seL4/sel4test supports multi-core? If so, the multi-core support is configured by default? If the sel4 does not support multi core, where can we get the experimental version supporting multi core? thanks Peng

2 1

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel