Transactions simplify concurrent programming by enabling computations on shared data that are isolated from other concurrent computations and resilient to failures. Modern databases provide different consistency models for transactions corresponding to different tradeoffs between consistency and availability. In this work, we investigate the problem of checking whether a given execution of a transactional database adheres to some consistency model. We show that consistency models like read committed, read atomic, and causal consistency are polynomial time checkable while prefix consistency and snapshot isolation are NP-complete in general. These results complement a previous NP-completeness result concerning serializability. Moreover, in the context of NP-complete consistency models, we devise algorithms which are polynomial time assuming that certain parameters in the input executions, e.g., the number of sessions, are fixed. We evaluate the scalability of these algorithms in the context of several production databases.
Modern data stores often need to provide both high scalability and strong transactional semantics.
They achieve scalability by partitioning data into shards and fault-tolerance by replicating each shard across several servers.
A key component of such systems is the protocol for atomically committing a transaction spanning multiple shards,
which is usually integrated with concurrency control.
Unfortunately, the classical theory of atomic commit is too restrictive to capture the complexities of such protocols.
I will present a new problem statement for atomic commit that more faithfully reflects modern requirements and will describe solutions to this problem in different classes of data stores.
This is joint work with Manuel Bravo (IMDEA) and Gregory Chockler (Royal Holloway, University of London).
TLA+ is a language for formal specification of all kinds of computer systems.
System designers use this language to specify concurrent, distributed, and
fault-tolerant protocols, which are traditionally presented in pseudo-code.
TLA+ is extremely concise yet expressive: The language primitives include
Booleans, integers, functions, tuples, records, sequences, and sets thereof,
which can be also nested. This is probably why the only model checker for TLA+
(called TLC) relies on explicit enumeration of values and states.
In this talk, we present a first symbolic model checker for TLA+. Like TLC,
it assumes that all specification parameters are fixed and all states are
finite structures. Unlike TLC, our model checker translates the underlying
transition relation into quantifier-free SMT constraints, which allows us to
exploit the power of SMT solvers.
Joint work with Jure Kukovec and Thanh Hai Tran (TU Wien, Austria).
State explosion is the central, fundamental obstacle to fully automated verification of distributed protocols. Modular verification methods are one way of ameliorating this problem. These methods side-step state explosion by reasoning locally and separately about each component of a program, subsequently combining those local results into a global proof. Although approximate, localized reasoning is often surprisingly effective, especially when a program is built out of "loosely coupled" components. For distributed protocols, which are typically composed of isomorphic processes, a recently developed notion of neighborhood symmetry further simplifies the task of modular reasoning. The symmetries also make it easier to construct a modular correctness proof for _all_ (i.e., an unbounded number of) instances of a protocol, by generalizing from modular proofs that are automatically constructed for small-scale instances. In the talk, I will also touch upon less understood but important questions about the scope of modular verification methods, and the potential for automatic synthesis of modularly-correct protocols from specifications of their behavior.
In networks of processes where the communication is performed by rendez-vous and the number of processes is a parameter, it is not always possible to find a cut-off, i.e. a minimal number of processes, which guarantees that the behavior of the network is correct. We show that for some reachability objective requiring all the processes to end in some specific states, the existence of a cut-off is a decidable problem and we provide algorithms to solve it for different hypothesis on the rendez-vous communication and on the presence of a leader in the network.
Verification of concurrent data structures is one of the most challenging tasks in software verification. The topic has received considerable attention over the course of the last decade. Nevertheless, human-driven techniques remain cumbersome and notoriously difficult while automated approaches suffer from limited applicability. The main obstacle for automation is the complexity of concurrent data structures. This is particularly true in the absence of garbage collection. The intricacy of lock-free memory management paired with the complexity of concurrent data structures makes automated verification prohibitive. In this work we present a method for verifying concurrent data structures and their memory management separately. We suggest two simpler verification tasks that imply the correctness of the data structure. The first task establishes an over-approximation of the reclamation behavior of the memory management. The second task exploits this over-approximation to verify the data structure without the need to consider the implementation of the memory management itself. To make the resulting verification tasks tractable for automated techniques, we establish a second result. We show that a verification tool needs to consider only executions where a single memory location is reused. We implemented our approach and were able to verify linearizability of Michael&Scott's queue and the DGLM queue for both hazard pointers and epoch-based reclamation. To the best of our knowledge, we are the first to verify such implementations fully automatically.