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.

翻译：近期分布式软件的需求促使基于Actor的框架日益流行。然而，即使采用Actor风格的消息传递模型，编写正确的分布式软件仍然困难重重。本文介绍我们在DS2（一个用于规约、综合和测试分布式Actor系统的集成框架）中实现的线性一致性检查工作。我们方法的核心洞见在于：分布式Actor系统的子组件往往代表常见算法或数据结构（如分布式哈希表或树），这些组件可以通过与系统的简单顺序模型进行验证。这使得开发者无需复杂规约即可验证其并发Actor系统。DS2自动探索系统可能达到的并发调度路径，并比较系统的观测输出以确保其等价于顺序实现可能产生的结果。我们描述了DS2的线性一致性检查方法，并在文献中多个并发复制算法上进行了测试。我们详细探讨了不同模型调度空间枚举算法在查找Actor系统缺陷方面的表现差异，并提出了我们针对Actor系统调度探索算法的改进方案，实验证明这些改进能有效发现系统缺陷。