Kent McLeod

> Maybe the same applies to tisr, in which case the asserts are wrong? Or the SET_REGISTER macro is used wrong in initTimer: It sets a mask, but it's used...

Hi @sannum, I'm not sure if this is something you are still interested in pursuing. If so, it would be better to bring this up as a new discussion thread...

What is a reasonable range of compiler versions to support? My preference is that we still support gcc-7 and treat the __naked__ attribute message as a bug we need to...

> Given that gcc-11 is the current version, gcc-7 seems fairly far behind. We compile the kernel with `-std=c99` so it's not like we need to update compilers to support...

> In that scenario I'd expect A to precede B in the ready queue, behind any threads that were already in the queue of prio P before the first signal....

(I'm only considering non-mcs and non-smp here) In the current implementation, whenever a thread is made runnable it is almost always inserted into the front of the queue for it's...

How does yield map onto the existing mechanisms? E.G. A high priority thread performs send on an endpoint (or notification) and unblocks a low priority thread. Both are now runnable....

> I don't think your example would work as equal priority notifications don't put the woken up task at the head of the queue (@kent-mcleod 's point 3, the `was_runnable`...

Inserting a call to seL4_Yield() before the call to seL4_Wait() would explicitly send the thread to the back of the ready queue before receiving the next notification.

> The problem is that putting unblocked tasks at the head of the queue often makes sense. Of the list of cases you posted the only problematic one is unblocking...