  Recent demand for distributed software had led to a surge in popularity in
actor-based frameworks. However, even with the stylized message passing model
of actors, writing correct distributed software is still difficult. We present
our work on linearizability checking in DS2, an integrated framework for
specifying, synthesizing, and testing distributed actor systems. The key
insight of our approach is that often subcomponents of distributed actor
systems represent common algorithms or data structures (e.g.\ a distributed
hash table or tree) that can be validated against a simple sequential model of
the system. This makes it easy for developers to validate their concurrent
actor systems without complex specifications. DS2 automatically explores the
concurrent schedules that system could arrive at, and it compares observed
output of the system to ensure it is equivalent to what the sequential
implementation could have produced. We describe DS2's linearizability checking
and test it on several concurrent replication algorithms from the literature.
We explore in detail how different algorithms for enumerating the model
schedule space fare in finding bugs in actor systems, and we present our own
refinements on algorithms for exploring actor system schedules that we show are
effective in finding bugs.
