在 READ COMMITTED 隔离级别上构建线性一致的日志

📋总体概括

Materialize团队介绍如何在PostgreSQL READ COMMITTED隔离级别之上构建线性一致性的元数据日志，替代此前依赖更严格隔离级别的方案。通过巧妙利用READ COMMITTED的可见性语义与设计协议规避写偏斜，系统获得3倍写吞吐提升，并用Lean 4定理证明器对核心协议的正确性给出机器可验证的证明，兼顾性能与形式化保障。