Information Technology Reference
In-Depth Information
For the qualified option, one can simply lookup the value of the attribute
x
.Forthe
unqualified option, one first looks up the value of the entity
y
and then determines
the handler of the referenced object. In either case, the result
q
is either the denoted
processor or the void value. One then checks whether
q
is in the set of processors of our
system. The overall idea of this inference rule is the same as in the case where
b
has
a separate type. The difference is in the processor creation, locking, and lock releasing
steps. Instead of creating a new processor, the instruction takes the existing processor
q
.If
q
=
p
, then the call to the creation procedure will be a non-separate call. In this
case, the instruction requires
p
's call stack lock. This lock is given because otherwise
p
would be waiting. If
p
q
and
q
has a lock on
p
, then the call to the creation procedure
will be a separate callback. In this case, the instruction requires
q
's call stack lock. This
is expressed in the condition with the help of the set
g
required cs locks
.If
p
=
q
and
q
does not have
p
's request queue lock, then the call to the creation procedure will be a
separate call. In this case, the instruction must obtain
q
's request queue lock, provided it
does not already have this lock. Only when it obtained
q
's request queue lock, does the
instruction have to issue an
unlock
operation and remove
q
from
p
's stack of obtained
request queue locks.
Create Instruction - Non-Existing Explicit Processor
=
de f
=
type of
(
Γ
,
b
)
h
=
<
x
>
¬
σ
.
procs
.
has
(
σ
.
val
(
p
,
x
))
q
de f
(
d
,
h
,
c
)
=
σ
.
new proc
o
de f
=
σ
.
new obj
(
c
)
de f
=
σ
.
add proc
(
q
)
.
add obj
(
q
,
o
)
r
de f
σ
=
σ
.
ref
(
o
)
ais fresh
Γ
p
::
create
b
.
f
(
e
1
,...,
e
n
)
;
s
p
,
σ
→
p
::
write
(
x
.
name
,
q
)
;
lock
(
{
q
}
)
;
write
(
b
.
name
,
r
)
;
b
.
f
(
e
1
,...,
e
n
)
;
provided
¬
f
.
class type
.
inv exists
∨
f
.
exported
then
nop
else
issue
(
q
,
eval
(
a
,
f
.
class type
.
inv
)
;
wait
(
a
))
end
;
issue
(
q
,
unlock
)
;
pop obtained rq locks
;
s
p
|
q
::
nop
,
σ
For the variant that handles non-existing processors, one has to verify that the specified
processor does not exist. To do so, one considers only unqualified processor specifica-
tions. In this case, the instruction creates a new processor
q
with a new object
o
and
reference
r
. The steps in this variant are similar to those in the variant where
b
has a
separate type. However, the instruction has to set the value of the processor attribute
x
to the newly created processor. This ensures that the denoted processor will be found to
exist in the future.
Search WWH ::
Custom Search