An Algebraic Approach to File Synchronization

Norman Ramsey and Elod Csirmaz

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).