Database Reference
In-Depth Information
•
P
1
=
ACOM
◦
COM
◦
t
2
◦
VCON is the kernel for COMMIT;
•
P
2
=
ACOM
◦
RBACK is the kernel for ROLLBACK;
3 are the kernels for embedded SQL formulas (
P
n
are the arrows in
RA
, composed of unary operators in
Σ
RA
).
Based on this abstracted transition system, where the nodes are simply the states of
the machines, we are able to define an algorithm of the resulting synchronization of
the states between the host and RDB machines:
•
P
n
,n
≥
Synchronization mapping algorithm
Smap(ATrS
U
, ATrS
R
)
Input.
The abstracted transition systems
ATrS
U
=
(π
2
(S
PU
),
→
P
)
and
ATrS
R
=
(π
2
(S
PR
),
→
P
)
for a given source program
P
.
Mapping
F
P
:
Output.
π
2
(S
PR
)
1. Let
st
(k)
be the idle state of
M
R
after the initialization process, when
M
R
is
waiting for the calls from
M
U
. Set
i
π
2
(S
PU
)
→
=
j
=
0.
2.
i
=
i
+
1. If
i
≤
max
{
l
|
st(l)
∈
π
2
(S
PU
)
}
go to Step 3.
Otherwise,
(st(m), st
(k))
F
P
,for
j
∈
≤
m
≤
i
−
1, go to Step 8.
3. If
st(i
−
1
)
=
∂
0
(g)
,for
g
∈{
COMMIT
,
ROLLBACL
,
CALL
n
}
,goto
Step 2.
4.
(st(m), st
(k))
F
P
,for
j
1, and
(st(i), st
(k
F
P
.
j
∈
≤
m
≤
i
−
+
1
))
∈
=
i
+
1.
5.
i
=
i
+
1. If
i
≤
max
{
l
|
st(l)
∈
π
2
(S
PU
)
}
go to Step 6.
Otherwise,
(st(m), st
(k
F
P
,for
j
+
1
))
∈
≤
m
≤
i
−
1, go to Step 8.
6.
(st(i), st
(k
F
P
.If
st(i)
=
∂
0
λIn
∗
EU
Out
R
st
(m)
=
∂
1
λIn
∗
EU
Out
R
st
(m)
+
1
))
∈
then go to Step 5.
7.
(st(i
1
), st
(m))
F
P
, where
st
(m)
+
∈
=
∂
1
(f
n
)
for
f
n
=
RETURN
◦
Out
R
◦
DEC
)
n
, and
∂
0
(f
n
)
st
(k
Ap
n
, with
Ap
n
=
P
n
◦
(t
4
◦
=
+
1
)
.
1. Go to Step 2.
8.
Return
the graph of the function
F
P
:
Set
k
=
m,i
=
i
+
1
,j
=
i
+
π
2
(S
PU
)
→
π
2
(S
PR
)
.
Based on this synchronization mapping of the algorithm
Smap(ATrS
U
, ATrS
R
)
,
we are able to define the following functorial semantics for the synchronization
process in Fig.
6.3
, Sect.
6.2
:
Proposition 29
For a given source program P with the abstract transitions systems
ATrS
U
=
(π
2
(S
PU
),
→
P
) and ATrS
R
=
(π
2
(S
PR
),
→
P
)
,
we define the following
two categories
:
1.
The category
U
P
which is equal to the ATrS
U
where the objects are the machine
states in ATrS
U
,
and the atomic arrows are the atomic transitions in ATrS
U
,
but
where the transitions Out
U
and the test transitions are substituted by the
NOP
transition
.
2.
The category
R
P
where the objects are the machine states in the image of the
mapping F
P
:
π
2
(S
PU
)
→
π
2
(S
PR
)
(
obtained by the algorithm Smap(ATrS
U
,
ATrS
R
)
),
and the atomic arrows are the Application Plans P
n
,
n
≥
3(
i
.
e
.,
the
