Information Technology Reference
In-Depth Information
AsmL and generated test sequences. Lacking tight .NET integration with DFS-
R, we resorted to using the FSM generation tool generate test cases in an XML
file and implement a reader that interprets the traces within DFS-R.
6
Reconciling Trees
sync
a
c
b
In this Section we illustrate the
use of a model-checker Zing [10]
for checking conflict resolution
strategies for concurrent moves.
Recall that one of the require-
ments for DFS-R was that it
replicate and maintain directory
hierarchies as tree-like struc-
tures. When machines are al-
lowed to move files around on
a network, it may however be
possible arriving at configura-
tions that cannot be reconciled
into a directory tree. Fig.6. illus-
trates an instance of this prob-
lem: two machines share direc-
tories
a
,
b
,and
c
.Onemachine
creates the tree
a → b → c
,the
other
c → b → a
. What should
b
's parent be?
We used Zing to check for
convergence of a proposed res-
olution method for concurrent
moves. Zing demonstrated that the proposal was open to divergence by pro-
ducing a counter-example along the lines of Fig.6. The counter-example found
by Zing, was subsequently tested against another shipped replication product
which failed to converge. This bug had gone undetected for several years.
a
c
b
move
b
under
c
move
b
under
a
a
c
b
a
c
move
a
under
b
b
move
c
under
b
c
b
a
a
b
c
?
Fig. 6.
Concurrent conflicting moves
6.1
Zing
Zing is a model checker for multi-process programs. Zing's input language is
perhaps easiest compared with Promela [11]. The notion of process and atomic
statements are similar, while Zing appeals to an object oriented programming
style.
6.2
A Zing Encoding
Our Zing encoding of the tree reconciliation problem uses the absolute minimal
features necessary to emulate conflict resolution of concurrent moves. Thus, each
Search WWH ::
Custom Search