An Algebraic Approach to File Synchronization

and . An Algebraic Approach to File Synchronization. In Proceedings of the Joint 8th European Software Engineering Conference and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering. ACM Press, . 175185.


A file synchronizer restores consistency after multiple replicas of a filesystem have been changed independently. We present an algebra for reasoning about operations on filesystems and show that it is sound and complete with respect to a simple model. The algebra 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 synchronizer's behavior precisely. We classify synchronizers by asking whether conflicts can be resolved at a single disconnected replica and whether all replicas are identical after synchronization. We also discuss timestamps and argue that there is no good way to propagate timestamps when there is severe clock skew between replicas.

Full paper

See also

A number of other papers extending these results: Algebraic File Synchronization: Adequacy and Completeness (2016); Algebra of Data Reconciliation (2021), in Studia (2022); Data Synchronization: A Complete Theoretical Solution for Filesystems (2022), in Future Internet (2022); Synchronizing Many Filesystems in Near Linear Time (2023); in Future Internet (2023).

OCaml implementations of the algorithms described in the paper, originally intended to work with the unison synchroniser, are available on GitHub.


In 2000, I participated in the Research Science Institute (RSI) at MIT, Cambridge. I worked with Prof. Norman Ramsey (Harvard Univ., EECS) on this paper, which was ranked among the first five of all 75 papers at RSI. The result was also presented at ESEC, the 8th European Software Engineering Conference and 9th ACM Sigsoft Symposium on Foundation of Software, 2001 in Vienna.