Information Technology Reference
In-Depth Information
These commands wrap up the mapping of processors to objects and the locking aspects.
The discussion continues with a number of auxiliary queries to simplify access to the
presented queries. The command
add obj
makes sure that a processor is assigned to
each object that gets added. This mapping is available through the query
handled objs
.
Thus it is possible to define an auxiliary query
handler
that is inverse to the query
handled objs
.
handler
:
REG
→
OBJ
PROC
k
.
handler
(
o
)
require
∃
p
∈
k
.
procs
:
k
.
handled objs
(
p
)
.
has
(
o
)
axioms
k
.
handled objs
(
k
.
handler
(
o
))
.
has
(
o
)
There are four different categories of locks that each processor can have. For both the
request queue locks and the call stack locks, there are queries for obtained and retrieved
locks. In some situations it is easier to just work with request queue locks and call stack
locks without splitting them into obtained and retrieved locks. The auxiliary queries
rq locks
and
cs locks
serve this purpose. The auxiliary query
rq locks
returns a set that
contains all the obtained and the retrieved request queue locks of a processor
p
. Simi-
larly, the auxiliary query
cs locks
returns all the call stack locks of a processor
p
.
rq locks
:
REG
→
PROC
SET
[
PROC
]
k
.
rq locks
(
p
)
require
k
.
procs
.
has
(
p
)
axioms
k
.
rq locks
(
p
)=
k
.
obtained rq locks
(
p
)
.
flat
∪
k
.
retrieved rq locks
(
p
)
.
flat
cs locks
:
REG
→
PROC
SET
[
PROC
]
k
.
cs locks
(
p
)
require
k
.
procs
.
has
(
p
)
axioms
k
.
cs locks
(
p
)=
{
k
.
obtained cs lock
(
p
)
}∪
k
.
retrieved cs locks
(
p
)
.
flat
Creation.
The constructor
make
creates a new instance of
REG
. The new instance has
no processors.
make
:
REG
axioms
make
.
procs
.
is empty
4.5 Store ADT
Each processor in the system has a call stack to execute features. Every time a proces-
sor executes a feature, a new call stack frame gets created on top of the call stack. The
new call stack frame stores the values of formal arguments, local variables, the current
object entity, and the result entity for the current feature execution. The call stack is
also responsible for the order of feature executions on the same processor. This formal-
ization separates the two concerns of the call stack. The
store
only models the values in
each stack frame. A store has a stack of environments for each processor, where each
environment
maps names to values. This section first presents an ADT for environments
and then presents an ADT for the store.
Search WWH ::
Custom Search