Information Technology Reference
In-Depth Information
3. Object creation. Ask
q
to create a new instance with class type
c
using the creation
procedure
f
. Attach the newly created object to
b
.
4. Invariant evaluation. If
f
is not exported, then ask
q
to evaluate the invariant.
5. Lock releasing. If
q
's request queue has been locked in the locking step, then ask
q
to unlock its request queue after it is done with the feature request.
There are four cases in the processor creation step:
-
The entity
b
has a separate type.
-
The entity
b
has an explicit processor specification and the denoted processor al-
ready exists.
-
The entity
b
has an explicit processor specification and the denoted processor does
not yet exist.
-
The entity
b
has a non-separate type.
For each of these cases, there is one inference rule. The discussion starts with the variant
where
b
has a separate type. In this case, the instruction defines
q
as a new processor
and
o
as a new object of class type
c
. The reference
r
points to this object. First the
instruction acquires a request queue lock on the new processor
q
so that it can issue
statements on
q
. Next, it writes the value
r
into the entity
b
. To make a call to the
creation procedure, it executes a command instruction. Once this is done, it checks
whether there is an invariant to evaluate. If
f
is exported, then the invariant will be
evaluated as part of
f
's feature application. In this case the instruction does nothing.
However, if
f
is not exported, then it must issue the invariant evaluation to
q
. After this
step, it can issue an
unlock
operation to
q
and remove the request queue lock from
p
's
obtained request queue locks.
Create Instruction - Top
de f
=
type of
(
Γ
,
b
)
(
d
,
h
,
c
)
h
=
q
de f
=
σ
.
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
::
lock
(
{
;
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
}
)
|
q
::
nop
,
σ
Search WWH ::
Custom Search