Yes, ideally we would want to run our experiments on the RT branch. But given the close deadline, i'd rather do it on the master branch, which I'm more familiar, and we can still keep the formally verified property :).

We kind of want to simulate a quick and simple real-time scheduling in the master branch.
Basically, the main thread wants to run a long task but we dont want it to hoard all resources. So we split it into a bunch of smaller tasks. Then, for a security reason, we want to run each of the smaller tasks atomically. One way I can think of is to temporarily raise the priority of the main thread when running each task and yield once a task is finished.  The goal is to complete the long task ASAP while allowing other processes to run if needed. I then want to see how much time other processes can use between two tasks.

Oak



On Thu, Oct 19, 2017 at 6:06 PM, <Anna.Lyons@data61.csiro.au> wrote:


Recall I stated that the scheduler is basic ;)


The timer ticks on the master kernel are started on boot, then not reset on any thread operation. This means that the actual thread timeslice is just 'X interrupts must come in'. So it's likely to vary by up to the tick ms value, as the yield does not have any relation with a new tick starting.

If you measured the time for many threads (100 or so) to all consumer their timeslice, you should see the error drop off and the average value approach the timeslice.  

I'm curious as to what exactly you are trying to do? the RT kernel may be more suited.

Thanks
Anna. 

From: Norrathep Rattanavipanon <nrattana@uci.edu>
Sent: Friday, 20 October 2017 11:52 AM

To: Lyons, Anna (Data61, Kensington NSW)
Cc: devel@sel4.systems
Subject: Re: [seL4] Questions on seL4's scheduling
 
Thanks Anna. So I tried to measure timeslice in userspace and it seems like it does not match with the settings. Any idea what happens or what is wrong with my code:
I ran it on IMX6-SabreLite, master branch/kernel version 4.0.

main thread:
sel4bench_init();
seL4_Yield();
uint64_t start = sel4bench_get_cycle_count();
seL4_Yield();
uint64_t end = sel4bench_get_cycle_count();
sel4bench_destroy();
printf("Takes %llu\n", (end-start));

second thread:
while(1);

Both of them have the same priority.

When I set TIMER_TICK_MS=5 and TIME_SLICE=2, it outputs 8000000, which is around 8msecs.
Also, if i set TIMER_TICK_MS=2 and TIME_SLICE=1, I get around 1.6msecs.

Best,

On Thu, Oct 19, 2017 at 5:03 PM, <Anna.Lyons@data61.csiro.au> wrote:

Hi Oak,


The timeslice value on the master kernel is only reset on thread creation and once the thread is depleted, so when a thread drops its priority the timeslice will not change, so it'll run for 2ms.


The timeslice cannot be set to lower than 1 ms, however you could change the timer driver on your target platform to do so (look at the initTimer function).

​

Note that the scheduler on the master kernel is fairly basic, the RT branch is far more fully featured (tickless and you can set different timeslices per thread). 


Cheers

Anna. 


From: Norrathep Rattanavipanon <nrattana@uci.edu>
Sent: Friday, 20 October 2017 10:18 AM
To: Lyons, Anna (Data61, Kensington NSW)
Cc: devel@sel4.systems
Subject: Re: [seL4] Questions on seL4's scheduling
 
Also, is it possible to set timeslice to be less than 1 milliseconds?

On Thu, Oct 19, 2017 at 3:08 PM, Norrathep Rattanavipanon <nrattana@uci.edu> wrote:
Thank you, Anna and Gernot for the answer.

One more question, so assuming a timeslice is 5ms, a thread with the highest priority has run for 3ms, then drops its priority to be the same as the other thread.
Then, the same thread will start running with the fresh timeslice and it will run for another 5ms or will it just run for 2ms to complete the timeslice?

Oak

On Mon, Oct 16, 2017 at 3:09 PM, <Anna.Lyons@data61.csiro.au> wrote:

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



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



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



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



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