                                        Mysteries of Dropbox
        Property-Based Testing of a Distributed Synchronization Service
                             John Hughes∗† , Benjamin C. Pierce‡ , Thomas Arts∗ , Ulf Norell∗† ,
                                                    ∗ Quviq AB, Göteborg, Sweden
            † Dept of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden
                       ‡ Dept of Computer and Information Science, University of Pennsylvania, PA, USA




   Abstract—File synchronization services such as Dropbox are              Our goal in this paper is to present a testable formal specifi-
used by hundreds of millions of people to replicate vital data.         cation for the core behavior of a file synchronizer. We do so via
Yet rigorous models of their behavior are lacking. We present           a model developed using Quviq QuickCheck [4]. Despite the
the first formal—and testable—model of the core behavior of a
modern file synchronizer, and we use it to discover surprising          apparent simplicity of the problem, we encountered interesting
behavior in two widely deployed synchronizers. Our model is             challenges regarding both specification and testing. We used
based on a technique for testing nondeterministic systems that          the model to test Dropbox, Google Drive, and ownCloud (an
avoids requiring that the system’s internal choices be made visible     open source alternative), exposing unexpected behavior in two
to the testing framework.                                               out of three.
                                                                           In Section II, we introduce our testing framework. Sec-
                       I. I NTRODUCTION                                 tion III gives a high-level overview of the concepts used in our
                                                                        model, in particular the operations performed by test cases, the
   File synchronization services—distributed systems that
                                                                        observations made when a test case is run on the system under
maintain consistency among multiple copies of a file or
                                                                        test (SUT), and the explanations that we construct to determine
directory structure—are now ubiquitous. Dropbox claim 400
                                                                        whether the test has passed or failed. Section IV presents the
million users,1 while Google Drive and Microsoft OneDrive
                                                                        formal specification itself, beginning with a naive version and
are reported to have over 240 million users each.2 In addition
                                                                        refining it in light of failed tests that reveal subtleties in the
to these large-scale commercial offerings and many smaller
                                                                        synchronizer’s handling of corner cases. Section V describes
ones, there are a plethora of open source synchronizers,
                                                                        further failed tests that, rather than pinpointing inadequacies
enabling users to create their own ‘cloud storage.’ With so
                                                                        in the specification, seem to us to exemplify unintended
many people trusting their data to synchronization services,
                                                                        behaviors of both Dropbox and ownCloud, including situations
their correctness should be a high priority indeed.
                                                                        where each system can lose data. In Section VI, we discuss the
   Surprisingly, then, it seems that only one file synchronizer
                                                                        pragmatics of our testing framework, in particular our methods
has been formally specified to date: Unison [1]–[3]. However,
                                                                        for triggering timing-dependent behaviors, for observing when
even Unison’s specification is not directly useful for testing;
                                                                        the system has reached quiescence, and for shrinking tests to
moreover, Unison works rather differently from contemporary
                                                                        minimal failing cases in the presence of nondeterminism. In
synchronization services: it synchronizes two peers at a time,
                                                                        Section VII, we sketch an initially promising attempt to formu-
rather than many clients with one server; synchronization is
                                                                        late the specification in terms of Lamport’s “happens before”
invoked explicitly by the user, rather than taking place auto-
                                                                        relation and explain why it ultimately proved unsuccessful.
matically in the background; and conflict resolution involves
                                                                        Section VIII surveys related work, and Sections IX and X
user interaction, rather than being performed automatically.
                                                                        present future directions and concluding remarks.
   Synchronizers are challenging not only to specify but also              Our main contributions are as follows: (1) We construct the
to test. They are large-scale, nondeterministic distributed sys-        first formal model of the core behavior of modern file synchro-
tems, with timing-dependent behavior. They must cope with               nizers. (2) To define the model, we develop a technique for
conflicts (when the same file is modified concurrently on two           testing nondeterministic systems that does not require that the
or more clients). They work in the background, and their                system’s internal choices be visible to the testing framework.
state is unobservable. Moreover, they are slow. They share              Our technique is based on an explicit representation of hidden
these difficulties with a large class of critical systems; thus,        system state plus “conjectured events” that mutate it. (3) We
techniques for addressing these problems are valuable, not              validate our final model against two commercial synchronizers
only for testing file synchronizers, but in a broader context.          and one open-source one, showing that their behavior agrees
                                                                        with the model in most situations. (4) We demonstrate the
  1 techcrunch.com, “Dropbox now has more than 400 million registered
                                                                        effectiveness of our model and testing framework by using it
users”, June 24th , 2015.
  2 fortune.com, “Who’s winning the consumer cloud storage wars?”       to reveal a number of surprising behaviors, likely not intended
November 6th , 2014.                                                    by the developers of these systems.
        II. T ESTING A S YNCHRONIZATION S ERVICE                    ones we have tested so far. In particular, we did not want to
                                                                    assume any direct access to remote servers outside our control.
   We begin by making a rather drastic simplifying assump-          Therefore, we treat the synchronizer as a ‘black box’, which
tion: we consider only one file, with operations to read,           we communicate with only through the file system; our tests
write, and delete it. We consider only operations that read         just read and write files on the virtual machines and check the
and write the entire file; we do not specify or test how the        results for validity. This allows us to write the specification
synchronizer interacts with open files as they are modified.        without dependencies on synchronizer-specific APIs.3
Restricting our attention to one file may seem extreme, but
even this simple setting forces us to confront essential issues                 III. OVERVIEW OF THE S PECIFICATION
of synchronization—in particular subtleties arising in the pres-       Our strategy for test case generation is very simple: we
ence of conflicts—and it is enough to expose surprising be-         generate test cases consisting of random sequences of calls to
haviors in real systems. A plan for extending the specification     a small set of basic filesystem operations. The basic operations
to multiple files and directories is sketched in Section IX.        we consider are
   We developed our model using Quviq QuickCheck [4],                  • R EAD N , which reads the (one) file on node N (one of
a descendant of Haskell QuickCheck [5]. QuickCheck tests                  the VMs), and
properties—universally quantified boolean formulæ—by gen-              • W RITE N V , which writes the value V (a string) to the
erating random values for the quantified variables and check-             file on node N .
ing that the formula evaluates to true. When a test fails,          We will introduce a few additional operations below.
QuickCheck “shrinks” it, searching for a similar but smaller           We use QuickCheck’s state machine library to generate
test that also fails and ultimately reporting a failing test that   tests, with a trivial model state—our tests are simply random
is ‘minimal’ in some sense. (This process is akin to delta-         sequences of R EADs and W RITEs, with random arguments.
debugging [6], although the details are slightly different.)        One might expect to track the file contents in the model state,
QuickCheck provides a domain-specific language for defining         and check that R EAD returns the modeled contents—but this
test data generators and shrinking searches; using this DSL,        could only work if synchronization were instantaneous, which
users can exert fine control over the random distribution of        of course it is not. Instead of trying to express our specification
test cases. A part of this DSL is a notation for specifying         in this synchronous style, we collect observed events as each
state machine models, which generate test cases consisting of       operation is actually executed, and we use a separate state
sequences of calls to an API under test [7], [8]; this is how       machine to validate the resulting sequence of events.
we generated test cases for synchronizers. Quviq QuickCheck            The observed events corresponding to the READ and WRITE
is embedded in the Erlang programming language—that is,             operations are as follows:
specifications are just Erlang programs that call libraries
                                                                       • when R EAD N returns the value V , we observe the event
