mcs: more uniformly handle ready and release queue updates

[michaelmcinerney]

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.

[lsf37]

This also affects non-MCS configs, so we can only merge once we have ported the verification of it to the master branch as well.

Maybe some words on the background of this: factoring out the queue updates means we only have to verify them once, not twice. The change in type is there to achieve that genericity, and the head/tail type is the same mechanism used for tcb_queue_t, so it's just re-using those ideas. The operations are slightly different, so there was no point trying to make it even more generic (and would probably be fighting C too much).

[Indanz]

Looks functionally correct to me.

[Indanz]

The operations are slightly different, so there was no point trying to make it even more generic

It's mostly the insert operation that's different, but that can be solved by first finding the spot and then inserting the item. The rest seems pretty generic. Still at this point it's probably not quite worth it. Especially tcbEPDequeue seems to be eye wateringly optimistic about being correctly used, but it does shave off a few cycles here and there.

(and would probably be fighting C too much).

The problem is not C, in C you would let the next/prev pointers point to queue_t in each item and have a macro like container_of which uses offsetof() to get a pointer to the parent object from the next/prev pointers. However, I doubt that kind of pointer arithmetic and type casting is legal in verified seL4 C code.

It's worth doing if more complex structures than lists are used in the future, like heaps or trees.

[lsf37]

This is now ready to merge if all tests pass.