4 ms·

> 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 detail

> 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.

coldtea 7y ago
>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...
- willtim 7y ago
  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.
  - robocat 7y ago
    > 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/ https://danluu.com/file-consistency/
    - willtim 7y ago
      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.
  - coldtea 7y ago
    >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/ https://danluu.com/deconstruct-files/
    - willtim 7y ago
      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.

coldtea 7y ago

>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...

willtim 7y ago
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.
- robocat 7y ago
  > 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/ https://danluu.com/file-consistency/
  - willtim 7y ago
    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.
- coldtea 7y ago
  >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/ https://danluu.com/deconstruct-files/
  - willtim 7y ago
    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.