工程趣聞 2026 年 7 月 27 日

2026-07-27 — Valkey 編碼陷阱、SQLite WAL 短命讀者被鎖、Lean 用一條定理寫出比 Rust 更快的 DEFLATE

primary=https://valkey.io/blog/secret-life-of-data/ primary=https://hynek.me/til/sqlite-read-only-wal-locked/ primary=https://kim-em.github.io/blog/2026-7-24-why-lean-is-faster-than-rust/

Valkey 資料的秘密生活:一個位元組如何讓雜湊記憶體暴增 77%

Valkey Blog · 2026-07-21

背景:使用者看到的型別,不是記憶體裡的型別

Valkey(Redis 的社群 fork)的每一種資料型別在對外 API 上只有一種樣貌,例如 hash 就是 hash、list 就是 list,但在記憶體裡實際存放的方式卻是另一回事。Valkey 工程師 Kyle Davis 在部落格文章中把這層抽象稱為「encoding」:使用者操作的資料模型與底層記憶體表示法被刻意分離,同一個 hash 隨著內容成長,可能悄悄從一種內部結構換成另一種。這篇文章要講的,就是這層切換何時發生、切換之後代價有多大。

核心機制:listpack 與 hashtable 之間的臨界點

Hash 型別預設用 listpack 這種緊湊、循序排列的編碼儲存欄位,只有在超過設定門檻時才會轉成 hashtable。這兩個門檻可用 hash-max-listpack-entries(預設 512 筆)與 hash-max-listpack-value(預設 64 bytes)控制;只要單一 value 超過 64 bytes,整個 hash 就會從 listpack 轉為 hashtable。List、Set、Sorted Set 也都有各自對應的門檻(如 list-max-listpack-sizeset-max-intset-entriesset-max-listpack-entrieszset-max-listpack-entries),但字串與 Stream 型別是寫死邏輯,無法調整。

文章用 redis-cli 實測展示這個臨界點多陡:對同一個 key 執行 HSET 塞入不同長度的字串,再用 MEMORY USAGE 量測。

Key    Value 長度   MEMORY USAGE   相對前一筆的變化
hash0     63 bytes     104 bytes     n/a
hash1     64 bytes     120 bytes     +15.38%
hash2     65 bytes     212 bytes     +76.67%

從 64 bytes 加到 65 bytes,只多了一個位元組,OBJECT ENCODING 回報的結果就從 listpack 變成 hashtable,記憶體用量卻暴增 76.67%。這代表門檻附近的資料成長模式,遠比看起來危險——不是線性增加記憶體,而是在某個位元組數跨過門檻的瞬間跳增。

延伸應用:一個設定值差出兩台伺服器

文章接著把這個微觀現象放大到叢集規模。假設一個 100GB 的叢集裡有 95% 的 key 都恰好超過 hash-max-listpack-value 門檻而落在 hashtable 編碼,只要調整門檻讓這些 key 改用 listpack,總記憶體可以從 100GB 降到 58.8GB,單一 key 的資料量也從 212 bytes 降到 120 bytes(約為原本的 56.6%)。這個差異直接反映在硬體成本上:原本需要 5 個 primary 節點外加對應的 replica,調整後只需要 3 個。這也解釋了為什麼 Valkey 官方建議在寫入前先評估好資料形狀(value 長度分布),而不是等叢集撐大了才回頭調 encoding 門檻。

原始來源:Valkey Blog: The secret life of data in Valkey


SQLite WAL 模式下,連線時間再短也可能被鎖住

Hynek Schlawack · 2026-07-26

背景:WAL 模式明明是為並行讀寫設計的

Python 開發者 Hynek Schlawack 在一篇 TIL(Today I Learned)筆記裡記錄了一個違反直覺的現象:多個獨立行程(process)反覆「開啟資料庫、執行一次 SELECT、關閉連線」,即使完全沒有任何寫入動作,還是偶爾收到 sqlite3.OperationalError: database is locked。SQLite 的 WAL(Write-Ahead Log)模式本該讓讀者與寫者互不阻塞,但短命的唯讀連線(short-lived readers)在沒有連線池的情況下,恰好踩中了 WAL 協調機制的一個死角。這個問題不是資料錯誤,而是純粹的連線層級鎖爭。

核心機制:靠 -shm 檔案協調的代價

WAL 模式下,所有連到同一個資料庫的行程都透過一個名為 -shm 的記憶體映射檔案共享「wal-index」——一份用來讓讀者快速定位 WAL 內頁面位置的資料結構。問題出在開啟與關閉連線的那一刻,而不是讀寫資料本身:當最後一個連線關閉資料庫時,它會先做一次 checkpoint,再刪除 WAL 與 -shm 檔案,而這段清理過程需要短暫取得獨佔鎖。如果另一個行程正好在這個時間點嘗試開啟並查詢同一個空的 WAL 資料庫,就可能拿到 SQLITE_BUSY

