summaryrefslogtreecommitdiff
path: root/ipc/ipc_right.c
diff options
context:
space:
mode:
authorJustus Winter <4winter@informatik.uni-hamburg.de>2015-08-16 02:18:47 +0200
committerJustus Winter <4winter@informatik.uni-hamburg.de>2015-08-16 02:19:38 +0200
commit80ffa7de3147b27c82667a7e2224439f92106f92 (patch)
treef4af5eae93780a12306c9026cfd381d8d7b33a4b /ipc/ipc_right.c
parent03955afa0a3cc6e9dece39ec631ce3744b1b08ba (diff)
codify locking contractspmm-2015-08-16
Diffstat (limited to 'ipc/ipc_right.c')
-rw-r--r--ipc/ipc_right.c2
1 files changed, 2 insertions, 0 deletions
diff --git a/ipc/ipc_right.c b/ipc/ipc_right.c
index 773b3b1..2e73cc3 100644
--- a/ipc/ipc_right.c
+++ b/ipc/ipc_right.c
@@ -114,6 +114,7 @@ ipc_right_reverse(
/* would switch on io_otype to handle multiple types of object */
+ assert(have_is_lock(space));
assert(space->is_active);
assert(io_otype(object) == IOT_PORT);
@@ -311,6 +312,7 @@ ipc_right_dncancel(
{
ipc_port_t dnrequest;
+ assert(have_is_write_lock(space));
assert(ip_active(port));
assert(port == (ipc_port_t) entry->ie_object);