Information Technology Reference
In-Depth Information
Suppose initially:
m
1
:
a
→
b
→
c
,clocks=
{
.That
is,
m
1
has
a
under the repli-
cated folder root,
b
under
a
,and
c
under
b
.Theclockof
b
is set
to 1, and
c
's clock is set to 2.
m
2
:
b
a
→
0
,b
→
1
,c
→
2
}
a
c
b
b
c
a
a → b
c
→
c
→
a
,clocks=
{
b
→
0
,c
→
11
,a
→
3
}
.
a
m
3
:
c
→
a
→
b
,clocks=
b
Fig. 9.
Parental demotion
{
c
→
0
,a
→
4
,b
→
5
}
.
m
4
:
a
→
c
→
b
,clocks=
{
a
→
0
,c
→
6
,b
→
7
}
.
m
5
:
c
→
b
→
a
,clocks=
{
c
→
0
,b
→
12
,a
→
8
}
.
m
6
:
b
→
a
→
c
,clocks=
{
b
→
0
,a
→
9
,c
→
10
}
.
m
5
sends
b
to
m
1
,
m
1
:
a
→
c
→
b
,clocks=
{
a
→
0
,b
→
12
,c
→
13
}
m
2
sends
c
to
m
4
:
m
4
:
a
→
b
→
c
,clocks=
{
a
→
0
,b
→
14
,c
→
11
}
m
1
sends
c
to
m
2
:
m
2
:
b
→
a
→
c
,clocks=
{
b
→
0
,c
→
13
,a
→
15
}
m
4
sends
b
to
m
5
:
m
5
:
c
→
a
→
b
,clocks=
{
c
→
0
,a
→
16
,b
→
14
}
m
2
sends
a
to
m
3
:
m
3
:
c
→
b
→
a
,clocks=
{
c
→
0
,b
→
17
,a
→
15
}
m
5
sends
a
to
m
6
:
m
6
:
b
→
c
→
a
,clocks=
{
b
→
0
,c
→
18
,a
→
16
}
That state is isomorphic to the starting state using the correspondence:
m
4
,m
2
→
m
6
,m
3
→
m
5
,m
4
→
m
1
,m
5
→
m
3
,m
6
→
m
2
}
{
m
1
→
(6)
At this point,
m
6
can take the role of
m
2
,and
m
3
can take the role of
m
5
to
kick off another round.
6.3
A Mountain Too High for Zing?
An attempt was made to extract a more realistic Zing model of DFS-R by using
the AsmL specification, and perform comprehensive model checking of the full
synchronization core. The resulting 3400 line model was then exercised by Zing,
which checked the model for consistency. Unfortunately, the resulting state space
was vastly larger than what Zing could reasonably handle. The most effective
way we know of performing state space exploration of DFS-R therefore remains
the depth-bounded search presented in Section 8.
6.4
The Zing Experience
This Section illustrated the concurrent directory move problem in the context
of using a state-space exploration tool, Zing, for checking design proposals. The
concurrent move problem is interesting in its own right, but the main take-
away here is that state space exploration tools, such as Zing, are valuable for
Search WWH ::
Custom Search