主要观点：介绍了 Delta Lake 的一致性模型，包括基本原理、ACID 事务保证、delta 日志和数据文件、写路径逻辑模型、并发控制以及读路径逻辑模型等方面，并通过 TLA+规范和模型检查进行了验证。
关键信息：

• Delta Lake 是基于对象存储的表格式之一，由预写日志和数据文件组成，支持 ACID 事务保证，读操作采用多版本并发控制（MVCC）。
• delta 日志记录事务信息，通过读取日志可构建表的快照，写操作会写入日志并创建新的数据文件或删除旧的文件。
• 并发控制支持乐观并发控制（OCC），有 PutIfAbsent 存储和写协调两种方式，避免覆盖 delta 日志条目文件。
• 读操作需加载 delta 日志，进行文件修剪后读取数据文件，TLA+规范用于检查一致性。
  重要细节：
• 写路径逻辑模型中，不同事务对数据的插入、删除和更新操作会创建新的数据文件并更新 delta 日志。
• 合并读（Merge-on-read）通过添加删除向量（DV）文件来避免整数据文件重写，但会增加读取时合并数据文件的成本。
• TLA+规范中的参数包括写者、列值、分区等，通过一系列动作和不变式来检查一致性和活性。
• 模型检查结果表明，启用 PutIfAbsent 或写协调时无一致性问题，禁用则会导致一致性违反。