本仓库收集了分布式系统学习的相关资料，
该课程是MIT的分布式系统课程，原名为6.824，课程内容通过阅读分布式系统领域经典论文来学习分布式系统的基本原理和关键技术。
其开源课程实验，通过若干次Lab以难度递增的方式来逐步实现一个基于Raft共识算法的分布式KV存储系统。
- Raft论文
- Lab1：实现简易的MapReduce系统，
- Lab2：实现简易的单机KV存储系统，仅支持单机存储。
- Lab3：实现Raft共识算法。
- Lab4：基于Raft共识算法实现分布式KV存储系统，实现服务端和客户端。
- Lab5：为分布式KV存储系统添加分片功能。
该课程是PingCap公司开设的分布式事务课程，学习分布式事务的基本原理。
PingCap基于TinySQL和TinyKV搭建了一个简易的分布式事务系统框架，学员需要通过实验逐步实现一个基于Percolator分布式事务算法的分布式事务系统。其中TinySQL和TinyKV是PingCap开源分布式数据库TiDB和TiKV的简化版本。
- Percolator
- Lab1：在TinyKV中实现事务相关接口。
- Lab2：在TinySQL中实现Percolator。
MiniOB是OceanBase团队开源的具有基础功能的小型关系型数据库，其中不考虑并发操作和复杂的事务管理，用于迅速了解数据库并深入学习数据库内核。
OceanBase数据库比赛设计了一系列题目，通过实现这些题目能够对数据库内核各个模块（网络、磁盘IO、索引、SQL解析、SQL执行等）有更深入的了解。
TLA+(Temporal Logic of Actions)是一种形式化规约语言，用于描述分布式系统的行为。TLA+由Leslie Lamport提出，通过TLA+可以描述系统的状态和状态转移，以及对系统的性质进行验证。
相关工具链：
该工作针对分布式协同服务系统ZooKeeper和其背后的分布式共识协议Zab，使用TLA+对其核心协议和系统实现分别进行了形式化验证。
- 论文
- 代码仓库
- 研究相关的中文论文
- 规约已被Apache ZooKeeper项目接受，详见Apache ZooKeeper TLA+规约
基于系统实现的模型检验工具（DMCK）在验证分布式系统正确性方面十分有效，但DMCK又面临着严重的状态空间爆炸问题。该工作提出SandTable技术，将状态空间遍历从代码实现级提升到规范级，有效减少状态空间爆炸问题，并成功发现了多个真实分布式系统的深层漏洞。
该技术框架通过动态追踪分布式系统的运行时行为，捕获系统各个组件之间的交互和状态变化，通过对记录事件的分析，发现系统潜在的异步时序问题。
- 相关工具: Jepsen是一个分布式系统测试框架，能够对分布式数据库、消息队列、共识系统等多种分布式系统进行黑盒测试。它专注于通过错误注入和离线分析来验证系统的事务正确性和安全性。它通过模拟诸如网络分区、时钟偏移、节点崩溃等故障，获取系统的执行结果信息，采用一系列检查器对执行历史的正确性进行检验，从而识别潜在的一致性问题。
该技术通过操控导致并发与分布式系统不确定性执行的因素：线程/协程调度、随机数、时钟、I/O等，使得系统的执行仅与一个初始的种子有关，从而便于诊断和复现系统深层次的缺陷。
相关工具：
- MadSim: 基于Rust tokio运行时的分布式系统确定性模拟测试框架，被RisingWave、Apache OpenDAL等项目使用。
- Turmoil: tokio开源的分布式系统确定性模拟测试框架。
- Hermit: Meta开源的并发程序确定性模拟执行容器环境。
深入阅读相关博客和工业实践：