4f4721706e
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>
37 lines
1.3 KiB
C
37 lines
1.3 KiB
C
/*
|
|
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
|
|
*
|
|
* SPDX-License-Identifier: GPL-2.0-only
|
|
*/
|
|
|
|
#pragma once
|
|
|
|
#include <types.h>
|
|
#include <api/failures.h>
|
|
#include <object/structures.h>
|
|
|
|
/* Unlink a reply from its tcb */
|
|
static inline void reply_unlink(reply_t *reply, tcb_t *tcb)
|
|
{
|
|
/* check that the tcb has a thread state with reply */
|
|
assert(thread_state_get_tsType(tcb->tcbState) == ThreadState_BlockedOnReceive ||
|
|
thread_state_get_tsType(tcb->tcbState) == ThreadState_BlockedOnReply);
|
|
|
|
/* check the tcb and reply are linked correctly */
|
|
assert(reply->replyTCB == tcb);
|
|
assert(thread_state_get_replyObject(tcb->tcbState) == REPLY_REF(reply));
|
|
|
|
reply->replyTCB = NULL;
|
|
/* This means the value of the thread state reply reference no longer matters. */
|
|
setThreadState(tcb, ThreadState_Inactive);
|
|
}
|
|
|
|
/* Push a reply object onto the call stack */
|
|
void reply_push(tcb_t *tcb_caller, tcb_t *tcb_callee, reply_t *reply, bool_t canDonate);
|
|
/* Pop the head reply from the call stack */
|
|
void reply_pop(reply_t *reply, tcb_t *tcb);
|
|
/* Remove a reply from the call stack - replyTCB must be in ThreadState_BlockedOnReply */
|
|
void reply_remove(reply_t *reply, tcb_t *tcb);
|
|
/* Remove a specific tcb, and the reply it is blocking on, from the call stack */
|
|
void reply_remove_tcb(tcb_t *tcb);
|
|
|