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