supplied by QuickCheck—and the generated tests invoke the
                                                                          R EADN → V , and
SUT directly via Erlang function calls. As a result, there is
                                                                       • when W RITE N V overwrites the value Vold , we observe
no distinction between ‘abstract’ and ‘concrete’ test cases, as
                                                                          the event W RITEN V → Vold .
there often is in model-based testing, and there is no need for
a ‘system adapter’; instead, generated test cases are directly      Notice that, when we write the file, we observe the previous
executable.                                                         contents as well as the new one (taking the ‘previous contents’
   We ran our tests on laptops running a host operating system      of a newly created file to be the special value ⊥). The value
(Windows 8.1 or Mac OS) together with several virtual ma-           that we overwrite matters, because of the way synchronizers
chines running Ubuntu Linux. The file synchronizer under test       handle conflicts. (This observation is not actually atomic, but
was installed on each virtual machine and under the host op-        it is very unlikely that the dropbox dæmon will overwrite the
erating system, so we could read and write files on any of the      file between our read and write, and we have not observed it
virtual machines, or on the host, and expect the synchronizer       to happen.)
to propagate changes to all of the others. We ran distributed          A conflict occurs when two or more clients write the
Erlang on the virtual machines and the host, using the host         file concurrently—that is, without having seen each other’s
to coordinate each test by making remote procedure calls            updates. For example, if client 1 writes ‘a’ to the file, and
on the virtual machines. All machines were also connected           client 2 then writes ‘b’ before ‘a’ has been delivered to client 2
to the internet, allowing us to test synchronization servers        by the synchronizer, a conflict is created. One of the two values
running either remotely (in the case of Dropbox and Google          wins, and eventually all clients will see this value in the file if
Drive), or on another VM (in the case of ownCloud). The use         there are no more writes, but conflicting values are also saved
of multiple VMs on a single physical machine was purely             in special files in the same directory, with names derived from
a matter of convenience: Erlang’s support for transparent             3 For testing the specification, we found it convenient to use limited
distribution would make it straightforward to run the same          communication with the local dæmon, where available; for example, the
setup on multiple nodes. We used 3 VMs for most tests.              Dropbox client on Ubuntu provides a handy Python script for querying
                                                                    whether the local dæmon thinks it is up to date, which we used to speed
   We wanted a model that would apply (perhaps with minor           up testing a bit. This adds <10 lines of code per synchronizer to the test
adjustments) to many file synchronizers, not just the specific      harness.
the name of the original file, such as ‘paper.tex (John’s            tests may well result in a stable state never being reached!
conflicted copy)’; these files are eventually replicated             In practice we wait up to 30 seconds, long enough to allow
to other clients just like any other file. To avoid depending        synchronization to finish if it is going to but short enough to
on implementation-chosen names, our model specifies just the         enable us to ‘shrink’ test cases (which involves running many,
set of values expected to appear in conflict files, and our test     many failing tests—see Section VI) in a reasonable amount of
harness assumes that any files that appear in the same directory     time. After 30 seconds we record a “failed stabilization” ob-
as the main one are conflict files.                                  servation of the form S TABILIZE → {(V1 , C1 ), . . . , (Vn , Cn )},
   One subtlety in the specification of conflicts is that, because   where each (Vi , Ci ) records the the file contents and conflict
conflicts can only be detected using global information, there       set on one of the nodes. Such an observation is regarded as
may be a delay in the creation of conflict files. Consider the       invalid by the specification, so any test that generates it is
following sequence of observations.                                  considered to fail.
                                                                        Since stabilization is slow—and most interesting after sev-
           Client 1               Client 2
                                                                     eral read and write operations—we include it only 1/10 as
           W RITE1 ‘a’ → ⊥
                                                                     often as R EADs and W RITEs. We also add a S TABILIZE at
                                   W RITE2 ‘b’ → ⊥
                                                                     the end of every test case, which improves the probability of
                                   R EAD2 → ‘a’
                                                                     detecting that something went wrong and also reduces the risk
The two writes are in conflict, and the write of ‘a’ has ’won’,      of one test influencing the outcome of the next one.
so the value ‘b’ should appear in a conflict file. However,             How can we decide whether a sequence of observed events
client 2 cannot determine this locally (since a different client     is valid? We use a separate state machine, which accepts or re-
could have overwritten ‘b’ with ‘a’ in the meantime). So we          jects a sequence of observed events. However, the observations
must wait for pending communications with the server to finish       we make do not tell the whole story: in the background, the
before checking for the existence of conflict files.                 synchronizer is also performing actions. This makes our tests
   We therefore add another operation to our test cases,             nondeterministic—we cannot tell, from the events we have
S TABILIZE, which waits for synchronization to complete on           observed, what state the whole system is in. We address this by
all client nodes. At this point, the same value V should be          adding conjectured events to the observed ones, representing
in the file on all clients, and all clients should have the same     actions taken by the synchronization service (messages be-
set of conflict files. Once the system is stable, we observe the     tween local dæmons and a central server, interactions between
event S TABILIZE → (V, C), where C is the set of values in the       dæmons and local filesystems, etc.). In general, we can add
conflict files (i.e., both the value and the conflict files should   conjectured events to a given sequence of observed events in
be eventually consistent; we will see later that our model can       many different ways, each resulting in a different combined
always reach such a state). Note that this is a system wide          sequence of observed and conjectured events, which we call an
event, not an event observed on just one client. To check that       explanation. If any of the explanations is accepted by our state
the correct conflict file is created in the example above, we        machine, we consider the test to have passed. If there is no
would add a S TABILIZE operation to the end of the test, which       way to insert conjectured events so the resulting explanation
should result in the following observed events:                      is accepted, then we consider that the test has failed.
           Client 1               Client 2                              Our conjectured events are uploads to, and downloads from,
           W RITE1 ‘a’ → ⊥                                           the server. We write these events as U PN and D OWNN ,
                               W RITE2 ‘b’ → ⊥                       where N is the node taking part in the up- or down-load.
                               R EAD2 → ‘a’                          Thus, when we model the state of the whole system, we will
                  S TABILIZE → (‘a’, {‘b’})                          need to include the server’s state in the model. (Of course,
                                                                     in reality ’the Dropbox server’ may itself be a replicated
If ‘b’ were missing from the conflict set in the last observed       service involving many hosts. Our model implicitly assumes
event, this would represent lost data and the test would fail.       strong consistency among these hosts; weaker consistency in
   But how can we implement S TABILIZE? That is, how can             Dropbox’s implementation might in principle cause our tests
we tell that synchronization is complete, given that we treat        to fail, but we have not observed this.)
the synchronizer as a black box? Our solution is a little ad
hoc. Certainly, the value in the file and the conflict files must      To make all of the above more concrete, here is an example
be the same on each client. Also, under Ubuntu, Dropbox              of a simple test case:
provides a handy Python script to check the local Dropbox
                                                                                       Client 1         Client 2
dæmon’s status; the dæmons on each client must be reporting
                                                                                       W RITE1 ‘a’
‘up to date’. We wait for these necessary conditions to become
                                                                                                         W RITE2 ‘b’
