Information Technology Reference
In-Depth Information
fresh
in the context. The context is either the set of all processors in the system or a
single processor. The heap remembers which once routines are fresh. For this purpose,
HEAP
declares the queries
is fresh
and
once result
. For any processor
p
and any once
routine
f
, the query
is fresh
states whether
f
is fresh on
p
or not. For a once function
f
that is not fresh on a processor
p
, the query
once result
returns the result of
f
on
p
.
Two commands change the once status of a fresh once routine to non-fresh. One ver-
sion works for once functions and the other one for once procedures. Both commands
take the once routine
f
and the processor
p
. The version for once functions also takes
a once result
r
. The two commands implement the semantics for once routines: a once
routine has either a once per system or a once per processor semantics. Once functions
declared as separate with or without an explicit processor specification have the once
per system semantics. In this case, the command
set once func not fresh
defines
f
as
non-fresh on all processors. Once functions with a non-separate result type have the
once per processor semantics. In this case, the command
set once func not fresh
sets
f
as non-fresh on
p
with the once result
r
. Once procedures have the once per processor
semantics. In this case, the command
set once proc not fresh
sets
f
as non-fresh on
p
.
set once func not fresh
:
HEAP
→
PROC
→
FEATURE
REF
HEAP
h
.
set once func not fresh
(
p
,
f
,
r
)
require
f
∈
FUNCTION
∧
f
.
is once
r
=
void
→
h
.
refs
.
has
(
r
)
axioms
(
∃
d
,
c
:
(
d
, •,
c
))
→
¬
h
.
set once func not fresh
(
p
,
f
,
r
)
.
is fresh
(
p
,
f
)
∧
h
.
set once func not fresh
(
p
,
f
,
r
)
.
once result
(
p
,
f
)=
r
Γ
f
:
(
∃
d
PROC
:
¬
h
.
set once func not fresh
(
p
,
f
,
r
)
.
is fresh
(
q
,
f
)
∧
h
.
set once func not fresh
(
p
,
f
,
r
)
.
once result
(
q
,
f
)=
r
,
c
:
Γ
f
:
(
d
,
p
,
c
)
∧
p
=
•
)
→∀
q
∈
set once proc not fresh
:
HEAP
→
PROC
→
FEATURE
HEAP
h
.
set once proc not fresh
(
p
,
f
)
require
f
∈
PROCEDURE
∧
f
.
is once
axioms
¬
h
.
set once proc not fresh
(
p
,
f
)
.
is fresh
(
p
,
f
)
Creation.
A new heap can be created with the constructor
make
. A new heap has no
objects and no references. All once routines are marked as fresh on all processors.
make
:
HEAP
axioms
make
.
objs
.
is empty
make
.
refs
.
is empty
∀
p
∈
PROC
,
f
∈
FEATURE
:
f
.
is once
→
make
.
is fresh
(
p
,
f
)
4.4 Regions ADT
The heap is partitioned into disjoint
regions
, and each region is assigned to exactly one
processor. This concept relates to the concept of a ken in Schmidt's work [30]. The
processor of a region is the handler of all the objects in the region. Regions are also
used to maintain locks. The following discussion first describes an ADT for processor
and then describes an ADT for regions.
Search WWH ::
Custom Search