Hi Oak,

Answers inline.

Cheers, Anna.

On 9/08/2016 12:43 PM, Norrathep Rattanavipanon wrote:

I have a few questions about how interrupts work in seL4.

1. Is it possible to enable/disable interrupt (i.e. __enable_irq or

__disable_irq for ARM) in the userspace code of sel4? We want to make sure that the execution of the code in the initial process does not get interrupt.

No. However if you assign your interrupt handler a lower priority than the task that you do not want interrupted, the handler won't be scheduled. This doesn't stop the irq handler from running in the kernel, but the notification won't be delivered until your lower priority thread is scheduled.

2. My understanding is that the scheduling mechanism in seL4 is

priority-based first and round-robin if two processes/threads have the same priority. Assume process A is the initial process spawned by kernel.

2.0) is my understanding about sel4 scheduling correct?

Yes.

2.1) Is the initial process guaranteed to have the maximum priority in seL4?

Yes.

2.2) If another process, say process B, is created by process A with lower priority. Is it possible for process B to interrupt process A and execute code in B instead while A is executing?

No.

Thanks,

-- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

---

Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Thanks for the responds.

I have played around a bit with the priority values and just want to confirm the following: It seems to be the case that a thread can decrease its own priority value (assuming it has a capability to do so) but cannot increase its priority.

Is this always the case, and part of the specification?

Oak

On Mon, Aug 8, 2016 at 7:43 PM, Norrathep Rattanavipanon nrattana@uci.edu wrote:

I have a few questions about how interrupts work in seL4.

1. Is it possible to enable/disable interrupt (i.e. __enable_irq or

__disable_irq for ARM) in the userspace code of sel4? We want to make sure that the execution of the code in the initial process does not get interrupt.

2. My understanding is that the scheduling mechanism in seL4 is

priority-based first and round-robin if two processes/threads have the same priority. Assume process A is the initial process spawned by kernel.

2.0) is my understanding about sel4 scheduling correct? 2.1) Is the initial process guaranteed to have the maximum priority in seL4? 2.2) If another process, say process B, is created by process A with lower priority. Is it possible for process B to interrupt process A and execute code in B instead while A is executing?

Thanks,

-- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

Actually i meant the original sel4 branch. Does it work the same?

On Aug 13, 2016 4:54 PM, Gernot.Heiser@data61.csiro.au wrote:

...

On 14 Aug 2016, at 9:09 , Norrathep Rattanavipanon nrattana@uci.edu

wrote:

...

Thanks for the responds.

I have played around a bit with the priority values and just want to

confirm the following:

...

It seems to be the case that a thread can decrease its own priority

value (assuming it has a capability to do so)

...

but cannot increase its priority.

I assume you are you using the RT branch?

A thread has an MCP (maximum controlled prio) parameter. It cannot raise any thread’s prio (own or other) higher than its MCP, but it can always decrease. Your thread may have an MCP of zero, which is what most threads should have.

Gernot