深入了解 Aether：一个用 Rust 实现的经过形式化验证的高性能存储引擎

开发数据库存储引擎通常被视为系统编程中最具挑战性的任务之一。它需要在原始性能、严格的 ACID 合规性以及在灾难性崩溃期间数据绝不丢失的绝对保证之间取得微妙的平衡。Aether 应运而生，这是一款用 Rust 编写的高性能存储引擎，试图将多个前沿的学术和工业概念整合进一个统一且内聚的框架中。

通过将 TLA+ 形式化验证与 swizzled pointers 和 Taurus WAL 算法等高性能原语相结合，Aether 旨在为从兼容 Redis 的缓存到专门的金融交易数据库等各种应用提供基础。本文将深入探讨 Aether 的架构、性能特征及其背后的技术哲学。

架构栈

Aether 被设计为一个分层系统，确保高层 API 调用能够高效地转换为页级磁盘 I/O。其架构遵循严格的层级结构：

  1. API 层：提供 KvStore 和 DbEnv 接口用于应用程序交互。
  2. 索引层：支持多种索引策略，包括 B+ Trees、Skiplists 和 RAX radix trees。
  3. LSM 框架：一个可选层，提供可插拔的压缩策略，其中最著名的是纯 HanoiDB 实现。
  4. 事务与恢复：实现 ARIES 恢复协议以确保原子性和持久性。
  5. WAL (Write-Ahead Logging)：利用 Taurus 算法实现无锁的每线程日志记录。
  6. 缓冲管理器：受 LeanStore 启发的管理器，使用 swizzled pointers 以最大限度地减少开销。
  7. 页层：管理数据在 4KB 页中的物理布局。

关键技术创新

受 LeanStore 启发的缓冲管理

Aether 实现了一个基于 LeanStore 论文的缓冲管理器，该论文专注于减少将虚拟页 ID 映射到物理内存地址的开销。通过使用 swizzled pointers，Aether 可以使页面在 HOT、COOL 和 EVICTED 状态之间转换。这使得页面访问的“热路径”速度可达 24ns（大约每秒 4100 万次操作），从而在访问频繁的数据时绕过了昂贵的哈希表查找。

使用 TLA+ 进行形式化验证

与许多仅依赖广泛测试的存储引擎不同，Aether 采用 TLA+ (Temporal Logic of Actions) 对其核心逻辑进行形式化验证。其规范专门针对：

  • LSN (Log Sequence Number) 唯一性：确保单调性和唯一性，以防止日志损坏。
  • 崩溃恢复：验证在崩溃期间不会丢失数据，并确保 ARIES 的 redo/undo 阶段在逻辑上是完备的。
  • 并发安全性：证明系统在高并发访问模式下保持一致性。

HanoiDB LSM 实现

对于写密集型工作负载，Aether 提供了一个 LSM tree 框架。其 HanoiDB 的实现因声称具有恒定的 2.0x 写放大而特别引人注目。通过将压缩工作分散到写入过程中（增量合并），Aether 实现了极其稳定的延迟，p99 处于 1-2µs 范围内，有效地消除了通常与 LSM 压缩相关的巨大延迟峰值。

性能基准

Aether 的设计选择在不同组件中转化为了显著的性能提升：

  • WAL 吞吐量：使用无锁的每线程流和组提交（group commits）使得 WAL 能够随线程数线性扩展，使其成为高并发环境的最佳选择。
  • LSM 延迟：该项目报告的 p999 延迟为 4-22µs，这比遭受“停顿世界”（stop-the-world）压缩事件影响的传统 LSM 实现要好几个数量级。
  • 恢复：基于 ARIES 的恢复随日志大小线性扩展，确保了故障后可预测的启动时间。

社区反响与批判性观点

尽管具有技术雄心，Aether 在开发者社区中引发了关于现代软件开发本质和“验证”定义的辩论。

一些批评者认为，如果实现没有严格细化（refine）该模型，那么对模型的形式化验证是不够的。正如用户 @Kab1r 所指出的：

“我认为仅仅证明模型是正确的形式化验证已经不够好了。你必须证明你的实现细化了该模型。”

其他人对代码的来源提出了质疑，认为其极高的复杂性和开发速度表明其严重依赖 LLM。虽然一些人认为这是领域专家的“100倍乘数”，但另一些人对处理关键任务数据存储时的“氛围编程”（vibe-coded）软件持怀疑态度，更倾向于使用经过实战检验的替代方案，如 SQLite 或 PostgreSQL。

结论

Aether 代表了一次大胆的尝试，试图将学术严谨性 (TLA+) 和高性能研究 (LeanStore, HanoiDB) 引入到实际的 Rust 实现中。无论它是作为一个学习项目还是一个生产级引擎，它都作为一个复杂的案例研究，展示了如何从零开始构建一个现代的、符合 ACID 标准的存储系统。

Sources