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 的...

红岩网校安卓部门今年的寒假答辩，答辩开始之前扫了一眼他们考核项目的代码。以往几年看到的项目代码都写得歪歪扭扭的，变量/方法命名也不符合规范。今年发现有几个学弟提交的考核项目代码写得相当标准，顿时感动得热泪盈眶，感觉网校终于要迎来复兴了。 结果真到了答辩的时候他们却一问三不知，不过倒也实诚，承认自己用 AI 写了“一部分”代码。往年当然也有学习态度不好的人直接去网上找项目抄代码，但今...

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

MagiskMagisk 获取 root 权限是纯用户态实现的：通过修改 boot.img，替换 init 文件为自己的 magiskinit。magiskinit 会启动 magiskd，由于 magiskd 由 init 进程启动，所以它继承了 init 进程的 root 权限。并且由于 init 负责对 selinux policy 进行加载，所以替换 init 文件可以对其进行挟持，...

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

嗯，不知不觉已经到了 2025 的最后一天。晚上下班后我就将坐上去往天津的高铁，最后跟红岩网校的学长学弟们一起聆听世纪钟的钟声跨年。今天公司绝大多数人都请假了，我们组只剩下了我一个人，其他人请假工作也没办法推进，就在公司摸一会鱼好了。 毕业四年的本科生活终究落下了帷幕，不得不感慨光阴似箭，刚刚走进大学时的记忆依然清晰而深刻。这四年里参与了一些有意义的事情，也虚度了不少光阴，但对我而言这四年中...

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

其实在此之前我就大概知道，stack unwinding 是反向回溯栈的一种机制，在 throw 了什么东西后一层层回溯栈，一层层析构掉这些栈上的 RAII 对象，直到找到 try catch 块后跳转到 catch 块。 但是问题是这种事情是怎样实现的？多说无益，我们直接从 throw 的源码入手分析。 首先我们编写一段示例代码: 12345678910111213141516171819...