在 Aether 內部：經形式驗證的高效能 Rust 儲存引擎

資料庫儲存引擎的開發常被視為系統程式設計中最具挑戰性的工作之一。它需要在原始效能、嚴格的 ACID 相容性，以及在災難性崩潰時資料絕不遺失的絕對保證之間取得微妙的平衡。於是 Aether 出現了，它是一個以 Rust 撰寫的高效能儲存引擎，試圖將多項前沿的學術與產業概念融合成單一且一致的框架。

透過結合 TLA+ 的形式驗證與高效能原語（如 swizzled pointers 與 Taurus WAL 演算法），Aether 旨在為從相容 Redis 的快取到專門的金融交易資料庫等各種應用提供基礎。本篇文章將深入探討 Aether 的架構、效能特性與背後的技術哲學。

架構層次

  1. API 層：提供 KvStore 與 DbEnv 介面供應用程式互動。
  2. 索引層：支援多種索引策略，包括 B+ 樹、跳表（Skiplists）以及 RAX 基數樹。
  3. LSM 框架：一個可選層，提供可插拔的壓縮策略，最顯著的是純粹的 HanoiDB 實作。
  4. 交易與復原：實作 ARIES 復原協定，以確保原子性與耐久性。
  5. WAL（預寫日誌）：使用 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（日誌序列號）唯一性：確保單調遞增與唯一性，以防止日誌損壞。
  • 崩潰復原：驗證在崩潰時不會遺失資料，且 ARIES 的 redo/undo 階段在邏輯上是正確的。
  • 並發安全：證明系統在高度並發的存取模式下仍保持一致性。

HanoiDB LSM 實作

針對寫入密集的工作負載，Aether 提供 LSM 樹框架。其 HanoiDB 的實作特別值得注意，因其聲稱具備恆定 2.0 倍的寫入放大。透過將壓縮工作分散至寫入過程（增量合併），Aether 能達到相當穩定的延遲，p99 延遲落在 1-2µs 範圍內，實質上消除 LSM 壓縮常見的大幅延遲峰值。

效能基準測試

Aether 的設計選擇在各個元件上帶來顯著的效能提升：

  • WAL 吞吐量：使用無鎖的每執行緒串流與群組提交，使 WAL 能隨執行緒數線性擴展，對高併發環境極為理想。
  • LSM 延遲：專案報告的 p999 延遲為 4-22µs，遠優於傳統 LSM 實作因「停頓」壓縮事件而產生的高延遲。
  • 復原：基於 ARIES 的復原隨日誌大小線性擴展，確保故障後的啟動時間可預測。

社群回應與批判觀點

儘管技術抱負十足，Aether 仍在開發者社群中引發關於現代軟體開發本質與「驗證」定義的討論。

一些批評者認為，僅對 模型 進行形式驗證仍不足，若 實作 未嚴格精煉該模型。正如使用者 @Kab1r 所指出：

「我認為僅僅形式驗證模型正確已不再足夠。必須證明你的實作精煉了模型。」

另一些人質疑程式碼的來源，認為其高度複雜性與開發速度暗示大量依賴大型語言模型（LLM）。雖然有些人將此視為領域專家的「100 倍乘數」，但在關鍵資料儲存方面，對於「感覺編碼」的軟體仍持懷疑態度，較偏好如 SQLite 或 PostgreSQL 等經過實戰驗證的替代方案。

結論

Aether 是一次將學術嚴謹性（TLA+）與高效能研究（LeanStore、HanoiDB）帶入實用 Rust 實作的勇敢嘗試。無論是作為學習專案或是可投入生產的引擎，它都提供了一個精緻的案例，說明如何從頭構建現代的 ACID 相容儲存系統。

Sources