Database Reference
In-Depth Information
5.
Stop
S
:
S
P
→{
0
,
1
}
is a total stop-criteria function such that
Stop
S
(i, st, ID
T
)
=
0if
i
is not the address of any instruction of
Pr(ID
T
).
6.3.2 The Concurrent Categorial Transaction Recovery
In what follows, the concurrent-categorial RDB machine
M
RC
will be considered
as a computation model for the operational semantics for the database mappings,
developed in the next chapter. In fact, in this section, we will demonstrate such a
property by the final Corollary
22
.
We may abstract a deterministic transition system
TrS
=
(S
PU
,
→
P
)
in Defi-
nition
45
, obtained by a concurrent execution of a program
P
=
P(
1
)
|···|
P(n)
on a machine
M
UC
, by forgetting the instruction addresses and Transaction iden-
tifiers, that is, by substituting the transitions
((j, st(i), ID
T
),(k,f (st(i)), ID
T
))
∈
→
P
by simple abstracted state-transitions
(st(i),f (st(i)))
∈→
P
.Let
ATrS
U
=
→
P
)
be the abstracted deterministic transitions system obtained from
the execution of the concurrent program
P
(π
2
(S
PU
),
=
|···|
P(
1
)
P(n)
on a host machine
M
UC
, with
π
2
(S
PU
)
S
U
being the set of its internal states
progressively numbered from 0 (initial state) to the last
N
th state (end of this pro-
gram).
Consequently, we are able to use the same synchronization mapping algorithm
Smap(ATrS
U
, ATrS
R
)
in Sect.
6.2.1
in order to define the mapping
={
st(i)
|
0
≤
i
≤
N
}⊆
F
P
:
π
2
(S
PU
)
→
π
2
(S
PU
).
Hence, also for the concurrent programs
P
1, we can use
Proposition
29
in order to define the categories
U
P
and
R
P
, and Fig.
6.4
in
Sect.
6.2.1
is valid also in this case for the “forgetful functor”
F
P
:
=
P(
1
)
|···|
P(n),n
≥
R
P
be-
cause each conversation between
M
UC
and
M
RC
is completely contained in a given
time-window (the atomic conversations in the time-sharing scenario).
Consequently, we are able to define a category with the sequential composition
of concurrent-programs, with the embedded SQL statements over a given database
schema, by the following generalization of Definition
41
:
U
P
→
Definition 46
where the
objects are the sequential compositions of the source programs with SQL state-
ments over this schema
Let
A
be a database schema. We define a category
P
A
A
, while the arrows are the actions
P
0
◦
_
:
P
1
→
P
2
such that
P
2
=
P
0
◦
P
1
is the program obtained by sequential composition of
P
1
=
(P
1
(
1
)
|···|
P
1
(n)),n
≥
1, and
P
0
=
(P
0
(
1
)
|···|
P
0
(m)),m
≥
1.
_ where
P
NOP
is the program com-
posed of only the instruction NOP. The associativity of composition of the arrows is
guaranteed by the associativity of the sequential composition of the programs, thus
P
A
Each identity arrow in
P
is equal to
P
NOP
◦
A
is well defined.
