NUS - Distributed Systems

01. 互斥 (Mutual Exclusion)

• 互斥算法属性
  • 互斥性 (Mutual Exclusion)
  • 进展性 (Progress)
  • 无饥饿性 (No Starvation)

• Peterson算法
  • 证明方法：矛盾法
    • 互斥性：turn变量的作用
    • 进展性：至少一个进程能进入临界区
    • 无饥饿性：等待进程最终能进入

• Lamport面包店算法
  • 基于“取号-服务”机制
  • 共享变量：choosing[]（取号中标记）、number[]（队列号）

• 硬件解决方案
  • 中断禁用
  • 原子指令（如TestAndSet）

02. 同步原语 (Synchronisation Primitives)

• 信号量 (Semaphores)
  • P()（等待）与V()（信号）的原子操作
  • 应用场景：互斥锁、生产者-消费者问题

• 哲学家就餐问题
  • 死锁条件：循环等待
  • 解决方案：资源有序分配

• 管程 (Monitors)
  • Hoare风格：notify()立即切换线程
  • Java风格：notify()后当前线程继续执行
  • 嵌套管程问题：wait()仅释放直接关联的锁

• 经典问题
  • 生产者-消费者（环形缓冲区）
  • 读者-写者（读写锁设计）

03. 一致性条件 (Consistency Conditions)

• 历史 (History)
  • 顺序历史 (Sequential) vs. 并发历史 (Concurrent)
  • 合法历史 (Legal History)：符合顺序语义

• 顺序一致性 (Sequential Consistency)
  • 存在合法顺序历史，保留进程顺序

• 线性化 (Linearizability)
  • 强于顺序一致性，保留外部事件顺序
  • 局部性：系统线性化当且仅当每个对象线性化

• 寄存器一致性模型
  • 原子性 (Atomic) > 正则性 (Regular) > 安全性 (Safe)

04. 模型与时钟 (Models & Clocks)

• 事件顺序
  • 进程顺序 (Process Order)
  • 发送-接收顺序 (Send-Receive Order)
  • 因果顺序 (Happened-Before Relation, →)

• 逻辑时钟 (Logical Clocks)
  • Lamport时钟：单调递增整数
  • 全序扩展：(timestamp, process_id)

• 向量时钟 (Vector Clocks)
  • 向量比较：v1 ≤ v2当且仅当所有分量满足
  • 精确捕获因果顺序

• 矩阵时钟 (Matrix Clocks)
  • 每个进程维护多个向量，跟踪其他进程的因果信息

05. 全局快照 (Global Snapshot)

• 一致性快照
  • 无“未来到过去”的消息（仅允许L→R消息）

• Chandy-Lamport协议
  • 标记消息 (Marker) 触发快照
  • 假设FIFO通道
  • 处理“飞行中”消息：记录通道状态

06. 消息排序 (Message Ordering)

• 因果顺序 (Causal Order)
  • 协议：矩阵维护消息计数，延迟乱序消息

• 全序广播 (Total Order Broadcast)
  • 协调者协议：集中分配序列号
  • Skeen算法：随机化+多数ACK确定序号

07. 领导者选举 (Leader Election)

• 环形网络选举
  • Chang-Roberts算法：ID竞争，复杂度O(n log n)
  • 匿名环中无法选举（无唯一ID）

• 通用图选举
  • 已知节点数：洪泛ID，最大ID胜出
  • 未知节点数：生成生成树统计节点

08. 分布式共识 (Distributed Consensus)

• 同步系统 (Synchronous)
  • f+1轮通信容忍f个节点崩溃
  • 协议：多轮广播，取最小值

• 异步系统 (Asynchronous)
  • FLP定理：即使单节点崩溃，共识不可解

• 拜占庭容错 (Byzantine Fault Tolerance)
  • 阈值条件：n ≥ 4f + 1
  • 协议：轮换协调者，多数投票

09. 自稳定 (Self-Stabilisation)

• 旋转特权问题
  • 合法状态：全相同值或两连续值带
  • 协议：红/蓝节点更新规则

• 自稳定生成树
  • 节点维护parent和dist
  • 周期性更新：选择最短路径邻居

附录：关键证明与算法

• Peterson算法无饥饿性：等待进程最终因turn变量切换进入

• 线性化局部性：通过拓扑排序构建全局合法历史

• FLP定理：异步系统中无法区分节点崩溃与消息延迟

整理后的内容覆盖课程核心概念，适合快速回顾与查漏补缺。