Understanding Filesystem Synchronization Software and Policies
There are a number of software tools that offer a user the ability to synchronize filesystems despite conflicting updates made to multiple filesystem replicas, and often is unclear what policies these tools employ and difficult to understand what the policies guarantee. Alloy, a lightweight formal modeling language, was used in an exploration of filesystem synchronization properties, specifications, and algorithms. Using the Alloy analyzer, a fully automatic simulation and checking tool, we discovered some surprising relationships between some popular pieces of filesystem synchronization software.