Alone Together: Compositional Reasoning and Inference for Weak Isolation

TL;DR

This paper introduces a novel program logic and inference method for reasoning about weakly-isolated transactions, enabling verification of high-level correctness properties in database systems with weaker isolation levels.

Contribution

It presents a new compositional logic and an automated inference procedure for understanding and verifying weak isolation semantics in concurrent transactions.

Findings

Successfully verified correctness properties in real-world applications

Automated inference determines the weakest safe isolation level

Case studies demonstrate practical utility of the approach

Abstract

Serializability is a well-understood correctness criterion that simplifies reasoning about the behavior of concurrent transactions by ensuring they are isolated from each other while they execute. However, enforcing serializable isolation comes at a steep cost in performance and hence database systems in practice support, and often encourage, developers to implement transactions using weaker alternatives. Unfortunately, the semantics of weak isolation is poorly understood, and usually explained only informally in terms of low-level implementation artifacts. Consequently, verifying high-level correctness properties in such environments remains a challenging problem. To address this issue, we present a novel program logic that enables compositional reasoning about the behavior of concurrently executing weakly-isolated transactions. Recognizing that the proof burden necessary to use this logic may dissuade application developers, we also describe an inference procedure based on this foundation that ascertains the weakest isolation level that still guarantees the safety of high-level consistency invariants associated with such transactions. The key to effective inference is the observation that weakly-isolated transactions can be viewed as functional (monadic) computations over an abstract database state, allowing us to treat their operations as state transformers over the database. This interpretation enables automated verification using off-the-shelf SMT solvers. Case studies and experiments of real-world applications (written in an embedded DSL in OCaml) demonstrate the utility of our approach.