seL4
thread state: abandon replyObject NULL invariant
We no longer guarantee the invariant that the replyObject reference is NULL when the thread state is not BlockedOnReceive or BlockedOnReply.
It is likely that this invariant was true in the kernel so far, but proving it would require a new proof that the reference is already NULL for any setThreadState to a simple state such as Running, Inactive, Restart. This either means reasoning about the state the thread had before setThreadSate, or explicitly setting the reference to NULL more
often.
There are many of these setThreadState instances, and the benefit of maintaining the invariant is low. Not maintaining the invariant removes some state updates from low-level functions (called often) at the cost of adding some if-checks in higher-level functions (called less often).
Putting this on top of #1296 to see if it it still triggers MULTICORE0004 on zynqmp
I don't like it: Overall the code becomes more complex, not less, and as far as I can tell the TCB can be left with a stale reply pointer that can point to anything if the reply object was re-used.
You're only allowed to use the reply pointer when the thread state is BlockedOnReceive or BlockedOnReply, and when these states are entered, the pointer always needs to be set fresh. What the current code is trying to do is rely on an additional invariant that a field that shouldn't be accessed at all is NULL allowing you to infer that you are not in BlockedOnReceive or BlockedOnReply. It is much better to explicitly test for that than relying on other code having done cleanup properly.
But in any case the code doesn't show that this invariant holds, it may or may not do enough cleanup for this to be true (the asserts so far seem to be true, but that doesn't really mean anything, there are by far not enough of them to cover all cases, and even then they would not cover all possible executions). To actually prove this would be very high effort, because every time you go into Restart or Running or any of these simple states, you either have to know the pointer is already NULL or you have to set it to NULL -- none of the code does that, because most of the code that deals with simple states is old and didn't have to worry about reply pointers.
I as a human can't easily verify that all the threadstate assertions are correct. What about
ThreadState_BlockedOnReply?
BlockedOnReply can't happen in any of the code paths that needed change (they are either in case expressions that check for a small number of states or are about endpoint/notification queues that can't have TCBs with BlockedOnReply in them).
Can't you just abandon the invariant without changing the code?
No, the code currently (probably wrongly) relies on this invariant, that's why there are a few new ifs. The change needed to actually properly rely on the invariant would introduce a lot more change (I haven't counted, but there are many times we set thread states to simple values -- they would all need something to change).