Thu 11 Jan 2018 11:20 - 11:45 at Bunker Hill - Consistency Chair(s): Xinyu Feng

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 because it necessarily restricts opportunities to exploit concurrency even when such opportunities would not violate application-specific invariants. As a result, database systems in practice support, and often encourage, developers to implement transactions using weaker alternatives. These alternatives break the strong isolation guarantees offered by serializable transactions to permit greater concurrency. 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 assertions 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. Notably, our development is parametric over a transaction’s specific isolation semantics, allowing it to be applicable over a range of concurrency control mechanisms. Case studies and experiments on real-world applications (written in an embedded DSL in OCaml) demonstrate the utility of our approach, and provide strong evidence that automated verification of weakly-isolated transactions can be placed on the same formal footing as their strongly-isolated serializable counterparts.

Thu 11 Jan
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

10:30 - 12:10: Research Papers - Consistency at Bunker Hill
Chair(s): Xinyu FengUniversity of Science and Technology of China
POPL-2018-papers10:30 - 10:55
Michael EmmiNokia Bell Labs, Constantin EneaUniversité Paris Diderot
POPL-2018-papers10:55 - 11:20
Oded PadonTel Aviv University, Jochen HoenickeUniversität Freiburg, Giuliano LosaUniversity of California at Los Angeles, USA, Andreas PodelskiUniversity of Freiburg, Germany, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university
POPL-2018-papers11:20 - 11:45
Gowtham KakiPurdue University, Kartik NagarPurdue University, Mahsa NajafzadehPurdue University, Suresh JagannathanPurdue University
POPL-2018-papers11:45 - 12:10
Ilya SergeyUniversity College London, James R. WilcoxUniversity of Washington, Zachary TatlockUniversity of Washington
DOI Pre-print