AnySystem

AnySystem 是一个用于分布式系统确定性模拟和测试的框架。它允许将任意系统表示为一组在由网络连接的节点上运行的 进程 集合。

进程通过发送和接收 消息 互相通信。位于不同节点的进程之间的消息通过网络传输。进程还可以接收和发送 本地消息，这些消息可以用来模拟与外部实体（如用户）的交互。最后，进程可以安排 计时器，在指定延迟后调用自身。可以为每个进程实现处理传入消息和计时器的任意逻辑。除了 Rust 之外，还可以使用 Python 实现进程。

系统是通过创建所需的节点和进程，并将每个进程绑定到某个节点来构建的。然后可以发送一些消息以启动系统执行。执行是通过逐步 模拟 实现的。每个步骤对应于某些事件的发生，例如消息传递或计时器触发。事件按照其时间戳的顺序处理，通过推进模拟时间并调用相应的进程。作为响应，进程可以执行产生新事件的操作，例如发送消息可以产生新的消息传递事件。目前，不模拟进程执行时间，即假设事件是瞬时处理的。通过使用用户定义值初始化的公共 RNG，系统执行是确定的。

AnySystem 支持对分布式系统中常见的典型情况进行建模，例如消息延迟、网络故障和节点崩溃。提供的网络模型可以配置为引入固定或随机传输延迟、消息丢失、重复或损坏。还可以模拟节点断开连接、控制节点之间的网络以及每个方向的网络，或引入网络分区。可以通过从网络断开连接并停止其上运行的所有进程来使节点崩溃。可以通过重新启动其进程并将其连接到网络来稍后恢复崩溃的节点。

所述功能可用于测试任何以进程集实现为分布式算法或应用的测试。逐步模拟可以通过发送消息和在特定时间引入故障来精确控制系统执行并产生不同的执行场景。它还可以在任何时间检查每个进程的状态或全局状态的正确性。如果发现错误，可以输出系统执行的跟踪以进行调试。由于确定性模拟，可以在错误修复之前可靠地重新生成错误执行。

除了基于模拟的测试之外，AnySystem还支持模型检查。这种方法基于从给定初始状态开始遍历可能系统状态的图。系统状态由进程、节点和网络的状态以及挂起事件列表确定。图中的弧对应于由事件引起的状态之间的转换。每次系统执行对应于图中的一个路径。虽然模拟仅检查单个执行路径，但模型检查允许探索所有可能的执行路径并彻底测试系统。然而，在实践中，这种方法通常受限于系统状态图的巨大大小。AnySystem允许灵活配置模型检查策略，以在合理执行时间和完全性之间进行权衡。

AnySystem用于HSE大学《分布式系统》课程的作业。分布式系统课程的每次作业中，学生都应该根据给定的要求实现某个系统的进程逻辑，例如分布式键值存储。解决方案的正确性和其他所需属性通过基于模拟和模型检查的测试进行验证。

许可证

AnySystem根据您的选择，受Apache-2.0许可证或MIT许可证的许可。

除非您明确声明，否则您故意提交以包含在AnySystem中的任何贡献，如Apache-2.0许可证中定义的，应按上述方式双重许可，不附加任何额外条款或条件。