Hacker News Reader

Comment by coldtea | Hacker News Reader

>Unison is the only bidirectional sync tool that I trust to get the details right. It is backed by a formal model with various proofs of correctness.

That's just about the sync process/stages, the easy part that can actually be formalized.

The "million fiddly things" are about OS and filesystem issues, incompatibilities, and so on, and Dropbox has a hugely larger test base for those things...

View on HN

I disagree. POSIX, although somewhat dated, has provided a good enough abstraction layer for filesystems and OSs. My proof of this is the number of different and successful filesystems for Unix/Linux. If the abstraction didn't work, everyone would be forced to use the same filesystem.

The issues and subtleties are with bidirectional sync. It is not "the easy part". Dropbox didn't get it right in the past, we have no proof they have it right now.

> POSIX, although somewhat dated, has provided a good enough abstraction layer for filesystems and OSs

I know nothing about POSIX, but I presume we all want stronger guarantees to avoid the risk of syncing a corrupted file.

https://danluu.com/file-consistency/

That's really the job of the filesystem to protect against corruption using checksums. ZFS will do this and hopefully more will follow. I suppose a file sync tool could detect a change of contents with no change of mtime, but that would be expensive.

>POSIX, although somewhat dated, has provided a good enough abstraction layer for filesystems and OSs.

First of all, POSIX semantics are not what Windows support. Second, even where available, POSIX is a tiny part of the possible issues. Adequate for naive apps that need to open or write some files, not for a reliable sync tool.

https://danluu.com/deconstruct-files/

The issues discussed in that link, such as concurrency, lack of atomicity and failure are all factors that make bi-directional sync a hard problem. Yes POSIX provides few guarantees and so that burden rests on the application code above. The formal model must consider the race conditions and failure modes, it is not "the easy part". I do acknowledge there is a modelling gap to overcome and some problems with POSIX, but I disagree that its the hardest part of the problem.

Reply on news.ycombinator.com