- Devel - lists.sel4.systems

Configuring CAmkES projects
by Grant Jurgensen 02 Feb '20

02 Feb '20

Hi everyone, I have a couple questions regarding the current CMake build structure for CAmkES projects. It seems that the current structure intends you to put your project in the camkes/apps folder, and then build your project with `../init-build -DCAMKES_APP=<project_name>`, or the equivalent using the griddle script. What I don't understand is how you are supposed to configure your project. It seems easy_settings.cmake is always loaded. Is it advisable to edit this file? In the past, I could also tweak configuration variables manually by invoking the ccmake gui on the top-level directory. Now that there is no CMakeLists.txt in the top-level directory, this does not work. If I try it in my project's directory, it tells me the cache is empty. Is it still possible to edit CMake cache variables with ccmake? Thanks! Grant Jurgensen

2 2

Recycle resources used by a thread after it terminates
by Alexandre Mutel 02 Feb '20

02 Feb '20

Hi, I have a design question regarding how to recycle capabilities/memory frames that were used by a thread once it terminates. Let's assume that there is a MemoryManager server responsible to serve virtual memory to user processes (e.g similar to implementing VirtualAlloc). The MemoryManager has to maintain the list of untyped object, retype them, maintain likely a list of resources allocated for a user thread, likely copy/mint the page frames to forward them to the user process...etc. But when a thread terminates, as I can't see any related events in seL4, I would assume that the user process would have to explicitly notify the MemoryManager on exit. Then the MemoryManager would know which user thread has exited and would update/recover the used capabilities and destroy them, in order to recover untyped objects. Would it be a proper design that plays well with seL4? Do you think that it could be done more efficiently with seL4? Thank you!

2 2

AMD CPUs and SMP scalability
by Demi M. Obenour 31 Jan '20

31 Jan '20

My understanding is that seL4 plans on scaling to large multi-core server processors by using Intel TSX. However, AMD has not implemented TSX, and TSX has been involved in many recent side-channel attacks. AMD systems are attractive both from a performance and a security perspective, but my understanding is that the performance of seL4 on them will be terrible. Are there plans to implement and verify a version of seL4 that scales to multicore AMD server-class CPUs? The problem with a multikernel is that not having thread migration is likely to cause starvation on many practical workloads Sincerely, Demi

2 2

Status of side-channel attack mitigation
by Demi M. Obenour 31 Jan '20

31 Jan '20

What is the current status of seL4 with respect to Meltdown, Spectre, L1TF, MDS and other CPU vulnerabilities? Thank you, Demi

2 2

(no subject)
by abdi mahmud haji 30 Jan '20

30 Jan '20

hi i have been wondering how can i install or put another OS( like , window ,linux )on the top of seL4 microkernel can some one help

2 1

Are there any plans to re-add seL4_Untyped_RetypeAtOffset?
by Andrew Warkentin 29 Jan '20

29 Jan '20

Speaking of things that would be useful for large dynamic systems, are there any plans to add seL4_Untyped_RetypeAtOffset from the old experimental branch to the current mainline kernel? I am writing a buddy untyped allocator for UX/RT, and being able to retype at arbitrary offsets would reduce overhead quite a bit because I could just retype from the highest-order untyped objects most of the time rather than having to create two child untyped objects per split. If not, I will probably end up re-adding it myself later on (sometime after UX/RT is running actual user programs).

5 20

Camkes and Memory-Mapped Peripherals
by Michael Neises 29 Jan '20

29 Jan '20

Hello, I'm trying to access a memory-mapped peripheral on the exynos5422 (ODROID XU4). I have the physical address of the peripheral's registers from the exynos5422 data sheet. As per the Camkes manual, I've used the seL4HardwareMMIO connection type to facilitate this. However, while I can use the excess bytes of the "dataport Buf" as expected, there is a data fault when I try to read from the peripheral's memory-mapped (and readable) registers: """ FAULT HANDLER: data fault from test_component.test_component_0_control (ID 0x1) on address 0, pc = 0x3250c, fsr = 0x211 """ Besides defining the hardware component and this connection in Camkes, is there anything else I must do? I will appreciate any guidance on this matter. Best, Michael Neises

