January 2020 - Devel - lists.sel4.systems

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

Re: [seL4] Request for enhancement: Notification queues
by Heiser, Gernot (Data61, Kensington NSW) 23 Jan '20

23 Jan '20

On 22 Jan 2020, at 14:44, Demi Obenour <demiobenour(a)gmail.com<mailto:demiobenour@gmail.com>> wrote: But everything needs a really convincing argument, that’s based on a functional limitation that prevents implementation of certain important classes of systems. If it’s only a performance argument, we’ll need to be convinced that it really is a performance bottleneck in realistic systems. Do you believe it is likely to be? I haven’t seen a convincing use case where it is. Gernot

1 0

Plans for verification of IOMMU support on x86? Binary verification?
by Demi M. Obenour 21 Jan '20

21 Jan '20

Are there plans to verify the IOMMU support on x86? x86 without DMA is not very useful, so IOMMU support is needed for the proofs to apply in practice. Sincerely, Demi

2 1

Initializing of the sel4 tutorials fails because of missing the CMakeLists.txt
by Florian Berenbrinker 16 Jan '20

16 Jan '20

2 3

Re: [seL4] Suggestion for Abdurahman
by Harry Butterworth 12 Jan '20

12 Jan '20

Take a look at Andy’s Binary Editor nyangau.org/be/be.html and implement an open source equivalent as an integrated debugger for seL4. You will need to be able to get keyboard input, write characters to the screen and get access to files containing the structure definitions. You can provide the structure definitions at boot time. You won’t need an OS or POSIX or even much of a standard library; the implementation just requires the language runtime, a parser, a few data structures, and a bit of printf-like code. You could write it all and make it completely self-contained which would allow you to keep the footprint really small. Steps to proceed are as follows: 1) Pick a language. I’d probably pick C++ for this but you might also consider D or Rust or maybe COGENT. 2) Work out how to write a small test program in your chosen language and get seL4 to run it. This will require an implementation of the runtime for the language. If this hasn’t been done already for the language you pick, you can implement bits of the runtime as you go along when they are needed. If you fail at this step, go back to step 1, pick a different language. 3) Work out how to get your test program to write characters to the screen (or serial console perhaps). 4) Work out how to get keyboard input. 5) Define the grammar for the structure definitions. If you happen to pick COGENT you might look at DARGENT. 6) Understand the Model View Controller design pattern. 7) Write a parser to parse the structure definitions to create a model. You’ll want the model to use lazy evaluation so the whole system defined by the structure definitions can be represented but there is only overhead for the bits that are being actively browsed. 8) Implement a view for the model which displays a selected part on the console. 9) Implement a controller for the view and model which is an event loop that handles keyboard input and manipulates the model and view accordingly. After getting your new debugger to work for browsing the entire system including the kernel data structures, find a way to integrate it which allows it to be configured to run with only the capability it needs for the debugging you want to do. After that you could make sure it can be used for debugging real time applications with a guarantee not to interfere with their real time operation. For bonus points, if you have picked COGENT, you might finish off with a formal proof that your debugger displays the correct characters on the console according to the structure definitions, contents of memory and history of keyboard input. This (in fact the whole task) would be complicated by the fact that the memory contents change all the time underneath you as you browse a live system so you’d have to work out how to incorporate that and still prove something useful. Enjoy On Fri, Jan 10, 2020 at 8:21 PM abdi mahmud haji < abdimahmudhaji227(a)gmail.com> wrote: > hey guys > I'm abdurahman and i have same question for you > i have been studying microkernel for a little well now specially seL4 and > i have done almost every tutorials in sel4 -tutorials and i have a crazy > idea ,that is i when try to build a 'shell or prompt' on the seL4 > mircokernel but i don't have any idea how to do or where to start . does > any one have a suggestion for me > > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel >

1 1

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

11 Jan '20

hey guys I'm abdurahman and i have same question for you i have been studying microkernel for a little well now specially seL4 and i have done almost every tutorials in sel4 -tutorials and i have a crazy idea ,that is i when try to build a 'shell or prompt' on the seL4 mircokernel but i don't have any idea how to do or where to start . does any one have a suggestion for me

4 3