A Serializability Condition for Multi-step Transactions Accessing Ordered Data

In mobile environments, unspecified numbers of transactions arrive in continuous streams. To prove correctness of their concurrent execution a method of modelling an infinite number of transactions is needed. Standard database techniques model fixed finite schedules of transactions. Lately, techniques based on temporal logic have been proposed as suitable for modelling infinite schedules. The drawback of these techniques is that proving the basic serializability correctness condition is impractical, as encoding (the absence of) conflict cyclicity within large sets of transactions results in prohibitively large temporal logic formulae. In this paper, we show that, under certain common assumptions on the graph structure of data items accessed by the transactions, conflict cyclicity need only be checked within all possible pairs of transactions. This results in formulae of considerably reduced size in any temporal-logic-based approach to proving serializability, and scales to arbitrary numbers of transactions.

Authors:

• Rafat Alshorman
• Walter Hussak

Keywords:

• multi-step transactions
• serializability
• directed graph.

References:

[1] R. Alshorman and W. Hussak, Multi-step transactions specification and
verification in a mobile database community. In 3rd IEEE International
Conference on Information Technologies: from Theory to Applications,
IEEE, ICTTA 08, Damacus, Syria, IEEE Computer Society Press, 2008,
pp. 1407-12.
[2] W. Hussak, Specifying strict serializability of iterated transactions in
Propositional Temporal Logic, International Journal of Computer Science,
vol. 2, issue 2 (2007), pp. 150-156.
[3] W. Hussak, The serializability problem for a temporal logic of transaction
queries, Journal of Applied Non-Classical Logics, vol. 18, issue 1 (2008),
pp. 67-78.
[4] C.H. Papadimitriou, The Theory of Database Concurrency Control,
Computer Science Press, Pockville, Maryland, 1986.
[5] W. Hussak, Serializable histories in Quantified Propositional Temporal
Logic, International Journal of Computer Mathematics, vol. 81, issue 10
(2004), pp. 1203-1211.
[6] R. Elmasri and S. Navathe, Fundamental of Database Systems. Addison-
Wesley, Fourth Edition, 2004.
[7] A. Philip Bernstein, Vassos Hadzilacos and Nathan Goodman: Concurrency
Control and Recovery in Database Systems. Addison Wesley
Publishing Company, 1987.
[8] R. Alshorman and W. Hussak, Computational Tree Logics for specifying
multi-step transactions, April 2009, Internal Report, No. 1102.