Information Technology Reference
In-Depth Information
add obj
:
REG
→
PROC
OBJ
REG
k
.
add obj
(
p
,
o
)
require
k
.
procs
.
has
(
p
)
∀
q
∈
k
.
procs
,
u
∈
k
.
handled objs
(
q
)
:
u
.
id
=
o
.
id
axioms
k
.
add obj
(
p
,
o
)
.
handled objs
(
p
)
.
has
(
o
)
In the opposite direction, the command
remove obj
removes an object that is handled
by a processor in
procs
from the regions.
remove obj
:
REG
→
OBJ
REG
k
.
remove obj
(
o
)
require
∃
p
∈
k
.
procs
:
k
.
handled objs
(
p
)
.
has
(
o
)
axioms
¬∃
p
∈
k
.
procs
:
k
.
remove obj
(
o
)
.
handled objs
(
p
)
.
has
(
o
)
The following part discusses the commands that deal with the locking aspects of the
regions. The command
lock rqs
locks the request queues of a set of processors
q
on
behalf of a processor
p
. None of these request queues must be locked beforehand.
lock rqs
:
REG
→
PROC
SET
[
PROC
]
REG
k
.
lock rqs
(
p
,
l
)
require
k
.
procs
.
has
(
p
)
∀
)
∀
x
∈
l
:
¬
k
.
rq locked
(
x
)
axioms
k
.
lock rqs
(
p
,
l
)
.
obtained rq locks
(
p
)=
k
.
obtained rq locks
(
p
)
.
push
(
l
)
∀
x
∈
l
:
k
.
lock rqs
(
p
,
l
)
.
rq locked
(
x
)
x
∈
l
:
k
.
procs
.
has
(
x
At some point, processor
p
will not require the obtained request queue locks anymore
because
p
made sure to enqueue all necessary features requests. Processor
p
uses the
command
pop obtained rq locks
to remove his claims on the obtained request queue
locks. This requires that processor
p
is in possession of these locks, i.e., that
p
did not
pass its locks.
pop obtained rq locks
:
REG
→
PROC
REG
k
.
pop obtained rq locks
(
p
)
require
k
.
procs
.
has
(
p
)
¬
k
.
obtained rq locks
(
p
)
.
is empty
¬
k
.
locks passed
(
p
)
axioms
k
.
pop obtained rq locks
(
p
)
.
obtained rq locks
(
p
)=
k
.
obtained rq locks
(
p
)
.
pop
Removing the locks from
p
's obtained request queue locks stack does not mean that
these request queues are unlocked. It just means that the request queue locks are not
claimed by
p
anymore and therefore
p
will not enqueue further feature requests on
the respective processors. The request queues remain locked until they get unlocked
with a call to the command
unlock rq
. This happens after the processors whose request
queues got locked by
p
finished all the requested feature applications. The precondition
of the command states that a request queue can only be unlocked if it is not claimed
by any other processor. This precondition guarantees that the request queue can only
Search WWH ::
Custom Search