Algebraic Specification of Serializability for Partitioned Transactions

The usual correctness condition for a schedule of concurrent database transactions is some form of serializability of the transactions. For general forms, the problem of deciding whether a schedule is serializable is NP-complete. In those cases other approaches to proving correctness, using proof rules that allow the steps of the proof of serializability to be guided manually, are desirable. Such an approach is possible in the case of conflict serializability which is proved algebraically by deriving serial schedules using commutativity of non-conflicting operations. However, conflict serializability can be an unnecessarily strong form of serializability restricting concurrency and thereby reducing performance. In practice, weaker, more general, forms of serializability for extended models of transactions are used. Currently, there are no known methods using proof rules for proving those general forms of serializability. In this paper, we define serializability for an extended model of partitioned transactions, which we show to be as expressive as serializability for general partitioned transactions. An algebraic method for proving general serializability is obtained by giving an initial-algebra specification of serializable schedules of concurrent transactions in the model. This demonstrates that it is possible to conduct algebraic proofs of correctness of concurrent transactions in general cases.

Authors:

• Walter Hussak
• John Keane

Keywords:

• Algebraic Specification
• Partitioned Transactions
• Serializability.

References:

[1] E. Astesiano, M. Broy and G. Regio, "Algebraic Specification of
Concurrent Systems," in Algebraic Foundations of System Specification,
IFIP State-of-the-Art Reports, chapter 13, Springer, 1999.
[2] E. Astesiano, M. Bidoit, H. Kirchner, B. Krieg-Br¨uckner, P. Mosses, D.
Sannella, and A. Tarlecki, "CASL: The Common Algebraic Specification
Language," Theoretical Computer Science, vol. 286(2), pp. 153-196,
2002.
[3] A.P. Black, V. Cremet, R. Guerraoui and M. Odersky, "An Equational
Theory for Transactions," Proc. Foundations of Software Technology and
Theoretical Computer Science 2003, LNCS vol. 2914, Springer-Verlag,
pp. 38-49, 2003.
[4] C.J. Date, An Introduction to Database Systems, Addison Wesley, 2004.
[5] H. Garcia-Molina and B. Kogan, "Achieving high availability in distributed
databases," IEEE Transactions on Software Engineering, vol.
14(7), 1988.
[6] J.A. Goguen, J.W. Thatcher and E.G. Wagner, "An Initial Algebra Approach
to the Specification, Correctness and Implementation of Abstract
Data Types," in Current Trends in Programming Methodology IV, R.T.
Yeh (ed.), pp. 68-95 Prentice-Hall, 1978.
[7] C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall,
1985.
[8] W. Hussak, "Serializable Histories in Quantified Propositional Temporal
Logic," International Journal of Computer Mathematics, vol. 81(10), pp.
1203-1211, 2004.
[9] W. Hussak and J.A. Keane, "Concurrency Control of Tiered Flat
Transactions," Proc. 13th British National Conference on Databases,
LNCS vol. 940, Springer-Verlag, pp. 172-182, 1995.
[10] S. Katz and D. Peled, "Defining conditional independence using collapses,"
Theoretical Computer Science, vol. 101, pp. 337-359, 1992.
[11] H. Korth and G. Speegle, "Formal Model of Correctness Without
Serializability," Proc. ACM SIGMOD, pp. 379-388, 1988.
[12] C. Papadimitriou, The Theory of Database Concurrency Control, Computer
Science Press, 1986.
[13] D. Peled, S. Katz, and A. Pnueli, "Specifying and proving serializability
in temporal logic," Proceedings LICS 1991, pp. 232-245, IEEE Computer
Society Press, 1991.
[14] D. Peled and A. Pnueli, "Proving partial order properties," Theoretical
Computer Science, vol. 126, pp. 143-182, 1994.
[15] D. Sangiorgi and D. Walker, The ¤Ç-calculus: a Theory of Mobile
Processes, Cambridge University Press, 2001.
[16] L. Sha, J.P. Lehoczky and E.D. Jensen, "Modular Concurrency Control
and Failure Recovery," IEEE Transactions on Computers, vol. 37(2), pp.
146-159, 1988.
[17] K. Vidyasankar, "Generalized Theory of Serializability," Acta Informatica,
vol. 24, pp. 105-119, 1987.
[18] P. Wolper, "Temporal Logic Can Be More Expressive," Information and
Control, vol. 56, pp. 72-99, 1983.