crack ⚡

通过符号执行验证分布式和无锁算法

附录：可靠工程哲学

对于大型有状态系统，提前进行额外规范可以节省大量努力

1. TLA+ 很有用，但学习成本很高。我们使用它来填补这个差距
2. 清洁室方法：指定所有非平凡块的预期行为
3. 通过在测试环境中按时间顺序、延迟或永不发送消息来模拟异步网络条件，该测试环境探索不同的路径（生成式或全状态枚举），具体取决于测试计算时间预算

行动中

1. 在编码之前，在 TLA+ 中建模核心通信算法
2. 使所有消息可插件
3. 使所有时间来源可插件
4. 依靠时间类型概念来减少消息交付延迟状态空间的爆炸性增长
5. 对所有非平凡块大量使用 debug_assert!