Analyze 这篇论文关注在如何使用黑盒的方式验证键值存储的的可串行化。 Background 如今许多客户选择使用云数据库提供的键值存储服务，客户程序的正确性受到云数据库的正确性的影响，云数据库的正确性常常通过可串行化来定义，即客户的事务仿佛以串行的方式执行，那么云数据库是否符合了可串行化的约束？这个问题有几个挑战，一方面数据库是黑盒的，我们无法得到数据库的代码，只能分析数据库的行为，即输入和输出，另一方面需要在数据库不断运行中，同步验证其是否符合可串行化的要求，这需要验证手段高效并具有可扩展性。 这篇论文的直觉来源于 SMT solver 以及计算能力的进步，认为其足以自动化的验证可串行化的问题，于是他们基于 SMT solver 提出 Cobra 框架，Cobra 包含一系列技术，做到了高效可扩展的验证可串行化，实验表明 Cobra 能验证实际场景下数据库的可串行化。 Structures Each client request is one of five operations: start, commit, abort (which refer to transactions), and read and write (which refer to keys). History collectors sit between clients and the database, capturing the requests that clients issue and the (possibly wrong) results delivered by the database. A verifier retrieves history fragments from collectors and attempts to verify whether the history is serializable. ...

Summary 一句话总结，就是：Re-implement the multi-version concurrency control mechanism of Postgres on shim layers. 因为这篇文章在组会上做了汇报，所以我就直接贴 PPT 了。 Content

FAQ What is the difference between receive and deliver? What does it mean by saying “Zab’s transaction log doubles as the database write-ahead transaction log” in page 3? ZooKeeper uses an in-memory database and stores transaction logs (Write-ahead log) and periodic snapshots on disk. Before a transaction is executed and its changes are applied to the in-memory database, it is first logged. This means that if the system crashes before the changes can be applied, the transaction can be replayed from the log to ensure data integrity. ...

本章是这本书最酣畅淋漓的一章，涉及到了一致性和共识问题的方方面面，知识点多而不失条理。第一部分先讲了 Linearizability, 为后面的知识点做铺垫。到了 “Ordering Guarantees” 这一小节，从因果关系的带来的 “Happened Before” 的关系开始讲起，讲到了序列号和 Lamport Timestamp，提出来 Lamport Timestamp 的一个缺点：无法在某事件发生时判断是否有冲突，然后引出了全序关系广播，在全序关系广播中又讲到了和 Linearizable 之间的等价关系，最后引出共识算法。太精彩了，值得反复阅读！ Consistency Guarantees Most replicated databases provide at least eventual consistency, which means that if you stop writing to the database and wait for some unspecified length of time, then eventually all read requests will return the same value. A better name for eventual consistency may be convergence, as we expect all replicas to eventually converge to the same value. ...

FAQ what is a version vector? A version vector is a construct used in distributed systems to track the version of data across different nodes in a network, ensuring consistency and helping to resolve conflicts. Version vectors are particularly useful in systems where multiple nodes may independently modify data and then need to synchronize with each other without relying on a central authority. This concept is fundamental in the context of eventual consistency and conflict resolution in distributed databases, file systems, and data replication scenarios. ...