History log of /seL4-test-master/kernel/src/object/reply.c
Revision Date Author Comments
# 4ee1f90a 14-Aug-2020 Miki Tanaka <miki.tanaka@data61.csiro.au>

mcs: add tcb argument to reply_unlink

reply_unlink takes a reply and remove the link between that reply
and its tcb. This link always exists at the call site and the tcb
information is always avaialble, or can be made available.

This commit adds this tcb as an extra argument to aid varification.

Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>


# 79da0792 01-Mar-2020 Gerwin Klein <gerwin.klein@data61.csiro.au>

Convert license tags to SPDX identifiers

This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.


# 7889580a 21-Oct-2019 Corey Lewis <corey.lewis@nicta.com.au>

mcs: Refactor reply_push

This removes an unnecessary if and asssert, and simplifies the proofs.


# 6195ea66 03-Oct-2018 Anna Lyons <Anna.Lyons@data61.csiro.au>

mcs: break call chain in reply_remove_tcb

Rather than preserving the chain break it completely. This changes the
semantics such that if a reply is removed in the middle of a call
chain, a donated scheduling context cannot return to the original
caller.


# 4f00022f 28-May-2018 Anna Lyons <Anna.Lyons@data61.csiro.au>

mcs: Use cancelIPC instead of reply_clear

- reply_clear only does half the job
- remove reply_clear no longer used


# 52beb5f3 24-May-2018 Anna Lyons <Anna.Lyons@data61.csiro.au>

reply_pop: do not call donate if SC is not NULL

This handles the specific case where a thread has donated its SC
over a Call but then is bound to another SC before the reply is
executed. In this edge-case, the donated SC remains with the callee.


# f103ac22 30-Nov-2017 Anna Lyons <Anna.Lyons@data61.csiro.au>

mcs: Refactor replies to solve revoke problems

Before this change, we set the replyObject in the thread state on recv
with no back pointer such that stray pointers would be left in the
thread state when a reply object was completed.

The new semantics are clearer and fix this problem by doing the
following:

- tcb->tcbReply is removed and the thread state field is always used,
this was unneccessary duplication previously
- the thread state value is set to the reply object only when the thread
is in BlockedOnReply or BlockedOnRecv
- the reply contains a back pointer, replyTCB, which points to that
thread
- if a thread has its reply removed, it must be set to
ThreadState_Inactive.
- deletion is easy in the blockedOnRecv case, we just unlink the reply
and the tcb.
- deletion is complicated for blockedOnReply. If we are deleing a tcb,
we remove the actual reply object and the call chain is broken. If we
are deleting a reply, we maintain the call chain by moving the tcb to
the next reply.
- we refactor the reply object interface to solve the above.
* reply_clear: removes the reply from any connections (tcb, sc)
* reply_unlink: just unlinks the tcb and reply, and sets the thread
state to inactive
* reply_remove: removes the reply from the call chain
* reply_remove_tcb: removes the exact reply that a tcb is bound to,
as we are removing that tcb. Breaks the call chain.


# 554f812d 08-Nov-2016 Anna Lyons <Anna.Lyons@data61.csiro.au>

mcs: scheduling context donation over ipc

After this commit, threads blocked on an endpoint can recieve a
scheduling context from the thread that wakes the blocked thread.