Devel

devel@sel4.systems

20 participants
1384 discussions

Adding a Rust kernel interface generator
by Corey Richardson 11 Sep '15

11 Sep '15

Hello, As part of the robigalia [0] project I must create a Rust interface to the kernel. I'm using the XML from kernel/libsel4 and have been creating a "new" generator by copying the existing Python scripts. Should I send a patch upstream once this is suitably complete, or should I maintain this completely externally? [0] - https://github.com/robigalia -- /cmr

2 2

how to detect the number of CPUs in the system
by 杰尔米 01 Sep '15

01 Sep '15

Hi all, i want to get the number of CPUs in the system and how many cores in one CPU. how to do that? Thanks! Jeremy Li

3 2

The pt/pd/as abstraction vs software TLBs
by Raymond Jennings 01 Sep '15

01 Sep '15

Hey, quick question. This is just hypothetical, but would making management of pagetables/pagedirectories a low level literal operation hurt seL4's portability to other architectures that might not even use page tables? I could be mistaken but I think there's some archs out there that only have software TLBs (openrisc IIRC among them) Please forgive me if I'm mistaken but my recent question about memory abstraction reminded me about this.

3 2

sharing memory between processes
by Raymond Jennings 01 Sep '15

01 Sep '15

Is there an easy way for one task to share address space with another task directly or does it have to go through the kernel/os and be emulated? I noticed that support for mapping memory is mostly low level assignment of physical frames to virtual frames via page tables, unlike Mach which uses memory objects.

6 7

virtual memory abstraction
by Raymond Jennings 31 Aug '15

31 Aug '15

I noticed that unlike mach, L4 does not directly manage virtual memory, but instead farms out address space, page directory, and page table capabilities to userspace and lets userspace decide what pages to map and where. Does this imply that virtual memory abstraction is userspace responsibility?

2 1

Port I/O - Permissions Question
by Josef M. 25 Aug '15

25 Aug '15

Hi, I'm experimenting with some x86 code that involves reading from I/O ports. I noticed--much to my surprise--that I don't have to use seL4_IA32_IOPort_In8() to read from a port; my program works just as fine using the "in" assembly statement directly, without any caps. The TSS segment limit is initialized with 0x67 https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/vspace.c#L158 and the "I/O Map base address" is initialized with 0 (zero) https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/vspace.c#L43 I believe the result is that ring 3 programs can access I/O port addresses below 0x388 (0x67 * 8) without triggering a protection violation. So my question is: Shouldn't capabilities be required for all ports? Or what what is the reason or motivation behind this? Thanks, Josef

2 1

Running Linux atop sel4
by Sebastian Lau 24 Aug '15

24 Aug '15

On the sel4.systems website, it says that the site is served by the Apache web server on Linux atop sel4. How does that work and could you operate the Linux middleware just on top of sel4, maybe something like mer?

1 0

Roadmap?
by Raymond Jennings 22 Aug '15

22 Aug '15

I remember awhile ago that someone was going to post the roadmap in response to my accessed/dirty bit suggestion...but I haven't seen it yet.

2 1

Some questions about seL4 operating system
by Qing Wei 22 Aug '15

22 Aug '15

Hi, I am a beginner to seL4 as well as microkernel, and very interested in it. I think it is great in terms of its minimality and formally verified security. However, I have some questions about it, (1) How is its performance compared to other monolithic kernel, say, Linux. Could it make use of multicore, multiprocessor to enjoy the performance scalability? (2) How is its ecosystem, fox example, how to support new hardware, does it need write the driver from scratch or could it make use of Linux driver? And how to write application on it, or, could it run Linux application without modification? (3) How is its virtualization support, could it run Linux vm, and does it need any modification to the guest os? Cheers, Qing Wei

3 4

Some comments.
by Mehdi Amiri 17 Aug '15

17 Aug '15

Hi, Thank you for all your efforts and time. I believe the user community is the main success key for all open source projects. Many users and researchers, do not have enough time to read, download and evaluate all the source code in order to investigate a system to see if it is suitable for their research or usage. Usually they will go for clean systems which are easy to use, simple to understand, well documented and have a strong community beside the commercial support to ask and get help in case they had a problem. Here are some comments which may help to increase the number of users and developers for seL4: A) I suggest to add some howtos to the website. It's better to be a wiki like system so other individuals, researchers and students can help in writing some titles. Some interesting topics (at least for me as a beginner in micro-kernel) could be: 1- Running Linux/Android on top of seL4. 2- Writing a simple user application with a use case (not just the SOC). 3. Examples on real-time application. 4- Writing a service (could be a device driver, file-system, etc) for seL4. 5- Documents on using possible run-times like Genode. 6- Documents or case studies on porting an opensource software from Linux or POSIX based system to directly run om seL4. B) Providing ready to use download binary images for supported platforms can also accelerate growth of community. C) A research areas page which can suggest researchers some ideas to chose a title and do their research to expand seL4 could also be useful. Ideas like rump-kernels, lib-OS, visualization (x86/ARM), etc seems to be possible research titles on seL4. I have seen the https://sel4.systems/GettingStarted/ page and I think other than CAmkES, ports and Qubes there could be many more titles. D) I know the major development platform of seL4 has been the Arm architecture, but optimizing the code to utilize the x86 architecture including virtualization can also bring a lot of attention to this project to use seL4 as a replacement for Linux-KVM and Xen in the cloud, IoT or real time systems when stability and security is a matter. Also please note, the archive of both development ( https://sel4.systems/pipermail/devel/) and announcements ( https://sel4.systems/pipermail/announce/) mailing lists are not accessible trough the website. I'm an OS researcher and a senior system engineer (mostly Linux) with a limited time, but I can help in some parts if you think it may be useful. Thank you again! Best Regards, Mehdi

2 1

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel