Models and Software Model Checking of a Distributed File Replication System - Formal Methods and Hybrid Real-Time Systems - page 15

Not only is it not obvious whether this solution is correct, but it is also wrong.
Zing found a two-machine counter-example by searching 1.5 million states in 4-5
minutes (on a 2GHz, 512MB Dell Optiplex). The counter example essentially
consisted of the configuration from Fig.6. Divergence is exercised when the two
machines ping-pong the directory b to each other.

Intentional grounding moves conflicting nodes to the root.

static atomic void resolve( int node, Node src, Machine dst) {

dst.move(node, -1, ++ globalClock);

}

This solution works (and works for Zing too), but it is overly pessimistic, as it
may move directories from deeply nested positions directly to the root. Within
the context of file systems, where directories have controlled access (using access
control lists, ACLs) this furthermore imposes security problems.

Permutation does not move conflicting nodes directly to the root, but moves
them beneath the immediate parent.

static atomic void resolve( int node, Node src, Machine dst) {

if (dst.tree[node].parent != -1) {

dst.move(node, dst.tree[dst.tree[node].parent].parent, ++ globalClock);
else

{
dst.tree[node].version = ++ globalClock;

}

}

While less pessimistic, it also suffers from security problems with access control:
the scheme allows moving directories to places they have never been moved by
any replicating machine.

Parental Demotion. Another appealing approach is to accept the instruction
as is, but if the instruction introduces a directory cycle, then move the new
parent under the previous parent of the node.

static atomic void resolve( int node, Node src, Machine dst) {

dst.move(src.parent, dst.tree[node].parent, ++ globalClock);
dst.move(node, src.parent, src.clock);

}

Unfortunately, we were able to find a configuration where this scheme diverges.
The smallest example we were able to find consists of 6 machines each with 3
directories. It requires a careful coordination between the machines to exercise
divergence. This time we had to find the counter-example manually. The state
space in this case proved larger than what Zing could handle.