#
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.
|