seL4
Improve formalisation of the reply objects and the reply stack
In MCS, a reply stack is formed to track the donation of a scheduling context. Currently, the reply stack is a doubly linked list of reply pointers, with the exception that the head of the list is the donated scheduling context. The implementation in the C and the formalisation in the abstract spec and the Haskell can be simplified by instead having the call stack be a doubly linked list of reply pointers, with a pointer, perhaps called replySC, from the head of the reply list to the donated scheduling context.
If we were to carry this out, it would involve a slight change to the definition of scReplies_of and sym_heap_scReplies, removing the need for the auxiliary functions getReplyNextPtr and getHeadScPtr.
We could also phrase bindScReply as a standard enqueue to the doubly linked list (similar to tcbQueuePrepend) together with an update linking the scheduling context with the new head of the list. reply_pop could use the relevant case from tcbQueueRemove, and then removing a reply from the middle of the reply stack, breaking the chain, could be a modified version of the last case in tcbQueueRemove. This would allow us to follow more closely the refinement approach used for the ready and release queues in Refine.
I think you are referring to replyNext either pointing to a reply object or a SC, which is very weird indeed.
We can get rid of the isHead bit too then, simplifying call_stack_t to just a pointer of a fixed type. Current code seems very convoluted.
We currently have an unused padding field, so this change won't cost extra memory either.
