I will definitively have a look a the RT document and the related CAmkES extensions. For now, how the kernel schedules tasks and handle time isolation is definitively confusing, especially for a kernel that is focused on security and reliability. If there is no timing service and no way to get a reliable concept of time, how can I implement a control law or a periodic tasks (that is potentially critical)?
I understand that drivers should be implemented in their own address spaces but we also want to make sure that the driver is executed. And for now, I do not see how I can do that with seL4 and from what I have read, it seems that if I am using domains, the driver might miss some interruptions (and so, not have an accurate/consistent value of time). On Mon, May 16, 2016 at 5:57 PM, Gernot Heiser <[email protected]> wrote: > Hi Julien, > > We’ll provide some answers to your RT questions shortly. > > For now just this re the domain scheduler: this is definitely aimed at > high-paranoia scenarios, and actually requires polled I/O, rather than > interrupts. > > We’re working on a better solution to confidentiality isolation. However, > the problem you identify with interrupt latencies and acknowledgment is > inherent in any partitioning approach, there’s no way around. > > Gernot > > On 17 May 2016, at 1:28 , Julien Delange <[email protected]> wrote: > > I assume this can be an issue when you are managing interrupts. As far as > I know, we cannot have interrupts handled by two partitions: in that case, > which one acknowledges the interrupts? How to keep track of the number of > ticks? And how to finally get the time? > > Even if partitions are isolated, we still need to manage the hardware and > answer to handle (at least some) interrupts. For example, managing the > timer interrupt. Some devices can be managed without managing the timer > (for example, a network driver can be implemented using polling) but it > might be critical for other to acknowledge the interrupt as soon as > possible. > > To enable time management, you need to have a separate partition to > receive the timer interrupts and keep track of the time. This partition is > then connected to other partitions that need timing services. I think this > is what has been done for SMACCM. If we keep partitions access the same > hardware resources, this is potentially a security design flaw (access of a > shared resource from partitions at different security level/domains). > > Now, about the real-time extensions, I do have some questions: > 1. Is there any documentation about it? > 2. What are the new features? Are they documented? Is there a support with > CAmkES? I remembered having seen something like _period and _budget > attributes in CAmkES but no documentation. What is the unit (processor > tickers, nanoseconds?)? Having documentation and/or examples would be > appreciated. > 3. Where to grab it, use it and experiment it? > > Thanks! > > On Sat, May 7, 2016 at 10:22 PM, Felix Kam <[email protected]> wrote: > >> Hi Will, >> >> My understanding (I may be wrong here, please do correct me :) ) is that >> the time domains are temporally isolated in the sense that a program >> running in domain A is not supposed to know anything about timing that >> happens in domain B, so that it can't use that to infer about information. >> >> So if you have 2 domains, A and B each with a time slice of 10ms, with >> some threads in both, B can't know when did A run out of runnable threads >> to run if it does(vice versa). If A ran out of things to do 5ms into its >> timeslice, I think the scheduler will just run the idle thread, until A's >> timeslice run out. >> >> Given that context, why do you want to run such a timer driver in user >> land ? If they are mutually distrusting, I think such a driver can become a >> timing side channel. Why not give each of them their own timer driver ? >> >> Cheers, >> Felix >> >> On Sun, May 8, 2016 at 11:41 AM, Will Klieber <[email protected]> wrote: >> >>> 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 >>> >>> _______________________________________________ >>> Devel mailing list >>> [email protected] >>> https://sel4.systems/lists/listinfo/devel >>> >> >> >> _______________________________________________ >> Devel mailing list >> [email protected] >> https://sel4.systems/lists/listinfo/devel >> >> > _______________________________________________ > Devel mailing list > [email protected] > https://sel4.systems/lists/listinfo/devel > > > > ------------------------------ > > 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. >
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
