基于 Actor 系统的高效线性一致性检查

近期对分布式软件的需求使得基于 actor 的框架广受欢迎。然而，即便使用 actor 的风格化消息传递模型，编写正确的分布式软件仍然困难。我们展示了在 DS2 中进行线性一致性检查的工作，DS2 是一个用于指定、综合和测试分布式 actor 系统的集成框架。我们方法的关键见解是，分布式 actor 系统的子组件通常代表常见算法或数据结构（例如分布式哈希表或树），可对照系统的简单顺序模型进行验证。这使得开发者无需复杂规约即可轻松验证其并发 actor 系统。DS2 自动探索系统可能到达的并发调度，并比较系统的观测输出以确保其等价于顺序实现所能产生的结果。我们描述 DS2 的线性一致性检查，并在文献中的若干并发复制算法上对其进行测试。我们详细探究了枚举模型调度空间的不同算法在发现 actor 系统缺陷方面的表现，并提出了我们对探索 actor 系统调度算法的改进，表明其在发现缺陷上有效。