Cimbiosys is a novel peer-to-peer replication platform that permits each device to define its own content-based filter criteria. Cimbiosys attains two properties not achieved by previous systems: (1) eventually, every device stores exactly those items whose latest version meets its arbitrary filter criteria, independent of any hierarchical namespace and (2) eventually, every device can summarize its metadata in a compact form, with size proportional to the number of devices rather than the number of items. The first property is a matter of correctness; the second a matter of efficiency.
This report describes and presents a specification of the Cimbiosys synchronization protocol, CIMSync. The specification is written in TLA+ and checked with the TLC model checker.