Gerwin Klein 4f4721706e reply: do not assume 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 like 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).

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

2025-02-10 15:53:08 +11:00

..

fastpath.h

reply: do not assume replyObject NULL invariant

2025-02-10 15:53:08 +11:00