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
By contrast, previous work builds the conflict-resolution
policy into the specification, or worse, does not specify the
We present several alternatives for conflict resolution, and we
address the knotty question of timestamps.
The paper is available as
US Letter PostScript (263K),
US Letter PDF (268K),
US Letter TeX DVI (98K).