seL4/include/model
Michael McInerney 686bba4d2a mcs: more uniformly handle ready and release queue
This introduces library functions for updating the linked lists which
use the tcbSchedNext and tcbSchedPrev pointers of a TCB, and uses these
to perform the updates to the ready queues and the release queue.

In order to accommodate this, ksReleaseQueue is now of type tcb_queue_t.

Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
2024-05-23 18:04:06 +10:00
..
preemption.h replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
smp.h replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
statedata.h mcs: more uniformly handle ready and release queue 2024-05-23 18:04:06 +10:00