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 <devel-bounces@sel4.systems> on behalf of Norrathep Rattanavipanon <nrattana@uci.edu>
Sent: Tuesday, 17 October 2017 8:35 AM
To: devel@sel4.systems
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