Algebraic Specification of Serializability for Partitioned Transactions

Authors: Walter Hussak, John Keane

Abstract:

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.

Keywords: Algebraic Specification, Partitioned Transactions, Serializability.

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

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.