An Algebraic Approach to File Synchronization
We present a sound and complete proof system for reasoning about
operations on filesystems.
The proof system enables us to specify a file-synchronization
algorithm that can be combined with several different
conflict-resolution policies.
By contrast, previous work builds the conflict-resolution
policy into the specification, or worse, does not specify the
behavior formally.
We present several alternatives for conflict resolution, and we
address the knotty question of timestamps.
Full paper
The paper is available as
US Letter PostScript (263K),
US Letter PDF (268K),
and
US Letter TeX DVI (98K).