News for hackers. Stuff that matters.

A comment on Unison File Synchronizer. Parent comment

Re:Unison File Synchronizer by willtim on Tuesday August 06, 2019 @04:10PM (#20629020)
> there's a million fiddly things to get right, and Unison hasn't had that much usage

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. Such models are also easily representated in OCaml; which I can assure you is more than a fine language, especially if one cares about correctness. Dropbox has struggled to get these details correct in the past (see the paper "Mysteries of DropBox", by Unison's author Professor Benjamin Pierce). TLDR, Pierce teaches these Python hackers how to fix their broken code.

[ Parent | on HN ]
Re:Unison File Synchronizer by coldtea on Tuesday August 06, 2019 @05:56PM (#20630078)
>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...

[ Parent | on HN ]
Re:Unison File Synchronizer by willtim on Tuesday August 06, 2019 @06:16PM (#20630231)
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.

[ Parent | on HN ]
Re:Unison File Synchronizer by coldtea on Tuesday August 06, 2019 @06:49PM (#20630449)
>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/

[ Parent | on HN ]
Re:Unison File Synchronizer by willtim on Wednesday August 07, 2019 @03:30AM (#20632649)
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.
[ Parent | on HN ]
Re:Unison File Synchronizer by robocat on Tuesday August 06, 2019 @06:38PM (#20630374)
> 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/

[ Parent | on HN ]
Re:Unison File Synchronizer by willtim on Tuesday August 06, 2019 @06:42PM (#20630395)
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.
[ Parent | on HN ]