Using Abstract State Machines for the Design of Multi-level Transaction Schedulers

Multi-level transactions have been suggested as an approach to increase transaction throughput in databases. The central idea is to enable some low-level conflicts to be ignored by taking higher-level application semantics into account. In this paper, we approach the formal specification of a multi-level transaction scheduler using Abstract State Machines. We are particularly interested in showing that concrete pmtocols for multi-level transaction processing arise as refinements of an abstract ground model specification. Furthermore, we are interested in the proof of desirable properties of such schedulers such as the correctness and if possible also completeness with respect to serialisability, and the recoverability of the accepted schedules. For this we investigate a two-phase locking and a hybrid protocol.