Information Technology Reference
In-Depth Information
The following discussion looks at the two variants for the cases where b has an ex-
plicit processor specification. There are two forms of explicit processor specifications:
unqualified and qualified. An unqualified explicit processor specification, i.e.,
,is
based on a processor attribute x with an attached type. The processor denoted by this ex-
plicit processor specification is the processor stored in x . A qualified explicit processor
specification, i.e.,
<
x
>
, is based on a non-writable entity y of attached type.
The processor denoted by this explicit processor specification is the same processor as
the one handling the object referenced by y . A qualified explicit processor specification
always denotes an existing processor because this specification is based on an attached
entity. This means that there is already an object attached to this entity and thus its
handler must exist. This insight helps to write the conditions for the two inference rule
variants.
<
y
.
handler
>
Create Instruction - Existing Explicit Processor
de f
= type of ( Γ , b )
h = < x > ∨ h = < y . handler >
q de f
( d , h , c )
σ . val ( p , x )
if t =( d ,< x >, c )
σ . handler ( σ . val ( p , y )) if t =( d ,< y . handler >, c )
σ . procs . has ( q )
g required cs locks
=
{ q } if q = p ( σ . rq locks ( q ) . has ( p ) σ . cs locks ( q ) . has ( p ))
{} otherwise
x g required cs locks : ¬ σ . locks passed ( p ) σ . cs locks ( p ) . has ( x )
o de f
de f
=
= σ . new obj ( c )
de f
= σ . add obj ( q , o )
r de f
σ
= σ .
ref
(
o
)
ais fresh
Γ p :: create b . f ( e 1 ,..., e n ) ; s p , σ
p :: provided q = p ∧¬ σ . rq locks ( p ) . has ( q ) ∧¬ σ . rq locks ( q ) . has ( p ) then
lock ( { q } )
else
nop
end ;
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 ;
provided q
∧¬ σ .
) ∧¬ σ .
=
p
rq locks
(
p
) .
has
(
q
rq locks
(
q
) .
has
(
p
) then
issue ( q , unlock ) ;
pop obtained rq locks
else
nop
end ;
s p , σ
The variant that handles existing processors states that the specified processor must
exist. To check this, one must consider both the qualified and the unqualified possibility.
Search WWH ::




Custom Search