ADT theory “代数数据类型（ADT）是在简单类型 λ-演算（或系统 F）的基础上，通过引入积类型（Product）与和类型（Sum）的组合，并允许递归定义（µ），从而构造出结构化数据的一种类型系统扩展。它本质上是范畴论中的初始代数（Initial Algebra），对应逻辑学中的归纳类型。” Product types比如 pair 类型，本质上是把两个类型做了乘积。比如类型 L...

https://stanford-cs242.github.io/f19/ Lambda Calculus 自由变量 (Free Variables): 外层 lamdba 函数没有声明的变量 Closed Term / Conbinator: 没有自由变量的 term Alpha Conversion: 参数别名的修改，例如 λx. x 等价于 λy. y Beta Red...

LevelDB 是 google 开源的 LSM Tree 键值数据库引擎，是大概十五年前的工业级实现，从 Bigtable 中抽离而来。在保持精简的实现的同时也支撑了开源世界许多重要的项目，阅读 LevelDB 代码可以在了解工业级的 LSM Tree 实现的同时学习高性能 C++ 编程。 整体架构 WALLevelDB 将 WAL 日志的结构编码成了一个字节数组，将他们以 block 的...

Static Analysis: ensure (or get close to) soundness, while making good trade-offs between analysis precision and analysis speed. Soundness & Completeness术语 Soundness（可靠性） 来自于形式逻辑和数理逻辑，如果一个证明系...

DDIA 第八章读书笔记，也算复习一下之前 CMU 15-445 学到的内容 ACIDAtomic, Consistency, Isolation, Durability Atomic：事务原子性，指的是事务中的内容要么全部发生，要么全部不发生。可以通过回滚实现这一点，异常发生时直接回滚所有更改，只需要保证 commit 操作原子即可。 Consistency：一致性，这里的一致性跟 R...

SwiftPaxos Fast Geo-Replicated State Machines 算法细节 Client 向所有节点广播 Cmd，这里注意，Client 本身也是一个节点 单个节点收到 Cmd 后会向其他节点广播 FastAck，其中包含自己收到 Cmd 的依赖路径 比如图一，我发送了一条指令 z，对于节点 p1，p2 ，xy 都在 z 的前面，所以 p1，p2 中 z 的依...

https://zhuanlan.zhihu.com/p/208680604 在本文中，我们首先介绍了以下三个贡献： 如何在云规模上实现可持久性，以及如何设计Quorum系统来应对关联故障。（第二节） 如何将传统数据库的下层部分转移到存储层实现智能存储。（第三节） 如何在分布式存储中移除多阶段同步、崩溃恢复以及Checkpoint。（第四节） Persistence...

Chain Replication论文原文：https://pdos.csail.mit.edu/6.824/papers/cr-osdi04.pdf 译文：https://zhuanlan.zhihu.com/p/533384629 CRAQ (Chain Replication with Apportioned Queries)论文原文：http://nil.csail.mit.edu/...

论文原文: http://nil.csail.mit.edu/6.5840/2024/papers/zookeeper.pdf 中文译文: https://github.com/mapleFU/zookeeper_paper_cn 定义ZooKeeper 提供了一系列简单，高性能的原语用于协调不同的分布式系统。它在多副本、中心化的服务中，组合了消息群发（_group messaging_）,...

http://nil.csail.mit.edu/6.5840/2024/papers/gfs.pdf 定义GFS (Google File System) 是谷歌的分布式文件系统，主要面向其他分布式系统提供存储服务。 Assumptions 跑节点的都是便宜机器，很容易 fail，因此需要 fault tolerance 系统存储的文件大部分都是大文件（原文中提到 > 100MB ...