true—but they are not sufficient, since the server may still
                                                                                       R EAD1
be holding data that will be sent to the clients. So if a
                                                                                                       W RITE2 ‘c’
S TABILIZE → (V, C) operation ever leads to an observation
                                                                                                S TABILIZE
that would cause test failure, then we wait a bit longer and
retry the operation. We cannot wait too long, because failed         Here is an observation that might arise from this test:
          Client 1               Client 2                          ‘a’ as the previous value), so it cannot have been in conflict
          W RITE1 ‘a’ → ⊥                                          with any of the other W RITEs.
                                 W RITE2 ‘b’ → ‘a’
           R EAD1 → ‘b’
                               W RITE2 ‘c’ → ‘b’                              IV. F ORMALIZING THE S PECIFICATION
                    S TABILIZE → (‘c’, ∅)
And here is a valid explanation of this observation:                  Formally, we use a deterministic state machine to accept or
                                                                   reject explanations. We define the state of the machine, the
          Client 1               Client 2                          system state, as follows:
          W RITE1 ‘a’ → ⊥
          U P1                                                       • a global stable value ServerVal (i.e., the value currently
                                 D OWN2                                held on the server)
                                 W RITE2 ‘b’ → ‘a’                   • a global conflict set Conflicts (a set of values)

                                 U P2                                • for each node N ,

           D OWN1                                                          – a local value LocalVal N ,
                                 W RITE2 ‘c’ → ‘b’                         – a local freshness, Fresh?N ∈ {FRESH, STALE}, and
                                 U P2                                      – a local cleanliness, Clean?N ∈ {CLEAN, DIRTY}.
           R EAD1 → ‘b’                                            Values (i.e., file contents) are just strings. (We define the result
           D OWN1                                                  of a R EAD or W RITE before the file has ever been written to
                   S TABILIZE → (‘c’, ∅)                           be the special value ⊥.)
Of course, the same test may give rise to different observations      In the initial state Sinit , the stable value and all the local
(and the same observation may be explained by many possible        values are ⊥, and all nodes are FRESH and CLEAN.
explanations). For example, here is another observation that          There are three kinds of observed events (R EAD, W RITE,
might arise from running the test above:                           and S TABILIZE) and two kinds of conjectured events (U P
          Client 1               Client 2                          and D OWN). A sequence of observed events is called an
                                                                   observation. A sequence of both kinds of events is called an
          W RITE1 ‘a’ → ⊥
                                                                   explanation. An explanation E explains an observation O if
                                 W RITE2 ‘b’ → ⊥
                                                                   deleting the conjectured events from E leaves just O.
           R EAD1 → ‘a’
                              W RITE2 ‘c’ → ‘b’                       For every event (of either kind), we will define a transition
                  S TABILIZE → (‘a’, {‘c’})                        consisting of a precondition (which tells us whether the event
                                                                   can happen in a given system state) and an effect (which
A valid explanation of this observation is:                        defines the change to the system state after the event has
                                                                   happened). Taken together, these preconditions and effects
          Client 1               Client 2
                                                                   define a partial function Next mapping a system state plus
          W RITE1 ‘a’ → ⊥
                                                                   an event to a new state (or failing, if the event’s precondition
                                 W RITE2 ‘b’ → ⊥
                                                                   is not satisfied by the state).
           R EAD1 → ‘a’
                                 W RITE2 ‘c’ → ‘b’                    An explanation E is valid with respect to some starting state
           U P1                                                    S if either (1) E is the empty sequence of events, or else (2) E
                              U P2                                 is a non-empty sequence e : E 0 (where : is ’cons’), such that
                  S TABILIZE → (‘a’, {‘c’})                        Next(S, e) yields a new state S 0 and E 0 is valid with respect
                                                                   to S 0 .
  Conversely, suppose the synchronizer under test were mis-           An observation O is valid if it is explained by some
behaving. Then the same test case might lead to an observation     explanation that is valid with respect to the initial state. There
with no valid explanations. For example:                           are only finitely many valid explanations for each observation,
          Client 1               Client 2                          as we explain below, so validity of observations is decidable.
          W RITE1 ‘a’ → ⊥                                             A test is a sequence of operations. It fails if the observation
                                 W RITE2 ‘b’ → ‘a’                 that arises by running it has no valid explanation; otherwise it
           R EAD1 → ‘b’                                            succeeds.
                              W RITE2 ‘c’ → ‘b’                       It remains only to define the transitions themselves. The
                  S TABILIZE → (‘c’, {‘a’})                        read and write transitions are straightforward:
