Modern web services crucially rely on high-performance distributed databases, where concurrent transactions are isolated from each other using concurrency control protocols. Relaxed isolation levels, which permit more complex concurrent behaviors than strong levels like serializability, are used in practice for higher performance and availability. In this paper, we present Eiger-PORT+, a concurrency control protocol that achieves a strong form of causal consistency, called TCCv (Transactional Causal Consistency with convergence). We show that Eiger-PORT+ also provides performance-optimal read transactions in the presence of transactional writes, thus refuting an open conjecture that this is impossible for TCCv. We also deductively verify that Eiger-PORT+ satisfies this isolation level by refining an abstract model of transactions. This yields the first deductive verification of a complex concurrency control protocol. Furthermore, we conduct a performance evaluation showing Eiger-PORT+'s superior performance over the state-of-the-art.

翻译：现代网络服务高度依赖于高性能分布式数据库，其中并发事务通过并发控制协议实现相互隔离。在实践中，为了获得更高的性能和可用性，通常会采用比可串行化等强隔离级别更宽松的隔离级别，这些级别允许更复杂的并发行为。本文提出了Eiger-PORT+，一种实现强形式因果一致性（称为TCCv，即具有收敛性的事务因果一致性）的并发控制协议。我们证明，在存在事务写入的情况下，Eiger-PORT+还能提供性能最优的读事务，从而反驳了关于TCCv无法实现此点的公开猜想。此外，我们通过对抽象事务模型进行精化，演绎式地验证了Eiger-PORT+满足该隔离级别。这实现了对复杂并发控制协议的首次演绎验证。进一步，我们进行了性能评估，结果表明Eiger-PORT+的性能优于现有最先进技术。