2 1

Re: [seL4] Request for enhancement: Notification queues
by Millar, Curtis (Data61, Kensington NSW) 25 Jan '20

25 Jan '20

> I strongly suspect the more fundamental and general extension would be > to remove the scalability limitation of Notifications, probably by > generalising them to a hierarchy, i.e. you signal a sub-notification > which then signals the higher-level notification. I?m not claiming > having thought this through, though. Having thought about this a little, I think that it is useful to observe that the case where such cases where large numbers of notifications need to be received the receiver uses a roughly similar interface to endpoints (seL4_Send to wait for an event and seL4_NBSend to poll for events). If we allow send queues of endpoints to include notification objects in addition to threads we could multiplex notifications via an endpoint by binding the notifications to the endpoint. This could also allow for the removal of notification binding for threads; if they want to receive both notifications and synchronous IPC they can bind the notification to the endpoint. This design should also work with MCS whereby donation of scheduling contexts from notification objects would become roughly the same as donation from a thread with a scheduling context. I think the cleanest implementation would be to allow a notification to contain its own endpoint capability, similar to the manner in which TCBs conatain capabilities. Any time an idle notification is invoked with a send it then queues on the endpoint to which is capability refers if one exists. Send invocations of 'active' (potentially queued) notifications would perform the same XOR operation as currently occurs. When receiving on an endpoint where the first blocked object is a notification the badge received is the badge of the endpoint capability owned by the notification and the notification word is simply placed in the first message register. Whilst I think that this (or something similar) is the most simple case for implementing multiplexing it would have some impact on the semantics and implementation of some objects. Even at this small a scale the verification burden will still be considerable as this change would impact all verified builds. I think further discussion and evaluation of a solution is needed before we can determine that it is sufficiently beneficial to have this feature in the kernel and to commit to maintaining the feature and including it in the verified configurations. Cheers, Curtis Millar

2 1

Request for enhancement: Notification queues
by Demi M. Obenour 24 Jan '20

24 Jan '20

While studying seL4, I noticed that there is no mechanism to wait for one of many notifications. This proposal solves this with a new type of capability, which I call a notification queue. I don’t have the knowledge to determine how they should be implemented, so instead I will describe the general idea. A notification queue is a capability to which notification objects can be attached. When an attached endpoint is notified, a user-provided pointer is pushed onto the queue. Notification queues are edge-triggered, so subsequent notifications do not cause further entries to be added to the queue unless the notification has been read. The queue is implemented as a buffer which is read-only to userspace, but read-write to seL4. When creating a notification queue, userspace must provide sufficient untyped memory to ensure that the queue will not fill up. This ensures that sending a notification cannot fail due to resource exhaustion. Queues can be resized by the application if needed. Attempts to add too many endpoints to a queue results in an error being returned. A notification object can only be attached to one notification queue at a time. It can be detached from a queue and later attached to another. Notification queues can be used whenever a notification object is expected, except that they cannot be badged. Badging a notification queue would make no sense. When polled, a notification queue returns the number of events that have been added to it since it was last polled. Adding one notification queue to another may or may not be allowed. Allowing it would increase flexibility, but also increase implementation complexity. It is also possible to attach a TCB to a queue; the queue is notified when the TCB exits. Only seL4 can send to a notification queue. No userspace process can ever possess a send capability to such a queue. While a notification queue can be accessed from any number of tasks, performance on multi-core systems may be improved if each queue is used from the same core that its attached notifications are used on. Constructive feedback on this proposal is welcome. Sincerely, Demi

3 8

seL4 on unverified ARM platforms
by Demi M. Obenour 23 Jan '20

23 Jan '20

My understanding is that seL4 is currently only verified for one particular ARM platform. Is it considered production-ready on other ARM boards? Sincerely, Demi

2 3