Here, the final S TABILIZE observation shows that a conflict
file has been created for the file value ‘a’. But ‘a’ was the            R EADN → V
first value written to the file, and it must have been the first      Precondition: LocalVal N = V
value uploaded to the server (because the second W RITE saw           Effect: none
    W RITEN Vnew → Vold                                                  U PN
   Precondition: LocalVal N = Vold                                      Precondition: Clean?N = DIRTY
   Effect: LocalVal N ← Vnew                                            Effect: Clean?N ← CLEAN
           Clean?N ← DIRTY                                                      if Fresh?N = FRESH then
                                                                                   Fresh?N 0 ← STALE for all N 0 6= N
A write event does have a precondition, because it observes                        ServerVal ← LocalVal N
the value that is overwritten. That is, a read or write event on                else Conflicts ← Conflicts ∪ {LocalVal N }
client node N is valid with respect to some model state if the
value that the event observes in the filesystem agrees with the      U PN is only allowed if node N is DIRTY (written since the last
model’s current value for that node. Observing a R EAD has no        D OWN). Its effect is either to update the server’s value from
effect on the model state, while observing a W RITE changes          node N ’s if N is currently FRESH—i.e., if it is not in conflict
the model’s local value for node N to the one that was written       with a W RITE on another node that has already reached the
by the W RITE operation and marks node N as DIRTY.                   server—or otherwise to mark the local value as a conflict. In
   The S TABILIZE → (V, C) event has no effects (it is like a        either case, node N is marked as CLEAN.
R EAD in this respect), but it has a very strict precondition:          To decide whether a test succeeded, we construct a valid
                                                                     explanation for the observation we made; that is, we insert
                                                                     a sequence of U P and D OWN events between each pair of
    S TABILIZE → (V, C)                                              observed events that makes the explanation valid. How many
   Precondition: ServerVal = V                                       conjectured events might we need to insert? First of all, note
                 Conflicts = C                                       that each U P event makes a DIRTY node CLEAN (and neither
                 for all N, Fresh?N = FRESH                          U P nor D OWN can make a CLEAN node DIRTY). So, if there
                            Clean?N = CLEAN                          are a total of N nodes, then at most N U P events can appear
   Effect: none                                                      between consecutive observed events. Secondly, note that each
                                                                     D OWN event makes a STALE node FRESH. So there can be at
The intuition for this precondition is that this observed event is   most N D OWN events in a row. Since an U P event makes
not considered valid unless the system model has also reached        N − 1 nodes STALE, each U P can be followed by up to
a stable state. The precondition can be satisfied by adding          N − 1 D OWN events before another U P or an observed event
conjectured upload and download actions to the explanation           must occur. Thus we need to insert at most N + N · (N − 1)
until all nodes in the system state are FRESH and CLEAN.             conjectured events between each pair of consecutive ordered
   The transition for failed stabilization events has an even        events; there are only finitely many possible explanations for
stricter precondition: such an event is never allowed!               each observation, so it is decidable whether a test has passed.
                                                                        In our implementation, we do not explore all possible
    S TABILIZE → {(V1 , C1 ), . . . , (Vn , Cn )}                    explanations. We construct the set of possible states before and
                                                                     after each observed event in an observation. Given the set of
   Precondition: False                                               possible states before such an event, we select those satisfying
   Effect: none                                                      the event’s precondition and apply the event’s action to them,
                                                                     resulting in the set of possible states after the event. If the set
This ensures that any observation including a failed stabiliza-
                                                                     of possible states ever becomes empty, then the test fails.
tion will be identified as a failing test case.
                                                                        Now, given the set S of possible states after an observed
   These are all the observed events. But we also need transi-       event, we construct the set of states before the following one
tions for the conjectured events U P and D OWN. Downloading          by taking the image of S under the transitive closure of U P and
a value from the server to a client node stores the server’s         D OWN . In any such state, (a) every node will have a LocalVal
value as the local value for that node in the system state;          drawn from the set V of all LocalVals plus the ServerVal in
it also changes the node from STALE to FRESH. However, it            the given state, (b) the ServerVal will also be an element of
can only be performed if the client node is currently CLEAN.         V , (c) the Conflicts will be the union of the Conflicts in
(Otherwise, it must be preceded by an U P event, which will          the given state, and a subset of V , and (d) each node will be
reconcile the local value with the server’s.)                        FRESH or STALE, CLEAN or DIRTY . Since the size of V is at
                                                                     most N + 1, it follows that there can be at most (N + 1)N +1 ·
    D OWNN                                                           2N +1 · 4N states reachable from S.
   Precondition: Fresh?N = STALE                                        Should this set become too large to deal with during testing,
                 Clean?N = CLEAN                                     a pragmatic solution would be to abandon that test case and
   Effect: LocalVal N ← ServerVal                                    generate another. We conjecture that most bugs can be found
           Fresh?N ← FRESH                                           by a relatively deterministic test, so we would not expect this
                                                                     solution to make many interesting bugs impossible to find.
  The most interesting case is the U P transition. Here is a            However, in our experiments, N was at most 3, giving a
simple first attempt (we will refine it below):                      bound of at most 262144 states reachable from each state—
a large but not unmanageable number. In practice, we have             that no further changes would be required. But QuickCheck
almost never seen more than 1,000 different possible states           soon finds this failing test case:
during a test. Synchronizers are so slow that there is plenty of       Client 1               Client 2           Client 3
time to compute 1,000 model states after each observed event!
                                                                       W RITE1 ‘a’ → ⊥
Refining the model: repeated values                                                           R EAD2 → ‘a’
                                                                       W RITE1 ⊥ → ‘a’
  Perhaps not surprisingly, with the first-draft model as
                                                                                              R EAD2 → ⊥
presented above, testing against Dropbox fails immediately.
                                                                                                                 W RITE3 ‘b’ → ‘a’
QuickCheck reports the following minimal counterexample:
                                                                       R EAD1 → ‘b’
            Client 1               Client 2
                                                                      Why does this test fail? Because: at step 4, the server value
            W RITE1 ‘a’ → ⊥
                                                                      must be ⊥, since client 2 saw ⊥ after client 1 wrote it (and
                                W RITE2 ‘a’ → ⊥
                                                                      client 2 previously read the value ‘a’, so client 2 is not simply
                     S TABILIZE → (‘a’, ∅)                            reading the initial ⊥); at step 5, because the value client 3
The test fails because the two writes conflict—neither saw the        overwrites is not the server value, a conflict is created; the
value written by the other. Our model says that both nodes            value ‘b’ should thus only appear in conflict files on other
must upload their values before the S TABILIZE and that, on           nodes, never as the value in the file itself—yet it does just
the second U P required to enable it, the value should be added       that in the last step. Thus, there can be no explanation for this
to the set of conflicts. Yet the set of conflicts is observed to be   observation.
empty at the end. The Next function as defined above admits              (This test is, of course, quite sensitive to timing. For
no valid explanations of this observation.                            example, the second operation (R EAD2 → ‘a’) reads the
   Evidently, Dropbox considers that there is no conflict if the      value written by the first W RITE1 ‘a’ → ⊥. This is only
same value is written independently by two clients. This is a         possible if enough time passes after the first W RITE to allow
sensible design decision, but it needs to be reflected in our         the synchronizer to act. The actual test case includes S LEEP
specification. To make the implementation and specification           operations recording the need for these pauses, but they are
agree, we need to refine the specification to add special cases       not shown in the observations we present. We will return to
in the U P event when the local and global values are identical:      the question of timing in more detail in Section VI.)
                                                                         We have discovered another inconsistency with our model,
    U PN                                                              but not yet a bug: in fact, the behavior we are seeing reflects
   Precondition: Clean?N = DIRTY                                      another sensible design decision—that when a delete and
   Effect: Clean?N ← CLEAN                                            a write conflict, the write should take precedence (and the
           if Fresh?N = FRESH then                                    deletion should be silently forgotten). We must amend our
              if LocalVal N 6= ServerVal then                         model to reflect this too:
                 Fresh?N 0 ← STALE for all N 0 6= N
                                                                          U PN
                 ServerVal ← LocalVal N
           else                                                          Precondition: Clean?N = DIRTY
              if LocalVal N 6= ServerVal then                            Effect: Clean?N ← CLEAN
                 Conflicts ← Conflicts ∪ {LocalVal N }                           if Fresh?N = FRESH then
                                                                                    if LocalVal N 6= ServerVal then
With this modification, the test case passes. Here is a (newly                         Fresh?N 0 ← STALE for all N 0 6= N
valid) explanation for the observation we made:                                        ServerVal ← LocalVal N
            Client 1               Client 2                                      else
            W RITE1 ‘a’ → ⊥                                                         if LocalVal N 6∈ {ServerVal , ⊥} then
            U P1                                                                       Conflicts ← Conflicts ∪ {LocalVal N }
                                W RITE2 ‘a’ → ⊥                       The change is in the second-to-last line, which now states that
                                U P2                                  neither uploading the same value as the stable value, nor a
                     S TABILIZE → (‘a’, ∅)                            deletion, ever generates a conflict. With this change, we believe
Adding deletion to the model                                          our model reflects the intended behavior of the synchronizers
                                                                      we have tested.
   Since we already model reading from a missing file by the
special value ⊥, deletion can be modelled simply as writing ⊥                                 V. S URPRISES
back to the file. Of course, when executing tests we actually           What about unintended behaviors?
implement this by performing a real file deletion, but the event
that we observe is just W RITEN ⊥ → Vold , where Vold is              Dropbox Surprises
the contents of the file just before deletion. Since the model          Up to this point, we were essentially debugging our model
already encompasses W RITE events, we might have expected             using Dropbox as a reference implementation. However, con-
tinued testing revealed further inconsistencies between our                     Here the file is created on one client, synchronized to the other,
model and Dropbox.                                                              and overwritten there—but Dropbox does not copy the new
   The first surprise was that Dropbox can (briefly) delete a                   value to the other client, and so the system never becomes
newly created file:                                                             stable. Further investigation shows that Client 1 behaves as
                                                                                though it is still FRESH, rather than STALE, so Client 2 never
             Client 1                   Client 2
                                                                                sees the value that Client 1 wrote, and if Client 2 writes
             W RITE1 ‘a’ → ⊥
                                                                                another value to the file then it is just copied onto Client 1—
             W RITE1 ⊥ → ‘a’
                                                                                no conflict is detected, and the value ‘a’ is lost forever.
                                        W RITE2 ‘b’ → ‘a’
                                                                                Again, the behavior is timing dependent, occuring when the
             W RITE1 ‘c’ → ⊥
                                                                                second W RITE happens very soon after the value ‘b’ arrives
             R EAD1 → ⊥
                                                                                on Client 1.
In this case, W RITE2 ‘b’ and W RITE1 ‘c’ are in conflict;                         Dropbox offered the following response to these surprises:
the final R EAD1 should see one of these values, with the                       Our engineers thoroughly investigated the file and data issues
other eventually appearing in a conflict file—but at the time                   and were able to reproduce them programatically. Fortunately,
we try to read the file, it is not there at all! In this case                   we don’t believe these issues have occurred outside of the lab
stabilization would restore a correct file contents, but the test               due to the precise conditions necessary for any data loss to
fails because our model does not allow the file to be missing,                  occur–namely, the local edit occurring within the same second
even briefly. (Of course, observing this transient behavior                     as the remote change and the saved file having the identical
requires executing the operations at just the right times; the                  file size as the original. While that fact gives us comfort,
test case found by QuickCheck includes S LEEP operations that                   Dropbox takes any potential data issue, no matter how remote
make this more likely.)                                                         in possibility, extremely seriously and we are developing fixes
    The second surprise was that Dropbox can re-create deleted                  for the issue. We are grateful to the researchers for their
files, even when only one client is modifying the file!4                        efforts in testing the Dropbox service using property-based
                                                                                testing and raising awareness of property-based testing within
                               Client 1
                                                                                Dropbox.
                           W RITE1 ‘b’ → ⊥
                           W RITE1 ⊥ → ‘b’
                            R EAD1 → ‘b’                                        ownCloud Surprises

In this case Dropbox does not later ‘correct the mistake’ by                       While most of our effort has been spent testing Dropbox, we
deleting the file again: it remains there permanently. (Again,                  have also used our model (unchanged) to test ownCloud and
of course, Dropbox does not always restore files after they                     Google Drive. So far, Google Drive has behaved as expected,
have been deleted: to provoke this behavior, the test case must                 but we elicited some surprising behavior from ownCloud.
include a S LEEP operation of just the right length.)                              The first surprise was that ownCloud can delete newly
   A similar test shows that deleted files can reappear even if                 created directories, instead of propagating them to other
the creation and deletion take place on different nodes:                        nodes. More surprising yet, we actually discovered this when
                                                                                our test setup failed! To mitigate the risk of one test case
             Client 1                   Client 2                                interfering with the next, we run each test in a new directory.
                                        W RITE2 ‘b’ → ⊥                         We create these directories in batches, to reduce the time
              W RITE1 ⊥ → ‘b’                                                   spent waiting for them to propagate to all the nodes. At the
              R EAD1 → ⊥                                                        start of a test run, we delete left-over test directories, then
                     S TABILIZE → (‘b’, ∅)                                      recreate the ones we need. So, our preparation for a testing
The R EAD1 → ⊥ verifies that the file was properly deleted;                     run looks like this: (1) On the host, delete all the left-over
but, after waiting for the system to stabilize, it reappears.                   directories from previous tests. (2) On each virtual machine,
  The most alarming behavior we observed shows that Drop-                       wait for the left-over directories to disappear. (3) On the
box can lose data completely:                                                   host, create several hundred ‘fresh’ directories for the first
                                                                                few hundred test cases to use. (4) On each virtual machine,
             Client 1                    Client 2                               wait for all these new directories to appear. To our surprise,
                                         W RITE2 ‘b’ → ⊥                        when using ownCloud as the synchronizer, step (4) often failed
             W RITE1 ‘a’ → ‘b’                                                  to terminate. On checking progress, we found that not only
             R EAD1 → ‘a’                                                       had the test directories not appeared on the virtual machines,
                           S TABILIZE →                                         but they had been deleted from the host! We surmise that
                 { (‘a’, ∅),           (‘b’, ∅) }                               ownCloud may arrange deletion followed by recreation of the
                                                                                same directory in the wrong order, if they occur sufficiently
   4 There were other machines logged in to the same Dropbox account, so
                                                                                close together in time.
Dropbox was synchronizing the file at the same time to these other machines.
However, they were not involved in the test, and were not modifying the files      After we worked around this issue, QuickCheck found one
in question; they were simply passive observers.                                further discrepancy between the specification and ownCloud’s
actual behavior: ownCloud can lose changes. The following             just to allow a fixed time for synchronization to complete,
observation illustrates what can happen:                              because the more file operations a test case performs, the
                                                                      slower synchronization becomes. It appears that synchronizers
          Client 1                 Client 2
                                                                      ‘back off’ when files are changing rapidly, waiting for a
          W RITE1 ‘a’ → ⊥
                                                                      more opportune moment to do their job. This was the original
                              W RITE2 ‘b’ → ‘a’
                                                                      reason for including stabilization operations in our test cases,
          W RITE1 ‘c’ → ‘a’
                                                                      combining observations from all of the virtual machines to try
                   S TABILIZE → (‘b’, ∅)
                                                                      to detect when the synchronizer has nothing left to do.
At the end, all clients have stabilized on the value ‘b’, while          The examples we presented above are minimized test cases,
‘c’ has been completely forgotten even though it was written          found by QuickCheck’s shrinking search. Shrinking tries to re-
independently from ‘b’ (both writes saw the previous value            duce the size of test cases by dropping calls from the sequence,
‘a’) and, according to the specification, it should at least          but also reducing the duration of SLEEP operations—shrunk
appear in the final conflict set. This time, we could confirm the     test cases should wait no longer than necessary to provoke
reason by reading the ownCloud source code. The ownCloud              a failure. We also noticed that counterexamples leading to
client uses a simple test for when a file has been changed and        wrong file contents were found in two forms: ending in a
needs to be uploaded to the server: it checks whether either the      READ operation, or ending in a deletion (a W RITE of ⊥),
file’s modification time or its length are different from their       which also observes the contents. We configured shrinking so
last seen values. But modification times are recorded in the          that deletions shrink to R EAD operations (provided the test
filesystem with a 1-second granularity. So if the file is written     still fails, of course), so that the latter form would shrink to
twice in quick succession (i.e., during the same second) and          the former.
the new contents is the same length as the old one, no change            Because of the non-determinism inherent in the system,
will be detected. Thus, ‘b’ is recorded as the file’s stable value:   failing test cases may not fail every time they are run. This is
no matter how long we wait, the value (‘c’) will never reach          problematic both when searching for a failing test case, and
the server or Client 2. If the next write to the file occurs on       when shrinking one. Our solution in both cases is to run each
Client 2, ‘c’ will be silently overwritten.                           test several times, and consider the test to have failed if any
                                                                      of the runs fails—thus reducing the probability of a ‘false
                VI. P RAGMATICS OF T ESTING                           negative’ result. While running random tests, we repeated
   Many of the behaviors we encountered were timing depen-            each test three times, but while shrinking test cases, we
dent (we have not included timings here, since their values will      repeated each one twenty times. (We work harder to avoid false
vary with factors like connection speed). Our main technique          negatives during shrinking, because they lead QuickCheck to
for provoking timing-dependent behaviors was to include               report non-minimal failing tests, which can waste a great deal
S LEEP operations in our tests, which cause the whole testing         of human debugging time. In consequence, shrinking a failed
framework to pause for a specific period (up to one second,           test to a minimal one can take 10–20 minutes to finish, at 10–
randomly chosen during test generation).                              15 seconds per test. Twenty repetitions was usually enough to
   We found that timing-dependent tests often failed with             minimize failing tests.)
fairly low probability, which we could increase manually—
once we’d identified a test case that sometimes failed—by                  VII. A N A LTERNATIVE S PECIFICATION ATTEMPT
‘triggering’ some of the W RITE operations on changes in the             There is an appealing analogy between file synchronization
file. That is, we busy-wait on some node until a specified            services and the memory subsystems of modern multiproces-
value appears in the file and then immediately execute an             sors. Network hosts with copies of a replicated file correspond
operation. Triggering an operation makes unexpected behavior          to individual processor cores, the local filesystems correspond
more likely, since it may create a race condition between             to per-core caches, and the central synchronization server
the test code running on node N , and the synchronization             corresponds to the main memory. This suggests that one might
dæmon on that node. For example, it allowed us to observe             try to leverage ideas from the literature on specifications of
the last two Dropbox surprises quite repeatably. It would be          memory-system behavior (see [9], [10] for surveys) to specify
interesting to go a step further and automatically generate           the desired behavior of a synchronizer. In particular, perhaps a
triggered operations as part of test cases; this would require        specification could be based on Lamport’s notion of happened
a slightly richer generation-time state so that we can predict        before relations [11], which express the causal ordering of
what value(s) might appear in the file.                               events in a distributed system. Indeed, an early version of our
   We found the slowness of file synchronizers to be quite            QuickCheck specification was written in this style, rather than
a problem; also the unpredictability of synchronization time.         the model-based style that we have described in this paper.
It is not easy to tell when synchronization is complete—in               This early specification used the same notions of tests and
particular, the icons that synchronizers display to show their        observed events as our current one. But instead of trying
status are often wrong: the local dæmon itself is confused            to match the observed behavior against the transitions of
about what state things are in! Yet we must know, if we are           a concrete model of the system (including the server), it
to detect synchronization failures reliably. It does not work         directly specified which observations were legal by attempting
to construct a partial ordering ≺ on the observed events such       directories—in particular, they spend considerable effort on
that (1) if an event e happened before e0 on the same client,       the subtleties of conflicts in this setting. However, they address
then e ≺ e0 , and (2) if e is the W RITE event that writes the      a different distribution scenario, in which the execution of
value observed by e0 , then e ≺ e0 . If such a relation exists,     the synchronizer is a visible user-initiated action rather than
then it can be taken as an explanation for the observation. For     a continuous background activity and in which there is no
example, the validity of the observation                            centralized “global value.” They have not been used for testing.
                                                                       We have implicitly assumed that the local filesystem is
      Client 1                    Client 2
                                                                    behaving correctly (so that discrepancies between our model
      e1 : W RITE1 ‘a’ → ⊥
                                                                    and actual observations are attributable to Dropbox). Ridge et
      e2 : W RITE1 ‘b’ → ‘a’
                                                                    al. [13] show how this can be tested, using a specification with
                                  e3 : W RITE2 ‘c’ → ‘b’
                                                                    significant similarities to ours.
is justified by this relation e1 ≺ e2 ≺ e3 . On the other hand,        A distinct body of specification work deals with specifying
if no ≺ relation exists that is consistent with the observations,   the behavior of operational transform services—middleware
then a bug (or at least a discrepancy between the system and        layers that maintain consistency of replicated data structures
the spec) has been detected. For example, the observation           (databases, documents, spreadsheets, etc.) under concurrent
             Client 1               Client 2                        updates. Operational transform algorithms are widely used—
             W RITE1 ‘a’ → ⊥                                        for example, they underlie behind the collaboration features
             W RITE1 ‘b’ → ‘a’                                      in Apache Wave and Google Docs—and their theory is well
                                     R EAD2 → ‘b’                   developed [14]–[16, etc.]. However, although it has been used
                                     R EAD2 → ‘a’                   for debugging replication algorithms using symbolic model-
                                                                    checking [17], the theory has not, to our knowledge, been
cannot be partially ordered in a way that respects the two          applied to testing of actual distributed implementations. In-
conditions above. To deal with conflicts, we specified that,        deed, since these specifications are based on notions of causal
at stabilization points, all of the maximal values in the partial   ordering, our experiences reported in Section VII suggest that
order (that is, the values written by every W RITE event e such     it might be difficult to do so, at least in a black-box style.
that for no W RITE event e0 do we have e ≺ e0 ) must appear            Fraser and Wotowa [18] present a model-based testing
either as the local value or in the conflict set on all nodes.      method for non-deterministic systems, using a model-checker
   Unfortunately, although this style of specification at first     to generate test cases (sequences of transitions in the model)
appeared quite natural and elegant, we found it difficult to        which fulfill selected structural coverage criteria. But when test
extend to encompass all the behaviors we cared about. In            cases are run, the implementation may choose to make differ-
particular, the fact that the same value can be written many        ent transitions, because of non-determinism. If the implemen-
times during the same test run (e.g., the value ⊥ is written        tation diverges from the model at a deterministic point, then
every time a file is deleted), renders the second condition         the test fails, but if divergence occurs at a non-deterministic
above—“if e is the W RITE event that writes the value observed      choice point, then the test is considered inconclusive. Fraser
by e0 ...”—impossible to test with certainty.                       and Wotowa show how to take inconclusive tests and generate
   We tried dealing with this indeterminacy by constructing         new branches, again using the model checker, that fulfill
≺ relations for all possible ways of matching W RITES with          the selected coverage goal, starting from the state that the
later observations (and accepting a test case if we succeeded       implementation chose. The test is repeated, and if the imple-
for any one of them), but the result was tricky to implement        mentation follows either the original or the newly generated
and slow because the set of possibilities quickly became            path, then the coverage goal is reached. If the implementation
large. Fortunately, this failed attempt gave us the idea of         diverges again, then the test is still inconclusive, and another
working with limited knowledge about what the system is             branch can be added in the same way. Tests generated in
doing by explicitly maintaining sets of possibilities, leading      this way are tree-structured, and hopefully eventually the
to the current model-based specification.                           implementation will follow one of the paths in the tree, and
                                                                    the coverage goal will be reached.
                    VIII. R ELATED WORK                                Arcaini et al. [19] generate tests with a model checker in
   As far as we know, this is the first work to address testing     a similar way, but instead of introducing branches, they reuse
a distributed synchronization service. But the problems of          the model as a run-time monitor, to check that even if the
specifying the behavior of synchronizers and of testing the         system follows a different path from the test case, then its
behavior of nondterministic and distributed systems have both       input-output behavior still conforms to the model. They do
received considerable attention.                                    assume that the inputs in the generated test can be supplied to
   A series of formal specifications of the Unison file syn-        the SUT even though it is following an unexpected path, and
chronizer [12] by Pierce and Balasubramaiam [1], Pierce             they assume that outputs from the SUT always provide enough
and Vouillon [2] and Ramsey and Csirmaz [3] were the                information to uniquely identify the corresponding model state
starting point for the present work. Those specifications go        (‘strong conformance’). They evaluate their approach using a
further than ours in that they deal with multiple files and         Tic-Tac-Toe game, in which the model requires moves to be
valid, but does not specify which moves the computer player          determinism in those papers is quite different to the one used
should make. The Java implementation must be annotated in            here.
order to link it to the model. No errors were discovered in the
Tic-Tac-Toe implementation (but neither were any expected).                                  IX. F UTURE W ORK
   In comparison, we use two state machines, a trivial one              We have considered just the case of a single file. Naturally,
for generating tests, and a more interesting one as a run-time       there are interesting questions to ask about a synchronizer’s be-
monitor. Our monitoring state machine is deterministic, but          havior in the presence of multiple files and directory structures,
includes unobservable transitions—eliding those transitions          such as “what happens when a directory is deleted on one
makes it non-deterministic. We allow multiple possible model         client, while a file is written into that directory on another?”
states during monitoring (‘weak conformance’ in the sense of            Extending the testing framework to multiple files and di-
[19]), and we treat the SUT as a black box—there is no need          rectories will require slightly richer model states at test case
for instrumentation of the implementation to connect it to our       generation time, including the paths that have been created
model. Our examples are more complex real applications, and          so far, so that operations can stay within this set with high
we found a number of unexpected behaviors.                           enough probability to provoke bugs.
   Ulrich and König propose architectures for testing dis-             One challenge that can be expected when we make this
tributed systems [20], but assume that all internal actions of the   extension is that the set of possible system states given a
SUT are observable by the tester, and that software probes are       sequence of observed events is likely to grow much more
inserted into the SUT to allow the tester to control the timing      quickly (it will be exponential in the number of files), and
of communications between nodes, and ensure that test runs           we will probably need to find clever representations for this
are deterministic. Neither assumption holds in our setting.          set. Possibilities include representing the set as a cartesian
   Boy et al. report on an approach to testing servers by            product of smaller sets—we can overapproximate the set of
running random sequences of API calls from a number of               possible states without introducing false positives, so ideas
clients, and checking that specified invariants hold over the        from abstract interpretation [32] should be applicable here.
resulting traces [21]. The invariants are specified as patterns         Another rich source of incorrect behaviors in distributed
that are matched against the traces, and assertions that must        systems is network partitions. To provoke such behaviors, it
hold if a pattern matches. Boy et al. found a subtle timing bug      might be useful to extend our test cases with operations to
in a lock server using this method. The approach does not            disconnect and reconnect hosts from the network.
address ‘conjectured events’, however, and does not include
shrinking—the lock-server bug was minimized by hand.                                          X. C ONCLUSIONS
   A variety of work on testing nondeterministic systems can            We have described an executable formal specification of
be phrased in terms of the theory of input-output conformance        the core behavior of file synchronization services. Since it’s
(ioco) testing [22], [23]. Indeed, there are some suggestive         written in a black-box style, avoiding synchronizer-specific
similarities between aspects of this theory and the structures       APIs and communicating only via the filesystem, we were able
we used in specification and testing of synchronizers—e.g.,          to apply it to three popular synchronizers—two commercial,
the inclusion in its labeled transition systems of quiescence        one open source—and found surprising behaviors in two of
transitions, which are reminescent of our stabilization events.      them. This shows the effectiveness of the method.
It would be interesting to try to reframe our development in
                                                                        Given that three different synchronizers appear to share the
terms of ioco concepts.
                                                                     same core specification, we expect that our model should be
   QuickCheck was originally developed in and for Haskell
                                                                     applicable (perhaps with small changes to the testing frame-
[5], and it has become the most widely used testing tool
                                                                     work) to many others—e.g., Microsoft OneDrive, Box.net,
in that community. The version we used was developed
                                                                     SpiderOak, Sugarsync, Seafile, Pulse, Wuala, Teamdrive,
by Quviq and supports Quviq’s core business: specification-
                                                                     Cloudme, Cx, etc. Given the surprising behaviors already
based testing tools and services. Quviq QuickCheck [24]
                                                                     found, this should be a valuable exercise.
extends the original version with libraries tailored for testing
industrial software, such as the state machine library used                                 ACKNOWLEDGMENTS
here. It has been used to test many large systems, including
telecoms products [4], a messaging gateway [25], refactoring            We thank John Lai and other Dropbox engineers for their
tools [26], [27], and quadcopters [28]. Probably the largest         feedback. This work is partially funded by the EU FP7
application so far was to test AUTOSAR basic software (C             project PROWESS (#317820), the Swedish Strategic Research
code which runs in cars), in which a million lines of C              Foundation (RAWFP), and the National Science Foundation
was tested against 3,000 pages of the AUTOSAR standard,              (CCF-1421243).
using 20,000 lines of QuickCheck code [29]. Most of these                                         R EFERENCES
systems are deterministic, but QuickCheck has also been used
to test for race conditions in concurrent programs [30], finding      [1] S. Balasubramaniam and B. C. Pierce, “What is a file synchronizer?” in
                                                                          Fourth Annual ACM/IEEE International Conference on Mobile Comput-
two long-standing race conditions in the database distributed             ing and Networking (MobiCom ’98), Oct. 1998, full version available
with Erlang [31]. However, the approach to handling non-                  as Indiana University CSCI technical report #507, April 1998.
 [2] B. C. Pierce and J. Vouillon, “What’s in Unison? A formal specification        [23] ——, “Model based testing with labelled transition systems,” in Formal
     and reference implementation of a file synchronizer,” Dept. of Computer             methods and testing. Springer, 2008, pp. 1–38. [Online]. Available:
     and Information Science, University of Pennsylvania, Tech. Rep. MS-                 http://liacs.leidenuniv.nl/∼bonsanguemm/Toos/P9 TestingTransSyst.pdf
     CIS-03-36, 2004.                                                               [24] J. Hughes, “Software testing with quickcheck,” in Proceedings of the
 [3] N. Ramsey and E. Csirmaz, “An algebraic approach to file synchro-                   Third Summer School Conference on Central European Functional
     nization,” in Proceedings of the 8th European Software Engineering                  Programming School, ser. CEFP’09. Berlin, Heidelberg: Springer-
     Conference. ACM Press, 2001, pp. 175–185.                                           Verlag, 2010, pp. 183–223. [Online]. Available: http://dl.acm.org/
 [4] T. Arts, J. Hughes, J. Johansson, and U. Wiger, “Testing telecoms                   citation.cfm?id=1939128.1939134
     software with quviq quickcheck,” in Proceedings of the 2006                    [25] J. Boberg, “Early fault detection with model-based testing,” in
     ACM SIGPLAN Workshop on Erlang, ser. ERLANG ’06. New                                Proceedings of the 7th ACM SIGPLAN Workshop on ERLANG, ser.
     York, NY, USA: ACM, 2006, pp. 2–10. [Online]. Available:                            ERLANG ’08. New York, NY, USA: ACM, 2008, pp. 9–20. [Online].
     http://doi.acm.org/10.1145/1159789.1159792                                          Available: http://doi.acm.org/10.1145/1411273.1411276
 [5] K. Claessen and J. Hughes, “Quickcheck: A lightweight tool for                 [26] D. Drienyovszky, D. Horpácsi, and S. Thompson, “Quickchecking
     random testing of haskell programs,” in Proceedings of the Fifth ACM                refactoring tools,” in Proceedings of the 9th ACM SIGPLAN Workshop
     SIGPLAN International Conference on Functional Programming, ser.                    on Erlang, ser. Erlang ’10. New York, NY, USA: ACM, 2010, pp. 75–
     ICFP ’00. New York, NY, USA: ACM, 2000, pp. 268–279. [Online].                      80. [Online]. Available: http://doi.acm.org/10.1145/1863509.1863521
     Available: http://doi.acm.org/10.1145/351240.351266                            [27] H. Li and S. Thompson, “Implementation and application of functional
                                                                                         languages,” O. Chitil, Z. Horváth, and V. Zsók, Eds. Berlin,
 [6] A. Zeller and R. Hildebrandt, “Simplifying and isolating failure-
                                                                                         Heidelberg: Springer-Verlag, 2008, ch. Testing Erlang Refactorings
     inducing input,” IEEE Trans. Softw. Eng., vol. 28, no. 2, pp. 183–200,
                                                                                         with QuickCheck, pp. 19–36. [Online]. Available: http://dx.doi.org/10.
     Feb. 2002. [Online]. Available: http://dx.doi.org/10.1109/32.988498
                                                                                         1007/978-3-540-85373-2 2
 [7] J. Hughes, “Quickcheck testing for fun and profit,” in Proceedings of          [28] B. Vedder, J. Vinter, and M. Jonsson, “Using simulation, fault injection
     the 9th International Conference on Practical Aspects of Declarative                and property-based testing to evaluate collision avoidance of a quad-
     Languages, ser. PADL’07, 2007, pp. 1–32.                                            copter system,” in Dependable Systems and Networks Workshops (DSN-
 [8] U. Norell, H. Svensson, and T. Arts, “Testing blocking operations                   W), 2015 IEEE International Conference on, June 2015, pp. 104–111.
     with quickcheck’s component library,” in Proceedings of the Twelfth            [29] T. Arts, J. Hughes, U. Norell, and H. Svensson, “Testing autosar soft-
     ACM SIGPLAN Workshop on Erlang, ser. Erlang ’13. New                                ware with quickcheck,” in Software Testing, Verification and Validation
     York, NY, USA: ACM, 2013, pp. 87–92. [Online]. Available:                           Workshops (ICSTW), 2015 IEEE Eighth International Conference on,
     http://doi.acm.org/10.1145/2505305.2505310                                          April 2015, pp. 1–4.
 [9] S. V. Adve and K. Gharachorloo, “Shared memory consistency models:             [30] K. Claessen, M. Palka, N. Smallbone, J. Hughes, H. Svensson,
     A tutorial,” computer, vol. 29, no. 12, pp. 66–76, 1996.                            T. Arts, and U. Wiger, “Finding race conditions in erlang with
[10] L. Higham, J. Kawash, and N. Verwaal, “Defining and comparing                       quickcheck and pulse,” in Proceedings of the 14th ACM SIGPLAN
     memory consistency models,” in In Proc. of the 10th Int’l Conf. on                  International Conference on Functional Programming, ser. ICFP ’09.
     Parallel and Distributed Computing Systems, 1997, pp. 349–356.                      New York, NY, USA: ACM, 2009, pp. 149–160. [Online]. Available:
[11] L. Lamport, “Time, clocks, and the ordering of events in a distributed              http://doi.acm.org/10.1145/1596550.1596574
     system,” Communications of the ACM, vol. 21, no. 7, pp. 558–565, 1978.         [31] J. M. Hughes and H. Bolinder, “Testing a database for race
[12] B. C. Pierce, T. Jim, and J. Vouillon, “U NISON: A portable, cross-                 conditions with quickcheck: None,” in Proceedings of the 10th
     platform file synchronizer,” 1999–present, http://www.cis.upenn.edu/                ACM SIGPLAN Workshop on Erlang, ser. Erlang ’11. New
     ∼bcpierce/unison.                                                                   York, NY, USA: ACM, 2011, pp. 72–77. [Online]. Available:
[13] T. Ridge, D. Sheets, T. Tuerk, A. Giugliano, A. Madhavapeddy, and                   http://doi.acm.org/10.1145/2034654.2034667
     P. Sewell, “Sibylfs: formal specification and oracle-based testing for         [32] P. Cousot and R. Cousot, “Abstract interpretation: a unified lattice model
     posix and real-world file systems,” in Proceedings of the 25th Symposium            for static analysis of programs by construction or approximation of
     on Operating Systems Principles. ACM, 2015, pp. 38–53.                              fixpoints,” in Proceedings of the 4th ACM SIGACT-SIGPLAN symposium
[14] C. A. Ellis and S. J. Gibbs, “Concurrency control in groupware systems,”            on Principles of programming languages. ACM, 1977, pp. 238–252.
     in Acm Sigmod Record, vol. 18, no. 2. ACM, 1989, pp. 399–407.
[15] D. B. Terry, M. M. Theimer, K. Petersen, A. J. Demers, M. J. Spreitzer,
     and C. H. Hauser, Managing update conflicts in Bayou, a weakly
     connected replicated storage system. ACM, 1995, vol. 29, no. 5.
[16] Y. Saito and M. Shapiro, “Optimistic replication,” ACM Computing
     Surveys (CSUR), vol. 37, no. 1, pp. 42–81, 2005.
[17] H. Boucheneb, A. Imine, and M. Najem, “Symbolic model-checking
     of optimistic replication algorithms,” in Integrated Formal Methods.
     Springer, 2010, pp. 89–104. [Online]. Available: https://hal.inria.fr/inria-
     00524535/document
[18] G. Fraser and F. Wotawa, “Test-case generation and coverage analysis
     for nondeterministic systems using model-checkers,” in Software En-
     gineering Advances, 2007. ICSEA 2007. International Conference on.
     IEEE, 2007, pp. 45–45.
[19] P. Arcaini, A. Gargantini, and E. Riccobene, “Combining model-based
     testing and runtime monitoring for program testing in the presence
     of nondeterminism,” in Software Testing, Verification and Validation
     Workshops (ICSTW), 2013 IEEE Sixth International Conference on.
     IEEE, 2013, pp. 178–187. [Online]. Available: http://citeseerx.ist.psu.
     edu/viewdoc/download?doi=10.1.1.309.7963&rep=rep1&type=pdf
[20] A. Ulrich and H. König, “Architectures for testing distributed systems,”
     in Testing of Communicating Systems. Springer, 1999, pp. 93–108.
[21] N. Boy, J. Casper, C. Pacheco, and A. Williams, “Automated testing
     of distributed systems,” May 2004, final project report for MIT 6.824:
     Distributed Computer Systems.
[22] J. Tretmans, “Test generation with inputs, outputs and repetitive
     quiescence,” Software—Concepts and Tools, no. TR-CTIT-96-26,
     1996. [Online]. Available: http://doc.utwente.nl/65463/1/Tre96-CTIT96-
     26.pdf
