Hi Oak,
Assuming your questions are about the master branch of the kernel, as on the RT
branch the kernel is tickless.
1. There are two config paramters
+ TIMER_TICK_MS is how many milliseconds per tick
+ TIME_SLICE is how many ticks per timeslice.
2. Assuming a thread is waiting on a notification object for an irq to arrive,
and another thread is running at the same priority when the irq arrives, the
thread waiting on the notification object will not be woken until the currently
running thread has exhausted it's timeslice.
Cheers,
Anna.
________________________________
From: Devel <[email protected]> on behalf of Norrathep Rattanavipanon
<[email protected]>
Sent: Tuesday, 17 October 2017 8:35 AM
To: [email protected]
Subject: [seL4] Questions on seL4's scheduling
Hello,
I have a few questions about seL4's scheduling model in the main (formally
verified) branch.
1) I see the time slice parameter in make menuconfig. Is that where I can
change the scheduler's time slice correct? And the unit is in timer tick period
I suppose?
2) I kind of remember the discussion we had that if an interrupt handler has
lower priority than the currently running task, then the interrupt wouldnt
happen.
So what if both of them have the same priority, would the kernel schedule the
currently running task until it uses up all of its timeslice, then issues the
interrupt notification or would the interrupting process get executed right
away?
Best Regards,
Oak
--
Norrathep (Oak) Rattanavipanon
M.S. in Computer Science
University of California - Irvine
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
