分布式系统

研究方向概览

分布式系统是本实验室最核心的研究方向。我们致力于探索大规模分布式计算与存储系统的基础理论问题，重点关注一致性协议的形式化验证与工程优化、分布式共识算法的吞吐量-延迟权衡，以及面向云原生环境的容错机制设计。研究成果已在 SOSP、OSDI、NSDI 等顶级系统会议上发表。分布式系统的研究具有独特的美感——在一个由不可靠组件构成的系统中，通过精巧的协议设计，在整体层面提供可靠的抽象，这一过程本身即是对工程创造力的最高考验。

分布式系统的理论基础可以追溯到20世纪70年代的FLP不可能性结果（Fischer, Lynch, Paterson, 1985）——在异步系统中，即使只有一个节点可能发生故障，也不存在确定性的共识算法能够在有限时间内达成一致。这一结果深刻影响了分布式系统设计的哲学：与其追求完美的确定性，不如在实用性上做出妥协，通过引入随机性（如Ben-Or算法）、故障检测器（如Ω Failure Detector）或部分同步假设来绕过FLP的约束。Raft协议正是建立在部分同步网络模型之上的工程杰作——它牺牲了最坏情况下的理论最优性，换来了可理解性和工程可实现性。

核心技术领域

• Paxos
• Raft
• EPaxos
• CRDT
• ZooKeeper
• etcd
• gRPC
• TLA+
• Jepsen
• Chaos Engineering

研究子方向

• 分布式一致性协议 — 深入研究了 Paxos、Raft、EPaxos 等经典共识算法的理论性质，包括安全性（Safety）与活性（Liveness）的形式化证明。使用 TLA+ 规约语言对 Raft 协议的 Leader Election 和 Log Replication 子协议进行了完整的模型检测（Model Checking），发现并修复了若干边界条件下的安全性违规路径。在工程层面，针对 Multi-Paxos 在 WAN 部署场景下的高延迟问题，提出了一种基于地理位置感知的 Leader 选举优化策略，将跨地域写延迟降低 40%。
• CRDT 与最终一致性 — 系统性地研究了无冲突复制数据类型（CRDT）的理论基础与工程实现。比较了 State-based CRDT（CvRDT）与 Operation-based CRDT（CmRDT）在不同网络条件下的收敛速度与元数据开销。在协同编辑场景下实现了一套基于 RGA（Replicated Growable Array）算法的实时协同文档系统，并通过 Yjs 框架验证了 CRDT 在实际应用中的可行性。
• CAP 理论的实践边界 — 通过构建大规模分布式系统实验平台，量化分析了 CAP 定理在真实网络环境中的表现。研究了网络分区（Network Partition）场景下，不同一致性级别（Strong/Sequential/Eventual）对系统可用性的影响。提出了基于自适应降级策略的可用性保障方案，在牺牲最小一致性的前提下最大化系统可用性。
• 分布式事务与隔离级别 — 深入研究了 Percolator 两阶段提交协议和 Google Spanner 的 TrueTime 机制。探索了在分布式环境下实现 Serializable 隔离级别的工程可行性，比较了乐观并发控制（OCC）、悲观两阶段锁（2PL）和 MVCC 混合策略在不同工作负载下的性能表现。
• 共识算法的性能工程 — 使用 Rust 语言从零实现了 Raft 共识算法的高性能版本，通过异步 I/O（tokio）、零拷贝日志复制和批量提交（Batching）等优化手段，在标准基准测试中将单 Leader 吞吐量提升至 50K ops/s。开源实现已被多个分布式数据库项目采用作为共识层。

理论基础与形式化验证方法论

分布式系统形式化验证的方法论框架包含三个层次：规约（Specification）、建模（Modeling）和验证（Verification）。在规约层面，我们使用TLA+语言描述系统的安全性与活性属性——安全性属性（如「任何时刻最多存在一个Leader」）通过不变式（Invariant）表达，活性属性（如「最终会选出一个Leader」）通过时序逻辑公式（Temporal Formula）表达。在建模层面，我们将协议的状态空间编码为TLA+的变量集合与状态转移关系，并利用对称性归约（Symmetry Reduction）和偏序归约（Partial Order Reduction）技术压缩状态空间的大小。在验证层面，TLC模型检测器在有限模型下穷举探索所有可达状态，检查不变式是否始终成立。

形式化验证在工业界的应用正逐步从「奢侈品」转变为「必需品」。Amazon使用TLA+验证了DynamoDB、S3等核心服务的协议正确性；Microsoft使用TLA+验证了Azure Cosmos DB的一致性协议；MongoDB使用TLA+验证了副本集协议。我们的研究工作深受这一工业趋势的影响，致力于将形式化方法从学术论文中「解放」出来，转化为可集成到CI/CD流水线中的实用工具。

工程挑战与解决方案

分布式系统在工程实现中面临几个核心挑战。首先是部分故障（Partial Failure）问题：在分布式环境中，故障不是二元的（正常/宕机），而是连续的（网络延迟增加、丢包率升高、时钟偏移增大等），这种「灰色故障」使得故障检测与恢复变得极为复杂。我们的解决方案包括：(1) 基于Phi Accrual Failure Detector的自适应故障检测算法，该算法使用历史心跳间隔的统计分布来动态调整故障怀疑阈值；(2) 基于Quorum机制的可调节一致性写策略，允许运维人员在一致性与可用性之间进行动态权衡。其次是时钟依赖问题：尽管TrueTime（Google Spanner）等硬件辅助方案提供了有界时钟偏移保证，但在通用云环境中，我们只能依赖NTP同步，其精度通常在1-10ms量级——我们的协议设计严格避免了对精确时钟同步的依赖。第三是网络分区问题：我们通过Jepsen框架系统性地模拟了各种网络分区模式（对称/非对称分区、部分分区、间歇性分区），并确保协议实现在所有场景下保持安全性。

未来研究方向

分布式系统研究的未来方向包括：一是拜占庭容错（BFT）的实用化——随着区块链和去中心化金融（DeFi）的发展，BFT共识协议（如PBFT、HotStuff、Tendermint）在性能与可扩展性方面的优化成为新的研究热点，我们关注如何将传统CFT协议的工程优化经验应用于BFT场景；二是地理分布式系统（Geo-Distributed Systems）——在跨大洲部署的分布式系统中，光速延迟（约70ms/10000km）成为无法逾越的物理限制，我们探索如何通过数据放置优化、CRDT等无冲突数据结构和异步编程模型来隐藏这一延迟；三是可信执行环境（TEE）在分布式系统中的应用——利用Intel SGX/AMD SEV等硬件安全技术，在不完全信任的云环境中构建可验证的分布式计算平台。这些方向延续了我们对分布式系统正确性与性能的双重追求。

代表性研究工作

在分布式共识协议的工程优化方面，我们提出了基于流水线（Pipelining）与批量提交（Batching）的混合优化策略，在保持 Raft 协议安全性不变的前提下，将跨数据中心日志复制吞吐量提升了 2.8 倍。该工作的技术报告已被多个开源分布式数据库项目引用。

在分布式系统的形式化验证方向，我们开发了一套基于 TLA+ 与 Jepsen 的自动化验证工具链，支持对 Paxos/Raft/EPaxos 等共识算法的模型检测与故障注入测试。该工具链已被 Apache Curator 社区采纳，显著降低了协议实现中的边界条件缺陷率。