Information Technology Reference
In-Depth Information
be unlocked when it is not used as an obtained or retrieved lock by any other processor
anymore. Note that there is no unlock command for call stack locks because the call
stack never gets unlocked.
unlock rq
:
REG
→
PROC
REG
k
.
unlock rq
(
p
)
require
k
.
procs
.
has
(
p
)
k
.
rq locked
(
p
)
∀
q
∈
k
:
¬
k
.
obtained rq locks
(
q
)
.
flat
.
has
(
p
)
axioms
¬
k
.
unlock rq
(
p
)
.
rq locked
(
p
)
The request queues remain locked until explicitly unlocked with a call to
unlock rq
.
Between the call to
pop obtained rq locks
and the call to
unlock rq
, the owner of these
locks is undefined. In some situations this is not satisfactory. A different solution must
be found if another processor wants to claim the locks until they are unlocked. The
command
delegate obtained rq locks
serves this purpose. It takes a processor
p
and
a number of processors
l
and makes
p
the owner of the request queue locks of all
processors in
l
by adding these locks to the obtained request queue locks stack of
p
.
This can only work if there is no current owner and the request queues are indeed
locked.
delegate obtained rq locks
:
REG
→
PROC
SET
[
PROC
]
REG
k
.
delegate obtained rq locks
(
p
,
l
)
require
k
.
procs
.
has
(
p
)
∀
x
∈
l
:
k
.
procs
.
has
(
x
)
∀
x
∈
l
:
¬∃
y
∈
k
.
procs
:
k
.
obtained rq locks
(
y
)
.
flat
.
has
(
x
)
∀
x
∈
l
:
k
.
rq locked
(
x
)
axioms
k
.
delegate obtained rq locks
(
p
,
l
)
.
obtained rq locks
(
p
)=
k
.
obtained rq locks
(
p
)
.
push
(
l
)
Delegation is different from lock passing:
delegation
is the permanent transfer of own-
ership and
lock passing
is the temporary transfer of the right to use the locks. The
following discussion looks at the commands to pass and revoke locks. The command
pass locks
takes a processor
p
and a processor
q
as well as a set of request queue locks
l
r
along with a set of call stack locks
l
c
. The result is an updated instance of
REG
in
which
l
r
and
l
c
have been passed from
p
to
q
. As a precondition for this task, processor
p
must be in possession of all these locks. This means that all the locks in
l
r
and
l
c
must
be obtained or retrieved locks of
p
and the locks must not be passed. The updated result
must reflect that some or all of
p
's locks have been passed. However, because the two
sets of locks can potentially be empty,
p
's locks must only be marked as passed if at
least one of the two sets of locks is non-empty. Lastly, the command must take care of
one special case of the lock passing operation. If a processor
q
different from processor
p
passed its locks in a previous lock passing operation and now the command passes
these locks back to
q
, then the command has to mark the locks of processor
q
as not
passed. This case is important to handle separate callbacks.
Search WWH ::
Custom Search