A Serializability Condition for Multi-step Transactions Accessing Ordered Data

Authors: Rafat Alshorman, Walter Hussak

Abstract:

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.

Keywords: multi-step transactions, serializability, directed graph.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1334235

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.