For the next seminar of the proofs and algorithms pole of LIX, we are happy to welcome Constantin Enea, who will talk about Automated Formal Testing of Transactional Databases and Applications.

The talk will be given online.

Abstract: Transactions simplify concurrent programming by enabling computations on shared data that are isolated from other concurrent computations and are resilient to failures. Modern databases provide different isolation levels for transactions corresponding to different tradeoffs between consistency and availability. The weaker the isolation level, the more behaviors a database is allowed to exhibit and it is up to the developer to ensure that their application can tolerate those behaviors.

I will present a series of recent results that concern the problem of testing transactional databases and database-backed applications. First, I will focus on the problem of checking whether a given execution of a transactional database adheres to some isolation level, showing that isolation levels 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 isolation levels, we devise algorithms that are polynomial time assuming that certain parameters in the input executions, e.g., the number of sessions, are fixed. Second, I will present MonkeyDB, a mock storage system for testing database-backed applications. MonkeyDB supports a Key-Value interface as well as SQL queries under multiple isolation levels. It uses a logical specification of the isolation level to compute, on a read operation, the set of all possible return values. MonkeyDB then returns a value randomly from this set. We show that MonkeyDB provides good coverage of weak behaviors, which is complete in the limit.

Next seminar will be on Monday 15 March 2021 at 14h00 by Niccolò Veltri.

The list of next seminars can be found at: https://smimram.gitlabpages.inria.fr/proofs-algorithms/seminar/

The calendar of seminars can be found at: https://smimram.gitlabpages.inria.fr/proofs-algorithms/seminar.ics