更棘手的是預設逾時值的落差:C 函式庫的 busy_timeout 預設是 0 秒,也就是鎖一衝突就立刻回傳錯誤;Python 的 sqlite3 模組則把預設值拉高到 5 秒。正是這個 0 秒與 5 秒的落差,決定了同一個底層問題會不會在應用層被觀察到。在他的案例裡,大量各自獨立、生命週期極短的連線疊加起來,即使等了 5 秒仍然不夠,問題才浮上檯面。

影響範圍:兩種修法,他選了保守的那個

Hynek 列出兩種解法:

  • 在 WAL 模式下把 busy_timeout 明確設成 1 秒以上,讓短暫的鎖爭有機會自然消退
  • 放棄 WAL,改用傳統的 DELETE journal 模式,適合讀多寫少、且讀取行程生命週期很短的場景

他最後選擇第二種做法,直接把 journal_mode 切換回 DELETE,錯誤完全消失。這則筆記提醒的重點是:WAL 並非在任何併發場景下都優於舊模式,當工作負載的特徵是大量短命、唯讀、無連線池的連線時,傳統模式反而更穩定。

原始來源:Hynek Schlawack: SQLite WAL Mode Can Lock Short-Lived ReadersSQLite 官方文件:Write-Ahead Logging


Lean 寫的 DEFLATE 為什麼贏過 Rust:靠的是一條定理

Kim Morrison (kim-em) · 2026-07-24

背景:一個定理證明器,拿來寫壓縮演算法

Lean 是一套以形式化數學證明聞名的定理證明器,但作者 Kim Morrison 用它寫了一套名為 lean-zipDEFLATE 壓縮函式庫,並在 Silesia 語料庫(212 MB)上,以壓縮等級 6 對比 Rust 的純軟體實作 miniz_oxide結果是 lean-zip 壓縮出的檔案更小、耗時更短:lean-zip 產出 67,944,712 bytes、耗時 4.97 秒,miniz_oxide 產出 68,112,144 bytes、耗時 5.78 秒,壓縮率更好之餘速度還快了將近 20%。這在一般直覺裡很反常:Rust 編譯到原生碼、沒有 GC,理論上應該更快。

核心發現:能證明正確,才敢讓 AI 自動優化

作者給出的解釋不是 Lean 編譯器有什麼特別的底層優化技巧,而是 lean-zip 連著一條機器檢查過的定理一起釋出:

theorem inflate_deflateRaw (data : ByteArray) (level : UInt8)
    (maxOutputSize : Nat) (hsize : data.size ≤ maxOutputSize) :
    inflate (deflateRaw data level) maxOutputSize = .ok data

這條定理陳述「解壓縮任何用 deflateRaw 壓縮出來的資料,一定能還原成原始輸入」。因為每一次修改都必須讓這條定理繼續通過型別檢查,作者得以放心讓 AI 自動嘗試各種底層優化,不需要人工逐行審查正確性——傳統 Rust/C 壓縮函式庫要做同等大膽的重構,得靠大量測試與人工 review 才敢合併。這種「證明先行、優化在後」的流程,是 lean-zip 追上甚至超過手寫 Rust 的關鍵路徑,而不是 Lean 語言本身的執行效能。

影響範圍:仍有代價,也仍有更快的對手

文章同時列出誠實的侷限:

  • lean-zip 比 miniz_oxide 吃更多記憶體
  • 解壓縮反而較慢,miniz_oxide 快了約 1.45 倍
  • 部分底層 ByteArray 操作目前仍要靠 @[extern] 標記呼叫外部函式,因為 Lean runtime 本身還缺這些原生操作
  • 在整個 Pareto 前緣(壓縮等級 L1 到 L9)上,SIMD 優化的 C 函式庫 libdeflate 依然全面領先,lean-zip 只是追上了 zlib-rszlib-ng 等同量級對手

作者也強調這份基準測試沒有涵蓋側通道攻擊或最壞情況下的效能保證,目前的定位是「證明可以又快又正確」的示範專案,而非要取代 libdeflate 這類手工調校到極限的 C 實作。原始碼與基準測試腳本都公開在 github.com/kim-em/lean-zip,並引用了 DEFLATE 的原始規格 RFC 1951 與 Silesia 語料庫作為對照基準。

原始來源:Kim Morrison: Fast DEFLATE compression in LeanGitHub: kim-em/lean-zip

End of article
0
Would love your thoughts, please comment.x
()
x