Correct execution of transactions at different isolation levels

Many transaction processing applications execute at isolation levels lower than SERIALIZABLE in order to increase throughput and reduce response time. However, the resulting schedules might not be serializable and, hence, not necessarily correct. The semantics of a particular application determines whether that application will run correctly at a lower level and, in practice, it appears that many applications do. The decision to choose an isolation level at which to run an application and the analysis of the correctness of the resulting execution is usually done informally. We develop a formal technique to analyze and reason about the correctness of the execution of an application at isolation levels other than SERIALIZABLE. We use a new notion of correctness, semantic correctness, a criterion weaker than serializability, to investigate correctness. In particular, for each isolation level, we prove a condition under which the execution of transactions at that level will be semantically correct. In addition to the ANSI/ISO isolation levels of READ UNCOMMITTED, READ COMMITTED, and REPEATABLE READ, we also prove a condition for correct execution at the READ-COMMITTED with first-committer-wins and at SNAPSHOT isolation. We assume that different transactions in the same application can be executing at different levels, but that each transaction is executing at least at READ UNCOMMITTED.