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

Re-animation. A basic (user) requirement for DFS-R was that directories
cannot be deleted if they contain files that have not been processed by the
deleting party. Thus, re-animation requires that files and even directories in a
transitive way get re-created. They are re-created to preserve content that was
created or modified independently of the (remote) deletion.

Convergence. A key property of replication is obviously that all replica mem-
bers should converge to the same mirror image when there are no independent
updates to the replica sets. In general one cannot check convergence as an invari-
ant. However, as our experience with Zing (Section 6) illustrates, it is possible
to find divergence bugs by checking invariants that imply convergence.

Feature Interaction. One of the hard problems with designing a distributed
application, like DFS-R, is taking feature interaction into account. Features that
are not directly related may interact in unpleasant ways when composed. An
illustrative example of two features that interact comprises of re-animation and
name-conflict resolution. Name conflict resolution has in DFS-R the side effect
of soft deletion. The name conflict loser gets moved to a conflict area, but from
the point of view of replication it is deleted. These two features do not compose:
a directory may lose a name conflict and be deleted, but a modification to a child
file may require the name conflicting directory to be re-animated. Consequently,
DFS-R has to take such conflicts into account.

4 Prototyping DFS-R with OCaml

Section 3 illustrated a simple file system model and replication protocol. As fea-
tures and requirements were added, the complexity of the problem rose, and we
could see that invariants were easily broken. We therefore found that an informal
design would be insucient in convincing us and our peers to the soundness of
any protocol proposal, so we developed a prototype system in OCaml.
Of particular interest was that the OCaml prototype supported both a sim-
ulation and a realistic mode. In simulation mode, the replication system would
manipulate in-memory data structures for file systems, and data-bases. In real-
istic mode, the prototype accessed files on NTFS and updated a persistent store.
Neither mode was using a network, so all remote procedure calls would be per-
formed by local procedure calls, and multiple copies of DFS-R ran in the same
process. The simulation mode was furthermore applicative in all essential oper-
ations. This made implementing a backtracking search over the actions trivial.
Operations in simulation mode were several orders of magnitude faster. We also
added ad-hoc partial order reduction techniques, and performed massive simu-
lations on top of the synchronization core. Prior to starting the implementation
of DFS-R we thus covered some 120 billion scenarios each comprising of 16 file
and synchronization actions. Section 8 elaborates on similar methods used for
the production core.