HN Explorer

4 comments

[ 3.2 ms ] story [ 16.4 ms ] thread
gcr
Abstract:

    > Abstract—File synchronization services such as Dropbox are used by
    > hundreds of millions of people to replicate vital data. Yet formal
    > models of their behavior are lacking. We present the first
    > formal—and testable—model of the core behavior of a modern file
    > synchronizer, and we use it to discover surprising behavior in two
    > widely deployed synchronizers. Our model is based on a technique for
    > testing nondeterministic systems that avoids requiring that the
    > system’s internal choices be made visible to the testing framework.
illumen
Property based testing really is getting some great results.
[deleted]
(comment deleted)
ineol1
To give more context, B. Pierce, one of the authors of the Dropbox paper is (one of?) the main author of Unison, and also coauthor of the paper you linked.

EDIT: The parent cited http://www.cis.upenn.edu/~bcpierce/papers/unisonspec.pdf by Pierce in 2004, where the authors stressed the difficulty of writing a specification for a file synchronizer, in this case Unison.