Derecho 的规范与运行时检查：一种面向云服务的快速复制协议
分布式、并行与集群计算
2023-05-23 v1
摘要
可靠的分布式系统需要分布式进程间的复制与共识，以容忍进程与通信故障。理解与保证复制与共识协议的正确性一直是一项重大挑战。本文描述了 Derecho 的精确规范与运行时检查，Derecho 是一种较新且复杂的、面向云服务的快速复制与共识协议。精确规范必须填补英文与伪代码算法描述中缺失的细节并消除歧义，同时忠实遵循描述。为协助检查协议正确性，我们还进行了细致的手工分析与日益系统的运行时检查。我们获得了一个可直接执行的完整规范，并发现并修复了伪代码中的若干问题。这些结果得益于 Derecho 已有的详尽伪代码，并因使用 DistAlgo（一种允许分布式算法被轻松清晰表达并直接执行的语言）而成为可能。
引用
@article{arxiv.2305.12040,
title = {Specification and Runtime Checking of Derecho, A Protocol for Fast Replication for Cloud Services},
author = {Kumar Shivam and Vishnu Paladugu and Yanhong A. Liu},
journal= {arXiv preprint arXiv:2305.12040},
year = {2023}
}